MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pire Structured version   Visualization version   GIF version

Theorem pire 24501
Description: π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
Assertion
Ref Expression
pire π ∈ ℝ

Proof of Theorem pire
StepHypRef Expression
1 pilem3 24497 . . 3 (π ∈ (2(,)4) ∧ (sin‘π) = 0)
21simpli 476 . 2 π ∈ (2(,)4)
3 elioore 12406 . 2 (π ∈ (2(,)4) → π ∈ ℝ)
42, 3ax-mp 5 1 π ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652  wcel 2155  cfv 6067  (class class class)co 6841  cr 10187  0cc0 10188  2c2 11326  4c4 11328  (,)cioo 12376  sincsin 15077  πcpi 15080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266  ax-addf 10267  ax-mulf 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-of 7094  df-om 7263  df-1st 7365  df-2nd 7366  df-supp 7497  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-2o 7764  df-oadd 7767  df-er 7946  df-map 8061  df-pm 8062  df-ixp 8113  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-fsupp 8482  df-fi 8523  df-sup 8554  df-inf 8555  df-oi 8621  df-card 9015  df-cda 9242  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-4 11336  df-5 11337  df-6 11338  df-7 11339  df-8 11340  df-9 11341  df-n0 11538  df-z 11624  df-dec 11740  df-uz 11886  df-q 11989  df-rp 12028  df-xneg 12145  df-xadd 12146  df-xmul 12147  df-ioo 12380  df-ioc 12381  df-ico 12382  df-icc 12383  df-fz 12533  df-fzo 12673  df-fl 12800  df-seq 13008  df-exp 13067  df-fac 13264  df-bc 13293  df-hash 13321  df-shft 14093  df-cj 14125  df-re 14126  df-im 14127  df-sqrt 14261  df-abs 14262  df-limsup 14488  df-clim 14505  df-rlim 14506  df-sum 14703  df-ef 15081  df-sin 15083  df-cos 15084  df-pi 15086  df-struct 16133  df-ndx 16134  df-slot 16135  df-base 16137  df-sets 16138  df-ress 16139  df-plusg 16228  df-mulr 16229  df-starv 16230  df-sca 16231  df-vsca 16232  df-ip 16233  df-tset 16234  df-ple 16235  df-ds 16237  df-unif 16238  df-hom 16239  df-cco 16240  df-rest 16350  df-topn 16351  df-0g 16369  df-gsum 16370  df-topgen 16371  df-pt 16372  df-prds 16375  df-xrs 16429  df-qtop 16434  df-imas 16435  df-xps 16437  df-mre 16513  df-mrc 16514  df-acs 16516  df-mgm 17509  df-sgrp 17551  df-mnd 17562  df-submnd 17603  df-mulg 17809  df-cntz 18014  df-cmn 18460  df-psmet 20010  df-xmet 20011  df-met 20012  df-bl 20013  df-mopn 20014  df-fbas 20015  df-fg 20016  df-cnfld 20019  df-top 20977  df-topon 20994  df-topsp 21016  df-bases 21029  df-cld 21102  df-ntr 21103  df-cls 21104  df-nei 21181  df-lp 21219  df-perf 21220  df-cn 21310  df-cnp 21311  df-haus 21398  df-tx 21644  df-hmeo 21837  df-fil 21928  df-fm 22020  df-flim 22021  df-flf 22022  df-xms 22403  df-ms 22404  df-tms 22405  df-cncf 22959  df-limc 23920  df-dv 23921
This theorem is referenced by:  picn  24502  pipos  24503  pirp  24504  sinhalfpilem  24506  halfpire  24507  sincosq1lem  24540  sincosq2sgn  24542  sincosq3sgn  24543  sincosq4sgn  24544  coseq00topi  24545  coseq0negpitopi  24546  tangtx  24548  sinq12gt0  24550  sinq12ge0  24551  sinq34lt0t  24552  cosq14gt0  24553  cosq14ge0  24554  sincos4thpi  24556  tan4thpi  24557  sincos6thpi  24558  pige3  24560  coskpi  24563  sineq0  24564  coseq1  24565  efeq1  24566  cosne0  24567  cosordlem  24568  cosord  24569  cos11  24570  sinord  24571  recosf1o  24572  resinf1o  24573  tanord1  24574  negpitopissre  24577  efif1olem1  24579  efif1olem2  24580  efif1olem4  24582  efif1o  24583  efifo  24584  eff1o  24586  ellogrn  24596  relogrn  24598  logimclad  24609  abslogimle  24610  logneg  24624  lognegb  24626  eflogeq  24638  logcj  24642  argregt0  24646  argrege0  24647  argimgt0  24648  argimlt0  24649  logimul  24650  logneg2  24651  abslogle  24654  logcnlem3  24680  dvloglem  24684  logf1o2  24686  efopnlem1  24692  efopnlem2  24693  cxpsqrtlem  24738  abscxpbnd  24784  root1eq1  24786  logreclem  24790  ang180lem1  24829  ang180lem2  24830  ang180lem3  24831  ang180lem4  24832  isosctrlem1  24838  1cubrlem  24858  asinneg  24903  asinsin  24909  asin1  24911  acosbnd  24917  atanlogaddlem  24930  atanlogsublem  24932  atanlogsub  24933  atantan  24940  atanbndlem  24942  atan1  24945  o1cxp  24991  lgamgulmlem4  25048  lgamgulmlem5  25049  lgamgulmlem6  25050  lgambdd  25053  basellem1  25097  basellem4  25100  basellem8  25104  basellem9  25105  circum  31945  logi  31996  bj-pinftyccb  33474  bj-minftyccb  33478  bj-pinftynminfty  33480  taupi  33535  sin2h  33755  cos2h  33756  tan2h  33757  pigt3  33758  proot1ex  38388  isosctrlem1ALT  39754  sineq0ALT  39757  negpilt0  40064  coseq0  40645  sinaover2ne0  40649  itgsin0pilem1  40735  itgsinexplem1  40739  itgsinexp  40740  wallispilem1  40851  wallispilem2  40852  wallispi  40856  stirlinglem15  40874  stirlingr  40876  dirker2re  40878  dirkerval2  40880  dirkerre  40881  dirkerper  40882  dirkertrigeqlem2  40885  dirkertrigeqlem3  40886  dirkertrigeq  40887  dirkeritg  40888  dirkercncflem1  40889  dirkercncflem2  40890  dirkercncflem4  40892  fourierdlem5  40898  fourierdlem9  40902  fourierdlem16  40909  fourierdlem18  40911  fourierdlem21  40914  fourierdlem22  40915  fourierdlem24  40917  fourierdlem38  40931  fourierdlem40  40933  fourierdlem43  40936  fourierdlem44  40937  fourierdlem46  40938  fourierdlem50  40942  fourierdlem58  40950  fourierdlem62  40954  fourierdlem66  40958  fourierdlem72  40964  fourierdlem74  40966  fourierdlem75  40967  fourierdlem76  40968  fourierdlem77  40969  fourierdlem78  40970  fourierdlem83  40975  fourierdlem85  40977  fourierdlem87  40979  fourierdlem88  40980  fourierdlem93  40985  fourierdlem94  40986  fourierdlem95  40987  fourierdlem101  40993  fourierdlem102  40994  fourierdlem103  40995  fourierdlem104  40996  fourierdlem111  41003  fourierdlem112  41004  fourierdlem113  41005  fourierdlem114  41006  sqwvfoura  41014  sqwvfourb  41015  fourierswlem  41016  fouriersw  41017  fouriercn  41018
  Copyright terms: Public domain W3C validator