Theorem pigt3

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

	Ref	Expression
Assertion	pigt3	⊢ 3 < π

Proof

Step	Hyp	Ref	Expression
1		sincos6thpi	⊢ ( ( sin ‘ ( π / 6 ) ) = ( 1 / 2 ) ∧ ( cos ‘ ( π / 6 ) ) = ( ( √ ‘ 3 ) / 2 ) )
2	1	simpli	⊢ ( sin ‘ ( π / 6 ) ) = ( 1 / 2 )
3		ax-1cn	⊢ 1 ∈ ℂ
4		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
5		3cn	⊢ 3 ∈ ℂ
6		3ne0	⊢ 3 ≠ 0
7	5 6	pm3.2i	⊢ ( 3 ∈ ℂ ∧ 3 ≠ 0 )
8		divcan5	⊢ ( ( 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( 3 · 1 ) / ( 3 · 2 ) ) = ( 1 / 2 ) )
9	3 4 7 8	mp3an	⊢ ( ( 3 · 1 ) / ( 3 · 2 ) ) = ( 1 / 2 )
10		3t1e3	⊢ ( 3 · 1 ) = 3
11		3t2e6	⊢ ( 3 · 2 ) = 6
12	10 11	oveq12i	⊢ ( ( 3 · 1 ) / ( 3 · 2 ) ) = ( 3 / 6 )
13	2 9 12	3eqtr2i	⊢ ( sin ‘ ( π / 6 ) ) = ( 3 / 6 )
14		pire	⊢ π ∈ ℝ
15		pipos	⊢ 0 < π
16	14 15	elrpii	⊢ π ∈ ℝ+
17		6re	⊢ 6 ∈ ℝ
18		6pos	⊢ 0 < 6
19	17 18	elrpii	⊢ 6 ∈ ℝ+
20		rpdivcl	⊢ ( ( π ∈ ℝ+ ∧ 6 ∈ ℝ+ ) → ( π / 6 ) ∈ ℝ+ )
21	16 19 20	mp2an	⊢ ( π / 6 ) ∈ ℝ+
22		sinltx	⊢ ( ( π / 6 ) ∈ ℝ+ → ( sin ‘ ( π / 6 ) ) < ( π / 6 ) )
23	21 22	ax-mp	⊢ ( sin ‘ ( π / 6 ) ) < ( π / 6 )
24	13 23	eqbrtrri	⊢ ( 3 / 6 ) < ( π / 6 )
25		3re	⊢ 3 ∈ ℝ
26	25 14 17 18	ltdiv1ii	⊢ ( 3 < π ↔ ( 3 / 6 ) < ( π / 6 ) )
27	24 26	mpbir	⊢ 3 < π