Theorem 1cnd 11133

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 11090	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11030  1c1 11033

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

This theorem is referenced by:  adddirp1d  11165  1p1times  11311  addcom  11326  addcomd  11342  muladd11r  11353  pncan1  11568  npcan1  11569  muls1d  11604  mulsubfacd  11605  recrec  11846  rec11  11847  rec11r  11848  rereccl  11867  subrecd  11978  nn1m1nn  12189  nnadd1com  12194  nnaddcom  12195  nnadddir  12227  nnmul1com  12228  nnmulcom  12229  add1p1  12422  sub1m1  12423  cnm2m1cnm3  12424  xp1d2m1eqxm1d2  12425  div4p1lem1div2  12426  nn0n0n1ge2  12499  zneo  12606  rpnnen1lem5  12925  lincmb01cmp  13442  iccf1o  13443  xov1plusxeqvd  13445  zpnn0elfzo1  13688  ubmelm1fzo  13712  fzosplitpr  13726  fzosplitprm1  13727  fzom1ne1  13734  fzoshftral  13736  fladdz  13778  2tnp1ge0ge0  13782  ltdifltdiv  13787  dfceil2  13792  negmod  13872  modnegd  13882  addmodlteq  13902  binom2sub1  14177  binom3  14180  zesq  14182  sqoddm1div8  14199  bcm1k  14271  bcp1n  14272  bcp1m1  14276  bcpasc  14277  bcn2m1  14280  hashfz  14383  hashfzo  14385  hashfzp1  14387  hashf1lem2  14412  hashf1  14413  hashdifsnp1  14462  lswccatn0lsw  14548  ccatws1lenp1b  14578  revccat  14722  repswrevw  14743  cshwidxm1  14763  cshwidxn  14765  cshweqrep  14777  cshimadifsn0  14786  swrds2m  14897  swrd2lsw  14908  relexpaddnn  15007  absexpz  15261  reccn2  15553  rlimno1  15610  isercolllem1  15621  isercoll2  15625  iseraltlem2  15639  iseraltlem3  15640  fsump1  15712  fsumconst1  15747  hashiun  15779  hash2iun1dif1  15781  indsumhash  15786  binomlem  15788  bcxmas  15794  incexc  15796  incexc2  15797  climcndslem1  15808  arisum  15819  arisum2  15820  trireciplem  15821  pwdif  15827  pwm1geoser  15828  geolim2  15830  georeclim  15831  mertenslem1  15843  prodfrec  15854  ntrivcvg  15856  ntrivcvgtail  15859  prodrblem  15888  prodmolem2a  15893  fprodntriv  15901  prod1  15903  fprodser  15908  fprodcl  15911  fprodm1  15926  fprodp1  15928  fprodclf  15951  risefacval2  15969  fallfacval2  15970  risefacp1  15988  fallfacp1  15989  risefacfac  15994  fallfacfwd  15995  binomfallfaclem2  15999  fallfacval4  16002  bpolydiflem  16013  ef0lem  16037  tanaddlem  16127  tanadd  16128  cos01bnd  16147  oddm1even  16306  oddp1even  16307  oexpneg  16308  ltoddhalfle  16324  halfleoddlt  16325  nn0ob  16347  pwp1fsum  16354  flodddiv4  16378  bitsp1o  16396  bitsf1  16409  sadcp1  16418  qredeu  16621  prmdiv  16749  prmdiveq  16750  vfermltlALT  16767  pc2dvds  16844  4sqlem11  16920  4sqlem12  16921  vdwapun  16939  vdwlem3  16948  vdwlem6  16951  vdwlem9  16954  ramub1lem2  16992  prmop1  17003  prmdvdsprmo  17007  prmgaplem8  17023  cshwshashnsame  17068  chnub  18582  chnlt  18583  chnccat  18586  chnrev  18587  gsumsgrpccat  18802  psgnunilem5  19463  psgnunilem2  19464  sylow1lem1  19567  efgredlemc  19714  odadd2  19818  ablsimpgfindlem1  20078  omndmul2  20102  srgbinomlem3  20203  srgbinomlem4  20204  cncrng  21381  cncrngOLD  21382  gzrngunit  21426  zringunit  21459  prmirredlem  21465  pzriprnglem12  21485  freshmansdream  21567  mhppwdeg  22129  psdmul  22145  cayhamlem1  22844  expcn  24852  iirevcn  24910  iihalf2cn  24914  icchmeo  24921  icopnfcnv  24922  icopnfhmeo  24923  evth  24939  pcoass  25004  pjthlem1  25417  ovolunlem1a  25476  ovolunlem1  25477  opnmbllem  25581  mbfi1fseqlem6  25700  bddibl  25820  dvnadd  25909  dvmptid  25937  dvmptdiv  25954  dvcnvlem  25956  dveflem  25959  dvef  25960  dvsincos  25961  dvlipcn  25974  dvivthlem1  25988  lhop2  25995  dvcvx  26000  dvfsumle  26001  dvfsumabs  26003  dvfsumlem1  26006  dvfsumlem2  26007  itgpowd  26030  ply1divex  26115  fta1glem1  26146  dgrcolem1  26251  dgrcolem2  26252  vieta1lem1  26290  aaliou3lem2  26323  aaliou3lem8  26325  dvtaylp  26350  dvntaylp  26351  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  abelthlem1  26412  abelthlem2  26413  abelthlem6  26417  abelthlem7  26419  logdivlti  26600  advlog  26634  advlogexp  26635  logtayl  26640  cxpmul2  26669  dvcxp1  26720  dvcxp2  26721  dvcncxp1  26723  dvcnsqrt  26724  loglesqrt  26741  relogbdiv  26759  ang180lem4  26792  ang180lem5  26793  isosctrlem2  26799  isosctrlem3  26800  affineequiv  26803  affineequiv2  26804  affineequiv3  26805  angpieqvdlem  26808  chordthmlem2  26813  chordthmlem3  26814  chordthmlem5  26816  dcubic2  26824  dcubic  26826  quart1lem  26835  quart1  26836  quart  26841  asinlem  26848  asinlem3  26851  atansopn  26912  dvatan  26915  leibpi  26922  birthdaylem2  26932  efrlim  26949  efrlimOLD  26950  cxplim  26952  divsqrtsumlem  26960  logdifbnd  26974  emcllem2  26977  emcllem3  26978  emcllem5  26980  zetacvg  26995  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamgulmlem4  27012  lgamgulmlem5  27013  lgamgulmlem6  27014  lgamgulm2  27016  lgamcvg2  27035  gamcvg  27036  gamcvg2lem  27039  lgam1  27044  gamfac  27047  wilthlem2  27049  wilthimp  27052  ftalem5  27057  basellem3  27063  basellem5  27065  basellem8  27068  basellem9  27069  sqff1o  27162  muinv  27173  logfaclbnd  27202  logfacrlim  27204  logexprlim  27205  perfectlem2  27210  dchr1cl  27231  dchrinvcl  27233  dchrfi  27235  dchr1  27237  dchrsum2  27248  bcmono  27257  bcp1ctr  27259  bclbnd  27260  bposlem9  27272  gausslemma2dlem1a  27345  gausslemma2dlem5  27351  lgseisenlem4  27358  lgsquadlem1  27360  m1lgs  27368  2lgslem3a  27376  2lgslem3b  27377  2lgslem3c  27378  2lgslem3d  27379  2lgslem3d1  27383  2lgsoddprmlem1  27388  2sqlem8  27406  2sq2  27413  addsqn2reu  27421  addsqrexnreu  27422  addsqnreup  27423  addsq2nreurex  27424  chtppilim  27455  rpvmasumlem  27467  dchrisumlem1  27469  dchrisum0re  27493  dchrisum0lem2a  27497  mudivsum  27510  mulogsumlem  27511  mulogsum  27512  2vmadivsumlem  27520  selberg4lem1  27540  pntrsumo1  27545  selberg34r  27551  pntrlog2bndlem2  27558  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntibndlem2  27571  pntlemg  27578  pntlemr  27582  pntlemf  27585  pntlemk  27586  pntlemo  27587  pntlem3  27589  ostth2lem2  27614  ttgcontlem1  28970  cusgrsize2inds  29540  wlklenvclwlk  29740  pthdadjvtx  29814  crctcshwlkn0lem1  29896  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  wlklnwwlkln2lem  29968  wlknwwlksnbij  29974  wwlksnred  29978  wwlksnext  29979  wwlksnextbi  29980  wwlksnredwwlkn  29981  wwlksnextwrd  29983  wwlksnextinj  29985  wwlksnextproplem2  29996  wwlksnextproplem3  29997  clwwlkccatlem  30077  clwlkclwwlklem2a1  30080  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwlkclwwlklem3  30089  clwlkclwwlk  30090  clwwisshclwwslemlem  30101  clwwisshclwws  30103  clwwlkel  30134  clwwlkf  30135  clwwlkwwlksb  30142  clwwlkext2edg  30144  wwlksext2clwwlk  30145  clwwlknonex2lem1  30195  clwwlknonex2lem2  30196  eucrct2eupth  30333  numclwwlk1lem2foalem  30439  numclwwlk1lem2fo  30446  numclwlk2lem2f  30465  numclwlk2lem2f1o  30467  numclwwlk6  30478  smcnlem  30786  receqid  32835  fzm1ne1  32879  bcm1n  32886  ltesubnnd  32914  sgn0bi  32931  oexpled  32938  wrdt2ind  33031  gsummptp1  33136  gsummulsubdishift1  33147  psgnfzto1stlem  33179  cycpmco2lem3  33207  cycpmco2lem4  33208  cycpmco2lem5  33209  cycpmco2lem6  33210  cycpmco2lem7  33211  cycpmco2  33212  archirngz  33268  archiabllem1a  33270  archiabllem2c  33274  gsumind  33423  esplyind  33737  esplyindfv  33738  esplyfvn  33739  vietadeg1  33740  vietalem  33741  ccfldextdgrr  33835  constrfin  33909  nn0constr  33924  iconstr  33929  constrrecl  33932  constrimcl  33933  constrreinvcl  33935  constrinvcl  33936  constrresqrtcl  33940  2sqr3minply  33943  cos9thpiminplylem1  33945  cos9thpiminplylem2  33946  cos9thpiminplylem3  33947  cos9thpiminply  33951  cos9thpinconstrlem1  33952  1smat1  33967  madjusmdetlem2  33991  madjusmdetlem4  33993  dya2icoseg  34440  iwrdsplit  34550  fibp1  34564  ballotlemfp1  34655  ballotlemfc0  34656  ballotlemfcc  34657  ballotlemic  34670  ballotlem1c  34671  ballotlemsgt1  34674  ballotlemsdom  34675  ballotlemsel1i  34676  ballotlemsi  34678  ballotlemsima  34679  ballotlem1ri  34698  signstfvn  34732  signsvtn0  34733  signstfveq0  34740  signsvfn  34745  signsvtn  34747  signshf  34751  hashreprin  34783  circlemeth  34803  logdivsqrle  34813  revpfxsfxrev  35317  revwlk  35326  swrdwlk  35328  subfacp1lem1  35380  subfacp1lem5  35385  cvxpconn  35443  sinccvglem  35873  divcnvlin  35934  bcm1nt  35938  bcprod  35939  bccolsum  35940  iprodgam  35943  faclimlem1  35944  faclimlem2  35945  faclimlem3  35946  faclim  35947  iprodfac  35948  faclim2  35949  fwddifnp1  36366  dnizphlfeqhlf  36755  dnibndlem3  36759  dnibndlem13  36769  unblimceq0  36786  knoppndvlem6  36796  knoppndvlem9  36799  knoppndvlem14  36804  knoppndvlem15  36805  knoppndvlem16  36806  knoppndvlem17  36807  bj-bary1lem1  37644  irrdiff  37659  poimirlem25  37983  poimirlem26  37984  poimirlem32  37990  opnmbllem0  37994  itg2addnclem2  38010  dvasin  38042  dvacos  38043  areacirclem1  38046  areacirclem4  38049  areacirc  38051  bfp  38162  fzsplitnd  42438  lcmfunnnd  42468  lcmineqlem1  42485  lcmineqlem3  42487  lcmineqlem4  42488  lcmineqlem7  42491  lcmineqlem8  42492  lcmineqlem10  42494  lcmineqlem11  42495  lcmineqlem12  42496  lcmineqlem18  42502  lcmineqlem19  42503  lcmineqlem22  42506  lcmineqlem23  42507  dvrelogpow2b  42524  aks4d1p1p4  42527  aks4d1p1p6  42529  aks4d1p1p7  42530  aks4d1p1p5  42531  aks4d1p1  42532  aks4d1p3  42534  aks4d1p7d1  42538  primrootsunit1  42553  posbezout  42556  primrootscoprbij  42558  primrootspoweq0  42562  aks6d1c1  42572  hashscontpow1  42577  2np3bcnp1  42600  sticksstones10  42611  sticksstones12a  42613  sticksstones12  42614  sticksstones16  42618  sticksstones22  42624  aks6d1c6lem3  42628  aks6d1c7lem1  42636  unitscyglem5  42655  3rdpwhole  42741  fz1sump1  42759  oddnumth  42760  nicomachus  42761  sumcubes  42762  tan3rdpi  42801  redvmptabs  42809  readvrec  42811  reixi  42872  sn-mullid  42885  sn-0tie0  42913  renegmulnnass  42927  fiabv  42998  fltnltalem  43112  fltnlta  43113  3cubeslem1  43133  3cubeslem2  43134  3cubeslem4  43138  pell1qrge1  43319  rmspecfund  43358  acongeq  43432  jm2.18  43437  jm2.19lem3  43440  jm2.25  43448  jm2.16nn0  43453  jm3.1lem1  43466  jm3.1lem2  43467  areaquad  43665  relexpmulnn  44157  relexpaddss  44166  cvgdvgrat  44761  radcnvrat  44762  hashnzfzclim  44770  ofdivrec  44774  expgrowthi  44781  bccm1k  44790  dvradcnv2  44795  binomcxplemwb  44796  binomcxplemnn0  44797  binomcxplemrat  44798  binomcxplemfrat  44799  binomcxplemdvbinom  44801  binomcxplemnotnn0  44804  refsum2cnlem1  45489  fzisoeu  45754  fperiodmullem  45757  fzdifsuc2  45764  xralrple2  45805  nnsplit  45809  infleinflem2  45821  fmul01lt1lem2  46036  fprodcn  46051  clim1fr1  46052  isumneg  46053  climneg  46061  sumnnodd  46081  reclimc  46102  coseq0  46313  coskpi2  46315  cosknegpi  46318  fprodcncf  46349  fprodsubrecnncnvlem  46356  fprodaddrecnncnvlem  46358  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnxpaek  46391  dvnmul  46392  dvmptfprod  46394  dvnprodlem3  46397  itgsinexp  46404  itgiccshift  46429  itgperiod  46430  itgsbtaddcnst  46431  stoweidlem1  46450  stoweidlem7  46456  stoweidlem10  46459  stoweidlem11  46460  stoweidlem14  46463  stoweidlem17  46466  stoweidlem34  46483  stoweidlem42  46491  wallispilem3  46516  wallispilem5  46518  wallispi  46519  wallispi2lem1  46520  wallispi2lem2  46521  wallispi2  46522  stirlinglem1  46523  stirlinglem3  46525  stirlinglem4  46526  stirlinglem5  46527  stirlinglem6  46528  stirlinglem7  46529  stirlinglem8  46530  stirlinglem10  46532  stirlinglem11  46533  stirlinglem12  46534  stirlinglem13  46535  stirlinglem15  46537  dirkertrigeqlem2  46548  dirkertrigeqlem3  46549  dirkertrigeq  46550  dirkercncflem1  46552  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem11  46567  fourierdlem15  46571  fourierdlem26  46582  fourierdlem36  46592  fourierdlem40  46596  fourierdlem41  46597  fourierdlem42  46598  fourierdlem48  46603  fourierdlem49  46604  fourierdlem56  46611  fourierdlem58  46613  fourierdlem59  46614  fourierdlem62  46617  fourierdlem64  46619  fourierdlem65  46620  fourierdlem78  46633  fourierdlem79  46634  sqwvfoura  46677  fourierswlem  46679  fouriersw  46680  etransclem23  46706  etransclem24  46707  etransclem28  46711  etransclem35  46718  etransclem38  46721  nnfoctbdjlem  46904  smfmullem1  47240  sigaradd  47315  chnerlem2  47332  sin3t  47338  cos3t  47339  sin5tlem1  47340  sin5tlem2  47341  sin5tlem4  47343  cjnpoly  47352  deccarry  47774  ceilbi  47800  flmrecm1  47806  m1modne  47817  m1modmmod  47827  modm1nep2  47837  modm1nem2  47838  fargshiftf1  47916  fargshiftfo  47917  fmtnof1  48013  sqrtpwpw2p  48016  fmtnorec2lem  48020  fmtnorec4  48027  fmtnoprmfac1lem  48042  fmtnoprmfac1  48043  fmtnoprmfac2  48045  2pwp1prm  48067  mod42tp1mod8  48080  sfprmdvdsmersenne  48081  lighneallem3  48085  lighneallem4  48088  ppivalnnprm  48103  ppivalnnnprmge6  48104  onego  48137  zofldiv2ALTV  48153  oexpnegALTV  48168  opoeALTV  48174  opeoALTV  48175  epee  48196  perfectALTVlem1  48212  fppr2odd  48222  fpprwppr  48230  gpg3nbgrvtx0  48567  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  0nodd  48661  2nodd  48663  nnsgrpnmnd  48669  1neven  48729  altgsumbc  48843  pw2m1lepw2m1  49011  zofldiv2  49022  nnpw2pmod  49074  blen1b  49079  blennn0em1  49082  dignn0flhalflem1  49106  dignn0flhalflem2  49107  nn0sumshdiglemB  49111  nn0sumshdiglem1  49112  nn0sumshdiglem2  49113  itcovalpclem2  49162  ackval1  49172  ackval2  49173  ackval3  49174  affineid  49195  1subrec1sub  49196  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  rrx2vlinest  49232