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 13288

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 11245	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
2	1	adantr 485	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≠ +∞)
3	2	necon2bi 2990	. . . . . . . . 9 ⊢ (𝐴 = +∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
4	3	adantl 486	. . . . . . . 8 ⊢ ((0 < 𝐵 ∧ 𝐴 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
5		renemnf 11246	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
6	5	adantr 485	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≠ -∞)
7	6	necon2bi 2990	. . . . . . . . 9 ⊢ (𝐴 = -∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
8	7	adantl 486	. . . . . . . 8 ⊢ ((𝐵 < 0 ∧ 𝐴 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
9	4, 8	jaoi 870	. . . . . . 7 ⊢ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
10		renepnf 11245	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ +∞)
11	10	adantl 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ +∞)
12	11	necon2bi 2990	. . . . . . . . 9 ⊢ (𝐵 = +∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
13	12	adantl 486	. . . . . . . 8 ⊢ ((0 < 𝐴 ∧ 𝐵 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
14		renemnf 11246	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ -∞)
15	14	adantl 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ -∞)
16	15	necon2bi 2990	. . . . . . . . 9 ⊢ (𝐵 = -∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
17	16	adantl 486	. . . . . . . 8 ⊢ ((𝐴 < 0 ∧ 𝐵 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
18	13, 17	jaoi 870	. . . . . . 7 ⊢ (((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
19	9, 18	jaoi 870	. . . . . 6 ⊢ ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
20	19	con2i 140	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))))
21	20	iffalsed 4494	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))
22	7	adantl 486	. . . . . . . 8 ⊢ ((0 < 𝐵 ∧ 𝐴 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
23	3	adantl 486	. . . . . . . 8 ⊢ ((𝐵 < 0 ∧ 𝐴 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
24	22, 23	jaoi 870	. . . . . . 7 ⊢ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
25	16	adantl 486	. . . . . . . 8 ⊢ ((0 < 𝐴 ∧ 𝐵 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
26	12	adantl 486	. . . . . . . 8 ⊢ ((𝐴 < 0 ∧ 𝐵 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
27	25, 26	jaoi 870	. . . . . . 7 ⊢ (((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
28	24, 27	jaoi 870	. . . . . 6 ⊢ ((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
29	28	con2i 140	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))))
30	29	iffalsed 4494	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)) = (𝐴 · 𝐵))
31	21, 30	eqtrd 2800	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = (𝐴 · 𝐵))
32	31	ifeq2d 4504	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, (𝐴 · 𝐵)))
33		rexr 11243	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
34		rexr 11243	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
35		xmulval 13242	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ·_e 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
36	33, 34, 35	syl2an 607	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·_e 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
37		ifid 4524	. . 3 ⊢ if((𝐴 = 0 ∨ 𝐵 = 0), (𝐴 · 𝐵), (𝐴 · 𝐵)) = (𝐴 · 𝐵)
38		oveq1 7407	. . . . . 6 ⊢ (𝐴 = 0 → (𝐴 · 𝐵) = (0 · 𝐵))
39		mul02lem2 11375	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → (0 · 𝐵) = 0)
40	39	adantl 486	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 · 𝐵) = 0)
41	38, 40	sylan9eqr 2822	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = 0) → (𝐴 · 𝐵) = 0)
42		oveq2 7408	. . . . . 6 ⊢ (𝐵 = 0 → (𝐴 · 𝐵) = (𝐴 · 0))
43		recn 11178	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
44	43	mul01d 11397	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0)
45	44	adantr 485	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 0) = 0)
46	42, 45	sylan9eqr 2822	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 = 0) → (𝐴 · 𝐵) = 0)
47	41, 46	jaodan 972	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 = 0 ∨ 𝐵 = 0)) → (𝐴 · 𝐵) = 0)
48	47	ifeq1da 4515	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐴 = 0 ∨ 𝐵 = 0), (𝐴 · 𝐵), (𝐴 · 𝐵)) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, (𝐴 · 𝐵)))
49	37, 48	eqtr3id 2814	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, (𝐴 · 𝐵)))
50	32, 36, 49	3eqtr4d 2810	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·_e 𝐵) = (𝐴 · 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 ∨ wo 860 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ifcif 4483 class class class wbr 5105 (class class class)co 7400 ℝcr 11087 0cc0 11088 · cmul 11093 +∞cpnf 11228 -∞cmnf 11229 ℝ^*cxr 11230 < clt 11231 ·_e cxmu 13127

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-br 5106 df-opab 5168 df-mpt 5187 df-id 5547 df-po 5560 df-so 5561 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-xmul 13130

This theorem is referenced by: xmulrid 13296 xmulgt0 13300 xmulasslem3 13303 xlemul1a 13305 xlemul1 13307 xadddilem 13311 nmoix 24847 nmoi2 24848 metnrmlem3 24980 nmoleub2lem 25234 nn0xmulclb 33028 hashxpe 33064 xrecex 33152 rexdiv 33158 pnfinf 33416 xrge0slmod 33583 fldextrspundgdvdslem 33987 fldextrspundgdvds 33988 fldext2rspun 33989 fldext2chn 34035 constrext2chnlem 34057 esumcst 34370 omssubadd 34607

W3C validator