Metamath Proof Explorer


Theorem pigt3

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

Ref Expression
Assertion pigt3
|- 3 < _pi

Proof

Step Hyp Ref Expression
1 sincos6thpi
 |-  ( ( sin ` ( _pi / 6 ) ) = ( 1 / 2 ) /\ ( cos ` ( _pi / 6 ) ) = ( ( sqrt ` 3 ) / 2 ) )
2 1 simpli
 |-  ( sin ` ( _pi / 6 ) ) = ( 1 / 2 )
3 ax-1cn
 |-  1 e. CC
4 2cnne0
 |-  ( 2 e. CC /\ 2 =/= 0 )
5 3cn
 |-  3 e. CC
6 3ne0
 |-  3 =/= 0
7 5 6 pm3.2i
 |-  ( 3 e. CC /\ 3 =/= 0 )
8 divcan5
 |-  ( ( 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 3 x. 1 ) / ( 3 x. 2 ) ) = ( 1 / 2 ) )
9 3 4 7 8 mp3an
 |-  ( ( 3 x. 1 ) / ( 3 x. 2 ) ) = ( 1 / 2 )
10 3t1e3
 |-  ( 3 x. 1 ) = 3
11 3t2e6
 |-  ( 3 x. 2 ) = 6
12 10 11 oveq12i
 |-  ( ( 3 x. 1 ) / ( 3 x. 2 ) ) = ( 3 / 6 )
13 2 9 12 3eqtr2i
 |-  ( sin ` ( _pi / 6 ) ) = ( 3 / 6 )
14 pire
 |-  _pi e. RR
15 pipos
 |-  0 < _pi
16 14 15 elrpii
 |-  _pi e. RR+
17 6re
 |-  6 e. RR
18 6pos
 |-  0 < 6
19 17 18 elrpii
 |-  6 e. RR+
20 rpdivcl
 |-  ( ( _pi e. RR+ /\ 6 e. RR+ ) -> ( _pi / 6 ) e. RR+ )
21 16 19 20 mp2an
 |-  ( _pi / 6 ) e. RR+
22 sinltx
 |-  ( ( _pi / 6 ) e. RR+ -> ( sin ` ( _pi / 6 ) ) < ( _pi / 6 ) )
23 21 22 ax-mp
 |-  ( sin ` ( _pi / 6 ) ) < ( _pi / 6 )
24 13 23 eqbrtrri
 |-  ( 3 / 6 ) < ( _pi / 6 )
25 3re
 |-  3 e. RR
26 25 14 17 18 ltdiv1ii
 |-  ( 3 < _pi <-> ( 3 / 6 ) < ( _pi / 6 ) )
27 24 26 mpbir
 |-  3 < _pi