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 / 𝐴 )