rexmul - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rexmul		Structured version Visualization version GIF version

Theorem rexmul 13214

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

**Assertion**
Ref	Expression
rexmul	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·_e 𝐵) = (𝐴 · 𝐵))

**Proof of Theorem rexmul**
Step	Hyp	Ref	Expression
1		renepnf 11184	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
2	1	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≠ +∞)
3	2	necon2bi 2963	. . . . . . . . 9 ⊢ (𝐴 = +∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
4	3	adantl 481	. . . . . . . 8 ⊢ ((0 < 𝐵 ∧ 𝐴 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
5		renemnf 11185	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
6	5	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≠ -∞)
7	6	necon2bi 2963	. . . . . . . . 9 ⊢ (𝐴 = -∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
8	7	adantl 481	. . . . . . . 8 ⊢ ((𝐵 < 0 ∧ 𝐴 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
9	4, 8	jaoi 858	. . . . . . 7 ⊢ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
10		renepnf 11184	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ +∞)
11	10	adantl 481	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ +∞)
12	11	necon2bi 2963	. . . . . . . . 9 ⊢ (𝐵 = +∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
13	12	adantl 481	. . . . . . . 8 ⊢ ((0 < 𝐴 ∧ 𝐵 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
14		renemnf 11185	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ -∞)
15	14	adantl 481	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ -∞)
16	15	necon2bi 2963	. . . . . . . . 9 ⊢ (𝐵 = -∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
17	16	adantl 481	. . . . . . . 8 ⊢ ((𝐴 < 0 ∧ 𝐵 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
18	13, 17	jaoi 858	. . . . . . 7 ⊢ (((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
19	9, 18	jaoi 858	. . . . . 6 ⊢ ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
20	19	con2i 139	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))))
21	20	iffalsed 4478	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))
22	7	adantl 481	. . . . . . . 8 ⊢ ((0 < 𝐵 ∧ 𝐴 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
23	3	adantl 481	. . . . . . . 8 ⊢ ((𝐵 < 0 ∧ 𝐴 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
24	22, 23	jaoi 858	. . . . . . 7 ⊢ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
25	16	adantl 481	. . . . . . . 8 ⊢ ((0 < 𝐴 ∧ 𝐵 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
26	12	adantl 481	. . . . . . . 8 ⊢ ((𝐴 < 0 ∧ 𝐵 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
27	25, 26	jaoi 858	. . . . . . 7 ⊢ (((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
28	24, 27	jaoi 858	. . . . . 6 ⊢ ((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
29	28	con2i 139	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))))
30	29	iffalsed 4478	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)) = (𝐴 · 𝐵))
31	21, 30	eqtrd 2772	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = (𝐴 · 𝐵))
32	31	ifeq2d 4488	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, (𝐴 · 𝐵)))
33		rexr 11182	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
34		rexr 11182	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
35		xmulval 13168	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ·_e 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
36	33, 34, 35	syl2an 597	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·_e 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
37		ifid 4508	. . 3 ⊢ if((𝐴 = 0 ∨ 𝐵 = 0), (𝐴 · 𝐵), (𝐴 · 𝐵)) = (𝐴 · 𝐵)
38		oveq1 7367	. . . . . 6 ⊢ (𝐴 = 0 → (𝐴 · 𝐵) = (0 · 𝐵))
39		mul02lem2 11314	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → (0 · 𝐵) = 0)
40	39	adantl 481	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 · 𝐵) = 0)
41	38, 40	sylan9eqr 2794	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = 0) → (𝐴 · 𝐵) = 0)
42		oveq2 7368	. . . . . 6 ⊢ (𝐵 = 0 → (𝐴 · 𝐵) = (𝐴 · 0))
43		recn 11119	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
44	43	mul01d 11336	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0)
45	44	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 0) = 0)
46	42, 45	sylan9eqr 2794	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 = 0) → (𝐴 · 𝐵) = 0)
47	41, 46	jaodan 960	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 = 0 ∨ 𝐵 = 0)) → (𝐴 · 𝐵) = 0)
48	47	ifeq1da 4499	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐴 = 0 ∨ 𝐵 = 0), (𝐴 · 𝐵), (𝐴 · 𝐵)) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, (𝐴 · 𝐵)))
49	37, 48	eqtr3id 2786	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, (𝐴 · 𝐵)))
50	32, 36, 49	3eqtr4d 2782	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·_e 𝐵) = (𝐴 · 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ifcif 4467 class class class wbr 5086 (class class class)co 7360 ℝcr 11028 0cc0 11029 · cmul 11034 +∞cpnf 11167 -∞cmnf 11168 ℝ^*cxr 11169 < clt 11170 ·_e cxmu 13053

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5519 df-po 5532 df-so 5533 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7363 df-oprab 7364 df-mpo 7365 df-er 8636 df-en 8887 df-dom 8888 df-sdom 8889 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-xmul 13056

This theorem is referenced by: xmulrid 13222 xmulgt0 13226 xmulasslem3 13229 xlemul1a 13231 xlemul1 13233 xadddilem 13237 nmoix 24704 nmoi2 24705 metnrmlem3 24837 nmoleub2lem 25091 nn0xmulclb 32859 hashxpe 32895 xrecex 32994 rexdiv 33000 pnfinf 33259 xrge0slmod 33423 fldextrspundgdvdslem 33840 fldextrspundgdvds 33841 fldext2rspun 33842 fldext2chn 33888 constrext2chnlem 33910 esumcst 34223 omssubadd 34460

W3C validator