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 A B A 𝑒 B = A B

Proof

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