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