pigt3 - Intuitionistic Logic Explorer

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

Theorem pigt3 13644

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 13642	. . . . 5 ⊢ ((sin‘(π / 6)) = (1 / 2) ∧ (cos‘(π / 6)) = ((√‘3) / 2))
2	1	simpli 110	. . . 4 ⊢ (sin‘(π / 6)) = (1 / 2)
3		ax-1cn 7871	. . . . 5 ⊢ 1 ∈ ℂ
4		2cn 8953	. . . . . 6 ⊢ 2 ∈ ℂ
5		2ap0 8975	. . . . . 6 ⊢ 2 # 0
6	4, 5	pm3.2i 270	. . . . 5 ⊢ (2 ∈ ℂ ∧ 2 # 0)
7		3cn 8957	. . . . . 6 ⊢ 3 ∈ ℂ
8		3ap0 8978	. . . . . 6 ⊢ 3 # 0
9	7, 8	pm3.2i 270	. . . . 5 ⊢ (3 ∈ ℂ ∧ 3 # 0)
10		divcanap5 8635	. . . . 5 ⊢ ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0) ∧ (3 ∈ ℂ ∧ 3 # 0)) → ((3 · 1) / (3 · 2)) = (1 / 2))
11	3, 6, 9, 10	mp3an 1333	. . . 4 ⊢ ((3 · 1) / (3 · 2)) = (1 / 2)
12		3t1e3 9037	. . . . 5 ⊢ (3 · 1) = 3
13		3t2e6 9038	. . . . 5 ⊢ (3 · 2) = 6
14	12, 13	oveq12i 5869	. . . 4 ⊢ ((3 · 1) / (3 · 2)) = (3 / 6)
15	2, 11, 14	3eqtr2i 2198	. . 3 ⊢ (sin‘(π / 6)) = (3 / 6)
16		pire 13586	. . . . . . 7 ⊢ π ∈ ℝ
17		6nn 9047	. . . . . . 7 ⊢ 6 ∈ ℕ
18		nndivre 8918	. . . . . . 7 ⊢ ((π ∈ ℝ ∧ 6 ∈ ℕ) → (π / 6) ∈ ℝ)
19	16, 17, 18	mp2an 424	. . . . . 6 ⊢ (π / 6) ∈ ℝ
20		6re 8963	. . . . . . 7 ⊢ 6 ∈ ℝ
21		pipos 13588	. . . . . . 7 ⊢ 0 < π
22		6pos 8983	. . . . . . 7 ⊢ 0 < 6
23	16, 20, 21, 22	divgt0ii 8839	. . . . . 6 ⊢ 0 < (π / 6)
24		1re 7923	. . . . . . 7 ⊢ 1 ∈ ℝ
25		pigt2lt4 13584	. . . . . . . . . 10 ⊢ (2 < π ∧ π < 4)
26	25	simpri 112	. . . . . . . . 9 ⊢ π < 4
27		4re 8959	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
28	16, 27, 20, 22	ltdiv1ii 8849	. . . . . . . . 9 ⊢ (π < 4 ↔ (π / 6) < (4 / 6))
29	26, 28	mpbi 144	. . . . . . . 8 ⊢ (π / 6) < (4 / 6)
30		4lt6 9062	. . . . . . . . 9 ⊢ 4 < 6
31	20, 22	elrpii 9617	. . . . . . . . . 10 ⊢ 6 ∈ ℝ⁺
32		divlt1lt 9685	. . . . . . . . . 10 ⊢ ((4 ∈ ℝ ∧ 6 ∈ ℝ⁺) → ((4 / 6) < 1 ↔ 4 < 6))
33	27, 31, 32	mp2an 424	. . . . . . . . 9 ⊢ ((4 / 6) < 1 ↔ 4 < 6)
34	30, 33	mpbir 145	. . . . . . . 8 ⊢ (4 / 6) < 1
35		nndivre 8918	. . . . . . . . . 10 ⊢ ((4 ∈ ℝ ∧ 6 ∈ ℕ) → (4 / 6) ∈ ℝ)
36	27, 17, 35	mp2an 424	. . . . . . . . 9 ⊢ (4 / 6) ∈ ℝ
37	19, 36, 24	lttri 8028	. . . . . . . 8 ⊢ (((π / 6) < (4 / 6) ∧ (4 / 6) < 1) → (π / 6) < 1)
38	29, 34, 37	mp2an 424	. . . . . . 7 ⊢ (π / 6) < 1
39	19, 24, 38	ltleii 8026	. . . . . 6 ⊢ (π / 6) ≤ 1
40		0xr 7970	. . . . . . 7 ⊢ 0 ∈ ℝ^*
41		elioc2 9897	. . . . . . 7 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ) → ((π / 6) ∈ (0(,]1) ↔ ((π / 6) ∈ ℝ ∧ 0 < (π / 6) ∧ (π / 6) ≤ 1)))
42	40, 24, 41	mp2an 424	. . . . . 6 ⊢ ((π / 6) ∈ (0(,]1) ↔ ((π / 6) ∈ ℝ ∧ 0 < (π / 6) ∧ (π / 6) ≤ 1))
43	19, 23, 39, 42	mpbir3an 1175	. . . . 5 ⊢ (π / 6) ∈ (0(,]1)
44		sin01bnd 11724	. . . . 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 4013	. 2 ⊢ (3 / 6) < (π / 6)
48		3re 8956	. . 3 ⊢ 3 ∈ ℝ
49	48, 16, 20, 22	ltdiv1ii 8849	. 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 974 = wceq 1349 ∈ wcel 2142 class class class wbr 3990 ‘cfv 5200 (class class class)co 5857 ℂcc 7776 ℝcr 7777 0cc0 7778 1c1 7779 · cmul 7783 ℝ^*cxr 7957 < clt 7958 ≤ cle 7959 − cmin 8094 # cap 8504 / cdiv 8593 ℕcn 8882 2c2 8933 3c3 8934 4c4 8935 6c6 8937 ℝ⁺crp 9614 (,]cioc 9850 ↑cexp 10479 √csqrt 10964 sincsin 11611 cosccos 11612 πcpi 11614

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 610 ax-in2 611 ax-io 705 ax-5 1441 ax-7 1442 ax-gen 1443 ax-ie1 1487 ax-ie2 1488 ax-8 1498 ax-10 1499 ax-11 1500 ax-i12 1501 ax-bndl 1503 ax-4 1504 ax-17 1520 ax-i9 1524 ax-ial 1528 ax-i5r 1529 ax-13 2144 ax-14 2145 ax-ext 2153 ax-coll 4105 ax-sep 4108 ax-nul 4116 ax-pow 4161 ax-pr 4195 ax-un 4419 ax-setind 4522 ax-iinf 4573 ax-cnex 7869 ax-resscn 7870 ax-1cn 7871 ax-1re 7872 ax-icn 7873 ax-addcl 7874 ax-addrcl 7875 ax-mulcl 7876 ax-mulrcl 7877 ax-addcom 7878 ax-mulcom 7879 ax-addass 7880 ax-mulass 7881 ax-distr 7882 ax-i2m1 7883 ax-0lt1 7884 ax-1rid 7885 ax-0id 7886 ax-rnegex 7887 ax-precex 7888 ax-cnre 7889 ax-pre-ltirr 7890 ax-pre-ltwlin 7891 ax-pre-lttrn 7892 ax-pre-apti 7893 ax-pre-ltadd 7894 ax-pre-mulgt0 7895 ax-pre-mulext 7896 ax-arch 7897 ax-caucvg 7898 ax-pre-suploc 7899 ax-addf 7900 ax-mulf 7901

