Theorem xdivpnfrp

Description: Plus infinity divided by a positive real number is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016)

	Ref	Expression
Assertion	xdivpnfrp	|- ( A e. RR+ -> ( +oo /e A ) = +oo )

Proof

Step	Hyp	Ref	Expression
1		rprene0	|- ( A e. RR+ -> ( A e. RR /\ A =/= 0 ) )
2		pnfxr	|- +oo e. RR*
3	1 2	jctil	|- ( A e. RR+ -> ( +oo e. RR* /\ ( A e. RR /\ A =/= 0 ) ) )
4		3anass	|- ( ( +oo e. RR* /\ A e. RR /\ A =/= 0 ) <-> ( +oo e. RR* /\ ( A e. RR /\ A =/= 0 ) ) )
5	3 4	sylibr	|- ( A e. RR+ -> ( +oo e. RR* /\ A e. RR /\ A =/= 0 ) )
6		xdivval	|- ( ( +oo e. RR* /\ A e. RR /\ A =/= 0 ) -> ( +oo /e A ) = ( iota_ x e. RR* ( A *e x ) = +oo ) )
7	5 6	syl	|- ( A e. RR+ -> ( +oo /e A ) = ( iota_ x e. RR* ( A *e x ) = +oo ) )
8	2	a1i	|- ( A e. RR+ -> +oo e. RR* )
9		xlemul2	|- ( ( +oo e. RR* /\ x e. RR* /\ A e. RR+ ) -> ( +oo <_ x <-> ( A *e +oo ) <_ ( A *e x ) ) )
10	2 9	mp3an1	|- ( ( x e. RR* /\ A e. RR+ ) -> ( +oo <_ x <-> ( A *e +oo ) <_ ( A *e x ) ) )
11	10	ancoms	|- ( ( A e. RR+ /\ x e. RR* ) -> ( +oo <_ x <-> ( A *e +oo ) <_ ( A *e x ) ) )
12		rpxr	|- ( A e. RR+ -> A e. RR* )
13		rpgt0	|- ( A e. RR+ -> 0 < A )
14		xmulpnf1	|- ( ( A e. RR* /\ 0 < A ) -> ( A *e +oo ) = +oo )
15	12 13 14	syl2anc	|- ( A e. RR+ -> ( A *e +oo ) = +oo )
16	15	adantr	|- ( ( A e. RR+ /\ x e. RR* ) -> ( A *e +oo ) = +oo )
17	16	breq1d	|- ( ( A e. RR+ /\ x e. RR* ) -> ( ( A *e +oo ) <_ ( A *e x ) <-> +oo <_ ( A *e x ) ) )
18	11 17	bitr2d	|- ( ( A e. RR+ /\ x e. RR* ) -> ( +oo <_ ( A *e x ) <-> +oo <_ x ) )
19		xmulcl	|- ( ( A e. RR* /\ x e. RR* ) -> ( A *e x ) e. RR* )
20	12 19	sylan	|- ( ( A e. RR+ /\ x e. RR* ) -> ( A *e x ) e. RR* )
21		xgepnf	|- ( ( A *e x ) e. RR* -> ( +oo <_ ( A *e x ) <-> ( A *e x ) = +oo ) )
22	20 21	syl	|- ( ( A e. RR+ /\ x e. RR* ) -> ( +oo <_ ( A *e x ) <-> ( A *e x ) = +oo ) )
23		xgepnf	|- ( x e. RR* -> ( +oo <_ x <-> x = +oo ) )
24	23	adantl	|- ( ( A e. RR+ /\ x e. RR* ) -> ( +oo <_ x <-> x = +oo ) )
25	18 22 24	3bitr3d	|- ( ( A e. RR+ /\ x e. RR* ) -> ( ( A *e x ) = +oo <-> x = +oo ) )
26	8 25	riota5	|- ( A e. RR+ -> ( iota_ x e. RR* ( A *e x ) = +oo ) = +oo )
27	7 26	eqtrd	|- ( A e. RR+ -> ( +oo /e A ) = +oo )