Metamath Proof Explorer

Theorem recgt0

Description: The reciprocal of a positive number is positive. Exercise 4 of Apostol p. 21. (Contributed by NM, 25-Aug-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion recgt0 ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < ( 1 / 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ )
2 1 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ∈ ℂ )
3 gt0ne0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
4 2 3 recne0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ≠ 0 )
5 4 necomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 ≠ ( 1 / 𝐴 ) )
6 5 neneqd ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ¬ 0 = ( 1 / 𝐴 ) )
7 0lt1 ⊢ 0 < 1
8 0re ⊢ 0 ∈ ℝ
9 1re ⊢ 1 ∈ ℝ
10 8 9 ltnsymi ⊢ ( 0 < 1 → ¬ 1 < 0 )
11 7 10 ax-mp ⊢ ¬ 1 < 0
12 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → 𝐴 ∈ ℝ )
13 3 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → 𝐴 ≠ 0 )
14 12 13 rereccld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → ( 1 / 𝐴 ) ∈ ℝ )
15 14 renegcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → - ( 1 / 𝐴 ) ∈ ℝ )
16 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → ( 1 / 𝐴 ) < 0 )
17 1 3 rereccld ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℝ )
18 17 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → ( 1 / 𝐴 ) ∈ ℝ )
19 18 lt0neg1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → ( ( 1 / 𝐴 ) < 0 ↔ 0 < - ( 1 / 𝐴 ) ) )
20 16 19 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → 0 < - ( 1 / 𝐴 ) )
21 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → 0 < 𝐴 )
22 15 12 20 21 mulgt0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → 0 < ( - ( 1 / 𝐴 ) · 𝐴 ) )
23 2 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → 𝐴 ∈ ℂ )
24 23 13 reccld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → ( 1 / 𝐴 ) ∈ ℂ )
25 24 23 mulneg1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → ( - ( 1 / 𝐴 ) · 𝐴 ) = - ( ( 1 / 𝐴 ) · 𝐴 ) )
26 23 13 recid2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → ( ( 1 / 𝐴 ) · 𝐴 ) = 1 )
27 26 negeqd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → - ( ( 1 / 𝐴 ) · 𝐴 ) = - 1 )
28 25 27 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → ( - ( 1 / 𝐴 ) · 𝐴 ) = - 1 )
29 22 28 breqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → 0 < - 1 )
30 1red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → 1 ∈ ℝ )
31 30 lt0neg1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → ( 1 < 0 ↔ 0 < - 1 ) )
32 29 31 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 1 / 𝐴 ) < 0 ) → 1 < 0 )
33 32 ex ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( 1 / 𝐴 ) < 0 → 1 < 0 ) )
34 11 33 mtoi ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ¬ ( 1 / 𝐴 ) < 0 )
35 ioran ⊢ ( ¬ ( 0 = ( 1 / 𝐴 ) ∨ ( 1 / 𝐴 ) < 0 ) ↔ ( ¬ 0 = ( 1 / 𝐴 ) ∧ ¬ ( 1 / 𝐴 ) < 0 ) )
36 6 34 35 sylanbrc ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ¬ ( 0 = ( 1 / 𝐴 ) ∨ ( 1 / 𝐴 ) < 0 ) )
37 axlttri ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ) → ( 0 < ( 1 / 𝐴 ) ↔ ¬ ( 0 = ( 1 / 𝐴 ) ∨ ( 1 / 𝐴 ) < 0 ) ) )
38 8 17 37 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 0 < ( 1 / 𝐴 ) ↔ ¬ ( 0 = ( 1 / 𝐴 ) ∨ ( 1 / 𝐴 ) < 0 ) ) )
39 36 38 mpbird ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < ( 1 / 𝐴 ) )