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

Theorem mulne0d 11508
Description: The product of two nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
msq0d.1 (𝜑𝐴 ∈ ℂ)
mul0ord.2 (𝜑𝐵 ∈ ℂ)
mulne0d.3 (𝜑𝐴 ≠ 0)
mulne0d.4 (𝜑𝐵 ≠ 0)
Assertion
Ref Expression
mulne0d (𝜑 → (𝐴 · 𝐵) ≠ 0)

Proof of Theorem mulne0d
StepHypRef Expression
1 mulne0d.3 . 2 (𝜑𝐴 ≠ 0)
2 mulne0d.4 . 2 (𝜑𝐵 ≠ 0)
3 msq0d.1 . . 3 (𝜑𝐴 ∈ ℂ)
4 mul0ord.2 . . 3 (𝜑𝐵 ∈ ℂ)
53, 4mulne0bd 11507 . 2 (𝜑 → ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) ↔ (𝐴 · 𝐵) ≠ 0))
61, 2, 5mpbi2and 712 1 (𝜑 → (𝐴 · 𝐵) ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  wne 2941  (class class class)co 7231  cc 10751  0cc0 10753   · cmul 10758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-mulcom 10817  ax-addass 10818  ax-mulass 10819  ax-distr 10820  ax-i2m1 10821  ax-1ne0 10822  ax-1rid 10823  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826  ax-pre-lttri 10827  ax-pre-lttrn 10828  ax-pre-ltadd 10829  ax-pre-mulgt0 10830
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-br 5068  df-opab 5130  df-mpt 5150  df-id 5469  df-po 5482  df-so 5483  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-riota 7188  df-ov 7234  df-oprab 7235  df-mpo 7236  df-er 8411  df-en 8647  df-dom 8648  df-sdom 8649  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-sub 11088  df-neg 11089
This theorem is referenced by:  divdivdiv  11557  absrpcl  14876  prodfn0  15482  ntrivcvgmullem  15489  fprodn0f  15577  tanval3  15719  tanaddlem  15751  tanadd  15752  lcmgcdlem  16187  pcqmul  16430  abvdom  19898  itg1mulc  24626  dgrmul  25188  aalioulem4  25252  taylthlem2  25290  tanarg  25531  mulcxp  25597  cxpmul2  25601  relogbmul  25684  angcan  25709  ssscongptld  25729  chordthmlem2  25740  quad2  25746  dcubic2  25751  dcubic  25753  mcubic  25754  cubic2  25755  cubic  25756  lgamgulmlem2  25936  lgsdilem2  26238  lgsdi  26239  pntrlog2bndlem2  26483  padicabv  26535  ttgcontlem1  27000  prmdvdsbc  30874  qqhghm  31674  qqhrhm  31675  itgexpif  32322  knoppndvlem1  34455  knoppndvlem2  34456  knoppndvlem7  34461  knoppndvlem14  34468  knoppndvlem16  34470  itg2addnclem  35591  areacirclem1  35628  lcmineqlem11  39807  lcmineqlem16  39812  lcmineqlem18  39814  dvrelogpow2b  39835  aks4d1p1p6  39840  aks4d1p1p7  39841  aks4d1p1p5  39842  2np3bcnp1  39851  3cubeslem2  40238  radcnvrat  41633  divcan8d  42552  mccllem  42841  clim1fr1  42845  reclimc  42897  dvdivcncf  43171  stoweidlem1  43245  wallispilem4  43312  wallispilem5  43313  wallispi2lem1  43315  wallispi2lem2  43316  wallispi2  43317  stirlinglem3  43320  stirlinglem4  43321  stirlinglem10  43327  stirlinglem12  43329  stirlinglem13  43330  stirlinglem14  43331  stirlinglem15  43332  dirker2re  43336  dirkerdenne0  43337  dirkerval2  43338  dirkerre  43339  dirkertrigeqlem2  43343  dirkertrigeqlem3  43344  dirkertrigeq  43345  dirkercncflem2  43348  dirkercncflem4  43350  fourierdlem43  43394  fourierdlem57  43407  fourierdlem58  43408  fourierdlem62  43412  fourierdlem66  43416  fourierdlem68  43418  fourierdlem72  43422  fourierdlem76  43426  fourierdlem78  43428  fourierdlem80  43430  fourierdlem103  43453  fourierdlem104  43454  fourierswlem  43474  fouriersw  43475  sigardiv  44077  cevathlem1  44083  quad1  44773  requad01  44774  requad1  44775
  Copyright terms: Public domain W3C validator