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

Theorem halfpire 23430
Description:  pi  /  2 is real. (Contributed by David Moews, 28-Feb-2017.)
Assertion
Ref Expression
halfpire  |-  ( pi 
/  2 )  e.  RR

Proof of Theorem halfpire
StepHypRef Expression
1 pire 23424 . 2  |-  pi  e.  RR
21rehalfcli 10850 1  |-  ( pi 
/  2 )  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1890  (class class class)co 6275   RRcr 9524    / cdiv 10257   2c2 10647   picpi 14129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-rep 4486  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-inf2 8132  ax-cnex 9581  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601  ax-pre-mulgt0 9602  ax-pre-sup 9603  ax-addf 9604  ax-mulf 9605
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-fal 1453  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-pss 3387  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-tp 3940  df-op 3942  df-uni 4168  df-int 4204  df-iun 4249  df-iin 4250  df-br 4374  df-opab 4433  df-mpt 4434  df-tr 4469  df-eprel 4722  df-id 4726  df-po 4732  df-so 4733  df-fr 4770  df-se 4771  df-we 4772  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-pred 5358  df-ord 5404  df-on 5405  df-lim 5406  df-suc 5407  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-isom 5569  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-of 6518  df-om 6680  df-1st 6780  df-2nd 6781  df-supp 6902  df-wrecs 7014  df-recs 7076  df-rdg 7114  df-1o 7168  df-2o 7169  df-oadd 7172  df-er 7349  df-map 7460  df-pm 7461  df-ixp 7509  df-en 7556  df-dom 7557  df-sdom 7558  df-fin 7559  df-fsupp 7870  df-fi 7911  df-sup 7942  df-inf 7943  df-oi 8011  df-card 8359  df-cda 8584  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-sub 9848  df-neg 9849  df-div 10258  df-nn 10598  df-2 10656  df-3 10657  df-4 10658  df-5 10659  df-6 10660  df-7 10661  df-8 10662  df-9 10663  df-10 10664  df-n0 10859  df-z 10927  df-dec 11041  df-uz 11149  df-q 11254  df-rp 11292  df-xneg 11398  df-xadd 11399  df-xmul 11400  df-ioo 11628  df-ioc 11629  df-ico 11630  df-icc 11631  df-fz 11775  df-fzo 11908  df-fl 12021  df-seq 12207  df-exp 12266  df-fac 12453  df-bc 12481  df-hash 12509  df-shft 13140  df-cj 13172  df-re 13173  df-im 13174  df-sqrt 13308  df-abs 13309  df-limsup 13536  df-clim 13562  df-rlim 13563  df-sum 13763  df-ef 14131  df-sin 14133  df-cos 14134  df-pi 14136  df-struct 15133  df-ndx 15134  df-slot 15135  df-base 15136  df-sets 15137  df-ress 15138  df-plusg 15213  df-mulr 15214  df-starv 15215  df-sca 15216  df-vsca 15217  df-ip 15218  df-tset 15219  df-ple 15220  df-ds 15222  df-unif 15223  df-hom 15224  df-cco 15225  df-rest 15331  df-topn 15332  df-0g 15350  df-gsum 15351  df-topgen 15352  df-pt 15353  df-prds 15356  df-xrs 15410  df-qtop 15416  df-imas 15417  df-xps 15420  df-mre 15502  df-mrc 15503  df-acs 15505  df-mgm 16498  df-sgrp 16537  df-mnd 16547  df-submnd 16593  df-mulg 16686  df-cntz 16981  df-cmn 17442  df-psmet 18972  df-xmet 18973  df-met 18974  df-bl 18975  df-mopn 18976  df-fbas 18977  df-fg 18978  df-cnfld 18981  df-top 19931  df-bases 19932  df-topon 19933  df-topsp 19934  df-cld 20044  df-ntr 20045  df-cls 20046  df-nei 20124  df-lp 20162  df-perf 20163  df-cn 20253  df-cnp 20254  df-haus 20341  df-tx 20587  df-hmeo 20780  df-fil 20871  df-fm 20963  df-flim 20964  df-flf 20965  df-xms 21345  df-ms 21346  df-tms 21347  df-cncf 21920  df-limc 22832  df-dv 22833
This theorem is referenced by:  neghalfpire  23431  cosneghalfpi  23436  sincosq1lem  23463  sincosq1sgn  23464  sincosq2sgn  23465  sincosq3sgn  23466  sincosq4sgn  23467  coseq00topi  23468  coseq0negpitopi  23469  tanabsge  23472  cosq14gt0  23476  cosq14ge0  23477  sincos6thpi  23481  cosne0  23490  sinord  23494  resinf1o  23496  tanord1  23497  tanord  23498  tanregt0  23499  efif1olem4  23505  argregt0  23570  argrege0  23571  logimul  23574  isosctrlem1  23758  asinsinlem  23828  asinsin  23829  acoscos  23830  asin1  23831  reasinsin  23833  acosbnd  23837  asinrecl  23839  acosrecl  23840  atanlogsublem  23852  atantan  23860  atanbndlem  23862  atanbnd  23863  atan1  23865  basellem4  24021  logi  30375  iexpire  30376  cos2h  31937  tan2h  31938  dvtanlemOLD  31992  dvacos  32030  fourierdlem62  38088
  Copyright terms: Public domain W3C validator