![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > halfpire | GIF version |
Description: π / 2 is real. (Contributed by David Moews, 28-Feb-2017.) |
Ref | Expression |
---|---|
halfpire | ⊢ (π / 2) ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pire 13840 | . 2 ⊢ π ∈ ℝ | |
2 | 1 | rehalfcli 9143 | 1 ⊢ (π / 2) ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2148 (class class class)co 5868 ℝcr 7788 / cdiv 8605 2c2 8946 πcpi 11626 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4115 ax-sep 4118 ax-nul 4126 ax-pow 4171 ax-pr 4205 ax-un 4429 ax-setind 4532 ax-iinf 4583 ax-cnex 7880 ax-resscn 7881 ax-1cn 7882 ax-1re 7883 ax-icn 7884 ax-addcl 7885 ax-addrcl 7886 ax-mulcl 7887 ax-mulrcl 7888 ax-addcom 7889 ax-mulcom 7890 ax-addass 7891 ax-mulass 7892 ax-distr 7893 ax-i2m1 7894 ax-0lt1 7895 ax-1rid 7896 ax-0id 7897 ax-rnegex 7898 ax-precex 7899 ax-cnre 7900 ax-pre-ltirr 7901 ax-pre-ltwlin 7902 ax-pre-lttrn 7903 ax-pre-apti 7904 ax-pre-ltadd 7905 ax-pre-mulgt0 7906 ax-pre-mulext 7907 ax-arch 7908 ax-caucvg 7909 ax-pre-suploc 7910 ax-addf 7911 ax-mulf 7912 |
This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-if 3535 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-disj 3978 df-br 4001 df-opab 4062 df-mpt 4063 df-tr 4099 df-id 4289 df-po 4292 df-iso 4293 df-iord 4362 df-on 4364 df-ilim 4365 df-suc 4367 df-iom 4586 df-xp 4628 df-rel 4629 df-cnv 4630 df-co 4631 df-dm 4632 df-rn 4633 df-res 4634 df-ima 4635 df-iota 5173 df-fun 5213 df-fn 5214 df-f 5215 df-f1 5216 df-fo 5217 df-f1o 5218 df-fv 5219 df-isom 5220 df-riota 5824 df-ov 5871 df-oprab 5872 df-mpo 5873 df-of 6076 df-1st 6134 df-2nd 6135 df-recs 6299 df-irdg 6364 df-frec 6385 df-1o 6410 df-oadd 6414 df-er 6528 df-map 6643 df-pm 6644 df-en 6734 df-dom 6735 df-fin 6736 df-sup 6976 df-inf 6977 df-pnf 7971 df-mnf 7972 df-xr 7973 df-ltxr 7974 df-le 7975 df-sub 8107 df-neg 8108 df-reap 8509 df-ap 8516 df-div 8606 df-inn 8896 df-2 8954 df-3 8955 df-4 8956 df-5 8957 df-6 8958 df-7 8959 df-8 8960 df-9 8961 df-n0 9153 df-z 9230 df-uz 9505 df-q 9596 df-rp 9628 df-xneg 9746 df-xadd 9747 df-ioo 9866 df-ioc 9867 df-ico 9868 df-icc 9869 df-fz 9983 df-fzo 10116 df-seqfrec 10419 df-exp 10493 df-fac 10677 df-bc 10699 df-ihash 10727 df-shft 10795 df-cj 10822 df-re 10823 df-im 10824 df-rsqrt 10978 df-abs 10979 df-clim 11258 df-sumdc 11333 df-ef 11627 df-sin 11629 df-cos 11630 df-pi 11632 df-rest 12625 df-topgen 12644 df-psmet 13120 df-xmet 13121 df-met 13122 df-bl 13123 df-mopn 13124 df-top 13129 df-topon 13142 df-bases 13174 df-ntr 13229 df-cn 13321 df-cnp 13322 df-tx 13386 df-cncf 13691 df-limced 13758 df-dvap 13759 |
This theorem is referenced by: neghalfpire 13847 cosneghalfpi 13852 sinhalfpip 13874 sinhalfpim 13875 coshalfpip 13876 coshalfpim 13877 sincosq1lem 13879 sincosq1sgn 13880 sincosq2sgn 13881 sincosq3sgn 13882 sincosq4sgn 13883 cosq14gt0 13886 cosq23lt0 13887 coseq0q4123 13888 coseq00topi 13889 coseq0negpitopi 13890 sincosq1eq 13893 sincos6thpi 13896 cos02pilt1 13905 |
Copyright terms: Public domain | W3C validator |