This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 < π