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 +∞ ) = +∞ )