Theorem pire 26434

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 26431	. . 3 ⊢ (π ∈ (2(,)4) ∧ (sin‘π) = 0)
2	1	simpli 483	. 2 ⊢ π ∈ (2(,)4)
3		elioore 13319	. 2 ⊢ (π ∈ (2(,)4) → π ∈ ℝ)
4	2, 3	ax-mp 5	1 ⊢ π ∈ ℝ

Syntax hints:   = wceq 1542   ∈ wcel 2114  ‘cfv 6492  (class class class)co 7360  ℝcr 11028  0cc0 11029  2c2 12227  4c4 12229  (,)cioo 13289  sincsin 16019  πcpi 16022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-inf2 9553  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107  ax-addf 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-of 7624  df-om 7811  df-1st 7935  df-2nd 7936  df-supp 8104  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-2o 8399  df-er 8636  df-map 8768  df-pm 8769  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9268  df-fi 9317  df-sup 9348  df-inf 9349  df-oi 9418  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-z 12516  df-dec 12636  df-uz 12780  df-q 12890  df-rp 12934  df-xneg 13054  df-xadd 13055  df-xmul 13056  df-ioo 13293  df-ioc 13294  df-ico 13295  df-icc 13296  df-fz 13453  df-fzo 13600  df-fl 13742  df-seq 13955  df-exp 14015  df-fac 14227  df-bc 14256  df-hash 14284  df-shft 15020  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-limsup 15424  df-clim 15441  df-rlim 15442  df-sum 15640  df-ef 16023  df-sin 16025  df-cos 16026  df-pi 16028  df-struct 17108  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192  df-plusg 17224  df-mulr 17225  df-starv 17226  df-sca 17227  df-vsca 17228  df-ip 17229  df-tset 17230  df-ple 17231  df-ds 17233  df-unif 17234  df-hom 17235  df-cco 17236  df-rest 17376  df-topn 17377  df-0g 17395  df-gsum 17396  df-topgen 17397  df-pt 17398  df-prds 17401  df-xrs 17457  df-qtop 17462  df-imas 17463  df-xps 17465  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-submnd 18743  df-mulg 19035  df-cntz 19283  df-cmn 19748  df-psmet 21336  df-xmet 21337  df-met 21338  df-bl 21339  df-mopn 21340  df-fbas 21341  df-fg 21342  df-cnfld 21345  df-top 22869  df-topon 22886  df-topsp 22908  df-bases 22921  df-cld 22994  df-ntr 22995  df-cls 22996  df-nei 23073  df-lp 23111  df-perf 23112  df-cn 23202  df-cnp 23203  df-haus 23290  df-tx 23537  df-hmeo 23730  df-fil 23821  df-fm 23913  df-flim 23914  df-flf 23915  df-xms 24295  df-ms 24296  df-tms 24297  df-cncf 24855  df-limc 25843  df-dv 25844

This theorem is referenced by:  picn  26435  pipos  26436  pine0  26437  pirp  26438  sinhalfpilem  26440  halfpire  26441  sincosq1lem  26474  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  coseq00topi  26479  coseq0negpitopi  26480  tangtx  26482  sinq12gt0  26484  sinq12ge0  26485  sinq34lt0t  26486  cosq14gt0  26487  cosq14ge0  26488  sincos4thpi  26490  tan4thpiOLD  26492  sincos6thpi  26493  pigt3  26495  pige3  26496  pige3ALT  26497  coskpi  26500  sineq0  26501  coseq1  26502  cos02pilt1  26503  cosq34lt1  26504  efeq1  26505  cosne0  26506  cosordlem  26507  cosord  26508  cos0pilt1  26509  cos11  26510  sinord  26511  recosf1o  26512  resinf1o  26513  tanord1  26514  negpitopissre  26517  efif1olem1  26519  efif1olem2  26520  efif1olem4  26522  efif1o  26523  efifo  26524  eff1o  26526  ellogrn  26536  relogrn  26538  logimclad  26549  abslogimle  26550  logi  26564  logneg  26565  lognegb  26567  eflogeq  26579  logcj  26583  argregt0  26587  argrege0  26588  argimgt0  26589  argimlt0  26590  logimul  26591  logneg2  26592  abslogle  26595  logcnlem3  26621  dvloglem  26625  logf1o2  26627  efopnlem1  26633  efopnlem2  26634  cxpsqrtlem  26679  abscxpbnd  26730  root1eq1  26732  logreclem  26739  ang180lem1  26786  ang180lem2  26787  ang180lem3  26788  ang180lem4  26789  isosctrlem1  26795  1cubrlem  26818  asinneg  26863  asinsin  26869  asin1  26871  acosbnd  26877  atanlogaddlem  26890  atanlogsublem  26892  atanlogsub  26893  atantan  26900  atanbndlem  26902  atan1  26905  o1cxp  26952  lgamgulmlem4  27009  lgamgulmlem5  27010  lgamgulmlem6  27011  lgambdd  27014  basellem1  27058  basellem4  27061  basellem8  27065  basellem9  27066  cos9thpinconstrlem1  33949  circum  35872  bj-pinftyccb  37551  bj-minftyccb  37555  bj-pinftynminfty  37557  taupi  37653  sin2h  37945  cos2h  37946  tan2h  37947  asin1half  42803  acos1half  42804  proot1ex  43642  isosctrlem1ALT  45378  sineq0ALT  45381  negpilt0  45732  coseq0  46310  sinaover2ne0  46314  itgsin0pilem1  46396  itgsinexplem1  46400  itgsinexp  46401  wallispilem1  46511  wallispilem2  46512  wallispi  46516  stirlinglem15  46534  stirlingr  46536  dirker2re  46538  dirkerval2  46540  dirkerre  46541  dirkerper  46542  dirkertrigeqlem2  46545  dirkertrigeqlem3  46546  dirkertrigeq  46547  dirkeritg  46548  dirkercncflem1  46549  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem5  46558  fourierdlem9  46562  fourierdlem16  46569  fourierdlem18  46571  fourierdlem21  46574  fourierdlem22  46575  fourierdlem24  46577  fourierdlem38  46591  fourierdlem40  46593  fourierdlem43  46596  fourierdlem44  46597  fourierdlem46  46598  fourierdlem50  46602  fourierdlem58  46610  fourierdlem62  46614  fourierdlem66  46618  fourierdlem72  46624  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem77  46629  fourierdlem78  46630  fourierdlem83  46635  fourierdlem85  46637  fourierdlem87  46639  fourierdlem88  46640  fourierdlem93  46645  fourierdlem94  46646  fourierdlem95  46647  fourierdlem101  46653  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  fourierdlem114  46666  sqwvfoura  46674  sqwvfourb  46675  fourierswlem  46676  fouriersw  46677  fouriercn  46678  goldrarr  47343  goldrapos  47345