Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ 0 < a, hypo. 03. 3 ⊢ 1/a ≤ 0, hypo. 04. 2 ⊢ 0 ≤ a, le_from_lt 2. 05. 2 ⊢ ¬0 = a, neq_from_lt 2. 06. 2 ⊢ ¬a = 0, neq_symm 5. 07. 1, 2 ⊢ 1/a ∈ ℝ, rreci_closed 1 6. 08. ⊢ 0 ∈ ℝ, calc. 09. 1, 2, 3 ⊢ a⋅(1/a) ≤ a⋅0, rle_compat_mull 7 8 1 3 4. 10. 1, 2 ⊢ a⋅(1/a) = 1, rmul_reci_cancel 1 6. 11. 1, 2 ⊢ 1 = a⋅(1/a), eq_symm 10. 12. 1, 2, 3 ⊢ 1 ≤ a⋅0, eq_le_trans 11 9. 13. 1 ⊢ a⋅0 = 0, rmul_rzero 1. 14. 1, 2, 3 ⊢ 1 ≤ 0, le_eq_trans 12 13. 15. ⊢ ¬1 ≤ 0, calc. 16. 1, 2, 3 ⊢ ⊥, neg_elim 15 14. 17. 1, 2 ⊢ ¬1/a ≤ 0, neg_intro 16. 18. 1, 2 ⊢ 0 ≤ 1/a, rle_neg 7 8 17. 19. 1, 2 ⊢ ¬1/a = 0, rreci_non_zero 1 6. 20. 1, 2 ⊢ ¬0 = 1/a, neq_symm 19. 21. 1, 2 ⊢ 0 < 1/a, lt_intro 18 20. rreci_positive. ⊢ a ∈ ℝ → 0 < a → 0 < 1/a, subj_intro_ii 21.
Dependencies
The given proof depends on 18 axioms:
efq, eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rinv_closed, rle_compat_add, rle_compat_mul, rle_total, rmul_closed, rmul_comm, rmul_distl_add, rmul_inv, rmul_neutr, rneg_closed.