Metamath Proof Explorer

Theorem xmulpnf1

Description: Multiplication by plus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulpnf1 ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e +∞ ) = +∞ )

Proof

Step Hyp Ref Expression
1 pnfxr ⊢ +∞ ∈ ℝ*
2 xmulval ⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 ·e +∞ ) = if ( ( 𝐴 = 0 ∨ +∞ = 0 ) , 0 , if ( ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < +∞ ∧ 𝐴 = -∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = -∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = +∞ ) ) ) , -∞ , ( 𝐴 · +∞ ) ) ) ) )
3 1 2 mpan2 ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ·e +∞ ) = if ( ( 𝐴 = 0 ∨ +∞ = 0 ) , 0 , if ( ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < +∞ ∧ 𝐴 = -∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = -∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = +∞ ) ) ) , -∞ , ( 𝐴 · +∞ ) ) ) ) )
4 3 adantr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e +∞ ) = if ( ( 𝐴 = 0 ∨ +∞ = 0 ) , 0 , if ( ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < +∞ ∧ 𝐴 = -∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = -∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = +∞ ) ) ) , -∞ , ( 𝐴 · +∞ ) ) ) ) )
5 0xr ⊢ 0 ∈ ℝ*
6 xrltne ⊢ ( ( 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
7 5 6 mp3an1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
8 0re ⊢ 0 ∈ ℝ
9 renepnf ⊢ ( 0 ∈ ℝ → 0 ≠ +∞ )
10 8 9 ax-mp ⊢ 0 ≠ +∞
11 10 necomi ⊢ +∞ ≠ 0
12 neanior ⊢ ( ( 𝐴 ≠ 0 ∧ +∞ ≠ 0 ) ↔ ¬ ( 𝐴 = 0 ∨ +∞ = 0 ) )
13 7 11 12 sylanblc ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ¬ ( 𝐴 = 0 ∨ +∞ = 0 ) )
14 13 iffalsed ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → if ( ( 𝐴 = 0 ∨ +∞ = 0 ) , 0 , if ( ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < +∞ ∧ 𝐴 = -∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = -∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = +∞ ) ) ) , -∞ , ( 𝐴 · +∞ ) ) ) ) = if ( ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < +∞ ∧ 𝐴 = -∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = -∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = +∞ ) ) ) , -∞ , ( 𝐴 · +∞ ) ) ) )
15 simpr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 0 < 𝐴 )
16 eqid ⊢ +∞ = +∞
17 15 16 jctir ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 0 < 𝐴 ∧ +∞ = +∞ ) )
18 17 orcd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) )
19 18 olcd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) )
20 19 iftrued ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → if ( ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < +∞ ∧ 𝐴 = -∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = -∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = +∞ ) ) ) , -∞ , ( 𝐴 · +∞ ) ) ) = +∞ )
21 4 14 20 3eqtrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e +∞ ) = +∞ )