Theorem 2cnd 11093

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

Step	Hyp	Ref	Expression
1		2cn 11091	. 2 |- 2 e. CC
2	1	a1i 11	1 |- ( ph -> 2 e. CC )

Syntax hints:   -> wi 4   e. wcel 1990   CCcc 9934   2c2 11070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-2 11079

This theorem is referenced by:  subhalfhalf  11266  cnm2m1cnm3  11285  xp1d2m1eqxm1d2  11286  zeo2  11464  fzosplitprm1  12578  2tnp1ge0ge0  12630  flhalf  12631  2txmodxeq0  12730  mulbinom2  12984  binom3  12985  zesq  12987  expmulnbnd  12996  discr  13001  sqoddm1div8  13028  mulsubdivbinom2  13046  amgm2  14109  iseraltlem2  14413  iseralt  14415  trirecip  14595  geo2sum  14604  bpolydiflem  14785  ege2le3  14820  tanval3  14864  sinhval  14884  tanhlt1  14890  sqrt2irrlem  14977  sqrt2irr  14979  even2n  15066  oddm1even  15067  oddp1even  15068  mod2eq1n2dvds  15071  ltoddhalfle  15085  m1exp1  15093  nn0enne  15094  flodddiv4  15137  flodddiv4t2lthalf  15140  bitsp1e  15154  bitsp1o  15155  bitsfzo  15157  bitsmod  15158  bitsinv1lem  15163  sadadd2lem2  15172  sadcaddlem  15179  bitsuz  15196  bitsshft  15197  prmdiv  15490  vfermltlALT  15507  iserodd  15540  4sqlem7  15648  4sqlem10  15651  4sqlem19  15667  prmgaplem7  15761  2expltfac  15799  efgredlemg  18155  frgpnabllem1  18276  metnrmlem3  22664  iihalf1cn  22731  iihalf2cn  22733  pcoass  22824  cphipval2  23040  csbren  23182  trirn  23183  minveclem2  23197  ovolunlem1a  23264  uniioombllem5  23355  uniioombl  23357  dyaddisjlem  23363  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  dvsincos  23744  lhop1  23777  cosargd  24354  dvcnsqrt  24485  root1id  24495  ssscongptld  24552  chordthmlem  24559  chordthmlem2  24560  chordthmlem4  24562  heron  24565  dcubic1  24572  mcubic  24574  cubic2  24575  quartlem4  24587  quart  24588  cosasin  24631  cosatan  24648  atantayl  24664  atantayl2  24665  atantayl3  24666  log2tlbnd  24672  cxp2limlem  24702  divsqrtsumlem  24706  lgamgulmlem2  24756  lgamgulmlem4  24758  lgamucov  24764  ftalem2  24800  basellem2  24808  basellem3  24809  basellem5  24811  basellem8  24814  logfaclbnd  24947  perfectlem2  24955  perfect  24956  bcp1ctr  25004  bposlem1  25009  bposlem2  25010  lgslem1  25022  lgsqrlem2  25072  gausslemma2dlem1a  25090  gausslemma2dlem3  25093  gausslemma2dlem4  25094  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgsquadlem1  25105  lgsquadlem2  25106  lgsquad2lem1  25109  2lgslem1a1  25114  2lgslem1a2  25115  2lgslem1b  25117  2lgslem1c  25118  2lgslem3a1  25125  2lgslem3d1  25128  chebbnd1lem3  25160  chto1ub  25165  dchrisumlem2  25179  dchrisum0flblem2  25198  dchrisum0fno1  25200  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2  25207  mulog2sumlem2  25224  vmalogdivsum2  25227  log2sumbnd  25233  selberglem2  25235  chpdifbndlem1  25242  selberg3lem1  25246  selberg3  25248  selberg4lem1  25249  selberg4  25250  selberg4r  25259  selberg34r  25260  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntpbnd1a  25274  pntpbnd2  25276  pntibndlem2  25280  pntlemb  25286  pntlemg  25287  pntlemh  25288  pntlemr  25291  pntlemk  25295  pntlemo  25296  ostth2lem1  25307  finsumvtxdg2ssteplem4  26444  upgrwlkdvdelem  26632  wwlksnextwrd  26792  wwlksnextinj  26794  clwlkclwwlklem2a1  26893  clwlkclwwlklem2a4  26898  clwlkclwwlklem3  26902  clwwlksext2edg  26923  extwwlkfablem1  27207  numclwwlkovf2exlem1  27211  numclwwlkovf2exlem2  27212  numclwlk1lem2foalem  27222  numclwlk1lem2fo  27228  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwwlk2  27240  ex-ind-dvds  27318  archirngz  29743  archiabllem2c  29749  sqsscirc1  29954  dya2icoseg  30339  dya2iocucvr  30346  oddpwdc  30416  eulerpartlemgs2  30442  fibp1  30463  signslema  30639  itgexpif  30684  vtsprod  30717  hgt750lemd  30726  logdivsqrle  30728  subfacp1lem1  31161  subfacp1lem5  31166  dnibndlem10  32477  knoppndvlem2  32504  knoppndvlem7  32509  knoppndvlem9  32511  knoppndvlem10  32512  knoppndvlem16  32518  itg2addnclem  33461  dvasin  33496  areacirclem1  33500  areacirclem3  33502  isbnd2  33582  rmspecsqrtnq  37470  rmxluc  37501  rmyluc2  37503  rmydbl  37505  jm2.18  37555  jm2.22  37562  jm2.25  37566  jm2.27c  37574  jm3.1lem2  37585  imo72b2lem0  38465  refsum2cnlem1  39196  oddfl  39489  xralrple2  39570  infleinflem2  39587  sumnnodd  39862  0ellimcdiv  39881  coseq0  40075  sinmulcos  40076  coskpi2  40077  sinaover2ne0  40079  cosknegpi  40080  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  itgsinexp  40170  stoweidlem1  40218  stoweidlem62  40279  wallispilem4  40285  wallispilem5  40286  wallispi  40287  wallispi2lem1  40288  wallispi2lem2  40289  wallispi2  40290  stirlinglem1  40291  stirlinglem3  40293  stirlinglem4  40294  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem8  40298  stirlinglem10  40300  stirlinglem11  40301  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  dirker2re  40309  dirkerdenne0  40310  dirkerval2  40311  dirkerre  40312  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkeritg  40319  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem43  40367  fourierdlem44  40368  fourierdlem56  40379  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fourierdlem66  40389  fourierdlem68  40391  fourierdlem72  40395  fourierdlem76  40399  fourierdlem79  40402  fourierdlem80  40403  fourierdlem83  40406  fourierdlem95  40418  fourierdlem104  40427  fourierdlem112  40435  fouriercnp  40443  fourierswlem  40447  sge0ad2en  40648  hoicvrrex  40770  hoiqssbllem2  40837  fmtnoodd  41445  sqrtpwpw2p  41450  fmtnorec2lem  41454  fmtnodvds  41456  goldbachthlem2  41458  fmtnoprmfac1lem  41476  fmtnoprmfac2  41479  fmtnofac1  41482  2pwp1prm  41503  mod42tp1mod8  41519  sfprmdvdsmersenne  41520  lighneallem2  41523  lighneallem4  41527  proththd  41531  dfodd6  41550  dfeven4  41551  enege  41558  onego  41559  dfeven2  41562  oddflALTV  41575  opoeALTV  41594  opeoALTV  41595  nn0onn0exALTV  41609  nn0enn0exALTV  41610  mogoldbblem  41629  perfectALTV  41632  sgoldbeven3prm  41671  0nodd  41810  2nodd  41812  2zlidl  41934  2zrngamgm  41939  2zrngagrp  41943  2zrngmmgm  41946  2zrngnmlid  41949  nn0onn0ex  42318  nn0enn0ex  42319  nnpw2even  42323  fldivexpfllog2  42359  blenpw2m1  42373  nnpw2blen  42374  blennn0em1  42385  dig2nn1st  42399  dig2bits  42408  dignn0flhalflem1  42409  dignn0flhalflem2  42410  dignn0ehalf  42411  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414