Theorem pire 26776

Description: π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)

Assertion

Ref	Expression
pire	⊢ π ∈ ℝ

Proof of Theorem pire

Step	Hyp	Ref	Expression
1		pilem3 26773	. . 3 ⊢ (π ∈ (2(,)4) ∧ (sin‘π) = 0)
2	1	simpli 489	. 2 ⊢ π ∈ (2(,)4)
3		elioore 13499	. 2 ⊢ (π ∈ (2(,)4) → π ∈ ℝ)
4	2, 3	ax-mp 5	1 ⊢ π ∈ ℝ

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  (class class class)co 7418  ℝcr 11192  0cc0 11193  2c2 12390  4c4 12392  (,)cioo 13469  sincsin 16222  πcpi 16225

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-inf2 9635  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270  ax-pre-sup 11271  ax-addf 11272

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-of 7691  df-om 7876  df-1st 7999  df-2nd 8000  df-supp 8171  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-2o 8470  df-er 8710  df-map 8842  df-pm 8843  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9347  df-fi 9396  df-sup 9427  df-inf 9428  df-oi 9497  df-card 10013  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-div 11967  df-nn 12329  df-2 12398  df-3 12399  df-4 12400  df-5 12401  df-6 12402  df-7 12403  df-8 12404  df-9 12405  df-n0 12600  df-z 12687  df-dec 12808  df-uz 12959  df-q 13069  df-rp 13114  df-xneg 13234  df-xadd 13235  df-xmul 13236  df-ioo 13473  df-ioc 13474  df-ico 13475  df-icc 13476  df-fz 13633  df-fzo 13782  df-fl 13925  df-seq 14138  df-exp 14198  df-fac 14411  df-bc 14440  df-hash 14468  df-shft 15213  df-cj 15259  df-re 15260  df-im 15261  df-sqrt 15395  df-abs 15396  df-limsup 15631  df-clim 15648  df-rlim 15649  df-sum 15847  df-ef 16226  df-sin 16228  df-cos 16229  df-pi 16231  df-struct 17318  df-sets 17335  df-slot 17353  df-ndx 17365  df-base 17381  df-ress 17402  df-plusg 17434  df-mulr 17435  df-starv 17436  df-sca 17437  df-vsca 17438  df-ip 17439  df-tset 17440  df-ple 17441  df-ds 17443  df-unif 17444  df-hom 17445  df-cco 17446  df-rest 17586  df-topn 17587  df-0g 17605  df-gsum 17606  df-topgen 17607  df-pt 17608  df-prds 17611  df-xrs 17667  df-qtop 17672  df-imas 17673  df-xps 17675  df-mre 17749  df-mrc 17750  df-acs 17752  df-mgm 18809  df-sgrp 18901  df-mnd 18917  df-submnd 18972  df-mulg 19271  df-cntz 19524  df-cmn 19989  df-psmet 21663  df-xmet 21664  df-met 21665  df-bl 21666  df-mopn 21667  df-fbas 21668  df-fg 21669  df-cnfld 21672  df-top 23205  df-topon 23222  df-topsp 23244  df-bases 23257  df-cld 23330  df-ntr 23331  df-cls 23332  df-nei 23409  df-lp 23447  df-perf 23448  df-cn 23538  df-cnp 23539  df-haus 23626  df-tx 23874  df-hmeo 24067  df-fil 24158  df-fm 24250  df-flim 24251  df-flf 24252  df-xms 24632  df-ms 24633  df-tms 24634  df-cncf 25192  df-limc 26179  df-dv 26180

This theorem is used by:  2pire  26777  picn  26778  pipos  26780  pige0  26781  pine0  26782  pirp  26783  sinhalfpilem  26785  halfpire  26786  sincosq1lem  26819  sincosq2sgn  26821  sincosq3sgn  26822  sincosq4sgn  26823  coseq00topi  26824  coseq0negpitopi  26825  tangtx  26827  sinq12gt0  26829  sinq12ge0  26830  sinq34lt0t  26831  cosq14gt0  26832  cosq14ge0  26833  sincos4thpi  26835  sincos6thpi  26837  pigt3  26839  pige3  26840  pige3ALT  26841  coskpi  26844  sineq0  26845  coseq1  26846  cos02pilt1  26847  cosq34lt1  26848  efeq1  26849  cosne0  26850  cosordlem  26851  cosord  26852  cos0pilt1  26853  cos11  26854  sinord  26855  recosf1o  26856  resinf1o  26857  tanord1  26858  negpitopissre  26861  efif1olem1  26863  efif1olem2  26864  efif1olem4  26866  efif1o  26867  efifo  26868  eff1o  26870  ellogrn  26880  relogrn  26882  logimclad  26893  abslogimle  26894  logi  26908  logneg  26909  lognegb  26911  eflogeq  26923  logcj  26927  argregt0  26931  argrege0  26932  argimgt0  26933  argimlt0  26934  logimul  26935  logneg2  26936  abslogle  26939  logcnlem3  26965  dvloglem  26969  logf1o2  26971  efopnlem1  26977  efopnlem2  26978  cxpsqrtlem  27023  abscxpbnd  27074  root1eq1  27076  logreclem  27083  ang180lem1  27130  ang180lem2  27131  ang180lem3  27132  ang180lem4  27133  isosctrlem1  27139  1cubrlem  27162  asinneg  27207  asinsin  27213  asin1  27215  acosbnd  27221  atanlogaddlem  27234  atanlogsublem  27236  atanlogsub  27237  atantan  27244  atanbndlem  27246  atan1  27249  o1cxp  27295  lgamgulmlem4  27352  lgamgulmlem5  27353  lgamgulmlem6  27354  lgambdd  27357  basellem1  27401  basellem4  27404  basellem8  27408  basellem9  27409  cos9thpinconstrlem1  34414  circum  36418  bj-pinftyccb  38122  bj-minftyccb  38126  bj-pinftynminfty  38128  taupi  38224  sin2h  38513  cos2h  38514  tan2h  38515  asin1half  43388  acos1half  43389  proot1ex  44182  isosctrlem1ALT  45901  sineq0ALT  45904  negpilt0  46266  coseq0  46843  sinaover2ne0  46847  itgsin0pilem1  46929  itgsinexplem1  46933  itgsinexp  46934  wallispilem1  47044  wallispilem2  47045  wallispi  47049  stirlinglem15  47067  stirlingr  47069  dirker2re  47071  dirkerval2  47073  dirkerre  47074  dirkertrigeqlem2  47078  dirkertrigeqlem3  47079  dirkertrigeq  47080  dirkeritg  47081  dirkercncflem1  47082  dirkercncflem4  47085  fourierdlem5  47091  fourierdlem9  47095  fourierdlem16  47102  fourierdlem18  47104  fourierdlem21  47107  fourierdlem22  47108  fourierdlem24  47110  fourierdlem38  47124  fourierdlem40  47126  fourierdlem43  47129  fourierdlem44  47130  fourierdlem46  47131  fourierdlem50  47135  fourierdlem58  47143  fourierdlem62  47147  fourierdlem66  47151  fourierdlem72  47157  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem77  47162  fourierdlem78  47163  fourierdlem83  47168  fourierdlem85  47170  fourierdlem87  47172  fourierdlem88  47173  fourierdlem93  47178  fourierdlem94  47179  fourierdlem95  47180  fourierdlem101  47186  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  fourierdlem112  47197  fourierdlem113  47198  fourierdlem114  47199  sqwvfoura  47207  sqwvfourb  47208  fourierswlem  47209  fouriersw  47210  fouriercn  47211  goldrarr  47897  goldrapos  47899