Theorem xrpxdivcld

Description: Closure law for extended division of positive extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016)

	Ref	Expression
Hypotheses	xrpxdivcld.1	|- ( ph -> A e. ( 0 [,] +oo ) )
	xrpxdivcld.2	|- ( ph -> B e. RR+ )
Assertion	xrpxdivcld	|- ( ph -> ( A /e B ) e. ( 0 [,] +oo ) )

Proof

Step	Hyp	Ref	Expression
1		xrpxdivcld.1	|- ( ph -> A e. ( 0 [,] +oo ) )
2		xrpxdivcld.2	|- ( ph -> B e. RR+ )
3		oveq1	|- ( A = 0 -> ( A /e B ) = ( 0 /e B ) )
4		xdiv0rp	|- ( B e. RR+ -> ( 0 /e B ) = 0 )
5	2 4	syl	|- ( ph -> ( 0 /e B ) = 0 )
6	3 5	sylan9eqr	|- ( ( ph /\ A = 0 ) -> ( A /e B ) = 0 )
7		elxrge02	|- ( ( A /e B ) e. ( 0 [,] +oo ) <-> ( ( A /e B ) = 0 \/ ( A /e B ) e. RR+ \/ ( A /e B ) = +oo ) )
8	7	biimpri	|- ( ( ( A /e B ) = 0 \/ ( A /e B ) e. RR+ \/ ( A /e B ) = +oo ) -> ( A /e B ) e. ( 0 [,] +oo ) )
9	8	3o1cs	|- ( ( A /e B ) = 0 -> ( A /e B ) e. ( 0 [,] +oo ) )
10	6 9	syl	|- ( ( ph /\ A = 0 ) -> ( A /e B ) e. ( 0 [,] +oo ) )
11		simpr	|- ( ( ph /\ A e. RR+ ) -> A e. RR+ )
12	2	adantr	|- ( ( ph /\ A e. RR+ ) -> B e. RR+ )
13	11 12	rpxdivcld	|- ( ( ph /\ A e. RR+ ) -> ( A /e B ) e. RR+ )
14	8	3o2cs	|- ( ( A /e B ) e. RR+ -> ( A /e B ) e. ( 0 [,] +oo ) )
15	13 14	syl	|- ( ( ph /\ A e. RR+ ) -> ( A /e B ) e. ( 0 [,] +oo ) )
16		oveq1	|- ( A = +oo -> ( A /e B ) = ( +oo /e B ) )
17		xdivpnfrp	|- ( B e. RR+ -> ( +oo /e B ) = +oo )
18	2 17	syl	|- ( ph -> ( +oo /e B ) = +oo )
19	16 18	sylan9eqr	|- ( ( ph /\ A = +oo ) -> ( A /e B ) = +oo )
20	8	3o3cs	|- ( ( A /e B ) = +oo -> ( A /e B ) e. ( 0 [,] +oo ) )
21	19 20	syl	|- ( ( ph /\ A = +oo ) -> ( A /e B ) e. ( 0 [,] +oo ) )
22		elxrge02	|- ( A e. ( 0 [,] +oo ) <-> ( A = 0 \/ A e. RR+ \/ A = +oo ) )
23	1 22	sylib	|- ( ph -> ( A = 0 \/ A e. RR+ \/ A = +oo ) )
24	10 15 21 23	mpjao3dan	|- ( ph -> ( A /e B ) e. ( 0 [,] +oo ) )