Metamath Proof Explorer

Theorem bru1

Description: The basic (and only) 1st root of unity is 1. (Contributed by AV, 24-Oct-2026)

Ref Expression
Assertion bru1 
|- ( bRoU ` 1 ) = 1

Proof

Step Hyp Ref Expression
1 1nn 
 |-  1 e. NN
2 bruval2 
 |-  ( 1 e. NN -> ( bRoU ` 1 ) = ( -u 1 ^c ( 2 / 1 ) ) )
3 1 2 ax-mp 
 |-  ( bRoU ` 1 ) = ( -u 1 ^c ( 2 / 1 ) )
4 2cn 
 |-  2 e. CC
5 4 div1i 
 |-  ( 2 / 1 ) = 2
6 5 oveq2i 
 |-  ( -u 1 ^c ( 2 / 1 ) ) = ( -u 1 ^c 2 )
7 neg1cn 
 |-  -u 1 e. CC
8 neg1ne0 
 |-  -u 1 =/= 0
9 2z 
 |-  2 e. ZZ
10 cxpexpz 
 |-  ( ( -u 1 e. CC /\ -u 1 =/= 0 /\ 2 e. ZZ ) -> ( -u 1 ^c 2 ) = ( -u 1 ^ 2 ) )
11 7 8 9 10 mp3an 
 |-  ( -u 1 ^c 2 ) = ( -u 1 ^ 2 )
12 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
13 11 12 eqtri 
 |-  ( -u 1 ^c 2 ) = 1
14 6 13 eqtri 
 |-  ( -u 1 ^c ( 2 / 1 ) ) = 1
15 3 14 eqtri 
 |-  ( bRoU ` 1 ) = 1