Metamath Proof Explorer

Theorem trisecnconstr

Description: Not all angles can be trisected. (Contributed by Thierry Arnoux, 15-Nov-2025)

Ref Expression
Assertion trisecnconstr 
|- -. A. o e. Constr ( o ^c ( 1 / 3 ) ) e. Constr

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
2 eqid 
 |-  ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ^c ( 1 / 3 ) ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ^c ( 1 / 3 ) )
3 1 2 cos9thpinconstr 
 |-  ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) e. Constr /\ ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ^c ( 1 / 3 ) ) e/ Constr )
4 3 simpri 
 |-  ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ^c ( 1 / 3 ) ) e/ Constr
5 4 neli 
 |-  -. ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ^c ( 1 / 3 ) ) e. Constr
6 3 simpli 
 |-  ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) e. Constr
7 oveq1 
 |-  ( o = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) -> ( o ^c ( 1 / 3 ) ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ^c ( 1 / 3 ) ) )
8 7 eleq1d 
 |-  ( o = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) -> ( ( o ^c ( 1 / 3 ) ) e. Constr <-> ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ^c ( 1 / 3 ) ) e. Constr ) )
9 8 rspcv 
 |-  ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) e. Constr -> ( A. o e. Constr ( o ^c ( 1 / 3 ) ) e. Constr -> ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ^c ( 1 / 3 ) ) e. Constr ) )
10 6 9 ax-mp 
 |-  ( A. o e. Constr ( o ^c ( 1 / 3 ) ) e. Constr -> ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ^c ( 1 / 3 ) ) e. Constr )
11 5 10 mto 
 |-  -. A. o e. Constr ( o ^c ( 1 / 3 ) ) e. Constr