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 ⊢A∈ℝ∧0<A→0<1A

Proof

Step Hyp Ref Expression
1 simpl ⊢A∈ℝ∧0<A→A∈ℝ
2 1 recnd ⊢A∈ℝ∧0<A→A∈ℂ
3 gt0ne0 ⊢A∈ℝ∧0<A→A≠0
4 2 3 recne0d ⊢A∈ℝ∧0<A→1A≠0
5 4 necomd ⊢A∈ℝ∧0<A→0≠1A
6 5 neneqd ⊢A∈ℝ∧0<A→¬0=1A
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 ⊢A∈ℝ∧0<A∧1A<0→A∈ℝ
13 3 adantr ⊢A∈ℝ∧0<A∧1A<0→A≠0
14 12 13 rereccld ⊢A∈ℝ∧0<A∧1A<0→1A∈ℝ
15 14 renegcld ⊢A∈ℝ∧0<A∧1A<0→−1A∈ℝ
16 simpr ⊢A∈ℝ∧0<A∧1A<0→1A<0
17 1 3 rereccld ⊢A∈ℝ∧0<A→1A∈ℝ
18 17 adantr ⊢A∈ℝ∧0<A∧1A<0→1A∈ℝ
19 18 lt0neg1d ⊢A∈ℝ∧0<A∧1A<0→1A<0↔0<−1A
20 16 19 mpbid ⊢A∈ℝ∧0<A∧1A<0→0<−1A
21 simplr ⊢A∈ℝ∧0<A∧1A<0→0<A
22 15 12 20 21 mulgt0d ⊢A∈ℝ∧0<A∧1A<0→0<−1A⁢A
23 2 adantr ⊢A∈ℝ∧0<A∧1A<0→A∈ℂ
24 23 13 reccld ⊢A∈ℝ∧0<A∧1A<0→1A∈ℂ
25 24 23 mulneg1d ⊢A∈ℝ∧0<A∧1A<0→−1A⁢A=−1A⁢A
26 23 13 recid2d ⊢A∈ℝ∧0<A∧1A<0→1A⁢A=1
27 26 negeqd ⊢A∈ℝ∧0<A∧1A<0→−1A⁢A=−1
28 25 27 eqtrd ⊢A∈ℝ∧0<A∧1A<0→−1A⁢A=−1
29 22 28 breqtrd ⊢A∈ℝ∧0<A∧1A<0→0<−1
30 1red ⊢A∈ℝ∧0<A∧1A<0→1∈ℝ
31 30 lt0neg1d ⊢A∈ℝ∧0<A∧1A<0→1<0↔0<−1
32 29 31 mpbird ⊢A∈ℝ∧0<A∧1A<0→1<0
33 32 ex ⊢A∈ℝ∧0<A→1A<0→1<0
34 11 33 mtoi ⊢A∈ℝ∧0<A→¬1A<0
35 ioran ⊢¬0=1A∨1A<0↔¬0=1A∧¬1A<0
36 6 34 35 sylanbrc ⊢A∈ℝ∧0<A→¬0=1A∨1A<0
37 axlttri ⊢0∈ℝ∧1A∈ℝ→0<1A↔¬0=1A∨1A<0
38 8 17 37 sylancr ⊢A∈ℝ∧0<A→0<1A↔¬0=1A∨1A<0
39 36 38 mpbird ⊢A∈ℝ∧0<A→0<1A