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 [,] +∞ ) )