Metamath Proof Explorer

Theorem rexmul

Description: The extended real multiplication when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion rexmul ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ·e 𝐵 ) = ( 𝐴 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 renepnf ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ +∞ )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ≠ +∞ )
3 2 necon2bi ⊢ ( 𝐴 = +∞ → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
4 3 adantl ⊢ ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
5 renemnf ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ -∞ )
6 5 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ≠ -∞ )
7 6 necon2bi ⊢ ( 𝐴 = -∞ → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
8 7 adantl ⊢ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
9 4 8 jaoi ⊢ ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
10 renepnf ⊢ ( 𝐵 ∈ ℝ → 𝐵 ≠ +∞ )
11 10 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ≠ +∞ )
12 11 necon2bi ⊢ ( 𝐵 = +∞ → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
13 12 adantl ⊢ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
14 renemnf ⊢ ( 𝐵 ∈ ℝ → 𝐵 ≠ -∞ )
15 14 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ≠ -∞ )
16 15 necon2bi ⊢ ( 𝐵 = -∞ → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
17 16 adantl ⊢ ( ( 𝐴 < 0 ∧ 𝐵 = -∞ ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
18 13 17 jaoi ⊢ ( ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
19 9 18 jaoi ⊢ ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
20 19 con2i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ¬ ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) )
21 20 iffalsed ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) ) = if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) )
22 7 adantl ⊢ ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
23 3 adantl ⊢ ( ( 𝐵 < 0 ∧ 𝐴 = +∞ ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
24 22 23 jaoi ⊢ ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
25 16 adantl ⊢ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
26 12 adantl ⊢ ( ( 𝐴 < 0 ∧ 𝐵 = +∞ ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
27 25 26 jaoi ⊢ ( ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
28 24 27 jaoi ⊢ ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
29 28 con2i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ¬ ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) )
30 29 iffalsed ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) = ( 𝐴 · 𝐵 ) )
31 21 30 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) ) = ( 𝐴 · 𝐵 ) )
32 31 ifeq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) , 0 , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) ) ) = if ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) , 0 , ( 𝐴 · 𝐵 ) ) )
33 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
34 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
35 xmulval ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e 𝐵 ) = if ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) , 0 , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) ) ) )
36 33 34 35 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ·e 𝐵 ) = if ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) , 0 , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) ) ) )
37 ifid ⊢ if ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) , ( 𝐴 · 𝐵 ) , ( 𝐴 · 𝐵 ) ) = ( 𝐴 · 𝐵 )
38 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 · 𝐵 ) = ( 0 · 𝐵 ) )
39 mul02lem2 ⊢ ( 𝐵 ∈ ℝ → ( 0 · 𝐵 ) = 0 )
40 39 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 · 𝐵 ) = 0 )
41 38 40 sylan9eqr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → ( 𝐴 · 𝐵 ) = 0 )
42 oveq2 ⊢ ( 𝐵 = 0 → ( 𝐴 · 𝐵 ) = ( 𝐴 · 0 ) )
43 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
44 43 mul01d ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )
45 44 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 0 ) = 0 )
46 42 45 sylan9eqr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 = 0 ) → ( 𝐴 · 𝐵 ) = 0 )
47 41 46 jaodan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 = 0 ∨ 𝐵 = 0 ) ) → ( 𝐴 · 𝐵 ) = 0 )
48 47 ifeq1da ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) , ( 𝐴 · 𝐵 ) , ( 𝐴 · 𝐵 ) ) = if ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) , 0 , ( 𝐴 · 𝐵 ) ) )
49 37 48 eqtr3id ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) = if ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) , 0 , ( 𝐴 · 𝐵 ) ) )
50 32 36 49 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ·e 𝐵 ) = ( 𝐴 · 𝐵 ) )