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	|- A e. RR
	recgt0i.2	|- 0 < A
Assertion	recgt0ii	|- 0 < ( 1 / A )

Proof

Step	Hyp	Ref	Expression
1		ltplus1.1	|- A e. RR
2		recgt0i.2	|- 0 < A
3		ax-1cn	|- 1 e. CC
4	1	recni	|- A e. CC
5		ax-1ne0	|- 1 =/= 0
6	1 2	gt0ne0ii	|- A =/= 0
7	3 4 5 6	divne0i	|- ( 1 / A ) =/= 0
8	7	nesymi	|- -. 0 = ( 1 / A )
9		0lt1	|- 0 < 1
10		0re	|- 0 e. RR
11		1re	|- 1 e. RR
12	10 11	ltnsymi	|- ( 0 < 1 -> -. 1 < 0 )
13	9 12	ax-mp	|- -. 1 < 0
14	1 6	rereccli	|- ( 1 / A ) e. RR
15	14	renegcli	|- -u ( 1 / A ) e. RR
16	15 1	mulgt0i	|- ( ( 0 < -u ( 1 / A ) /\ 0 < A ) -> 0 < ( -u ( 1 / A ) x. A ) )
17	2 16	mpan2	|- ( 0 < -u ( 1 / A ) -> 0 < ( -u ( 1 / A ) x. A ) )
18	14	recni	|- ( 1 / A ) e. CC
19	18 4	mulneg1i	|- ( -u ( 1 / A ) x. A ) = -u ( ( 1 / A ) x. A )
20	4 6	recidi	|- ( A x. ( 1 / A ) ) = 1
21	4 18 20	mulcomli	|- ( ( 1 / A ) x. A ) = 1
22	21	negeqi	|- -u ( ( 1 / A ) x. A ) = -u 1
23	19 22	eqtri	|- ( -u ( 1 / A ) x. A ) = -u 1
24	17 23	breqtrdi	|- ( 0 < -u ( 1 / A ) -> 0 < -u 1 )
25		lt0neg1	|- ( ( 1 / A ) e. RR -> ( ( 1 / A ) < 0 <-> 0 < -u ( 1 / A ) ) )
26	14 25	ax-mp	|- ( ( 1 / A ) < 0 <-> 0 < -u ( 1 / A ) )
27		lt0neg1	|- ( 1 e. RR -> ( 1 < 0 <-> 0 < -u 1 ) )
28	11 27	ax-mp	|- ( 1 < 0 <-> 0 < -u 1 )
29	24 26 28	3imtr4i	|- ( ( 1 / A ) < 0 -> 1 < 0 )
30	13 29	mto	|- -. ( 1 / A ) < 0
31	8 30	pm3.2ni	|- -. ( 0 = ( 1 / A ) \/ ( 1 / A ) < 0 )
32		axlttri	|- ( ( 0 e. RR /\ ( 1 / A ) e. RR ) -> ( 0 < ( 1 / A ) <-> -. ( 0 = ( 1 / A ) \/ ( 1 / A ) < 0 ) ) )
33	10 14 32	mp2an	|- ( 0 < ( 1 / A ) <-> -. ( 0 = ( 1 / A ) \/ ( 1 / A ) < 0 ) )
34	31 33	mpbir	|- 0 < ( 1 / A )