# 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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{\cdot }_{𝑒}{B}={A}{B}$

### Proof

Step Hyp Ref Expression
1 renepnf ${⊢}{A}\in ℝ\to {A}\ne \mathrm{+\infty }$
2 1 adantr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}\ne \mathrm{+\infty }$
3 2 necon2bi ${⊢}{A}=\mathrm{+\infty }\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
4 3 adantl ${⊢}\left(0<{B}\wedge {A}=\mathrm{+\infty }\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
5 renemnf ${⊢}{A}\in ℝ\to {A}\ne \mathrm{-\infty }$
6 5 adantr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}\ne \mathrm{-\infty }$
7 6 necon2bi ${⊢}{A}=\mathrm{-\infty }\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
8 7 adantl ${⊢}\left({B}<0\wedge {A}=\mathrm{-\infty }\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
9 4 8 jaoi ${⊢}\left(\left(0<{B}\wedge {A}=\mathrm{+\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{-\infty }\right)\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
10 renepnf ${⊢}{B}\in ℝ\to {B}\ne \mathrm{+\infty }$
11 10 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {B}\ne \mathrm{+\infty }$
12 11 necon2bi ${⊢}{B}=\mathrm{+\infty }\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
13 12 adantl ${⊢}\left(0<{A}\wedge {B}=\mathrm{+\infty }\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
14 renemnf ${⊢}{B}\in ℝ\to {B}\ne \mathrm{-\infty }$
15 14 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {B}\ne \mathrm{-\infty }$
16 15 necon2bi ${⊢}{B}=\mathrm{-\infty }\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
17 16 adantl ${⊢}\left({A}<0\wedge {B}=\mathrm{-\infty }\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
18 13 17 jaoi ${⊢}\left(\left(0<{A}\wedge {B}=\mathrm{+\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{-\infty }\right)\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
19 9 18 jaoi ${⊢}\left(\left(\left(0<{B}\wedge {A}=\mathrm{+\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{-\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{+\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{-\infty }\right)\right)\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
20 19 con2i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to ¬\left(\left(\left(0<{B}\wedge {A}=\mathrm{+\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{-\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{+\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{-\infty }\right)\right)\right)$
21 20 iffalsed ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to if\left(\left(\left(\left(0<{B}\wedge {A}=\mathrm{+\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{-\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{+\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{-\infty }\right)\right)\right),\mathrm{+\infty },if\left(\left(\left(\left(0<{B}\wedge {A}=\mathrm{-\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{-\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{+\infty }\right)\right)\right),\mathrm{-\infty },{A}{B}\right)\right)=if\left(\left(\left(\left(0<{B}\wedge {A}=\mathrm{-\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{-\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{+\infty }\right)\right)\right),\mathrm{-\infty },{A}{B}\right)$
22 7 adantl ${⊢}\left(0<{B}\wedge {A}=\mathrm{-\infty }\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
23 3 adantl ${⊢}\left({B}<0\wedge {A}=\mathrm{+\infty }\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
24 22 23 jaoi ${⊢}\left(\left(0<{B}\wedge {A}=\mathrm{-\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{+\infty }\right)\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
25 16 adantl ${⊢}\left(0<{A}\wedge {B}=\mathrm{-\infty }\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
26 12 adantl ${⊢}\left({A}<0\wedge {B}=\mathrm{+\infty }\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
27 25 26 jaoi ${⊢}\left(\left(0<{A}\wedge {B}=\mathrm{-\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{+\infty }\right)\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
28 24 27 jaoi ${⊢}\left(\left(\left(0<{B}\wedge {A}=\mathrm{-\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{-\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{+\infty }\right)\right)\right)\to ¬\left({A}\in ℝ\wedge {B}\in ℝ\right)$
29 28 con2i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to ¬\left(\left(\left(0<{B}\wedge {A}=\mathrm{-\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{-\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{+\infty }\right)\right)\right)$
30 29 iffalsed ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to if\left(\left(\left(\left(0<{B}\wedge {A}=\mathrm{-\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{-\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{+\infty }\right)\right)\right),\mathrm{-\infty },{A}{B}\right)={A}{B}$
31 21 30 eqtrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to if\left(\left(\left(\left(0<{B}\wedge {A}=\mathrm{+\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{-\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{+\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{-\infty }\right)\right)\right),\mathrm{+\infty },if\left(\left(\left(\left(0<{B}\wedge {A}=\mathrm{-\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{-\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{+\infty }\right)\right)\right),\mathrm{-\infty },{A}{B}\right)\right)={A}{B}$
32 31 ifeq2d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to if\left(\left({A}=0\vee {B}=0\right),0,if\left(\left(\left(\left(0<{B}\wedge {A}=\mathrm{+\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{-\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{+\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{-\infty }\right)\right)\right),\mathrm{+\infty },if\left(\left(\left(\left(0<{B}\wedge {A}=\mathrm{-\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{-\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{+\infty }\right)\right)\right),\mathrm{-\infty },{A}{B}\right)\right)\right)=if\left(\left({A}=0\vee {B}=0\right),0,{A}{B}\right)$
33 rexr ${⊢}{A}\in ℝ\to {A}\in {ℝ}^{*}$
34 rexr ${⊢}{B}\in ℝ\to {B}\in {ℝ}^{*}$
35 xmulval ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}{\cdot }_{𝑒}{B}=if\left(\left({A}=0\vee {B}=0\right),0,if\left(\left(\left(\left(0<{B}\wedge {A}=\mathrm{+\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{-\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{+\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{-\infty }\right)\right)\right),\mathrm{+\infty },if\left(\left(\left(\left(0<{B}\wedge {A}=\mathrm{-\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{-\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{+\infty }\right)\right)\right),\mathrm{-\infty },{A}{B}\right)\right)\right)$
36 33 34 35 syl2an ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{\cdot }_{𝑒}{B}=if\left(\left({A}=0\vee {B}=0\right),0,if\left(\left(\left(\left(0<{B}\wedge {A}=\mathrm{+\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{-\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{+\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{-\infty }\right)\right)\right),\mathrm{+\infty },if\left(\left(\left(\left(0<{B}\wedge {A}=\mathrm{-\infty }\right)\vee \left({B}<0\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(0<{A}\wedge {B}=\mathrm{-\infty }\right)\vee \left({A}<0\wedge {B}=\mathrm{+\infty }\right)\right)\right),\mathrm{-\infty },{A}{B}\right)\right)\right)$
37 ifid ${⊢}if\left(\left({A}=0\vee {B}=0\right),{A}{B},{A}{B}\right)={A}{B}$
38 oveq1 ${⊢}{A}=0\to {A}{B}=0\cdot {B}$
39 mul02lem2 ${⊢}{B}\in ℝ\to 0\cdot {B}=0$
40 39 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to 0\cdot {B}=0$
41 38 40 sylan9eqr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}=0\right)\to {A}{B}=0$
42 oveq2 ${⊢}{B}=0\to {A}{B}={A}\cdot 0$
43 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
44 43 mul01d ${⊢}{A}\in ℝ\to {A}\cdot 0=0$
45 44 adantr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}\cdot 0=0$
46 42 45 sylan9eqr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {B}=0\right)\to {A}{B}=0$
47 41 46 jaodan ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({A}=0\vee {B}=0\right)\right)\to {A}{B}=0$
48 47 ifeq1da ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to if\left(\left({A}=0\vee {B}=0\right),{A}{B},{A}{B}\right)=if\left(\left({A}=0\vee {B}=0\right),0,{A}{B}\right)$
49 37 48 syl5eqr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{B}=if\left(\left({A}=0\vee {B}=0\right),0,{A}{B}\right)$
50 32 36 49 3eqtr4d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{\cdot }_{𝑒}{B}={A}{B}$