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	⊢ ( 𝐴 ∈ ℝ+ → ( +∞ /𝑒 𝐴 ) = +∞ )

Proof

Step	Hyp	Ref	Expression
1		rprene0	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) )
2		pnfxr	⊢ +∞ ∈ ℝ*
3	1 2	jctil	⊢ ( 𝐴 ∈ ℝ+ → ( +∞ ∈ ℝ* ∧ ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ) )
4		3anass	⊢ ( ( +∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ↔ ( +∞ ∈ ℝ* ∧ ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ) )
5	3 4	sylibr	⊢ ( 𝐴 ∈ ℝ+ → ( +∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) )
6		xdivval	⊢ ( ( +∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( +∞ /𝑒 𝐴 ) = ( ℩ 𝑥 ∈ ℝ* ( 𝐴 ·e 𝑥 ) = +∞ ) )
7	5 6	syl	⊢ ( 𝐴 ∈ ℝ+ → ( +∞ /𝑒 𝐴 ) = ( ℩ 𝑥 ∈ ℝ* ( 𝐴 ·e 𝑥 ) = +∞ ) )
8	2	a1i	⊢ ( 𝐴 ∈ ℝ+ → +∞ ∈ ℝ* )
9		xlemul2	⊢ ( ( +∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝐴 ∈ ℝ+ ) → ( +∞ ≤ 𝑥 ↔ ( 𝐴 ·e +∞ ) ≤ ( 𝐴 ·e 𝑥 ) ) )
10	2 9	mp3an1	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ∈ ℝ+ ) → ( +∞ ≤ 𝑥 ↔ ( 𝐴 ·e +∞ ) ≤ ( 𝐴 ·e 𝑥 ) ) )
11	10	ancoms	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ* ) → ( +∞ ≤ 𝑥 ↔ ( 𝐴 ·e +∞ ) ≤ ( 𝐴 ·e 𝑥 ) ) )
12		rpxr	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ* )
13		rpgt0	⊢ ( 𝐴 ∈ ℝ+ → 0 < 𝐴 )
14		xmulpnf1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e +∞ ) = +∞ )
15	12 13 14	syl2anc	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ·e +∞ ) = +∞ )
16	15	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ* ) → ( 𝐴 ·e +∞ ) = +∞ )
17	16	breq1d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ* ) → ( ( 𝐴 ·e +∞ ) ≤ ( 𝐴 ·e 𝑥 ) ↔ +∞ ≤ ( 𝐴 ·e 𝑥 ) ) )
18	11 17	bitr2d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ* ) → ( +∞ ≤ ( 𝐴 ·e 𝑥 ) ↔ +∞ ≤ 𝑥 ) )
19		xmulcl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝐴 ·e 𝑥 ) ∈ ℝ* )
20	12 19	sylan	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ* ) → ( 𝐴 ·e 𝑥 ) ∈ ℝ* )
21		xgepnf	⊢ ( ( 𝐴 ·e 𝑥 ) ∈ ℝ* → ( +∞ ≤ ( 𝐴 ·e 𝑥 ) ↔ ( 𝐴 ·e 𝑥 ) = +∞ ) )
22	20 21	syl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ* ) → ( +∞ ≤ ( 𝐴 ·e 𝑥 ) ↔ ( 𝐴 ·e 𝑥 ) = +∞ ) )
23		xgepnf	⊢ ( 𝑥 ∈ ℝ* → ( +∞ ≤ 𝑥 ↔ 𝑥 = +∞ ) )
24	23	adantl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ* ) → ( +∞ ≤ 𝑥 ↔ 𝑥 = +∞ ) )
25	18 22 24	3bitr3d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ* ) → ( ( 𝐴 ·e 𝑥 ) = +∞ ↔ 𝑥 = +∞ ) )
26	8 25	riota5	⊢ ( 𝐴 ∈ ℝ+ → ( ℩ 𝑥 ∈ ℝ* ( 𝐴 ·e 𝑥 ) = +∞ ) = +∞ )
27	7 26	eqtrd	⊢ ( 𝐴 ∈ ℝ+ → ( +∞ /𝑒 𝐴 ) = +∞ )