Metamath Proof Explorer


Theorem xrpxdivcld

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

Ref Expression
Hypotheses xrpxdivcld.1 ( 𝜑𝐴 ∈ ( 0 [,] +∞ ) )
xrpxdivcld.2 ( 𝜑𝐵 ∈ ℝ+ )
Assertion xrpxdivcld ( 𝜑 → ( 𝐴 /𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 xrpxdivcld.1 ( 𝜑𝐴 ∈ ( 0 [,] +∞ ) )
2 xrpxdivcld.2 ( 𝜑𝐵 ∈ ℝ+ )
3 oveq1 ( 𝐴 = 0 → ( 𝐴 /𝑒 𝐵 ) = ( 0 /𝑒 𝐵 ) )
4 xdiv0rp ( 𝐵 ∈ ℝ+ → ( 0 /𝑒 𝐵 ) = 0 )
5 2 4 syl ( 𝜑 → ( 0 /𝑒 𝐵 ) = 0 )
6 3 5 sylan9eqr ( ( 𝜑𝐴 = 0 ) → ( 𝐴 /𝑒 𝐵 ) = 0 )
7 elxrge02 ( ( 𝐴 /𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐴 /𝑒 𝐵 ) = 0 ∨ ( 𝐴 /𝑒 𝐵 ) ∈ ℝ+ ∨ ( 𝐴 /𝑒 𝐵 ) = +∞ ) )
8 7 biimpri ( ( ( 𝐴 /𝑒 𝐵 ) = 0 ∨ ( 𝐴 /𝑒 𝐵 ) ∈ ℝ+ ∨ ( 𝐴 /𝑒 𝐵 ) = +∞ ) → ( 𝐴 /𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )
9 8 3o1cs ( ( 𝐴 /𝑒 𝐵 ) = 0 → ( 𝐴 /𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )
10 6 9 syl ( ( 𝜑𝐴 = 0 ) → ( 𝐴 /𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )
11 simpr ( ( 𝜑𝐴 ∈ ℝ+ ) → 𝐴 ∈ ℝ+ )
12 2 adantr ( ( 𝜑𝐴 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ )
13 11 12 rpxdivcld ( ( 𝜑𝐴 ∈ ℝ+ ) → ( 𝐴 /𝑒 𝐵 ) ∈ ℝ+ )
14 8 3o2cs ( ( 𝐴 /𝑒 𝐵 ) ∈ ℝ+ → ( 𝐴 /𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )
15 13 14 syl ( ( 𝜑𝐴 ∈ ℝ+ ) → ( 𝐴 /𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )
16 oveq1 ( 𝐴 = +∞ → ( 𝐴 /𝑒 𝐵 ) = ( +∞ /𝑒 𝐵 ) )
17 xdivpnfrp ( 𝐵 ∈ ℝ+ → ( +∞ /𝑒 𝐵 ) = +∞ )
18 2 17 syl ( 𝜑 → ( +∞ /𝑒 𝐵 ) = +∞ )
19 16 18 sylan9eqr ( ( 𝜑𝐴 = +∞ ) → ( 𝐴 /𝑒 𝐵 ) = +∞ )
20 8 3o3cs ( ( 𝐴 /𝑒 𝐵 ) = +∞ → ( 𝐴 /𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )
21 19 20 syl ( ( 𝜑𝐴 = +∞ ) → ( 𝐴 /𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )
22 elxrge02 ( 𝐴 ∈ ( 0 [,] +∞ ) ↔ ( 𝐴 = 0 ∨ 𝐴 ∈ ℝ+𝐴 = +∞ ) )
23 1 22 sylib ( 𝜑 → ( 𝐴 = 0 ∨ 𝐴 ∈ ℝ+𝐴 = +∞ ) )
24 10 15 21 23 mpjao3dan ( 𝜑 → ( 𝐴 /𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )