MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2cnd Structured version   Unicode version

Theorem 2cnd 10614
Description: 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
2cnd  |-  ( ph  ->  2  e.  CC )

Proof of Theorem 2cnd
StepHypRef Expression
1 2cn 10612 . 2  |-  2  e.  CC
21a1i 11 1  |-  ( ph  ->  2  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   CCcc 9493   2c2 10591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rrecex 9567  ax-cnre 9568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284  df-2 10600
This theorem is referenced by:  cnm2m1cnm3  10796  zeo2  10955  flhalf  11941  2txmodxeq0  12026  binom3  12266  zesq  12268  expmulnbnd  12277  discr  12282  amgm2  13181  iseraltlem2  13484  iseralt  13486  trirecip  13653  geo2sum  13661  ege2le3  13703  tanval3  13746  sinhval  13766  tanhlt1  13772  sqrt2irr  13859  oddm1even  13924  oddp1even  13925  bitsp1e  13959  bitsp1o  13960  bitsfzo  13962  bitsmod  13963  bitsinv1lem  13968  sadadd2lem2  13977  sadcaddlem  13984  bitsuz  14001  bitsshft  14002  prmdiv  14192  iserodd  14236  4sqlem7  14339  4sqlem10  14342  4sqlem19  14358  2expltfac  14454  efgredlemg  16634  frgpnabllem1  16751  metnrmlem3  21238  iihalf1cn  21305  iihalf2cn  21307  pcoass  21397  csbren  21699  trirn  21700  minveclem2  21714  ovolunlem1a  21780  uniioombllem5  21869  uniioombl  21871  dyaddisjlem  21877  mbfi1fseqlem5  21999  mbfi1fseqlem6  22000  dvsincos  22255  lhop1  22288  cosargd  22865  root1id  23000  ssscongptld  23028  chordthmlem  23035  chordthmlem2  23036  chordthmlem4  23038  heron  23041  dcubic1  23048  mcubic  23050  cubic2  23051  quartlem4  23063  quart  23064  cosasin  23107  cosatan  23124  atantayl  23140  atantayl2  23141  atantayl3  23142  log2tlbnd  23148  cxp2limlem  23177  divsqrtsumlem  23181  ftalem2  23219  basellem2  23227  basellem3  23228  basellem5  23230  basellem8  23233  logfaclbnd  23369  perfect  23378  bcp1ctr  23426  bposlem1  23431  bposlem2  23432  lgslem1  23443  lgsqrlem2  23489  lgseisenlem1  23496  lgseisenlem2  23497  lgseisenlem3  23498  lgseisenlem4  23499  lgsquadlem1  23501  lgsquadlem2  23502  lgsquad2lem1  23505  chebbnd1lem3  23528  chto1ub  23533  dchrisumlem2  23547  dchrisum0flblem2  23566  dchrisum0fno1  23568  dchrisum0lem1b  23572  dchrisum0lem1  23573  dchrisum0lem2  23575  mulog2sumlem2  23592  vmalogdivsum2  23595  log2sumbnd  23601  selberglem2  23603  chpdifbndlem1  23610  selberg3lem1  23614  selberg3  23616  selberg4lem1  23617  selberg4  23618  selberg4r  23627  selberg34r  23628  pntrlog2bndlem3  23636  pntrlog2bndlem4  23637  pntrlog2bndlem5  23638  pntrlog2bndlem6  23640  pntpbnd1a  23642  pntpbnd2  23644  pntibndlem2  23648  pntlemb  23654  pntlemg  23655  pntlemh  23656  pntlemr  23659  pntlemk  23663  pntlemo  23664  ostth2lem1  23675  wwlkextwrd  24600  wwlkextinj  24602  clwlkisclwwlklem2a1  24651  clwlkisclwwlklem2a4  24656  clwlkisclwwlklem0  24660  clwwlkext2edg  24674  extwwlkfablem1  24946  extwwlkfablem2  24950  numclwwlkovf2ex  24958  numclwlk1lem2foa  24963  numclwlk1lem2fo  24967  numclwwlk2lem1  24974  numclwlk2lem2f  24975  numclwwlk2  24979  ex-ind-dvds  25042  archirngz  27606  archiabllem2c  27612  sqsscirc1  27763  dya2icoseg  28121  dya2iocucvr  28128  oddpwdc  28166  eulerpartlemgs2  28192  fibp1  28213  signslema  28392  lgamgulmlem2  28445  lgamgulmlem4  28447  lgamucov  28453  subfacp1lem1  28496  subfacp1lem5  28501  bpolydiflem  29791  itg2addnclem  30041  dvcnsqrt  30076  dvasin  30078  areacirclem1  30082  areacirclem3  30084  isbnd2  30254  rmxluc  30847  rmyluc2  30849  rmydbl  30851  jm2.18  30905  jm2.22  30912  jm2.25  30916  jm2.27c  30924  jm3.1lem2  30935  refsum2cnlem1  31366  oddfl  31408  m1expeven  31513  sumnnodd  31544  0ellimcdiv  31563  coseq0  31571  sinmulcos  31572  coskpi2  31573  sinaover2ne0  31575  cosknegpi  31576  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  itgsinexp  31643  stoweidlem1  31672  stoweidlem62  31733  wallispilem4  31739  wallispilem5  31740  wallispi  31741  wallispi2lem1  31742  wallispi2lem2  31743  wallispi2  31744  stirlinglem1  31745  stirlinglem3  31747  stirlinglem4  31748  stirlinglem5  31749  stirlinglem6  31750  stirlinglem7  31751  stirlinglem8  31752  stirlinglem10  31754  stirlinglem11  31755  stirlinglem13  31757  stirlinglem14  31758  stirlinglem15  31759  dirker2re  31763  dirkerdenne0  31764  dirkerval2  31765  dirkerre  31766  dirkertrigeqlem1  31769  dirkertrigeqlem2  31770  dirkertrigeqlem3  31771  dirkertrigeq  31772  dirkeritg  31773  dirkercncflem1  31774  dirkercncflem2  31775  dirkercncflem4  31777  fourierdlem43  31821  fourierdlem44  31822  fourierdlem56  31834  fourierdlem57  31835  fourierdlem58  31836  fourierdlem62  31840  fourierdlem66  31844  fourierdlem68  31846  fourierdlem72  31850  fourierdlem76  31854  fourierdlem79  31857  fourierdlem80  31858  fourierdlem83  31861  fourierdlem95  31873  fourierdlem104  31882  fourierdlem112  31890  fouriercnp  31898  fourierswlem  31902  0nodd  32335  2nodd  32337  2zlidl  32450  2zrngamgm  32455  2zrngagrp  32459  2zrngmmgm  32462  2zrngnmlid  32465  imo72b2lem0  37651
  Copyright terms: Public domain W3C validator