pige3ALT

Description: Alternate proof of pige3 . This proof is based on the geometric observation that a hexagon of unit side length has perimeter 6, which is less than the unit-radius circumcircle, of perimeter 2pi . We translate this to algebra by looking at the function e ^ (i x ) as x goes from 0 to pi / 3 ; it moves at unit speed and travels distance 1 , hence 1 <_ _pi / 3 . (Contributed by Mario Carneiro, 21-May-2016) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	pige3ALT	$⊢ 3 \leq π$

Proof

Step	Hyp	Ref	Expression
1		3cn	$⊢ 3 \in ℂ$
2	1	mullidi	$⊢ 1 \cdot 3 = 3$
3		tru	$⊢ ⊤$
4		0xr	$⊢ 0 \in ℝ^{*}$
5		pirp	$⊢ π \in ℝ^{+}$
6		3rp	$⊢ 3 \in ℝ^{+}$
7		rpdivcl	$⊢ (π \in ℝ^{+} \land 3 \in ℝ^{+}) \to \frac{π}{3} \in ℝ^{+}$
8	5 6 7	mp2an	$⊢ \frac{π}{3} \in ℝ^{+}$
9		rpxr	$⊢ \frac{π}{3} \in ℝ^{+} \to \frac{π}{3} \in ℝ^{*}$
10	8 9	ax-mp	$⊢ \frac{π}{3} \in ℝ^{*}$
11		rpge0	$⊢ \frac{π}{3} \in ℝ^{+} \to 0 \leq \frac{π}{3}$
12	8 11	ax-mp	$⊢ 0 \leq \frac{π}{3}$
13		lbicc2	$⊢ (0 \in ℝ^{} \land \frac{π}{3} \in ℝ^{} \land 0 \leq \frac{π}{3}) \to 0 \in [0, \frac{π}{3}]$
14	4 10 12 13	mp3an	$⊢ 0 \in [0, \frac{π}{3}]$
15		ubicc2	$⊢ (0 \in ℝ^{} \land \frac{π}{3} \in ℝ^{} \land 0 \leq \frac{π}{3}) \to \frac{π}{3} \in [0, \frac{π}{3}]$
16	4 10 12 15	mp3an	$⊢ \frac{π}{3} \in [0, \frac{π}{3}]$
17	14 16	pm3.2i	$⊢ (0 \in [0, \frac{π}{3}] \land \frac{π}{3} \in [0, \frac{π}{3}])$
18		0re	$⊢ 0 \in ℝ$
19	18	a1i	$⊢ ⊤ \to 0 \in ℝ$
20		pire	$⊢ π \in ℝ$
21		3re	$⊢ 3 \in ℝ$
22		3ne0	$⊢ 3 \neq 0$
23	20 21 22	redivcli	$⊢ \frac{π}{3} \in ℝ$
24	23	a1i	$⊢ ⊤ \to \frac{π}{3} \in ℝ$
25		efcn	$⊢ \exp : ℂ \underset{cn}{⟶} ℂ$
26	25	a1i	$⊢ ⊤ \to \exp : ℂ \underset{cn}{⟶} ℂ$
27		iccssre	$⊢ (0 \in ℝ \land \frac{π}{3} \in ℝ) \to [0, \frac{π}{3}] \subseteq ℝ$
28	18 23 27	mp2an	$⊢ [0, \frac{π}{3}] \subseteq ℝ$
29		ax-resscn	$⊢ ℝ \subseteq ℂ$
30	28 29	sstri	$⊢ [0, \frac{π}{3}] \subseteq ℂ$
31		resmpt	$⊢ [0, \frac{π}{3}] \subseteq ℂ \to {(x \in ℂ ⟼ i x) ↾}_{[0, \frac{π}{3}]} = (x \in [0, \frac{π}{3}] ⟼ i x)$
32	30 31	mp1i	$⊢ ⊤ \to {(x \in ℂ ⟼ i x) ↾}_{[0, \frac{π}{3}]} = (x \in [0, \frac{π}{3}] ⟼ i x)$
33		ssidd	$⊢ ⊤ \to ℂ \subseteq ℂ$
34		ax-icn	$⊢ i \in ℂ$
35		simpr	$⊢ (⊤ \land x \in ℂ) \to x \in ℂ$
36		mulcl	$⊢ (i \in ℂ \land x \in ℂ) \to i x \in ℂ$
37	34 35 36	sylancr	$⊢ (⊤ \land x \in ℂ) \to i x \in ℂ$
38	37	fmpttd	$⊢ ⊤ \to (x \in ℂ ⟼ i x) : ℂ ⟶ ℂ$
39		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
40	39	a1i	$⊢ ⊤ \to ℂ \in \{ℝ, ℂ\}$
41		ax-1cn	$⊢ 1 \in ℂ$
42	41	a1i	$⊢ (⊤ \land x \in ℂ) \to 1 \in ℂ$
43	40	dvmptid	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ x)}{d_{ℂ} x} = (x \in ℂ ⟼ 1)$
44	34	a1i	$⊢ ⊤ \to i \in ℂ$
45	40 35 42 43 44	dvmptcmul	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ i x)}{d_{ℂ} x} = (x \in ℂ ⟼ i \cdot 1)$
46	34	mulridi	$⊢ i \cdot 1 = i$
47	46	mpteq2i	$⊢ (x \in ℂ ⟼ i \cdot 1) = (x \in ℂ ⟼ i)$
48	45 47	eqtrdi	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ i x)}{d_{ℂ} x} = (x \in ℂ ⟼ i)$
49	48	dmeqd	$⊢ ⊤ \to dom \frac{d (x \in ℂ⟼ i x)}{d_{ℂ} x} = dom (x \in ℂ ⟼ i)$
50	34	elexi	$⊢ i \in V$
51		eqid	$⊢ (x \in ℂ ⟼ i) = (x \in ℂ ⟼ i)$
52	50 51	dmmpti	$⊢ dom (x \in ℂ ⟼ i) = ℂ$
53	49 52	eqtrdi	$⊢ ⊤ \to dom \frac{d (x \in ℂ⟼ i x)}{d_{ℂ} x} = ℂ$
54		dvcn	$⊢ ((ℂ \subseteq ℂ \land (x \in ℂ ⟼ i x) : ℂ ⟶ ℂ \land ℂ \subseteq ℂ) \land dom \frac{d (x \in ℂ⟼ i x)}{d_{ℂ} x} = ℂ) \to (x \in ℂ ⟼ i x) : ℂ \underset{cn}{⟶} ℂ$
55	33 38 33 53 54	syl31anc	$⊢ ⊤ \to (x \in ℂ ⟼ i x) : ℂ \underset{cn}{⟶} ℂ$
56		rescncf	$⊢ [0, \frac{π}{3}] \subseteq ℂ \to ((x \in ℂ ⟼ i x) : ℂ \underset{cn}{⟶} ℂ \to ({(x \in ℂ ⟼ i x) ↾}_{[0, \frac{π}{3}]}) : [0, \frac{π}{3}] \underset{cn}{⟶} ℂ)$
57	30 55 56	mpsyl	$⊢ ⊤ \to ({(x \in ℂ ⟼ i x) ↾}_{[0, \frac{π}{3}]}) : [0, \frac{π}{3}] \underset{cn}{⟶} ℂ$
58	32 57	eqeltrrd	$⊢ ⊤ \to (x \in [0, \frac{π}{3}] ⟼ i x) : [0, \frac{π}{3}] \underset{cn}{⟶} ℂ$
59	26 58	cncfmpt1f	$⊢ ⊤ \to (x \in [0, \frac{π}{3}] ⟼ e^{i x}) : [0, \frac{π}{3}] \underset{cn}{⟶} ℂ$
60		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
61	60	a1i	$⊢ ⊤ \to ℝ \in \{ℝ, ℂ\}$
62		recn	$⊢ x \in ℝ \to x \in ℂ$
63		efcl	$⊢ i x \in ℂ \to e^{i x} \in ℂ$
64	37 63	syl	$⊢ (⊤ \land x \in ℂ) \to e^{i x} \in ℂ$
65	62 64	sylan2	$⊢ (⊤ \land x \in ℝ) \to e^{i x} \in ℂ$
66		mulcl	$⊢ (e^{i x} \in ℂ \land i \in ℂ) \to e^{i x} i \in ℂ$
67	64 34 66	sylancl	$⊢ (⊤ \land x \in ℂ) \to e^{i x} i \in ℂ$
68	62 67	sylan2	$⊢ (⊤ \land x \in ℝ) \to e^{i x} i \in ℂ$
69		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
70	69	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
71		toponmax	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ) \to ℂ \in TopOpen (ℂ_{fld})$
72	70 71	mp1i	$⊢ ⊤ \to ℂ \in TopOpen (ℂ_{fld})$
73	29	a1i	$⊢ ⊤ \to ℝ \subseteq ℂ$
74		dfss2	$⊢ ℝ \subseteq ℂ \leftrightarrow ℝ \cap ℂ = ℝ$
75	73 74	sylib	$⊢ ⊤ \to ℝ \cap ℂ = ℝ$
76	34	a1i	$⊢ (⊤ \land x \in ℂ) \to i \in ℂ$
77		efcl	$⊢ y \in ℂ \to e^{y} \in ℂ$
78	77	adantl	$⊢ (⊤ \land y \in ℂ) \to e^{y} \in ℂ$
79		dvef	$⊢ ℂ D \exp = \exp$
80		eff	$⊢ \exp : ℂ ⟶ ℂ$
81	80	a1i	$⊢ ⊤ \to \exp : ℂ ⟶ ℂ$
82	81	feqmptd	$⊢ ⊤ \to \exp = (y \in ℂ ⟼ e^{y})$
83	82	oveq2d	$⊢ ⊤ \to ℂ D \exp = \frac{d (y \in ℂ⟼ e^{y})}{d_{ℂ} y}$
84	79 83 82	3eqtr3a	$⊢ ⊤ \to \frac{d (y \in ℂ⟼ e^{y})}{d_{ℂ} y} = (y \in ℂ ⟼ e^{y})$
85		fveq2	$⊢ y = i x \to e^{y} = e^{i x}$
86	40 40 37 76 78 78 48 84 85 85	dvmptco	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ e^{i x})}{d_{ℂ} x} = (x \in ℂ ⟼ e^{i x} i)$
87	69 61 72 75 64 67 86	dvmptres3	$⊢ ⊤ \to \frac{d (x \in ℝ⟼ e^{i x})}{d_{ℝ} x} = (x \in ℝ ⟼ e^{i x} i)$
88	28	a1i	$⊢ ⊤ \to [0, \frac{π}{3}] \subseteq ℝ$
89	69	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
90		iccntr	$⊢ (0 \in ℝ \land \frac{π}{3} \in ℝ) \to int (topGen (ran (.))) ([0, \frac{π}{3}]) = (0, \frac{π}{3})$
91	18 24 90	sylancr	$⊢ ⊤ \to int (topGen (ran (.))) ([0, \frac{π}{3}]) = (0, \frac{π}{3})$
92	61 65 68 87 88 89 69 91	dvmptres2	$⊢ ⊤ \to \frac{d (x \in [0, \frac{π}{3}]⟼ e^{i x})}{d_{ℝ} x} = (x \in (0, \frac{π}{3}) ⟼ e^{i x} i)$
93	92	dmeqd	$⊢ ⊤ \to dom \frac{d (x \in [0, \frac{π}{3}]⟼ e^{i x})}{d_{ℝ} x} = dom (x \in (0, \frac{π}{3}) ⟼ e^{i x} i)$
94		ovex	$⊢ e^{i x} i \in V$
95		eqid	$⊢ (x \in (0, \frac{π}{3}) ⟼ e^{i x} i) = (x \in (0, \frac{π}{3}) ⟼ e^{i x} i)$
96	94 95	dmmpti	$⊢ dom (x \in (0, \frac{π}{3}) ⟼ e^{i x} i) = (0, \frac{π}{3})$
97	93 96	eqtrdi	$⊢ ⊤ \to dom \frac{d (x \in [0, \frac{π}{3}]⟼ e^{i x})}{d_{ℝ} x} = (0, \frac{π}{3})$
98		1re	$⊢ 1 \in ℝ$
99	98	a1i	$⊢ ⊤ \to 1 \in ℝ$
100	92	fveq1d	$⊢ ⊤ \to \frac{d (x \in [0, \frac{π}{3}]⟼ e^{i x})}{d_{ℝ} x} (y) = (x \in (0, \frac{π}{3}) ⟼ e^{i x} i) (y)$
101		oveq2	$⊢ x = y \to i x = i y$
102	101	fveq2d	$⊢ x = y \to e^{i x} = e^{i y}$
103	102	oveq1d	$⊢ x = y \to e^{i x} i = e^{i y} i$
104	103 95 94	fvmpt3i	$⊢ y \in (0, \frac{π}{3}) \to (x \in (0, \frac{π}{3}) ⟼ e^{i x} i) (y) = e^{i y} i$
105	100 104	sylan9eq	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to \frac{d (x \in [0, \frac{π}{3}]⟼ e^{i x})}{d_{ℝ} x} (y) = e^{i y} i$
106	105	fveq2d	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to \|\frac{d (x \in [0, \frac{π}{3}]⟼ e^{i x})}{d_{ℝ} x} (y)\| = \|e^{i y} i\|$
107		ioossre	$⊢ (0, \frac{π}{3}) \subseteq ℝ$
108	107	a1i	$⊢ ⊤ \to (0, \frac{π}{3}) \subseteq ℝ$
109	108	sselda	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to y \in ℝ$
110	109	recnd	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to y \in ℂ$
111		mulcl	$⊢ (i \in ℂ \land y \in ℂ) \to i y \in ℂ$
112	34 110 111	sylancr	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to i y \in ℂ$
113		efcl	$⊢ i y \in ℂ \to e^{i y} \in ℂ$
114	112 113	syl	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to e^{i y} \in ℂ$
115		absmul	$⊢ (e^{i y} \in ℂ \land i \in ℂ) \to \|e^{i y} i\| = \|e^{i y}\| \|i\|$
116	114 34 115	sylancl	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to \|e^{i y} i\| = \|e^{i y}\| \|i\|$
117		absefi	$⊢ y \in ℝ \to \|e^{i y}\| = 1$
118	109 117	syl	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to \|e^{i y}\| = 1$
119		absi	$⊢ \|i\| = 1$
120	119	a1i	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to \|i\| = 1$
121	118 120	oveq12d	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to \|e^{i y}\| \|i\| = 1 \cdot 1$
122	41	mulridi	$⊢ 1 \cdot 1 = 1$
123	121 122	eqtrdi	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to \|e^{i y}\| \|i\| = 1$
124	106 116 123	3eqtrd	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to \|\frac{d (x \in [0, \frac{π}{3}]⟼ e^{i x})}{d_{ℝ} x} (y)\| = 1$
125		1le1	$⊢ 1 \leq 1$
126	124 125	eqbrtrdi	$⊢ (⊤ \land y \in (0, \frac{π}{3})) \to \|\frac{d (x \in [0, \frac{π}{3}]⟼ e^{i x})}{d_{ℝ} x} (y)\| \leq 1$
127	19 24 59 97 99 126	dvlip	$⊢ (⊤ \land (0 \in [0, \frac{π}{3}] \land \frac{π}{3} \in [0, \frac{π}{3}])) \to \|(x \in [0, \frac{π}{3}] ⟼ e^{i x}) (0) - (x \in [0, \frac{π}{3}] ⟼ e^{i x}) (\frac{π}{3})\| \leq 1 \|0 - (\frac{π}{3})\|$
128	3 17 127	mp2an	$⊢ \|(x \in [0, \frac{π}{3}] ⟼ e^{i x}) (0) - (x \in [0, \frac{π}{3}] ⟼ e^{i x}) (\frac{π}{3})\| \leq 1 \|0 - (\frac{π}{3})\|$
129		oveq2	$⊢ x = 0 \to i x = i \cdot 0$
130		it0e0	$⊢ i \cdot 0 = 0$
131	129 130	eqtrdi	$⊢ x = 0 \to i x = 0$
132	131	fveq2d	$⊢ x = 0 \to e^{i x} = e^{0}$
133		ef0	$⊢ e^{0} = 1$
134	132 133	eqtrdi	$⊢ x = 0 \to e^{i x} = 1$
135		eqid	$⊢ (x \in [0, \frac{π}{3}] ⟼ e^{i x}) = (x \in [0, \frac{π}{3}] ⟼ e^{i x})$
136		fvex	$⊢ e^{i x} \in V$
137	134 135 136	fvmpt3i	$⊢ 0 \in [0, \frac{π}{3}] \to (x \in [0, \frac{π}{3}] ⟼ e^{i x}) (0) = 1$
138	14 137	ax-mp	$⊢ (x \in [0, \frac{π}{3}] ⟼ e^{i x}) (0) = 1$
139		oveq2	$⊢ x = \frac{π}{3} \to i x = i (\frac{π}{3})$
140	139	fveq2d	$⊢ x = \frac{π}{3} \to e^{i x} = e^{i (\frac{π}{3})}$
141	140 135 136	fvmpt3i	$⊢ \frac{π}{3} \in [0, \frac{π}{3}] \to (x \in [0, \frac{π}{3}] ⟼ e^{i x}) (\frac{π}{3}) = e^{i (\frac{π}{3})}$
142	16 141	ax-mp	$⊢ (x \in [0, \frac{π}{3}] ⟼ e^{i x}) (\frac{π}{3}) = e^{i (\frac{π}{3})}$
143	138 142	oveq12i	$⊢ (x \in [0, \frac{π}{3}] ⟼ e^{i x}) (0) - (x \in [0, \frac{π}{3}] ⟼ e^{i x}) (\frac{π}{3}) = 1 - e^{i (\frac{π}{3})}$
144	23	recni	$⊢ \frac{π}{3} \in ℂ$
145	34 144	mulcli	$⊢ i (\frac{π}{3}) \in ℂ$
146		efcl	$⊢ i (\frac{π}{3}) \in ℂ \to e^{i (\frac{π}{3})} \in ℂ$
147	145 146	ax-mp	$⊢ e^{i (\frac{π}{3})} \in ℂ$
148		negicn	$⊢ - i \in ℂ$
149	148 144	mulcli	$⊢ (- i) (\frac{π}{3}) \in ℂ$
150		efcl	$⊢ (- i) (\frac{π}{3}) \in ℂ \to e^{(- i) (\frac{π}{3})} \in ℂ$
151	149 150	ax-mp	$⊢ e^{(- i) (\frac{π}{3})} \in ℂ$
152		cosval	$⊢ \frac{π}{3} \in ℂ \to \cos (\frac{π}{3}) = \frac{e^{i (\frac{π}{3})} + e^{(- i) (\frac{π}{3})}}{2}$
153	144 152	ax-mp	$⊢ \cos (\frac{π}{3}) = \frac{e^{i (\frac{π}{3})} + e^{(- i) (\frac{π}{3})}}{2}$
154		sincos3rdpi	$⊢ (\sin (\frac{π}{3}) = \frac{\sqrt{3}}{2} \land \cos (\frac{π}{3}) = \frac{1}{2})$
155	154	simpri	$⊢ \cos (\frac{π}{3}) = \frac{1}{2}$
156	153 155	eqtr3i	$⊢ \frac{e^{i (\frac{π}{3})} + e^{(- i) (\frac{π}{3})}}{2} = \frac{1}{2}$
157	147 151	addcli	$⊢ e^{i (\frac{π}{3})} + e^{(- i) (\frac{π}{3})} \in ℂ$
158		2cn	$⊢ 2 \in ℂ$
159		2ne0	$⊢ 2 \neq 0$
160	157 41 158 159	div11i	$⊢ \frac{e^{i (\frac{π}{3})} + e^{(- i) (\frac{π}{3})}}{2} = \frac{1}{2} \leftrightarrow e^{i (\frac{π}{3})} + e^{(- i) (\frac{π}{3})} = 1$
161	156 160	mpbi	$⊢ e^{i (\frac{π}{3})} + e^{(- i) (\frac{π}{3})} = 1$
162	41 147 151 161	subaddrii	$⊢ 1 - e^{i (\frac{π}{3})} = e^{(- i) (\frac{π}{3})}$
163		mulneg12	$⊢ (i \in ℂ \land \frac{π}{3} \in ℂ) \to (- i) (\frac{π}{3}) = i (- \frac{π}{3})$
164	34 144 163	mp2an	$⊢ (- i) (\frac{π}{3}) = i (- \frac{π}{3})$
165	164	fveq2i	$⊢ e^{(- i) (\frac{π}{3})} = e^{i (- \frac{π}{3})}$
166	143 162 165	3eqtri	$⊢ (x \in [0, \frac{π}{3}] ⟼ e^{i x}) (0) - (x \in [0, \frac{π}{3}] ⟼ e^{i x}) (\frac{π}{3}) = e^{i (- \frac{π}{3})}$
167	166	fveq2i	$⊢ \|(x \in [0, \frac{π}{3}] ⟼ e^{i x}) (0) - (x \in [0, \frac{π}{3}] ⟼ e^{i x}) (\frac{π}{3})\| = \|e^{i (- \frac{π}{3})}\|$
168	144	absnegi	$⊢ \|- \frac{π}{3}\| = \|\frac{π}{3}\|$
169		df-neg	$⊢ - \frac{π}{3} = 0 - (\frac{π}{3})$
170	169	fveq2i	$⊢ \|- \frac{π}{3}\| = \|0 - (\frac{π}{3})\|$
171	168 170	eqtr3i	$⊢ \|\frac{π}{3}\| = \|0 - (\frac{π}{3})\|$
172		rprege0	$⊢ \frac{π}{3} \in ℝ^{+} \to (\frac{π}{3} \in ℝ \land 0 \leq \frac{π}{3})$
173		absid	$⊢ (\frac{π}{3} \in ℝ \land 0 \leq \frac{π}{3}) \to \|\frac{π}{3}\| = \frac{π}{3}$
174	8 172 173	mp2b	$⊢ \|\frac{π}{3}\| = \frac{π}{3}$
175	171 174	eqtr3i	$⊢ \|0 - (\frac{π}{3})\| = \frac{π}{3}$
176	175	oveq2i	$⊢ 1 \|0 - (\frac{π}{3})\| = 1 (\frac{π}{3})$
177	128 167 176	3brtr3i	$⊢ \|e^{i (- \frac{π}{3})}\| \leq 1 (\frac{π}{3})$
178	23	renegcli	$⊢ - \frac{π}{3} \in ℝ$
179		absefi	$⊢ - \frac{π}{3} \in ℝ \to \|e^{i (- \frac{π}{3})}\| = 1$
180	178 179	ax-mp	$⊢ \|e^{i (- \frac{π}{3})}\| = 1$
181	144	mullidi	$⊢ 1 (\frac{π}{3}) = \frac{π}{3}$
182	177 180 181	3brtr3i	$⊢ 1 \leq \frac{π}{3}$
183		3pos	$⊢ 0 < 3$
184	21 183	pm3.2i	$⊢ (3 \in ℝ \land 0 < 3)$
185		lemuldiv	$⊢ (1 \in ℝ \land π \in ℝ \land (3 \in ℝ \land 0 < 3)) \to (1 \cdot 3 \leq π \leftrightarrow 1 \leq \frac{π}{3})$
186	98 20 184 185	mp3an	$⊢ 1 \cdot 3 \leq π \leftrightarrow 1 \leq \frac{π}{3}$
187	182 186	mpbir	$⊢ 1 \cdot 3 \leq π$
188	2 187	eqbrtrri	$⊢ 3 \leq π$

Metamath Proof Explorer

Theorem pige3ALT

Proof