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

Theorem rexmul 12302
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
StepHypRef Expression
1 renepnf 10340 . . . . . . . . . . 11 (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
21adantr 472 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≠ +∞)
32necon2bi 2966 . . . . . . . . 9 (𝐴 = +∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
43adantl 473 . . . . . . . 8 ((0 < 𝐵𝐴 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
5 renemnf 10341 . . . . . . . . . . 11 (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
65adantr 472 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≠ -∞)
76necon2bi 2966 . . . . . . . . 9 (𝐴 = -∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
87adantl 473 . . . . . . . 8 ((𝐵 < 0 ∧ 𝐴 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
94, 8jaoi 883 . . . . . . 7 (((0 < 𝐵𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
10 renepnf 10340 . . . . . . . . . . 11 (𝐵 ∈ ℝ → 𝐵 ≠ +∞)
1110adantl 473 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ +∞)
1211necon2bi 2966 . . . . . . . . 9 (𝐵 = +∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
1312adantl 473 . . . . . . . 8 ((0 < 𝐴𝐵 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
14 renemnf 10341 . . . . . . . . . . 11 (𝐵 ∈ ℝ → 𝐵 ≠ -∞)
1514adantl 473 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ -∞)
1615necon2bi 2966 . . . . . . . . 9 (𝐵 = -∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
1716adantl 473 . . . . . . . 8 ((𝐴 < 0 ∧ 𝐵 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
1813, 17jaoi 883 . . . . . . 7 (((0 < 𝐴𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
199, 18jaoi 883 . . . . . 6 ((((0 < 𝐵𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
2019con2i 136 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (((0 < 𝐵𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))))
2120iffalsed 4253 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((((0 < 𝐵𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = if((((0 < 𝐵𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))
227adantl 473 . . . . . . . 8 ((0 < 𝐵𝐴 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
233adantl 473 . . . . . . . 8 ((𝐵 < 0 ∧ 𝐴 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
2422, 23jaoi 883 . . . . . . 7 (((0 < 𝐵𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
2516adantl 473 . . . . . . . 8 ((0 < 𝐴𝐵 = -∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
2612adantl 473 . . . . . . . 8 ((𝐴 < 0 ∧ 𝐵 = +∞) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
2725, 26jaoi 883 . . . . . . 7 (((0 < 𝐴𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
2824, 27jaoi 883 . . . . . 6 ((((0 < 𝐵𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
2928con2i 136 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (((0 < 𝐵𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))))
3029iffalsed 4253 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((((0 < 𝐵𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)) = (𝐴 · 𝐵))
3121, 30eqtrd 2798 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((((0 < 𝐵𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = (𝐴 · 𝐵))
3231ifeq2d 4261 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, (𝐴 · 𝐵)))
33 rexr 10338 . . 3 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
34 rexr 10338 . . 3 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
35 xmulval 12257 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
3633, 34, 35syl2an 589 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
37 ifid 4281 . . 3 if((𝐴 = 0 ∨ 𝐵 = 0), (𝐴 · 𝐵), (𝐴 · 𝐵)) = (𝐴 · 𝐵)
38 oveq1 6848 . . . . . 6 (𝐴 = 0 → (𝐴 · 𝐵) = (0 · 𝐵))
39 mul02lem2 10466 . . . . . . 7 (𝐵 ∈ ℝ → (0 · 𝐵) = 0)
4039adantl 473 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 · 𝐵) = 0)
4138, 40sylan9eqr 2820 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = 0) → (𝐴 · 𝐵) = 0)
42 oveq2 6849 . . . . . 6 (𝐵 = 0 → (𝐴 · 𝐵) = (𝐴 · 0))
43 recn 10278 . . . . . . . 8 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
4443mul01d 10488 . . . . . . 7 (𝐴 ∈ ℝ → (𝐴 · 0) = 0)
4544adantr 472 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 0) = 0)
4642, 45sylan9eqr 2820 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 = 0) → (𝐴 · 𝐵) = 0)
4741, 46jaodan 980 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 = 0 ∨ 𝐵 = 0)) → (𝐴 · 𝐵) = 0)
4847ifeq1da 4272 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐴 = 0 ∨ 𝐵 = 0), (𝐴 · 𝐵), (𝐴 · 𝐵)) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, (𝐴 · 𝐵)))
4937, 48syl5eqr 2812 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, (𝐴 · 𝐵)))
5032, 36, 493eqtr4d 2808 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐵) = (𝐴 · 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wo 873   = wceq 1652  wcel 2155  wne 2936  ifcif 4242   class class class wbr 4808  (class class class)co 6841  cr 10187  0cc0 10188   · cmul 10193  +∞cpnf 10324  -∞cmnf 10325  *cxr 10326   < clt 10327   ·e cxmu 12144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-po 5197  df-so 5198  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-er 7946  df-en 8160  df-dom 8161  df-sdom 8162  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-xmul 12147
This theorem is referenced by:  xmulid1  12310  xmulgt0  12314  xmulasslem3  12317  xlemul1a  12319  xlemul1  12321  xadddilem  12325  nmoix  22811  nmoi2  22812  metnrmlem3  22942  nmoleub2lem  23191  xrecex  30009  rexdiv  30015  pnfinf  30118  xrge0slmod  30225  esumcst  30506  omssubadd  30743
  Copyright terms: Public domain W3C validator