![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pipos | Structured version Visualization version GIF version |
Description: π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
Ref | Expression |
---|---|
pipos | ⊢ 0 < π |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2pos 11547 | . 2 ⊢ 0 < 2 | |
2 | pigt2lt4 24739 | . . 3 ⊢ (2 < π ∧ π < 4) | |
3 | 2 | simpli 476 | . 2 ⊢ 2 < π |
4 | 0re 10437 | . . 3 ⊢ 0 ∈ ℝ | |
5 | 2re 11511 | . . 3 ⊢ 2 ∈ ℝ | |
6 | pire 24741 | . . 3 ⊢ π ∈ ℝ | |
7 | 4, 5, 6 | lttri 10562 | . 2 ⊢ ((0 < 2 ∧ 2 < π) → 0 < π) |
8 | 1, 3, 7 | mp2an 679 | 1 ⊢ 0 < π |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 4927 0cc0 10331 < clt 10470 2c2 11492 4c4 11494 πcpi 15274 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2747 ax-rep 5047 ax-sep 5058 ax-nul 5065 ax-pow 5117 ax-pr 5184 ax-un 7277 ax-inf2 8894 ax-cnex 10387 ax-resscn 10388 ax-1cn 10389 ax-icn 10390 ax-addcl 10391 ax-addrcl 10392 ax-mulcl 10393 ax-mulrcl 10394 ax-mulcom 10395 ax-addass 10396 ax-mulass 10397 ax-distr 10398 ax-i2m1 10399 ax-1ne0 10400 ax-1rid 10401 ax-rnegex 10402 ax-rrecex 10403 ax-cnre 10404 ax-pre-lttri 10405 ax-pre-lttrn 10406 ax-pre-ltadd 10407 ax-pre-mulgt0 10408 ax-pre-sup 10409 ax-addf 10410 ax-mulf 10411 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2756 df-cleq 2768 df-clel 2843 df-nfc 2915 df-ne 2965 df-nel 3071 df-ral 3090 df-rex 3091 df-reu 3092 df-rmo 3093 df-rab 3094 df-v 3414 df-sbc 3681 df-csb 3786 df-dif 3831 df-un 3833 df-in 3835 df-ss 3842 df-pss 3844 df-nul 4178 df-if 4349 df-pw 4422 df-sn 4440 df-pr 4442 df-tp 4444 df-op 4446 df-uni 4711 df-int 4748 df-iun 4792 df-iin 4793 df-br 4928 df-opab 4990 df-mpt 5007 df-tr 5029 df-id 5309 df-eprel 5314 df-po 5323 df-so 5324 df-fr 5363 df-se 5364 df-we 5365 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-pred 5984 df-ord 6030 df-on 6031 df-lim 6032 df-suc 6033 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193 df-fv 6194 df-isom 6195 df-riota 6935 df-ov 6977 df-oprab 6978 df-mpo 6979 df-of 7225 df-om 7395 df-1st 7498 df-2nd 7499 df-supp 7631 df-wrecs 7747 df-recs 7809 df-rdg 7847 df-1o 7901 df-2o 7902 df-oadd 7905 df-er 8085 df-map 8204 df-pm 8205 df-ixp 8256 df-en 8303 df-dom 8304 df-sdom 8305 df-fin 8306 df-fsupp 8625 df-fi 8666 df-sup 8697 df-inf 8698 df-oi 8765 df-card 9158 df-cda 9384 df-pnf 10472 df-mnf 10473 df-xr 10474 df-ltxr 10475 df-le 10476 df-sub 10668 df-neg 10669 df-div 11095 df-nn 11436 df-2 11500 df-3 11501 df-4 11502 df-5 11503 df-6 11504 df-7 11505 df-8 11506 df-9 11507 df-n0 11705 df-z 11791 df-dec 11909 df-uz 12056 df-q 12160 df-rp 12202 df-xneg 12321 df-xadd 12322 df-xmul 12323 df-ioo 12555 df-ioc 12556 df-ico 12557 df-icc 12558 df-fz 12706 df-fzo 12847 df-fl 12974 df-seq 13182 df-exp 13242 df-fac 13446 df-bc 13475 df-hash 13503 df-shft 14281 df-cj 14313 df-re 14314 df-im 14315 df-sqrt 14449 df-abs 14450 df-limsup 14683 df-clim 14700 df-rlim 14701 df-sum 14898 df-ef 15275 df-sin 15277 df-cos 15278 df-pi 15280 df-struct 16335 df-ndx 16336 df-slot 16337 df-base 16339 df-sets 16340 df-ress 16341 df-plusg 16428 df-mulr 16429 df-starv 16430 df-sca 16431 df-vsca 16432 df-ip 16433 df-tset 16434 df-ple 16435 df-ds 16437 df-unif 16438 df-hom 16439 df-cco 16440 df-rest 16546 df-topn 16547 df-0g 16565 df-gsum 16566 df-topgen 16567 df-pt 16568 df-prds 16571 df-xrs 16625 df-qtop 16630 df-imas 16631 df-xps 16633 df-mre 16709 df-mrc 16710 df-acs 16712 df-mgm 17704 df-sgrp 17746 df-mnd 17757 df-submnd 17798 df-mulg 18006 df-cntz 18212 df-cmn 18662 df-psmet 20233 df-xmet 20234 df-met 20235 df-bl 20236 df-mopn 20237 df-fbas 20238 df-fg 20239 df-cnfld 20242 df-top 21200 df-topon 21217 df-topsp 21239 df-bases 21252 df-cld 21325 df-ntr 21326 df-cls 21327 df-nei 21404 df-lp 21442 df-perf 21443 df-cn 21533 df-cnp 21534 df-haus 21621 df-tx 21868 df-hmeo 22061 df-fil 22152 df-fm 22244 df-flim 22245 df-flf 22246 df-xms 22627 df-ms 22628 df-tms 22629 df-cncf 23183 df-limc 24161 df-dv 24162 |
This theorem is referenced by: pirp 24744 sinhalfpilem 24746 sincos4thpi 24796 sincos6thpi 24798 pigt3 24800 sineq0 24806 coseq1 24807 efeq1 24808 cosne0 24809 recosf1o 24814 tanord1 24816 efif1olem2 24822 efif1olem4 24824 relogrn 24840 logneg 24866 eflogeq 24880 logneg2 24893 logf1o2 24928 root1eq1 25031 logbrec 25055 ang180lem1 25082 ang180lem2 25083 ang180lem3 25084 asin1 25167 basellem4 25357 itgexpif 31516 logi 32456 bj-pinftyccb 33937 bj-minftyccb 33941 bj-pinftynminfty 33943 tan2h 34303 proot1ex 39175 isosctrlem1ALT 40664 sineq0ALT 40667 negpilt0 40954 coseq0 41554 sinaover2ne0 41558 itgsin0pilem1 41644 itgsinexplem1 41648 wallispilem2 41761 wallispi 41765 stirlinglem15 41783 stirlingr 41785 dirker2re 41787 dirkerdenne0 41788 dirkerval2 41789 dirkerre 41790 dirkertrigeqlem1 41793 dirkertrigeqlem2 41794 dirkertrigeqlem3 41795 dirkertrigeq 41796 dirkeritg 41797 dirkercncflem1 41798 dirkercncflem2 41799 dirkercncflem4 41801 fourierdlem16 41818 fourierdlem21 41823 fourierdlem22 41824 fourierdlem24 41826 fourierdlem62 41863 fourierdlem66 41867 fourierdlem83 41884 fourierdlem94 41895 fourierdlem95 41896 fourierdlem102 41903 fourierdlem103 41904 fourierdlem104 41905 fourierdlem111 41912 fourierdlem112 41913 fourierdlem113 41914 fourierdlem114 41915 sqwvfoura 41923 sqwvfourb 41924 fourierswlem 41925 fouriersw 41926 |
Copyright terms: Public domain | W3C validator |