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

Theorem pire 23350
Description:  pi is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
Assertion
Ref Expression
pire  |-  pi  e.  RR

Proof of Theorem pire
StepHypRef Expression
1 pilem3 23346 . . 3  |-  ( pi  e.  ( 2 (,) 4 )  /\  ( sin `  pi )  =  0 )
21simpli 459 . 2  |-  pi  e.  ( 2 (,) 4
)
3 elioore 11612 . 2  |-  ( pi  e.  ( 2 (,) 4 )  ->  pi  e.  RR )
42, 3ax-mp 5 1  |-  pi  e.  RR
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1872   ` cfv 5539  (class class class)co 6244   RRcr 9484   0cc0 9485   2c2 10605   4c4 10607   (,)cioo 11581   sincsin 14054   picpi 14057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-inf2 8094  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562  ax-pre-sup 9563  ax-addf 9564  ax-mulf 9565
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-int 4194  df-iun 4239  df-iin 4240  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-se 4751  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-isom 5548  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-of 6484  df-om 6646  df-1st 6746  df-2nd 6747  df-supp 6865  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-2o 7133  df-oadd 7136  df-er 7313  df-map 7424  df-pm 7425  df-ixp 7473  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-fsupp 7832  df-fi 7873  df-sup 7904  df-inf 7905  df-oi 7973  df-card 8320  df-cda 8544  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-div 10216  df-nn 10556  df-2 10614  df-3 10615  df-4 10616  df-5 10617  df-6 10618  df-7 10619  df-8 10620  df-9 10621  df-10 10622  df-n0 10816  df-z 10884  df-dec 10998  df-uz 11106  df-q 11211  df-rp 11249  df-xneg 11355  df-xadd 11356  df-xmul 11357  df-ioo 11585  df-ioc 11586  df-ico 11587  df-icc 11588  df-fz 11731  df-fzo 11862  df-fl 11973  df-seq 12159  df-exp 12218  df-fac 12405  df-bc 12433  df-hash 12461  df-shft 13069  df-cj 13101  df-re 13102  df-im 13103  df-sqrt 13237  df-abs 13238  df-limsup 13464  df-clim 13490  df-rlim 13491  df-sum 13691  df-ef 14059  df-sin 14061  df-cos 14062  df-pi 14064  df-struct 15061  df-ndx 15062  df-slot 15063  df-base 15064  df-sets 15065  df-ress 15066  df-plusg 15141  df-mulr 15142  df-starv 15143  df-sca 15144  df-vsca 15145  df-ip 15146  df-tset 15147  df-ple 15148  df-ds 15150  df-unif 15151  df-hom 15152  df-cco 15153  df-rest 15259  df-topn 15260  df-0g 15278  df-gsum 15279  df-topgen 15280  df-pt 15281  df-prds 15284  df-xrs 15338  df-qtop 15344  df-imas 15345  df-xps 15348  df-mre 15430  df-mrc 15431  df-acs 15433  df-mgm 16426  df-sgrp 16465  df-mnd 16475  df-submnd 16521  df-mulg 16614  df-cntz 16909  df-cmn 17370  df-psmet 18900  df-xmet 18901  df-met 18902  df-bl 18903  df-mopn 18904  df-fbas 18905  df-fg 18906  df-cnfld 18909  df-top 19858  df-bases 19859  df-topon 19860  df-topsp 19861  df-cld 19971  df-ntr 19972  df-cls 19973  df-nei 20051  df-lp 20089  df-perf 20090  df-cn 20180  df-cnp 20181  df-haus 20268  df-tx 20514  df-hmeo 20707  df-fil 20798  df-fm 20890  df-flim 20891  df-flf 20892  df-xms 21272  df-ms 21273  df-tms 21274  df-cncf 21847  df-limc 22758  df-dv 22759
This theorem is referenced by:  picn  23351  pipos  23352  pirp  23353  sinhalfpilem  23355  halfpire  23356  sincosq1lem  23389  sincosq2sgn  23391  sincosq3sgn  23392  sincosq4sgn  23393  coseq00topi  23394  coseq0negpitopi  23395  tangtx  23397  sinq12gt0  23399  sinq12ge0  23400  sinq34lt0t  23401  cosq14gt0  23402  cosq14ge0  23403  sincos4thpi  23405  tan4thpi  23406  sincos6thpi  23407  pige3  23409  coskpi  23412  sineq0  23413  coseq1  23414  efeq1  23415  cosne0  23416  cosordlem  23417  cosord  23418  cos11  23419  sinord  23420  recosf1o  23421  resinf1o  23422  tanord1  23423  negpitopissre  23426  efif1olem1  23428  efif1olem2  23429  efif1olem4  23431  efif1o  23432  efifo  23433  eff1o  23435  ellogrn  23446  relogrn  23448  logimclad  23459  abslogimle  23460  logneg  23474  lognegb  23476  eflogeq  23488  logcj  23492  argregt0  23496  argrege0  23497  argimgt0  23498  argimlt0  23499  logimul  23500  logneg2  23501  abslogle  23504  logcnlem3  23526  dvloglem  23530  logf1o2  23532  efopnlem1  23538  efopnlem2  23539  cxpsqrtlem  23584  abscxpbnd  23630  root1eq1  23632  logreclem  23636  ang180lem1  23675  ang180lem2  23676  ang180lem3  23677  ang180lem4  23678  isosctrlem1  23684  1cubrlem  23704  asinneg  23749  asinsin  23755  asin1  23757  acosbnd  23763  atanlogaddlem  23776  atanlogsublem  23778  atanlogsub  23779  atantan  23786  atanbndlem  23788  atan1  23791  o1cxp  23837  lgamgulmlem4  23894  lgamgulmlem5  23895  lgamgulmlem6  23896  lgambdd  23899  basellem1  23944  basellem4  23947  basellem8  23951  basellem9  23952  circum  30265  logi  30316  bj-pinftyccb  31570  bj-minftyccb  31574  bj-pinftynminfty  31576  taupi  31631  sin2h  31842  cos2h  31843  tan2h  31844  pigt3  31845  dvtanlemOLD  31898  proot1ex  35991  isosctrlem1ALT  37247  sineq0ALT  37250  negpilt0  37387  coseq0  37622  sinaover2ne0  37626  itgsin0pilem1  37709  itgsinexplem1  37713  itgsinexp  37714  wallispilem1  37810  wallispilem2  37811  wallispi  37815  stirlinglem15  37833  stirlingr  37835  dirker2re  37837  dirkerval2  37839  dirkerre  37840  dirkerper  37841  dirkertrigeqlem2  37844  dirkertrigeqlem3  37845  dirkertrigeq  37846  dirkeritg  37847  dirkercncflem1  37848  dirkercncflem2  37849  dirkercncflem4  37851  fourierdlem5  37857  fourierdlem9  37861  fourierdlem16  37868  fourierdlem18  37870  fourierdlem21  37873  fourierdlem22  37874  fourierdlem24  37876  fourierdlem38  37891  fourierdlem40  37893  fourierdlem43  37897  fourierdlem44  37898  fourierdlem46  37899  fourierdlem50  37903  fourierdlem58  37911  fourierdlem62  37915  fourierdlem66  37919  fourierdlem72  37925  fourierdlem74  37927  fourierdlem75  37928  fourierdlem76  37929  fourierdlem77  37930  fourierdlem78  37931  fourierdlem83  37936  fourierdlem85  37938  fourierdlem87  37940  fourierdlem88  37941  fourierdlem93  37946  fourierdlem94  37947  fourierdlem95  37948  fourierdlem101  37954  fourierdlem102  37955  fourierdlem103  37956  fourierdlem104  37957  fourierdlem111  37964  fourierdlem112  37965  fourierdlem113  37966  fourierdlem114  37967  sqwvfoura  37975  sqwvfourb  37976  fourierswlem  37977  fouriersw  37978  fouriercn  37979
  Copyright terms: Public domain W3C validator