pigt3 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > pigt3		GIF version

Theorem pigt3 13405

Description: π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Assertion**
Ref	Expression
pigt3	⊢ 3 < π

**Proof of Theorem pigt3**
Step	Hyp	Ref	Expression
1		sincos6thpi 13403	. . . . 5 ⊢ ((sin‘(π / 6)) = (1 / 2) ∧ (cos‘(π / 6)) = ((√‘3) / 2))
2	1	simpli 110	. . . 4 ⊢ (sin‘(π / 6)) = (1 / 2)
3		ax-1cn 7846	. . . . 5 ⊢ 1 ∈ ℂ
4		2cn 8928	. . . . . 6 ⊢ 2 ∈ ℂ
5		2ap0 8950	. . . . . 6 ⊢ 2 # 0
6	4, 5	pm3.2i 270	. . . . 5 ⊢ (2 ∈ ℂ ∧ 2 # 0)
7		3cn 8932	. . . . . 6 ⊢ 3 ∈ ℂ
8		3ap0 8953	. . . . . 6 ⊢ 3 # 0
9	7, 8	pm3.2i 270	. . . . 5 ⊢ (3 ∈ ℂ ∧ 3 # 0)
10		divcanap5 8610	. . . . 5 ⊢ ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0) ∧ (3 ∈ ℂ ∧ 3 # 0)) → ((3 · 1) / (3 · 2)) = (1 / 2))
11	3, 6, 9, 10	mp3an 1327	. . . 4 ⊢ ((3 · 1) / (3 · 2)) = (1 / 2)
12		3t1e3 9012	. . . . 5 ⊢ (3 · 1) = 3
13		3t2e6 9013	. . . . 5 ⊢ (3 · 2) = 6
14	12, 13	oveq12i 5854	. . . 4 ⊢ ((3 · 1) / (3 · 2)) = (3 / 6)
15	2, 11, 14	3eqtr2i 2192	. . 3 ⊢ (sin‘(π / 6)) = (3 / 6)
16		pire 13347	. . . . . . 7 ⊢ π ∈ ℝ
17		6nn 9022	. . . . . . 7 ⊢ 6 ∈ ℕ
18		nndivre 8893	. . . . . . 7 ⊢ ((π ∈ ℝ ∧ 6 ∈ ℕ) → (π / 6) ∈ ℝ)
19	16, 17, 18	mp2an 423	. . . . . 6 ⊢ (π / 6) ∈ ℝ
20		6re 8938	. . . . . . 7 ⊢ 6 ∈ ℝ
21		pipos 13349	. . . . . . 7 ⊢ 0 < π
22		6pos 8958	. . . . . . 7 ⊢ 0 < 6
23	16, 20, 21, 22	divgt0ii 8814	. . . . . 6 ⊢ 0 < (π / 6)
24		1re 7898	. . . . . . 7 ⊢ 1 ∈ ℝ
25		pigt2lt4 13345	. . . . . . . . . 10 ⊢ (2 < π ∧ π < 4)
26	25	simpri 112	. . . . . . . . 9 ⊢ π < 4
27		4re 8934	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
28	16, 27, 20, 22	ltdiv1ii 8824	. . . . . . . . 9 ⊢ (π < 4 ↔ (π / 6) < (4 / 6))
29	26, 28	mpbi 144	. . . . . . . 8 ⊢ (π / 6) < (4 / 6)
30		4lt6 9037	. . . . . . . . 9 ⊢ 4 < 6
31	20, 22	elrpii 9592	. . . . . . . . . 10 ⊢ 6 ∈ ℝ⁺
32		divlt1lt 9660	. . . . . . . . . 10 ⊢ ((4 ∈ ℝ ∧ 6 ∈ ℝ⁺) → ((4 / 6) < 1 ↔ 4 < 6))
33	27, 31, 32	mp2an 423	. . . . . . . . 9 ⊢ ((4 / 6) < 1 ↔ 4 < 6)
34	30, 33	mpbir 145	. . . . . . . 8 ⊢ (4 / 6) < 1
35		nndivre 8893	. . . . . . . . . 10 ⊢ ((4 ∈ ℝ ∧ 6 ∈ ℕ) → (4 / 6) ∈ ℝ)
36	27, 17, 35	mp2an 423	. . . . . . . . 9 ⊢ (4 / 6) ∈ ℝ
37	19, 36, 24	lttri 8003	. . . . . . . 8 ⊢ (((π / 6) < (4 / 6) ∧ (4 / 6) < 1) → (π / 6) < 1)
38	29, 34, 37	mp2an 423	. . . . . . 7 ⊢ (π / 6) < 1
39	19, 24, 38	ltleii 8001	. . . . . 6 ⊢ (π / 6) ≤ 1
40		0xr 7945	. . . . . . 7 ⊢ 0 ∈ ℝ^*
41		elioc2 9872	. . . . . . 7 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ) → ((π / 6) ∈ (0(,]1) ↔ ((π / 6) ∈ ℝ ∧ 0 < (π / 6) ∧ (π / 6) ≤ 1)))
42	40, 24, 41	mp2an 423	. . . . . 6 ⊢ ((π / 6) ∈ (0(,]1) ↔ ((π / 6) ∈ ℝ ∧ 0 < (π / 6) ∧ (π / 6) ≤ 1))
43	19, 23, 39, 42	mpbir3an 1169	. . . . 5 ⊢ (π / 6) ∈ (0(,]1)
44		sin01bnd 11698	. . . . 5 ⊢ ((π / 6) ∈ (0(,]1) → (((π / 6) − (((π / 6)↑3) / 3)) < (sin‘(π / 6)) ∧ (sin‘(π / 6)) < (π / 6)))
45	43, 44	ax-mp 5	. . . 4 ⊢ (((π / 6) − (((π / 6)↑3) / 3)) < (sin‘(π / 6)) ∧ (sin‘(π / 6)) < (π / 6))
46	45	simpri 112	. . 3 ⊢ (sin‘(π / 6)) < (π / 6)
47	15, 46	eqbrtrri 4005	. 2 ⊢ (3 / 6) < (π / 6)
48		3re 8931	. . 3 ⊢ 3 ∈ ℝ
49	48, 16, 20, 22	ltdiv1ii 8824	. 2 ⊢ (3 < π ↔ (3 / 6) < (π / 6))
50	47, 49	mpbir 145	1 ⊢ 3 < π

