Theorem pire 25721

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  ‘cfv 6484  (class class class)co 7342  ℝcr 10976  0cc0 10977  2c2 12134  4c4 12136  (,)cioo 13185  sincsin 15873  πcpi 15876

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5234  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655  ax-inf2 9503  ax-cnex 11033  ax-resscn 11034  ax-1cn 11035  ax-icn 11036  ax-addcl 11037  ax-addrcl 11038  ax-mulcl 11039  ax-mulrcl 11040  ax-mulcom 11041  ax-addass 11042  ax-mulass 11043  ax-distr 11044  ax-i2m1 11045  ax-1ne0 11046  ax-1rid 11047  ax-rnegex 11048  ax-rrecex 11049  ax-cnre 11050  ax-pre-lttri 11051  ax-pre-lttrn 11052  ax-pre-ltadd 11053  ax-pre-mulgt0 11054  ax-pre-sup 11055  ax-addf 11056  ax-mulf 11057

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3921  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-tp 4583  df-op 4585  df-uni 4858  df-int 4900  df-iun 4948  df-iin 4949  df-br 5098  df-opab 5160  df-mpt 5181  df-tr 5215  df-id 5523  df-eprel 5529  df-po 5537  df-so 5538  df-fr 5580  df-se 5581  df-we 5582  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6243  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-f1 6489  df-fo 6490  df-f1o 6491  df-fv 6492  df-isom 6493  df-riota 7298  df-ov 7345  df-oprab 7346  df-mpo 7347  df-of 7600  df-om 7786  df-1st 7904  df-2nd 7905  df-supp 8053  df-frecs 8172  df-wrecs 8203  df-recs 8277  df-rdg 8316  df-1o 8372  df-2o 8373  df-er 8574  df-map 8693  df-pm 8694  df-ixp 8762  df-en 8810  df-dom 8811  df-sdom 8812  df-fin 8813  df-fsupp 9232  df-fi 9273  df-sup 9304  df-inf 9305  df-oi 9372  df-card 9801  df-pnf 11117  df-mnf 11118  df-xr 11119  df-ltxr 11120  df-le 11121  df-sub 11313  df-neg 11314  df-div 11739  df-nn 12080  df-2 12142  df-3 12143  df-4 12144  df-5 12145  df-6 12146  df-7 12147  df-8 12148  df-9 12149  df-n0 12340  df-z 12426  df-dec 12544  df-uz 12689  df-q 12795  df-rp 12837  df-xneg 12954  df-xadd 12955  df-xmul 12956  df-ioo 13189  df-ioc 13190  df-ico 13191  df-icc 13192  df-fz 13346  df-fzo 13489  df-fl 13618  df-seq 13828  df-exp 13889  df-fac 14094  df-bc 14123  df-hash 14151  df-shft 14878  df-cj 14910  df-re 14911  df-im 14912  df-sqrt 15046  df-abs 15047  df-limsup 15280  df-clim 15297  df-rlim 15298  df-sum 15498  df-ef 15877  df-sin 15879  df-cos 15880  df-pi 15882  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-starv 17075  df-sca 17076  df-vsca 17077  df-ip 17078  df-tset 17079  df-ple 17080  df-ds 17082  df-unif 17083  df-hom 17084  df-cco 17085  df-rest 17231  df-topn 17232  df-0g 17250  df-gsum 17251  df-topgen 17252  df-pt 17253  df-prds 17256  df-xrs 17311  df-qtop 17316  df-imas 17317  df-xps 17319  df-mre 17393  df-mrc 17394  df-acs 17396  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-submnd 18529  df-mulg 18798  df-cntz 19020  df-cmn 19484  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-fbas 20700  df-fg 20701  df-cnfld 20704  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cld 22276  df-ntr 22277  df-cls 22278  df-nei 22355  df-lp 22393  df-perf 22394  df-cn 22484  df-cnp 22485  df-haus 22572  df-tx 22819  df-hmeo 23012  df-fil 23103  df-fm 23195  df-flim 23196  df-flf 23197  df-xms 23579  df-ms 23580  df-tms 23581  df-cncf 24147  df-limc 25136  df-dv 25137

