Theorem mulne0d 11887

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

Step	Hyp	Ref	Expression
1		mulne0d.3	. 2 ⊢ (𝜑 → 𝐴 ≠ 0)
2		mulne0d.4	. 2 ⊢ (𝜑 → 𝐵 ≠ 0)
3		msq0d.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		mul0ord.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	3, 4	mulne0bd 11886	. 2 ⊢ (𝜑 → ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) ↔ (𝐴 · 𝐵) ≠ 0))
6	1, 2, 5	mpbi2and 712	1 ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0)

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2932  (class class class)co 7403  ℂcc 11125  0cc0 11127   · cmul 11132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467

This theorem is referenced by:  divdivdiv  11940  absrpcl  15305  prodfn0  15908  ntrivcvgmullem  15915  fprodn0f  16005  tanval3  16150  tanaddlem  16182  tanadd  16183  lcmgcdlem  16623  prmdvdsbc  16743  pcqmul  16871  abvdom  20788  itg1mulc  25655  dgrmul  26226  aalioulem4  26293  taylthlem2  26332  taylthlem2OLD  26333  tanarg  26578  mulcxp  26644  cxpmul2  26648  relogbmul  26737  angcan  26762  ssscongptld  26782  chordthmlem2  26793  quad2  26799  dcubic2  26804  dcubic  26806  mcubic  26807  cubic2  26808  cubic  26809  lgamgulmlem2  26990  lgsdilem2  27294  lgsdi  27295  pntrlog2bndlem2  27539  padicabv  27591  ttgcontlem1  28810  quad3d  32673  iconstr  33746  constrrecl  33749  cos9thpiminplylem2  33763  cos9thpiminplylem3  33764  qqhghm  33965  qqhrhm  33966  itgexpif  34584  knoppndvlem1  36476  knoppndvlem2  36477  knoppndvlem7  36482  knoppndvlem14  36489  knoppndvlem16  36491  itg2addnclem  37641  areacirclem1  37678  lcmineqlem11  41998  lcmineqlem16  42003  lcmineqlem18  42005  dvrelogpow2b  42027  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  2np3bcnp1  42103  ef11d  42335  3cubeslem2  42655  radcnvrat  44286  divcan8d  45289  mccllem  45574  clim1fr1  45578  reclimc  45630  dvdivcncf  45904  stoweidlem1  45978  wallispilem4  46045  wallispilem5  46046  wallispi2lem1  46048  wallispi2lem2  46049  wallispi2  46050  stirlinglem3  46053  stirlinglem4  46054  stirlinglem10  46060  stirlinglem12  46062  stirlinglem13  46063  stirlinglem14  46064  stirlinglem15  46065  dirker2re  46069  dirkerdenne0  46070  dirkerval2  46071  dirkerre  46072  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem43  46127  fourierdlem57  46140  fourierdlem58  46141  fourierdlem62  46145  fourierdlem66  46149  fourierdlem68  46151  fourierdlem72  46155  fourierdlem76  46159  fourierdlem78  46161  fourierdlem80  46163  fourierdlem103  46186  fourierdlem104  46187  fourierswlem  46207  fouriersw  46208  sigardiv  46838  cevathlem1  46844  quad1  47582  requad01  47583  requad1  47584