This theorem depends on definitions: df-bi 116 df-stab 827 df-dc 831 df-3or 975 df-3an 976 df-tru 1352 df-fal 1355 df-nf 1455 df-sb 1757 df-eu 2023 df-mo 2024 df-clab 2158 df-cleq 2164 df-clel 2167 df-nfc 2302 df-ne 2342 df-nel 2437 df-ral 2454 df-rex 2455 df-reu 2456 df-rmo 2457 df-rab 2458 df-v 2733 df-sbc 2957 df-csb 3051 df-dif 3124 df-un 3126 df-in 3128 df-ss 3135 df-nul 3416 df-if 3528 df-pw 3569 df-sn 3590 df-pr 3591 df-op 3593 df-uni 3798 df-int 3833 df-iun 3876 df-disj 3968 df-br 3991 df-opab 4052 df-mpt 4053 df-tr 4089 df-id 4279 df-po 4282 df-iso 4283 df-iord 4352 df-on 4354 df-ilim 4355 df-suc 4357 df-iom 4576 df-xp 4618 df-rel 4619 df-cnv 4620 df-co 4621 df-dm 4622 df-rn 4623 df-res 4624 df-ima 4625 df-iota 5162 df-fun 5202 df-fn 5203 df-f 5204 df-f1 5205 df-fo 5206 df-f1o 5207 df-fv 5208 df-isom 5209 df-riota 5813 df-ov 5860 df-oprab 5861 df-mpo 5862 df-of 6065 df-1st 6123 df-2nd 6124 df-recs 6288 df-irdg 6353 df-frec 6374 df-1o 6399 df-oadd 6403 df-er 6517 df-map 6632 df-pm 6633 df-en 6723 df-dom 6724 df-fin 6725 df-sup 6965 df-inf 6966 df-pnf 7960 df-mnf 7961 df-xr 7962 df-ltxr 7963 df-le 7964 df-sub 8096 df-neg 8097 df-reap 8498 df-ap 8505 df-div 8594 df-inn 8883 df-2 8941 df-3 8942 df-4 8943 df-5 8944 df-6 8945 df-7 8946 df-8 8947 df-9 8948 df-n0 9140 df-z 9217 df-uz 9492 df-q 9583 df-rp 9615 df-xneg 9733 df-xadd 9734 df-ioo 9853 df-ioc 9854 df-ico 9855 df-icc 9856 df-fz 9970 df-fzo 10103 df-seqfrec 10406 df-exp 10480 df-fac 10664 df-bc 10686 df-ihash 10714 df-shft 10783 df-cj 10810 df-re 10811 df-im 10812 df-rsqrt 10966 df-abs 10967 df-clim 11246 df-sumdc 11321 df-ef 11615 df-sin 11617 df-cos 11618 df-pi 11620 df-rest 12585 df-topgen 12604 df-psmet 12866 df-xmet 12867 df-met 12868 df-bl 12869 df-mopn 12870 df-top 12875 df-topon 12888 df-bases 12920 df-ntr 12975 df-cn 13067 df-cnp 13068 df-tx 13132 df-cncf 13437 df-limced 13504 df-dvap 13505

This theorem is referenced by: pige3 13645

W3C validator