Metamath Proof Explorer

Theorem trisecnconstr

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

Ref Expression
Assertion trisecnconstr ¬ ∀ 𝑜 ∈ Constr ( 𝑜 ↑𝑐 ( 1 / 3 ) ) ∈ Constr

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) )
2 eqid ⊢ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑𝑐 ( 1 / 3 ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑𝑐 ( 1 / 3 ) )
3 1 2 cos9thpinconstr ⊢ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ Constr ∧ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑𝑐 ( 1 / 3 ) ) ∉ Constr )
4 3 simpri ⊢ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑𝑐 ( 1 / 3 ) ) ∉ Constr
5 4 neli ⊢ ¬ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑𝑐 ( 1 / 3 ) ) ∈ Constr
6 3 simpli ⊢ ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ Constr
7 oveq1 ⊢ ( 𝑜 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) → ( 𝑜 ↑𝑐 ( 1 / 3 ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑𝑐 ( 1 / 3 ) ) )
8 7 eleq1d ⊢ ( 𝑜 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) → ( ( 𝑜 ↑𝑐 ( 1 / 3 ) ) ∈ Constr ↔ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑𝑐 ( 1 / 3 ) ) ∈ Constr ) )
9 8 rspcv ⊢ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ Constr → ( ∀ 𝑜 ∈ Constr ( 𝑜 ↑𝑐 ( 1 / 3 ) ) ∈ Constr → ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑𝑐 ( 1 / 3 ) ) ∈ Constr ) )
10 6 9 ax-mp ⊢ ( ∀ 𝑜 ∈ Constr ( 𝑜 ↑𝑐 ( 1 / 3 ) ) ∈ Constr → ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑𝑐 ( 1 / 3 ) ) ∈ Constr )
11 5 10 mto ⊢ ¬ ∀ 𝑜 ∈ Constr ( 𝑜 ↑𝑐 ( 1 / 3 ) ) ∈ Constr