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 13172

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 11167	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
2	1	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≠ +∞)
3	2	necon2bi 2959	. . . . . . . . 9 ⊢ (𝐴 = +∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
4	3	adantl 481	. . . . . . . 8 ⊢ ((0 < 𝐵 ∧ 𝐴 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
5		renemnf 11168	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
6	5	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≠ -∞)
7	6	necon2bi 2959	. . . . . . . . 9 ⊢ (𝐴 = -∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
8	7	adantl 481	. . . . . . . 8 ⊢ ((𝐵 < 0 ∧ 𝐴 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
9	4, 8	jaoi 857	. . . . . . 7 ⊢ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
10		renepnf 11167	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ +∞)
11	10	adantl 481	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ +∞)
12	11	necon2bi 2959	. . . . . . . . 9 ⊢ (𝐵 = +∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
13	12	adantl 481	. . . . . . . 8 ⊢ ((0 < 𝐴 ∧ 𝐵 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
14		renemnf 11168	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ -∞)
15	14	adantl 481	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ -∞)
16	15	necon2bi 2959	. . . . . . . . 9 ⊢ (𝐵 = -∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
17	16	adantl 481	. . . . . . . 8 ⊢ ((𝐴 < 0 ∧ 𝐵 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
18	13, 17	jaoi 857	. . . . . . 7 ⊢ (((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
19	9, 18	jaoi 857	. . . . . 6 ⊢ ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
20	19	con2i 139	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))))
21	20	iffalsed 4485	. . . 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 857	. . . . . . 7 ⊢ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
25	16	adantl 481	. . . . . . . 8 ⊢ ((0 < 𝐴 ∧ 𝐵 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
26	12	adantl 481	. . . . . . . 8 ⊢ ((𝐴 < 0 ∧ 𝐵 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
27	25, 26	jaoi 857	. . . . . . 7 ⊢ (((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
28	24, 27	jaoi 857	. . . . . 6 ⊢ ((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
29	28	con2i 139	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))))
30	29	iffalsed 4485	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)) = (𝐴 · 𝐵))
31	21, 30	eqtrd 2768	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = (𝐴 · 𝐵))
32	31	ifeq2d 4495	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, (𝐴 · 𝐵)))
33		rexr 11165	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
34		rexr 11165	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
35		xmulval 13126	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ·_e 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
36	33, 34, 35	syl2an 596	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·_e 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
37		ifid 4515	. . 3 ⊢ if((𝐴 = 0 ∨ 𝐵 = 0), (𝐴 · 𝐵), (𝐴 · 𝐵)) = (𝐴 · 𝐵)
38		oveq1 7359	. . . . . 6 ⊢ (𝐴 = 0 → (𝐴 · 𝐵) = (0 · 𝐵))
39		mul02lem2 11297	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → (0 · 𝐵) = 0)
40	39	adantl 481	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 · 𝐵) = 0)
41	38, 40	sylan9eqr 2790	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = 0) → (𝐴 · 𝐵) = 0)
42		oveq2 7360	. . . . . 6 ⊢ (𝐵 = 0 → (𝐴 · 𝐵) = (𝐴 · 0))
43		recn 11103	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
44	43	mul01d 11319	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0)
45	44	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 0) = 0)
46	42, 45	sylan9eqr 2790	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 = 0) → (𝐴 · 𝐵) = 0)
47	41, 46	jaodan 959	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 = 0 ∨ 𝐵 = 0)) → (𝐴 · 𝐵) = 0)
48	47	ifeq1da 4506	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐴 = 0 ∨ 𝐵 = 0), (𝐴 · 𝐵), (𝐴 · 𝐵)) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, (𝐴 · 𝐵)))
49	37, 48	eqtr3id 2782	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, (𝐴 · 𝐵)))
50	32, 36, 49	3eqtr4d 2778	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·_e 𝐵) = (𝐴 · 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 ifcif 4474 class class class wbr 5093 (class class class)co 7352 ℝcr 11012 0cc0 11013 · cmul 11018 +∞cpnf 11150 -∞cmnf 11151 ℝ^*cxr 11152 < clt 11153 ·_e cxmu 13012

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-br 5094 df-opab 5156 df-mpt 5175 df-id 5514 df-po 5527 df-so 5528 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-ov 7355 df-oprab 7356 df-mpo 7357 df-er 8628 df-en 8876 df-dom 8877 df-sdom 8878 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-xmul 13015

This theorem is referenced by: xmulrid 13180 xmulgt0 13184 xmulasslem3 13187 xlemul1a 13189 xlemul1 13191 xadddilem 13195 nmoix 24645 nmoi2 24646 metnrmlem3 24778 nmoleub2lem 25042 nn0xmulclb 32758 hashxpe 32794 xrecex 32907 rexdiv 32913 pnfinf 33159 xrge0slmod 33320 fldextrspundgdvdslem 33714 fldextrspundgdvds 33715 fldext2rspun 33716 fldext2chn 33762 constrext2chnlem 33784 esumcst 34097 omssubadd 34334

W3C validator