Theorem pire 26581

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  ‘cfv 6534  (class class class)co 7408  ℝcr 11095  0cc0 11096  2c2 12291  4c4 12293  (,)cioo 13368  sincsin 16113  πcpi 16116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5239  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-inf2 9606  ax-cnex 11152  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173  ax-pre-sup 11174  ax-addf 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4874  df-int 4914  df-iun 4959  df-iin 4960  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6300  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-isom 6543  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-of 7672  df-om 7859  df-1st 7982  df-2nd 7983  df-supp 8153  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-2o 8450  df-er 8690  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9318  df-fi 9367  df-sup 9398  df-inf 9399  df-oi 9468  df-card 9921  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440  df-div 11868  df-nn 12230  df-2 12299  df-3 12300  df-4 12301  df-5 12302  df-6 12303  df-7 12304  df-8 12305  df-9 12306  df-n0 12501  df-z 12588  df-dec 12708  df-uz 12859  df-q 12969  df-rp 13013  df-xneg 13133  df-xadd 13134  df-xmul 13135  df-ioo 13372  df-ioc 13373  df-ico 13374  df-icc 13375  df-fz 13532  df-fzo 13679  df-fl 13821  df-seq 14034  df-exp 14094  df-fac 14306  df-bc 14335  df-hash 14363  df-shft 15100  df-cj 15146  df-re 15147  df-im 15148  df-sqrt 15282  df-abs 15283  df-limsup 15518  df-clim 15535  df-rlim 15536  df-sum 15734  df-ef 16117  df-sin 16119  df-cos 16120  df-pi 16122  df-struct 17203  df-sets 17220  df-slot 17238  df-ndx 17250  df-base 17266  df-ress 17287  df-plusg 17319  df-mulr 17320  df-starv 17321  df-sca 17322  df-vsca 17323  df-ip 17324  df-tset 17325  df-ple 17326  df-ds 17328  df-unif 17329  df-hom 17330  df-cco 17331  df-rest 17471  df-topn 17472  df-0g 17490  df-gsum 17491  df-topgen 17492  df-pt 17493  df-prds 17496  df-xrs 17552  df-qtop 17557  df-imas 17558  df-xps 17560  df-mre 17634  df-mrc 17635  df-acs 17637  df-mgm 18694  df-sgrp 18773  df-mnd 18789  df-submnd 18838  df-mulg 19130  df-cntz 19383  df-cmn 19848  df-psmet 21479  df-xmet 21480  df-met 21481  df-bl 21482  df-mopn 21483  df-fbas 21484  df-fg 21485  df-cnfld 21488  df-top 23016  df-topon 23033  df-topsp 23055  df-bases 23068  df-cld 23141  df-ntr 23142  df-cls 23143  df-nei 23220  df-lp 23258  df-perf 23259  df-cn 23349  df-cnp 23350  df-haus 23437  df-tx 23684  df-hmeo 23877  df-fil 23968  df-fm 24060  df-flim 24061  df-flf 24062  df-xms 24442  df-ms 24443  df-tms 24444  df-cncf 25002  df-limc 25990  df-dv 25991

This theorem is referenced by:  2pire  26582  picn  26583  pipos  26585  pige0  26586  pine0  26587  pirp  26588  sinhalfpilem  26590  halfpire  26591  sincosq1lem  26624  sincosq2sgn  26626  sincosq3sgn  26627  sincosq4sgn  26628  coseq00topi  26629  coseq0negpitopi  26630  tangtx  26632  sinq12gt0  26634  sinq12ge0  26635  sinq34lt0t  26636  cosq14gt0  26637  cosq14ge0  26638  sincos4thpi  26640  tan4thpiOLD  26642  sincos6thpi  26643  pigt3  26645  pige3  26646  pige3ALT  26647  coskpi  26650  sineq0  26651  coseq1  26652  cos02pilt1  26653  cosq34lt1  26654  efeq1  26655  cosne0  26656  cosordlem  26657  cosord  26658  cos0pilt1  26659  cos11  26660  sinord  26661  recosf1o  26662  resinf1o  26663  tanord1  26664  negpitopissre  26667  efif1olem1  26669  efif1olem2  26670  efif1olem4  26672  efif1o  26673  efifo  26674  eff1o  26676  ellogrn  26686  relogrn  26688  logimclad  26699  abslogimle  26700  logi  26714  logneg  26715  lognegb  26717  eflogeq  26729  logcj  26733  argregt0  26737  argrege0  26738  argimgt0  26739  argimlt0  26740  logimul  26741  logneg2  26742  abslogle  26745  logcnlem3  26771  dvloglem  26775  logf1o2  26777  efopnlem1  26783  efopnlem2  26784  cxpsqrtlem  26829  abscxpbnd  26880  root1eq1  26882  logreclem  26889  ang180lem1  26936  ang180lem2  26937  ang180lem3  26938  ang180lem4  26939  isosctrlem1  26945  1cubrlem  26968  asinneg  27013  asinsin  27019  asin1  27021  acosbnd  27027  atanlogaddlem  27040  atanlogsublem  27042  atanlogsub  27043  atantan  27050  atanbndlem  27052  atan1  27055  o1cxp  27101  lgamgulmlem4  27158  lgamgulmlem5  27159  lgamgulmlem6  27160  lgambdd  27163  basellem1  27207  basellem4  27210  basellem8  27214  basellem9  27215  cos9thpinconstrlem1  34120  circum  36061  bj-pinftyccb  37748  bj-minftyccb  37752  bj-pinftynminfty  37754  taupi  37850  sin2h  38144  cos2h  38145  tan2h  38146  asin1half  43003  acos1half  43004  proot1ex  43810  isosctrlem1ALT  45529  sineq0ALT  45532  negpilt0  45887  coseq0  46465  sinaover2ne0  46469  itgsin0pilem1  46551  itgsinexplem1  46555  itgsinexp  46556  wallispilem1  46666  wallispilem2  46667  wallispi  46671  stirlinglem15  46689  stirlingr  46691  dirker2re  46693  dirkerval2  46695  dirkerre  46696  dirkertrigeqlem2  46700  dirkertrigeqlem3  46701  dirkertrigeq  46702  dirkeritg  46703  dirkercncflem1  46704  dirkercncflem4  46707  fourierdlem5  46713  fourierdlem9  46717  fourierdlem16  46724  fourierdlem18  46726  fourierdlem21  46729  fourierdlem22  46730  fourierdlem24  46732  fourierdlem38  46746  fourierdlem40  46748  fourierdlem43  46751  fourierdlem44  46752  fourierdlem46  46753  fourierdlem50  46757  fourierdlem58  46765  fourierdlem62  46769  fourierdlem66  46773  fourierdlem72  46779  fourierdlem74  46781  fourierdlem75  46782  fourierdlem76  46783  fourierdlem77  46784  fourierdlem78  46785  fourierdlem83  46790  fourierdlem85  46792  fourierdlem87  46794  fourierdlem88  46795  fourierdlem93  46800  fourierdlem94  46801  fourierdlem95  46802  fourierdlem101  46808  fourierdlem102  46809  fourierdlem103  46810  fourierdlem104  46811  fourierdlem111  46818  fourierdlem112  46819  fourierdlem113  46820  fourierdlem114  46821  sqwvfoura  46829  sqwvfourb  46830  fourierswlem  46831  fouriersw  46832  fouriercn  46833  goldrarr  47502  goldrapos  47504