This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem recgt0ii

Description: The reciprocal of a positive number is positive. Exercise 4 of Apostol p. 21. (Contributed by NM, 15-May-1999)

Ref Expression
Hypotheses ltplus1.1 ⊢ A ∈ ℝ
recgt0i.2 ⊢ 0 < A
Assertion recgt0ii ⊢ 0 < 1 A

Proof

Step Hyp Ref Expression
1 ltplus1.1 ⊢ A ∈ ℝ
2 recgt0i.2 ⊢ 0 < A
3 ax-1cn ⊢ 1 ∈ ℂ
4 1 recni ⊢ A ∈ ℂ
5 ax-1ne0 ⊢ 1 ≠ 0
6 1 2 gt0ne0ii ⊢ A ≠ 0
7 3 4 5 6 divne0i ⊢ 1 A ≠ 0
8 7 nesymi ⊢ ¬ 0 = 1 A
9 0lt1 ⊢ 0 < 1
10 0re ⊢ 0 ∈ ℝ
11 1re ⊢ 1 ∈ ℝ
12 10 11 ltnsymi ⊢ 0 < 1 → ¬ 1 < 0
13 9 12 ax-mp ⊢ ¬ 1 < 0
14 1 6 rereccli ⊢ 1 A ∈ ℝ
15 14 renegcli ⊢ − 1 A ∈ ℝ
16 15 1 mulgt0i ⊢ 0 < − 1 A ∧ 0 < A → 0 < − 1 A ⁢ A
17 2 16 mpan2 ⊢ 0 < − 1 A → 0 < − 1 A ⁢ A
18 14 recni ⊢ 1 A ∈ ℂ
19 18 4 mulneg1i ⊢ − 1 A ⁢ A = − 1 A ⁢ A
20 4 6 recidi ⊢ A ⁢ 1 A = 1
21 4 18 20 mulcomli ⊢ 1 A ⁢ A = 1
22 21 negeqi ⊢ − 1 A ⁢ A = − 1
23 19 22 eqtri ⊢ − 1 A ⁢ A = − 1
24 17 23 breqtrdi ⊢ 0 < − 1 A → 0 < − 1
25 lt0neg1 ⊢ 1 A ∈ ℝ → 1 A < 0 ↔ 0 < − 1 A
26 14 25 ax-mp ⊢ 1 A < 0 ↔ 0 < − 1 A
27 lt0neg1 ⊢ 1 ∈ ℝ → 1 < 0 ↔ 0 < − 1
28 11 27 ax-mp ⊢ 1 < 0 ↔ 0 < − 1
29 24 26 28 3imtr4i ⊢ 1 A < 0 → 1 < 0
30 13 29 mto ⊢ ¬ 1 A < 0
31 8 30 pm3.2ni ⊢ ¬ 0 = 1 A ∨ 1 A < 0
32 axlttri ⊢ 0 ∈ ℝ ∧ 1 A ∈ ℝ → 0 < 1 A ↔ ¬ 0 = 1 A ∨ 1 A < 0
33 10 14 32 mp2an ⊢ 0 < 1 A ↔ ¬ 0 = 1 A ∨ 1 A < 0
34 31 33 mpbir ⊢ 0 < 1 A