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