This theorem is referenced by:  picn  25722  pipos  25723  pirp  25724  sinhalfpilem  25726  halfpire  25727  sincosq1lem  25760  sincosq2sgn  25762  sincosq3sgn  25763  sincosq4sgn  25764  coseq00topi  25765  coseq0negpitopi  25766  tangtx  25768  sinq12gt0  25770  sinq12ge0  25771  sinq34lt0t  25772  cosq14gt0  25773  cosq14ge0  25774  sincos4thpi  25776  tan4thpi  25777  sincos6thpi  25778  pigt3  25780  pige3  25781  pige3ALT  25782  coskpi  25785  sineq0  25786  coseq1  25787  cos02pilt1  25788  cosq34lt1  25789  efeq1  25790  cosne0  25791  cosordlem  25792  cosord  25793  cos0pilt1  25794  cos11  25795  sinord  25796  recosf1o  25797  resinf1o  25798  tanord1  25799  negpitopissre  25802  efif1olem1  25804  efif1olem2  25805  efif1olem4  25807  efif1o  25808  efifo  25809  eff1o  25811  ellogrn  25821  relogrn  25823  logimclad  25834  abslogimle  25835  logneg  25849  lognegb  25851  eflogeq  25863  logcj  25867  argregt0  25871  argrege0  25872  argimgt0  25873  argimlt0  25874  logimul  25875  logneg2  25876  abslogle  25879  logcnlem3  25905  dvloglem  25909  logf1o2  25911  efopnlem1  25917  efopnlem2  25918  cxpsqrtlem  25963  abscxpbnd  26012  root1eq1  26014  logreclem  26018  ang180lem1  26065  ang180lem2  26066  ang180lem3  26067  ang180lem4  26068  isosctrlem1  26074  1cubrlem  26097  asinneg  26142  asinsin  26148  asin1  26150  acosbnd  26156  atanlogaddlem  26169  atanlogsublem  26171  atanlogsub  26172  atantan  26179  atanbndlem  26181  atan1  26184  o1cxp  26230  lgamgulmlem4  26287  lgamgulmlem5  26288  lgamgulmlem6  26289  lgambdd  26292  basellem1  26336  basellem4  26339  basellem8  26343  basellem9  26344  circum  33929  logi  33990  bj-pinftyccb  35546  bj-minftyccb  35550  bj-pinftynminfty  35552  taupi  35648  sin2h  35921  cos2h  35922  tan2h  35923  acos1half  40476  proot1ex  41338  isosctrlem1ALT  42925  sineq0ALT  42928  negpilt0  43204  coseq0  43791  sinaover2ne0  43795  itgsin0pilem1  43877  itgsinexplem1  43881  itgsinexp  43882  wallispilem1  43992  wallispilem2  43993  wallispi  43997  stirlinglem15  44015  stirlingr  44017  dirker2re  44019  dirkerval2  44021  dirkerre  44022  dirkerper  44023  dirkertrigeqlem2  44026  dirkertrigeqlem3  44027  dirkertrigeq  44028  dirkeritg  44029  dirkercncflem1  44030  dirkercncflem2  44031  dirkercncflem4  44033  fourierdlem5  44039  fourierdlem9  44043  fourierdlem16  44050  fourierdlem18  44052  fourierdlem21  44055  fourierdlem22  44056  fourierdlem24  44058  fourierdlem38  44072  fourierdlem40  44074  fourierdlem43  44077  fourierdlem44  44078  fourierdlem46  44079  fourierdlem50  44083  fourierdlem58  44091  fourierdlem62  44095  fourierdlem66  44099  fourierdlem72  44105  fourierdlem74  44107  fourierdlem75  44108  fourierdlem76  44109  fourierdlem77  44110  fourierdlem78  44111  fourierdlem83  44116  fourierdlem85  44118  fourierdlem87  44120  fourierdlem88  44121  fourierdlem93  44126  fourierdlem94  44127  fourierdlem95  44128  fourierdlem101  44134  fourierdlem102  44135  fourierdlem103  44136  fourierdlem104  44137  fourierdlem111  44144  fourierdlem112  44145  fourierdlem113  44146  fourierdlem114  44147  sqwvfoura  44155  sqwvfourb  44156  fourierswlem  44157  fouriersw  44158  fouriercn  44159