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\in {ℝ}^{+}\to \mathrm{+\infty }{÷}_{𝑒}A=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		rprene0	$$⊢A\in {ℝ}^{+}\to \left(A\in ℝ\wedge A\ne 0\right)$$
2		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
3	1 2	jctil	$$⊢A\in {ℝ}^{+}\to \left(\mathrm{+\infty }\in {ℝ}^{*}\wedge \left(A\in ℝ\wedge A\ne 0\right)\right)$$
4		3anass	$$⊢\left(\mathrm{+\infty }\in {ℝ}^{*}\wedge A\in ℝ\wedge A\ne 0\right)\leftrightarrow \left(\mathrm{+\infty }\in {ℝ}^{*}\wedge \left(A\in ℝ\wedge A\ne 0\right)\right)$$
5	3 4	sylibr	$$⊢A\in {ℝ}^{+}\to \left(\mathrm{+\infty }\in {ℝ}^{*}\wedge A\in ℝ\wedge A\ne 0\right)$$
6		xdivval	$$⊢\left(\mathrm{+\infty }\in {ℝ}^{*}\wedge A\in ℝ\wedge A\ne 0\right)\to \mathrm{+\infty }{÷}_{𝑒}A=\left(\iota x\in {ℝ}^{*}|A{\cdot }_{𝑒}x=\mathrm{+\infty }\right)$$
7	5 6	syl	$$⊢A\in {ℝ}^{+}\to \mathrm{+\infty }{÷}_{𝑒}A=\left(\iota x\in {ℝ}^{*}|A{\cdot }_{𝑒}x=\mathrm{+\infty }\right)$$
8	2	a1i	$$⊢A\in {ℝ}^{+}\to \mathrm{+\infty }\in {ℝ}^{*}$$
9		xlemul2	$$⊢\left(\mathrm{+\infty }\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\wedge A\in {ℝ}^{+}\right)\to \left(\mathrm{+\infty }\le x\leftrightarrow A{\cdot }_{𝑒}\mathrm{+\infty }\le A{\cdot }_{𝑒}x\right)$$
10	2 9	mp3an1	$$⊢\left(x\in {ℝ}^{*}\wedge A\in {ℝ}^{+}\right)\to \left(\mathrm{+\infty }\le x\leftrightarrow A{\cdot }_{𝑒}\mathrm{+\infty }\le A{\cdot }_{𝑒}x\right)$$
11	10	ancoms	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{*}\right)\to \left(\mathrm{+\infty }\le x\leftrightarrow A{\cdot }_{𝑒}\mathrm{+\infty }\le A{\cdot }_{𝑒}x\right)$$
12		rpxr	$$⊢A\in {ℝ}^{+}\to A\in {ℝ}^{*}$$
13		rpgt0	$$⊢A\in {ℝ}^{+}\to 0<A$$
14		xmulpnf1	$$⊢\left(A\in {ℝ}^{*}\wedge 0<A\right)\to A{\cdot }_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
15	12 13 14	syl2anc	$$⊢A\in {ℝ}^{+}\to A{\cdot }_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
16	15	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{*}\right)\to A{\cdot }_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
17	16	breq1d	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{*}\right)\to \left(A{\cdot }_{𝑒}\mathrm{+\infty }\le A{\cdot }_{𝑒}x\leftrightarrow \mathrm{+\infty }\le A{\cdot }_{𝑒}x\right)$$
18	11 17	bitr2d	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{*}\right)\to \left(\mathrm{+\infty }\le A{\cdot }_{𝑒}x\leftrightarrow \mathrm{+\infty }\le x\right)$$
19		xmulcl	$$⊢\left(A\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to A{\cdot }_{𝑒}x\in {ℝ}^{*}$$
20	12 19	sylan	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{*}\right)\to A{\cdot }_{𝑒}x\in {ℝ}^{*}$$
21		xgepnf	$$⊢A{\cdot }_{𝑒}x\in {ℝ}^{*}\to \left(\mathrm{+\infty }\le A{\cdot }_{𝑒}x\leftrightarrow A{\cdot }_{𝑒}x=\mathrm{+\infty }\right)$$
22	20 21	syl	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{*}\right)\to \left(\mathrm{+\infty }\le A{\cdot }_{𝑒}x\leftrightarrow A{\cdot }_{𝑒}x=\mathrm{+\infty }\right)$$
23		xgepnf	$$⊢x\in {ℝ}^{*}\to \left(\mathrm{+\infty }\le x\leftrightarrow x=\mathrm{+\infty }\right)$$
24	23	adantl	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{*}\right)\to \left(\mathrm{+\infty }\le x\leftrightarrow x=\mathrm{+\infty }\right)$$
25	18 22 24	3bitr3d	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{*}\right)\to \left(A{\cdot }_{𝑒}x=\mathrm{+\infty }\leftrightarrow x=\mathrm{+\infty }\right)$$
26	8 25	riota5	$$⊢A\in {ℝ}^{+}\to \left(\iota x\in {ℝ}^{*}|A{\cdot }_{𝑒}x=\mathrm{+\infty }\right)=\mathrm{+\infty }$$
27	7 26	eqtrd	$$⊢A\in {ℝ}^{+}\to \mathrm{+\infty }{÷}_{𝑒}A=\mathrm{+\infty }$$