Theorem pigt3

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

	Ref	Expression
Assertion	pigt3	$$⊢3<\mathrm{\pi }$$

Proof

Step	Hyp	Ref	Expression
1		sincos6thpi	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{6}\right)=\frac{1}{2}\wedge \cos \left(\frac{\mathrm{\pi }}{6}\right)=\frac{\sqrt{3}}{2}\right)$$
2	1	simpli	$$⊢\sin \left(\frac{\mathrm{\pi }}{6}\right)=\frac{1}{2}$$
3		ax-1cn	$$⊢1\in ℂ$$
4		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
5		3cn	$$⊢3\in ℂ$$
6		3ne0	$$⊢3\ne 0$$
7	5 6	pm3.2i	$$⊢\left(3\in ℂ\wedge 3\ne 0\right)$$
8		divcan5	$$⊢\left(1\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(3\in ℂ\wedge 3\ne 0\right)\right)\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 \left(\frac{\mathrm{\pi }}{6}\right)=\frac{3}{6}$$
14		pire	$$⊢\mathrm{\pi }\in ℝ$$
15		pipos	$$⊢0<\mathrm{\pi }$$
16	14 15	elrpii	$$⊢\mathrm{\pi }\in {ℝ}^{+}$$
17		6re	$$⊢6\in ℝ$$
18		6pos	$$⊢0<6$$
19	17 18	elrpii	$$⊢6\in {ℝ}^{+}$$
20		rpdivcl	$$⊢\left(\mathrm{\pi }\in {ℝ}^{+}\wedge 6\in {ℝ}^{+}\right)\to \frac{\mathrm{\pi }}{6}\in {ℝ}^{+}$$
21	16 19 20	mp2an	$$⊢\frac{\mathrm{\pi }}{6}\in {ℝ}^{+}$$
22		sinltx	$$⊢\frac{\mathrm{\pi }}{6}\in {ℝ}^{+}\to \sin \left(\frac{\mathrm{\pi }}{6}\right)<\frac{\mathrm{\pi }}{6}$$
23	21 22	ax-mp	$$⊢\sin \left(\frac{\mathrm{\pi }}{6}\right)<\frac{\mathrm{\pi }}{6}$$
24	13 23	eqbrtrri	$$⊢\frac{3}{6}<\frac{\mathrm{\pi }}{6}$$
25		3re	$$⊢3\in ℝ$$
26	25 14 17 18	ltdiv1ii	$$⊢3<\mathrm{\pi }\leftrightarrow \frac{3}{6}<\frac{\mathrm{\pi }}{6}$$
27	24 26	mpbir	$$⊢3<\mathrm{\pi }$$