Theorem picn 25031

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 25030	. 2 ⊢ π ∈ ℝ
2	1	recni 10641	1 ⊢ π ∈ ℂ

Syntax hints:   ∈ wcel 2114  ℂcc 10521  πcpi 15405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-inf2 9090  ax-cnex 10579  ax-resscn 10580  ax-1cn 10581  ax-icn 10582  ax-addcl 10583  ax-addrcl 10584  ax-mulcl 10585  ax-mulrcl 10586  ax-mulcom 10587  ax-addass 10588  ax-mulass 10589  ax-distr 10590  ax-i2m1 10591  ax-1ne0 10592  ax-1rid 10593  ax-rnegex 10594  ax-rrecex 10595  ax-cnre 10596  ax-pre-lttri 10597  ax-pre-lttrn 10598  ax-pre-ltadd 10599  ax-pre-mulgt0 10600  ax-pre-sup 10601  ax-addf 10602  ax-mulf 10603

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-pss 3942  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-tp 4558  df-op 4560  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5446  df-eprel 5451  df-po 5460  df-so 5461  df-fr 5500  df-se 5501  df-we 5502  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-pred 6134  df-ord 6180  df-on 6181  df-lim 6182  df-suc 6183  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-isom 6350  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-of 7395  df-om 7567  df-1st 7675  df-2nd 7676  df-supp 7817  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-oadd 8092  df-er 8275  df-map 8394  df-pm 8395  df-ixp 8448  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-fsupp 8820  df-fi 8861  df-sup 8892  df-inf 8893  df-oi 8960  df-card 9354  df-pnf 10663  df-mnf 10664  df-xr 10665  df-ltxr 10666  df-le 10667  df-sub 10858  df-neg 10859  df-div 11284  df-nn 11625  df-2 11687  df-3 11688  df-4 11689  df-5 11690  df-6 11691  df-7 11692  df-8 11693  df-9 11694  df-n0 11885  df-z 11969  df-dec 12086  df-uz 12231  df-q 12336  df-rp 12377  df-xneg 12494  df-xadd 12495  df-xmul 12496  df-ioo 12729  df-ioc 12730  df-ico 12731  df-icc 12732  df-fz 12883  df-fzo 13024  df-fl 13152  df-seq 13360  df-exp 13420  df-fac 13624  df-bc 13653  df-hash 13681  df-shft 14411  df-cj 14443  df-re 14444  df-im 14445  df-sqrt 14579  df-abs 14580  df-limsup 14813  df-clim 14830  df-rlim 14831  df-sum 15028  df-ef 15406  df-sin 15408  df-cos 15409  df-pi 15411  df-struct 16468  df-ndx 16469  df-slot 16470  df-base 16472  df-sets 16473  df-ress 16474  df-plusg 16561  df-mulr 16562  df-starv 16563  df-sca 16564  df-vsca 16565  df-ip 16566  df-tset 16567  df-ple 16568  df-ds 16570  df-unif 16571  df-hom 16572  df-cco 16573  df-rest 16679  df-topn 16680  df-0g 16698  df-gsum 16699  df-topgen 16700  df-pt 16701  df-prds 16704  df-xrs 16758  df-qtop 16763  df-imas 16764  df-xps 16766  df-mre 16840  df-mrc 16841  df-acs 16843  df-mgm 17835  df-sgrp 17884  df-mnd 17895  df-submnd 17940  df-mulg 18208  df-cntz 18430  df-cmn 18891  df-psmet 20520  df-xmet 20521  df-met 20522  df-bl 20523  df-mopn 20524  df-fbas 20525  df-fg 20526  df-cnfld 20529  df-top 21485  df-topon 21502  df-topsp 21524  df-bases 21537  df-cld 21610  df-ntr 21611  df-cls 21612  df-nei 21689  df-lp 21727  df-perf 21728  df-cn 21818  df-cnp 21819  df-haus 21906  df-tx 22153  df-hmeo 22346  df-fil 22437  df-fm 22529  df-flim 22530  df-flf 22531  df-xms 22913  df-ms 22914  df-tms 22915  df-cncf 23469  df-limc 24449  df-dv 24450

This theorem is referenced by:  negpicn  25034  pidiv2halves  25039  efhalfpi  25043  cospi  25044  efipi  25045  sin2pi  25047  cos2pi  25048  ef2pi  25049  ef2kpi  25050  efper  25051  sinperlem  25052  sin2kpi  25055  cos2kpi  25056  sin2pim  25057  cos2pim  25058  sinmpi  25059  cosmpi  25060  sinppi  25061  cosppi  25062  efimpi  25063  ptolemy  25068  sinq12gt0  25079  sinq34lt0t  25081  cosq14gt0  25082  cosq14ge0  25083  sincosq1eq  25084  sincos6thpi  25087  sincos3rdpi  25088  abssinper  25092  sinkpi  25093  coskpi  25094  sineq0  25095  coseq1  25096  efeq1  25099  cosne0  25100  resinf1o  25106  eff1o  25119  logneg  25157  logm1  25158  eflogeq  25171  argimgt0  25181  logneg2  25184  logf1o2  25219  cxpsqrt  25272  abscxpbnd  25320  root1eq1  25322  cxpeq  25324  ang180lem1  25373  ang180lem2  25374  ang180lem3  25375  ang180lem4  25376  acosf  25438  acosneg  25451  acoscos  25457  acos1  25459  sinacos  25469  atanlogsublem  25479  atanlogsub  25480  atantan  25487  atanbndlem  25489  basellem1  25644  efmul2picn  31874  itgexpif  31884  vtscl  31916  vtsprod  31917  circlemeth  31918  logi  32973  cos2h  34917  tan2h  34918  areacirc  35019  proot1ex  39893  coseq0  42235  coskpi2  42237  cosnegpi  42238  sinaover2ne0  42239  cosknegpi  42240  itgsinexplem1  42329  wallispilem4  42443  wallispi  42445  stirlinglem15  42463  dirker2re  42467  dirkerdenne0  42468  dirkerper  42471  dirkertrigeqlem1  42473  dirkertrigeqlem2  42474  dirkertrigeqlem3  42475  dirkertrigeq  42476  dirkeritg  42477  dirkercncflem1  42478  dirkercncflem2  42479  fourierdlem62  42543  fourierdlem66  42547  fourierdlem94  42575  fourierdlem95  42576  fourierdlem101  42582  fourierdlem102  42583  fourierdlem103  42584  fourierdlem111  42592  fourierdlem112  42593  fourierdlem113  42594  fourierdlem114  42595  sqwvfoura  42603  sqwvfourb  42604  fourierswlem  42605  fouriersw  42606