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 𝐵 ) = ( 𝐴 · 𝐵 ) )