pigt3

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

		Ref	Expression
	Assertion	pigt3	$⊢ 3 < π$

Step	Hyp	Ref	Expression
1		sincos6thpi	$⊢ (\sin (\frac{π}{6}) = \frac{1}{2} \land \cos (\frac{π}{6}) = \frac{\sqrt{3}}{2})$
2	1	simpli	$⊢ \sin (\frac{π}{6}) = \frac{1}{2}$
3		ax-1cn	$⊢ 1 \in ℂ$
4		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
5		3cn	$⊢ 3 \in ℂ$
6		3ne0	$⊢ 3 \neq 0$
7	5 6	pm3.2i	$⊢ (3 \in ℂ \land 3 \neq 0)$
8		divcan5	$⊢ (1 \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land (3 \in ℂ \land 3 \neq 0)) \to \frac{3 \cdot 1}{3 \cdot 2} = \frac{1}{2}$
9	3 4 7 8	mp3an	$⊢ \frac{3 \cdot 1}{3 \cdot 2} = \frac{1}{2}$
10		3t1e3	$⊢ 3 \cdot 1 = 3$
11		3t2e6	$⊢ 3 \cdot 2 = 6$
12	10 11	oveq12i	$⊢ \frac{3 \cdot 1}{3 \cdot 2} = \frac{3}{6}$
13	2 9 12	3eqtr2i	$⊢ \sin (\frac{π}{6}) = \frac{3}{6}$
14		pire	$⊢ π \in ℝ$
15		pipos	$⊢ 0 < π$
16	14 15	elrpii	$⊢ π \in ℝ^{+}$
17		6re	$⊢ 6 \in ℝ$
18		6pos	$⊢ 0 < 6$
19	17 18	elrpii	$⊢ 6 \in ℝ^{+}$
20		rpdivcl	$⊢ (π \in ℝ^{+} \land 6 \in ℝ^{+}) \to \frac{π}{6} \in ℝ^{+}$
21	16 19 20	mp2an	$⊢ \frac{π}{6} \in ℝ^{+}$
22		sinltx	$⊢ \frac{π}{6} \in ℝ^{+} \to \sin (\frac{π}{6}) < \frac{π}{6}$
23	21 22	ax-mp	$⊢ \sin (\frac{π}{6}) < \frac{π}{6}$
24	13 23	eqbrtrri	$⊢ \frac{3}{6} < \frac{π}{6}$
25		3re	$⊢ 3 \in ℝ$
26	25 14 17 18	ltdiv1ii	$⊢ 3 < π \leftrightarrow \frac{3}{6} < \frac{π}{6}$
27	24 26	mpbir	$⊢ 3 < π$

Metamath Proof Explorer