Theorem picn 26579

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

Assertion

Ref	Expression
picn	⊢ π ∈ ℂ

Proof of Theorem picn

Step	Hyp	Ref	Expression
1		pire 26577	. 2 ⊢ π ∈ ℝ
2	1	recni 11211	1 ⊢ π ∈ ℂ

Syntax hints:   ∈ wcel 2145  ℂcc 11086  πcpi 16110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-inf2 9598  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165  ax-pre-sup 11166  ax-addf 11167

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4869  df-int 4909  df-iun 4954  df-iin 4955  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-se 5606  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-isom 6534  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-of 7664  df-om 7851  df-1st 7974  df-2nd 7975  df-supp 8145  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-1o 8441  df-2o 8442  df-er 8682  df-map 8814  df-pm 8815  df-ixp 8884  df-en 8932  df-dom 8933  df-sdom 8934  df-fin 8935  df-fsupp 9310  df-fi 9359  df-sup 9390  df-inf 9391  df-oi 9460  df-card 9913  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-div 11860  df-nn 12225  df-2 12294  df-3 12295  df-4 12296  df-5 12297  df-6 12298  df-7 12299  df-8 12300  df-9 12301  df-n0 12496  df-z 12583  df-dec 12703  df-uz 12854  df-q 12964  df-rp 13008  df-xneg 13128  df-xadd 13129  df-xmul 13130  df-ioo 13367  df-ioc 13368  df-ico 13369  df-icc 13370  df-fz 13527  df-fzo 13674  df-fl 13816  df-seq 14029  df-exp 14089  df-fac 14301  df-bc 14330  df-hash 14358  df-shft 15094  df-cj 15140  df-re 15141  df-im 15142  df-sqrt 15276  df-abs 15277  df-limsup 15512  df-clim 15529  df-rlim 15530  df-sum 15728  df-ef 16111  df-sin 16113  df-cos 16114  df-pi 16116  df-struct 17197  df-sets 17214  df-slot 17232  df-ndx 17244  df-base 17260  df-ress 17281  df-plusg 17313  df-mulr 17314  df-starv 17315  df-sca 17316  df-vsca 17317  df-ip 17318  df-tset 17319  df-ple 17320  df-ds 17322  df-unif 17323  df-hom 17324  df-cco 17325  df-rest 17465  df-topn 17466  df-0g 17484  df-gsum 17485  df-topgen 17486  df-pt 17487  df-prds 17490  df-xrs 17546  df-qtop 17551  df-imas 17552  df-xps 17554  df-mre 17628  df-mrc 17629  df-acs 17631  df-mgm 18688  df-sgrp 18767  df-mnd 18783  df-submnd 18832  df-mulg 19125  df-cntz 19378  df-cmn 19843  df-psmet 21474  df-xmet 21475  df-met 21476  df-bl 21477  df-mopn 21478  df-fbas 21479  df-fg 21480  df-cnfld 21483  df-top 23012  df-topon 23029  df-topsp 23051  df-bases 23064  df-cld 23137  df-ntr 23138  df-cls 23139  df-nei 23216  df-lp 23254  df-perf 23255  df-cn 23345  df-cnp 23346  df-haus 23433  df-tx 23680  df-hmeo 23873  df-fil 23964  df-fm 24056  df-flim 24057  df-flf 24058  df-xms 24438  df-ms 24439  df-tms 24440  df-cncf 24998  df-limc 25986  df-dv 25987

This theorem is referenced by:  2picn  26580  negpicn  26585  pidiv2halves  26590  efhalfpi  26594  cospi  26595  efipi  26596  sin2pi  26598  cos2pi  26599  ef2pi  26600  ef2kpi  26601  efper  26602  sinperlem  26603  sin2kpi  26606  cos2kpi  26607  sin2pim  26608  cos2pim  26609  sinmpi  26610  cosmpi  26611  sinppi  26612  cosppi  26613  efimpi  26614  ptolemy  26619  sinq12gt0  26630  sinq34lt0t  26632  cosq14gt0  26633  cosq14ge0  26634  sincosq1eq  26635  tan4thpi  26637  sincos6thpi  26639  sincos3rdpi  26640  abssinper  26644  sinkpi  26645  coskpi  26646  sineq0  26647  coseq1  26648  efeq1  26651  cosne0  26652  resinf1o  26659  eff1o  26672  logi  26710  logneg  26711  logm1  26712  eflogeq  26725  argimgt0  26735  logneg2  26738  logf1o2  26773  cxpsqrt  26826  abscxpbnd  26876  root1eq1  26878  cxpeq  26880  ang180lem1  26932  ang180lem2  26933  ang180lem3  26934  ang180lem4  26935  acosf  26997  acosneg  27010  acoscos  27016  acos1  27018  sinacos  27028  atanlogsublem  27038  atanlogsub  27039  atantan  27046  atanbndlem  27048  basellem1  27203  cos9thpiminplylem3  34091  cos9thpiminplylem4  34092  cos9thpiminplylem5  34093  cos9thpiminply  34095  cos9thpinconstrlem1  34096  cos9thpinconstrlem2  34097  cos9thpinconstr  34098  efmul2picn  34900  itgexpif  34910  vtscl  34942  vtsprod  34943  circlemeth  34944  cos2h  38122  tan2h  38123  areacirc  38224  ef11d  42960  cxp112d  42962  cxp111d  42963  cxpi11d  42964  tanhalfpim  42970  sinpim  42971  cospim  42972  tan3rdpi  42973  sin2t3rdpi  42974  cos2t3rdpi  42975  sin4t3rdpi  42976  cos4t3rdpi  42977  acos1half  42979  proot1ex  43785  coseq0  46436  coskpi2  46438  cosnegpi  46439  sinaover2ne0  46440  cosknegpi  46441  itgsinexplem1  46526  wallispilem4  46640  wallispi  46642  stirlinglem15  46660  dirker2re  46664  dirkerdenne0  46665  dirkerper  46668  dirkertrigeqlem1  46670  dirkertrigeqlem2  46671  dirkertrigeqlem3  46672  dirkertrigeq  46673  dirkeritg  46674  dirkercncflem1  46675  dirkercncflem2  46676  fourierdlem62  46740  fourierdlem66  46744  fourierdlem94  46772  fourierdlem95  46773  fourierdlem101  46779  fourierdlem102  46780  fourierdlem103  46781  fourierdlem111  46789  fourierdlem112  46790  fourierdlem113  46791  fourierdlem114  46792  sqwvfoura  46800  sqwvfourb  46801  fourierswlem  46802  fouriersw  46803  cos5t  47471  goldrasin  47474  goldracos5teq  47477  tannpoly  47482  sinnpoly  47483