Theorem pipos 24743

Description: π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)

Assertion

Ref	Expression
pipos	⊢ 0 < π

Proof of Theorem pipos

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 < π

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