Colors of variables: wff set class

Syntax hints: ∧ wa 103 ↔ wb 104 ∧ w3a 968 = wceq 1343 ∈ wcel 2136 class class class wbr 3982 ‘cfv 5188 (class class class)co 5842 ℂcc 7751 ℝcr 7752 0cc0 7753 1c1 7754 · cmul 7758 ℝ^*cxr 7932 < clt 7933 ≤ cle 7934 − cmin 8069 # cap 8479 / cdiv 8568 ℕcn 8857 2c2 8908 3c3 8909 4c4 8910 6c6 8912 ℝ⁺crp 9589 (,]cioc 9825 ↑cexp 10454 √csqrt 10938 sincsin 11585 cosccos 11586 πcpi 11588

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-mulrcl 7852 ax-addcom 7853 ax-mulcom 7854 ax-addass 7855 ax-mulass 7856 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-1rid 7860 ax-0id 7861 ax-rnegex 7862 ax-precex 7863 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-apti 7868 ax-pre-ltadd 7869 ax-pre-mulgt0 7870 ax-pre-mulext 7871 ax-arch 7872 ax-caucvg 7873 ax-pre-suploc 7874 ax-addf 7875 ax-mulf 7876

This theorem depends on definitions: df-bi 116 df-stab 821 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rmo 2452 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-disj 3960 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-po 4274 df-iso 4275 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-isom 5197 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-of 6050 df-1st 6108 df-2nd 6109 df-recs 6273 df-irdg 6338 df-frec 6359 df-1o 6384 df-oadd 6388 df-er 6501 df-map 6616 df-pm 6617 df-en 6707 df-dom 6708 df-fin 6709 df-sup 6949 df-inf 6950 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-reap 8473 df-ap 8480 df-div 8569 df-inn 8858 df-2 8916 df-3 8917 df-4 8918 df-5 8919 df-6 8920 df-7 8921 df-8 8922 df-9 8923 df-n0 9115 df-z 9192 df-uz 9467 df-q 9558 df-rp 9590 df-xneg 9708 df-xadd 9709 df-ioo 9828 df-ioc 9829 df-ico 9830 df-icc 9831 df-fz 9945 df-fzo 10078 df-seqfrec 10381 df-exp 10455 df-fac 10639 df-bc 10661 df-ihash 10689 df-shft 10757 df-cj 10784 df-re 10785 df-im 10786 df-rsqrt 10940 df-abs 10941 df-clim 11220 df-sumdc 11295 df-ef 11589 df-sin 11591 df-cos 11592 df-pi 11594 df-rest 12558 df-topgen 12577 df-psmet 12627 df-xmet 12628 df-met 12629 df-bl 12630 df-mopn 12631 df-top 12636 df-topon 12649 df-bases 12681 df-ntr 12736 df-cn 12828 df-cnp 12829 df-tx 12893 df-cncf 13198 df-limced 13265 df-dvap 13266

This theorem is referenced by: pige3 13406

W3C validator