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