Metamath Proof Explorer

Theorem root1id

Description: Property of an N -th root of unity. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion root1id ( ๐‘ โˆˆ โ„• โ†’ ( ( - 1 โ†‘๐‘ ( 2 / ๐‘ ) ) โ†‘ ๐‘ ) = 1 )

Proof

Step Hyp Ref Expression
1 neg1cn โŠข - 1 โˆˆ โ„‚
2 1 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ - 1 โˆˆ โ„‚ )
3 2re โŠข 2 โˆˆ โ„
4 nndivre โŠข ( ( 2 โˆˆ โ„ โˆง ๐‘ โˆˆ โ„• ) โ†’ ( 2 / ๐‘ ) โˆˆ โ„ )
5 3 4 mpan โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 / ๐‘ ) โˆˆ โ„ )
6 5 recnd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 / ๐‘ ) โˆˆ โ„‚ )
7 nnnn0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„•0 )
8 2 6 7 cxpmul2d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( - 1 โ†‘๐‘ ( ( 2 / ๐‘ ) ยท ๐‘ ) ) = ( ( - 1 โ†‘๐‘ ( 2 / ๐‘ ) ) โ†‘ ๐‘ ) )
9 2cnd โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„‚ )
10 nncn โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚ )
11 nnne0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โ‰  0 )
12 9 10 11 divcan1d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 / ๐‘ ) ยท ๐‘ ) = 2 )
13 12 oveq2d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( - 1 โ†‘๐‘ ( ( 2 / ๐‘ ) ยท ๐‘ ) ) = ( - 1 โ†‘๐‘ 2 ) )
14 2nn0 โŠข 2 โˆˆ โ„•0
15 cxpexp โŠข ( ( - 1 โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0 ) โ†’ ( - 1 โ†‘๐‘ 2 ) = ( - 1 โ†‘ 2 ) )
16 1 14 15 mp2an โŠข ( - 1 โ†‘๐‘ 2 ) = ( - 1 โ†‘ 2 )
17 ax-1cn โŠข 1 โˆˆ โ„‚
18 sqneg โŠข ( 1 โˆˆ โ„‚ โ†’ ( - 1 โ†‘ 2 ) = ( 1 โ†‘ 2 ) )
19 17 18 ax-mp โŠข ( - 1 โ†‘ 2 ) = ( 1 โ†‘ 2 )
20 sq1 โŠข ( 1 โ†‘ 2 ) = 1
21 16 19 20 3eqtri โŠข ( - 1 โ†‘๐‘ 2 ) = 1
22 13 21 eqtrdi โŠข ( ๐‘ โˆˆ โ„• โ†’ ( - 1 โ†‘๐‘ ( ( 2 / ๐‘ ) ยท ๐‘ ) ) = 1 )
23 8 22 eqtr3d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( - 1 โ†‘๐‘ ( 2 / ๐‘ ) ) โ†‘ ๐‘ ) = 1 )