Theorem 1cnd 11127

Description: One is a complex number, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1cnd	⊢ (𝜑 → 1 ∈ ℂ)

Proof of Theorem 1cnd

Step	Hyp	Ref	Expression
1		ax-1cn 11084	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11024  1c1 11027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 11084

This theorem is referenced by:  adddirp1d  11158  1p1times  11304  addcom  11319  addcomd  11335  muladd11r  11346  pncan1  11561  npcan1  11562  muls1d  11597  mulsubfacd  11598  recrec  11838  rec11  11839  rec11r  11840  rereccl  11859  subrecd  11970  nn1m1nn  12166  add1p1  12392  sub1m1  12393  cnm2m1cnm3  12394  xp1d2m1eqxm1d2  12395  div4p1lem1div2  12396  nn0n0n1ge2  12469  zneo  12575  rpnnen1lem5  12894  lincmb01cmp  13411  iccf1o  13412  xov1plusxeqvd  13414  zpnn0elfzo1  13655  ubmelm1fzo  13679  fzosplitpr  13693  fzosplitprm1  13694  fzom1ne1  13701  fzoshftral  13703  fladdz  13745  2tnp1ge0ge0  13749  ltdifltdiv  13754  dfceil2  13759  negmod  13839  modnegd  13849  addmodlteq  13869  binom2sub1  14144  binom3  14147  zesq  14149  sqoddm1div8  14166  bcm1k  14238  bcp1n  14239  bcp1m1  14243  bcpasc  14244  bcn2m1  14247  hashfz  14350  hashfzo  14352  hashfzp1  14354  hashf1lem2  14379  hashf1  14380  hashdifsnp1  14429  lswccatn0lsw  14515  ccatws1lenp1b  14545  revccat  14689  repswrevw  14710  cshwidxm1  14730  cshwidxn  14732  cshweqrep  14744  cshimadifsn0  14753  swrds2m  14864  swrd2lsw  14875  relexpaddnn  14974  absexpz  15228  reccn2  15520  rlimno1  15577  isercolllem1  15588  isercoll2  15592  iseraltlem2  15606  iseraltlem3  15607  fsump1  15679  hashiun  15745  hash2iun1dif1  15747  binomlem  15752  bcxmas  15758  incexc  15760  incexc2  15761  climcndslem1  15772  arisum  15783  arisum2  15784  trireciplem  15785  pwdif  15791  pwm1geoser  15792  geolim2  15794  georeclim  15795  mertenslem1  15807  prodfrec  15818  ntrivcvg  15820  ntrivcvgtail  15823  prodrblem  15852  prodmolem2a  15857  fprodntriv  15865  prod1  15867  fprodser  15872  fprodcl  15875  fprodm1  15890  fprodp1  15892  fprodclf  15915  risefacval2  15933  fallfacval2  15934  risefacp1  15952  fallfacp1  15953  risefacfac  15958  fallfacfwd  15959  binomfallfaclem2  15963  fallfacval4  15966  bpolydiflem  15977  ef0lem  16001  tanaddlem  16091  tanadd  16092  cos01bnd  16111  oddm1even  16270  oddp1even  16271  oexpneg  16272  ltoddhalfle  16288  halfleoddlt  16289  nn0ob  16311  pwp1fsum  16318  flodddiv4  16342  bitsp1o  16360  bitsf1  16373  sadcp1  16382  qredeu  16585  prmdiv  16712  prmdiveq  16713  vfermltlALT  16730  pc2dvds  16807  4sqlem11  16883  4sqlem12  16884  vdwapun  16902  vdwlem3  16911  vdwlem6  16914  vdwlem9  16917  ramub1lem2  16955  prmop1  16966  prmdvdsprmo  16970  prmgaplem8  16986  cshwshashnsame  17031  chnub  18545  chnlt  18546  chnccat  18549  chnrev  18550  gsumsgrpccat  18765  psgnunilem5  19423  psgnunilem2  19424  sylow1lem1  19527  efgredlemc  19674  odadd2  19778  ablsimpgfindlem1  20038  omndmul2  20062  srgbinomlem3  20163  srgbinomlem4  20164  cncrng  21343  cncrngOLD  21344  gzrngunit  21388  zringunit  21421  prmirredlem  21427  pzriprnglem12  21447  freshmansdream  21529  mhppwdeg  22093  psdmul  22109  cayhamlem1  22810  expcn  24819  expcnOLD  24821  iirevcn  24880  iihalf2cn  24885  iihalf2cnOLD  24886  icchmeo  24894  icchmeoOLD  24895  icopnfcnv  24896  icopnfhmeo  24897  evth  24914  pcoass  24980  pjthlem1  25393  ovolunlem1a  25453  ovolunlem1  25454  opnmbllem  25558  mbfi1fseqlem6  25677  bddibl  25797  dvnadd  25887  dvmptid  25917  dvmptdiv  25934  dvcnvlem  25936  dveflem  25939  dvef  25940  dvsincos  25941  dvlipcn  25955  dvivthlem1  25969  lhop2  25976  dvcvx  25981  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem1  25988  dvfsumlem2  25989  dvfsumlem2OLD  25990  itgpowd  26013  ply1divex  26098  fta1glem1  26129  dgrcolem1  26235  dgrcolem2  26236  vieta1lem1  26274  aaliou3lem2  26307  aaliou3lem8  26309  dvtaylp  26334  dvntaylp  26335  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  abelthlem1  26397  abelthlem2  26398  abelthlem6  26402  abelthlem7  26404  logdivlti  26585  advlog  26619  advlogexp  26620  logtayl  26625  cxpmul2  26654  dvcxp1  26705  dvcxp2  26706  dvcncxp1  26708  dvcnsqrt  26709  loglesqrt  26727  relogbdiv  26745  ang180lem4  26778  ang180lem5  26779  isosctrlem2  26785  isosctrlem3  26786  affineequiv  26789  affineequiv2  26790  affineequiv3  26791  angpieqvdlem  26794  chordthmlem2  26799  chordthmlem3  26800  chordthmlem5  26802  dcubic2  26810  dcubic  26812  quart1lem  26821  quart1  26822  quart  26827  asinlem  26834  asinlem3  26837  atansopn  26898  dvatan  26901  leibpi  26908  birthdaylem2  26918  efrlim  26935  efrlimOLD  26936  cxplim  26938  divsqrtsumlem  26946  logdifbnd  26960  emcllem2  26963  emcllem3  26964  emcllem5  26966  zetacvg  26981  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem4  26998  lgamgulmlem5  26999  lgamgulmlem6  27000  lgamgulm2  27002  lgamcvg2  27021  gamcvg  27022  gamcvg2lem  27025  lgam1  27030  gamfac  27033  wilthlem2  27035  wilthimp  27038  ftalem5  27043  basellem3  27049  basellem5  27051  basellem8  27054  basellem9  27055  sqff1o  27148  muinv  27159  logfaclbnd  27189  logfacrlim  27191  logexprlim  27192  perfectlem2  27197  dchr1cl  27218  dchrinvcl  27220  dchrfi  27222  dchr1  27224  dchrsum2  27235  bcmono  27244  bcp1ctr  27246  bclbnd  27247  bposlem9  27259  gausslemma2dlem1a  27332  gausslemma2dlem5  27338  lgseisenlem4  27345  lgsquadlem1  27347  m1lgs  27355  2lgslem3a  27363  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  2lgslem3d1  27370  2lgsoddprmlem1  27375  2sqlem8  27393  2sq2  27400  addsqn2reu  27408  addsqrexnreu  27409  addsqnreup  27410  addsq2nreurex  27411  chtppilim  27442  rpvmasumlem  27454  dchrisumlem1  27456  dchrisum0re  27480  dchrisum0lem2a  27484  mudivsum  27497  mulogsumlem  27498  mulogsum  27499  2vmadivsumlem  27507  selberg4lem1  27527  pntrsumo1  27532  selberg34r  27538  pntrlog2bndlem2  27545  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntibndlem2  27558  pntlemg  27565  pntlemr  27569  pntlemf  27572  pntlemk  27573  pntlemo  27574  pntlem3  27576  ostth2lem2  27601  ttgcontlem1  28957  cusgrsize2inds  29527  wlklenvclwlk  29727  pthdadjvtx  29801  crctcshwlkn0lem1  29883  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  wlklnwwlkln2lem  29955  wlknwwlksnbij  29961  wwlksnred  29965  wwlksnext  29966  wwlksnextbi  29967  wwlksnredwwlkn  29968  wwlksnextwrd  29970  wwlksnextinj  29972  wwlksnextproplem2  29983  wwlksnextproplem3  29984  clwwlkccatlem  30064  clwlkclwwlklem2a1  30067  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwlkclwwlklem3  30076  clwlkclwwlk  30077  clwwisshclwwslemlem  30088  clwwisshclwws  30090  clwwlkel  30121  clwwlkf  30122  clwwlkwwlksb  30129  clwwlkext2edg  30131  wwlksext2clwwlk  30132  clwwlknonex2lem1  30182  clwwlknonex2lem2  30183  eucrct2eupth  30320  numclwwlk1lem2foalem  30426  numclwwlk1lem2fo  30433  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  numclwwlk6  30465  smcnlem  30772  receqid  32824  fzm1ne1  32868  bcm1n  32875  ltesubnnd  32903  sgn0bi  32921  oexpled  32928  wrdt2ind  33035  gsummptp1  33140  gsummulsubdishift1  33151  psgnfzto1stlem  33182  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  archirngz  33271  archiabllem1a  33273  archiabllem2c  33277  gsumind  33426  esplyind  33731  esplyindfv  33732  esplyfvn  33733  vietadeg1  33734  vietalem  33735  ccfldextdgrr  33829  constrfin  33903  nn0constr  33918  iconstr  33923  constrrecl  33926  constrimcl  33927  constrreinvcl  33929  constrinvcl  33930  constrresqrtcl  33934  2sqr3minply  33937  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  cos9thpiminplylem3  33941  cos9thpiminply  33945  cos9thpinconstrlem1  33946  1smat1  33961  madjusmdetlem2  33985  madjusmdetlem4  33987  dya2icoseg  34434  iwrdsplit  34544  fibp1  34558  ballotlemfp1  34649  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemic  34664  ballotlem1c  34665  ballotlemsgt1  34668  ballotlemsdom  34669  ballotlemsel1i  34670  ballotlemsi  34672  ballotlemsima  34673  ballotlem1ri  34692  signstfvn  34726  signsvtn0  34727  signstfveq0  34734  signsvfn  34739  signsvtn  34741  signshf  34745  hashreprin  34777  circlemeth  34797  logdivsqrle  34807  revpfxsfxrev  35310  revwlk  35319  swrdwlk  35321  subfacp1lem1  35373  subfacp1lem5  35378  cvxpconn  35436  sinccvglem  35866  divcnvlin  35927  bcm1nt  35931  bcprod  35932  bccolsum  35933  iprodgam  35936  faclimlem1  35937  faclimlem2  35938  faclimlem3  35939  faclim  35940  iprodfac  35941  faclim2  35942  fwddifnp1  36359  dnizphlfeqhlf  36676  dnibndlem3  36680  dnibndlem13  36690  unblimceq0  36707  knoppndvlem6  36717  knoppndvlem9  36720  knoppndvlem14  36725  knoppndvlem15  36726  knoppndvlem16  36727  knoppndvlem17  36728  bj-bary1lem1  37516  irrdiff  37531  poimirlem25  37846  poimirlem26  37847  poimirlem32  37853  opnmbllem0  37857  itg2addnclem2  37873  dvasin  37905  dvacos  37906  areacirclem1  37909  areacirclem4  37912  areacirc  37914  bfp  38025  fzsplitnd  42246  lcmfunnnd  42276  lcmineqlem1  42293  lcmineqlem3  42295  lcmineqlem4  42296  lcmineqlem7  42299  lcmineqlem8  42300  lcmineqlem10  42302  lcmineqlem11  42303  lcmineqlem12  42304  lcmineqlem18  42310  lcmineqlem19  42311  lcmineqlem22  42314  lcmineqlem23  42315  dvrelogpow2b  42332  aks4d1p1p4  42335  aks4d1p1p6  42337  aks4d1p1p7  42338  aks4d1p1p5  42339  aks4d1p1  42340  aks4d1p3  42342  aks4d1p7d1  42346  primrootsunit1  42361  posbezout  42364  primrootscoprbij  42366  primrootspoweq0  42370  aks6d1c1  42380  hashscontpow1  42385  2np3bcnp1  42408  sticksstones10  42419  sticksstones12a  42421  sticksstones12  42422  sticksstones16  42426  sticksstones22  42432  aks6d1c6lem3  42436  aks6d1c7lem1  42444  unitscyglem5  42463  nnadd1com  42532  nnaddcom  42533  nnadddir  42535  nnmul1com  42536  nnmulcom  42537  3rdpwhole  42557  fz1sump1  42575  oddnumth  42576  nicomachus  42577  sumcubes  42578  tan3rdpi  42617  redvmptabs  42625  readvrec  42627  reixi  42688  sn-mullid  42701  sn-0tie0  42716  renegmulnnass  42730  fiabv  42801  fltnltalem  42915  fltnlta  42916  3cubeslem1  42936  3cubeslem2  42937  3cubeslem4  42941  pell1qrge1  43122  rmspecfund  43161  acongeq  43235  jm2.18  43240  jm2.19lem3  43243  jm2.25  43251  jm2.16nn0  43256  jm3.1lem1  43269  jm3.1lem2  43270  areaquad  43468  relexpmulnn  43960  relexpaddss  43969  cvgdvgrat  44564  radcnvrat  44565  hashnzfzclim  44573  ofdivrec  44577  expgrowthi  44584  bccm1k  44593  dvradcnv2  44598  binomcxplemwb  44599  binomcxplemnn0  44600  binomcxplemrat  44601  binomcxplemfrat  44602  binomcxplemdvbinom  44604  binomcxplemnotnn0  44607  refsum2cnlem1  45292  fzisoeu  45558  fperiodmullem  45561  fzdifsuc2  45568  xralrple2  45609  nnsplit  45613  infleinflem2  45625  fmul01lt1lem2  45841  fprodcn  45856  clim1fr1  45857  isumneg  45858  climneg  45866  sumnnodd  45886  reclimc  45907  coseq0  46118  coskpi2  46120  cosknegpi  46123  fprodcncf  46154  fprodsubrecnncnvlem  46161  fprodaddrecnncnvlem  46163  ioodvbdlimc1lem2  46186  ioodvbdlimc2lem  46188  dvnxpaek  46196  dvnmul  46197  dvmptfprod  46199  dvnprodlem3  46202  itgsinexp  46209  itgiccshift  46234  itgperiod  46235  itgsbtaddcnst  46236  stoweidlem1  46255  stoweidlem7  46261  stoweidlem10  46264  stoweidlem11  46265  stoweidlem14  46268  stoweidlem17  46271  stoweidlem34  46288  stoweidlem42  46296  wallispilem3  46321  wallispilem5  46323  wallispi  46324  wallispi2lem1  46325  wallispi2lem2  46326  wallispi2  46327  stirlinglem1  46328  stirlinglem3  46330  stirlinglem4  46331  stirlinglem5  46332  stirlinglem6  46333  stirlinglem7  46334  stirlinglem8  46335  stirlinglem10  46337  stirlinglem11  46338  stirlinglem12  46339  stirlinglem13  46340  stirlinglem15  46342  dirkertrigeqlem2  46353  dirkertrigeqlem3  46354  dirkertrigeq  46355  dirkercncflem1  46357  dirkercncflem2  46358  dirkercncflem4  46360  fourierdlem11  46372  fourierdlem15  46376  fourierdlem26  46387  fourierdlem36  46397  fourierdlem40  46401  fourierdlem41  46402  fourierdlem42  46403  fourierdlem48  46408  fourierdlem49  46409  fourierdlem56  46416  fourierdlem58  46418  fourierdlem59  46419  fourierdlem62  46422  fourierdlem64  46424  fourierdlem65  46425  fourierdlem78  46438  fourierdlem79  46439  sqwvfoura  46482  fourierswlem  46484  fouriersw  46485  etransclem23  46511  etransclem24  46512  etransclem28  46516  etransclem35  46523  etransclem38  46526  nnfoctbdjlem  46709  smfmullem1  47045  sigaradd  47120  chnerlem2  47137  cjnpoly  47145  deccarry  47567  ceilbi  47589  m1modne  47604  m1modmmod  47614  modm1nep2  47624  modm1nem2  47625  fargshiftf1  47697  fargshiftfo  47698  fmtnof1  47791  sqrtpwpw2p  47794  fmtnorec2lem  47798  fmtnorec4  47805  fmtnoprmfac1lem  47820  fmtnoprmfac1  47821  fmtnoprmfac2  47823  2pwp1prm  47845  mod42tp1mod8  47858  sfprmdvdsmersenne  47859  lighneallem3  47863  lighneallem4  47866  onego  47902  zofldiv2ALTV  47918  oexpnegALTV  47933  opoeALTV  47939  opeoALTV  47940  epee  47961  perfectALTVlem1  47977  fppr2odd  47987  fpprwppr  47995  gpg3nbgrvtx0  48332  pgnbgreunbgrlem2lem1  48370  pgnbgreunbgrlem2lem2  48371  0nodd  48426  2nodd  48428  nnsgrpnmnd  48434  1neven  48494  altgsumbc  48608  pw2m1lepw2m1  48776  zofldiv2  48787  nnpw2pmod  48839  blen1b  48844  blennn0em1  48847  dignn0flhalflem1  48871  dignn0flhalflem2  48872  nn0sumshdiglemB  48876  nn0sumshdiglem1  48877  nn0sumshdiglem2  48878  itcovalpclem2  48927  ackval1  48937  ackval2  48938  ackval3  48939  affineid  48960  1subrec1sub  48961  eenglngeehlnmlem1  48993  eenglngeehlnmlem2  48994  rrx2vlinest  48997