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 ⊢ 𝐴 ∈ ℝ
recgt0i.2 ⊢ 0 < 𝐴
Assertion recgt0ii 0 < ( 1 / 𝐴 )

Proof

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