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

Theorem 2cnne0 11442
Description: 2 is a nonzero complex number. (Contributed by David A. Wheeler, 7-Dec-2018.)
Assertion
Ref Expression
2cnne0 (2 ∈ ℂ ∧ 2 ≠ 0)

Proof of Theorem 2cnne0
StepHypRef Expression
1 2cn 11291 . 2 2 ∈ ℂ
2 2ne0 11313 . 2 2 ≠ 0
31, 2pm3.2i 456 1 (2 ∈ ℂ ∧ 2 ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  wa 382  wcel 2145  wne 2943  cc 10134  0cc0 10136  2c2 11270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212  ax-pre-mulgt0 10213
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-po 5170  df-so 5171  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-er 7894  df-en 8108  df-dom 8109  df-sdom 8110  df-pnf 10276  df-mnf 10277  df-xr 10278  df-ltxr 10279  df-le 10280  df-sub 10468  df-neg 10469  df-2 11279
This theorem is referenced by:  1mhlfehlf  11451  2halves  11460  halfaddsub  11465  nneo  11661  zeo  11663  2tnp1ge0ge0  12831  fldiv4lem1div2uz2  12838  fldiv4lem1div2  12839  sqoddm1div8  13228  faclbnd2  13275  bpoly3  14988  cosmul  15102  sin01bnd  15114  rpnnen2lem3  15144  rpnnen2lem11  15152  odd2np1  15266  mulsucdiv2z  15278  ltoddhalfle  15286  halfleoddlt  15287  flodddiv4  15338  flodddiv4t2lthalf  15341  pythagtriplem12  15731  pythagtriplem14  15733  pythagtriplem15  15734  pythagtriplem16  15735  pythagtriplem17  15736  aaliou3lem2  24311  aaliou3lem3  24312  aaliou3lem6  24316  ptolemy  24462  sincosq4sgn  24467  sinq12gt0  24473  coskpi  24486  efeq1  24489  dvsqrt  24697  ang180lem2  24754  dquartlem1  24792  quart1  24797  atan1  24869  log2cnv  24885  basellem1  25021  basellem3  25023  ppiub  25143  bposlem6  25228  bposlem9  25231  gausslemma2dlem1a  25304  gausslemma2dlem3  25307  2lgslem1a2  25329  threehalves  29956  tan2h  33727  pigt3  33728  dvasin  33821  heiborlem6  33940  areaquad  38321  stoweidlem24  40751  wallispilem4  40795  dirkerper  40823  dirkertrigeqlem3  40827  dirkercncflem1  40830  dirkercncflem2  40831  fourierswlem  40957  fmtnorec1  41970  fmtnoprmfac2lem1  41999  fmtnoprmfac2  42000  sfprmdvdsmersenne  42041  zofldiv2ALTV  42095  1neven  42453  2zrngnmlid  42470  zofldiv2  42846  dignn0ehalf  42932
  Copyright terms: Public domain W3C validator