Metamath Proof Explorer

Theorem 3exp4mod41

Description: 3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020)

Ref Expression
Assertion 3exp4mod41 
|- ( ( 3 ^ 4 ) mod ; 4 1 ) = ( -u 1 mod ; 4 1 )

Proof

Step Hyp Ref Expression
1 2p2e4 
 |-  ( 2 + 2 ) = 4
2 1 eqcomi 
 |-  4 = ( 2 + 2 )
3 2 oveq2i 
 |-  ( 3 ^ 4 ) = ( 3 ^ ( 2 + 2 ) )
4 3cn 
 |-  3 e. CC
5 2nn0 
 |-  2 e. NN0
6 expadd 
 |-  ( ( 3 e. CC /\ 2 e. NN0 /\ 2 e. NN0 ) -> ( 3 ^ ( 2 + 2 ) ) = ( ( 3 ^ 2 ) x. ( 3 ^ 2 ) ) )
7 4 5 5 6 mp3an 
 |-  ( 3 ^ ( 2 + 2 ) ) = ( ( 3 ^ 2 ) x. ( 3 ^ 2 ) )
8 sq3 
 |-  ( 3 ^ 2 ) = 9
9 8 8 oveq12i 
 |-  ( ( 3 ^ 2 ) x. ( 3 ^ 2 ) ) = ( 9 x. 9 )
10 9t9e81 
 |-  ( 9 x. 9 ) = ; 8 1
11 9 10 eqtri 
 |-  ( ( 3 ^ 2 ) x. ( 3 ^ 2 ) ) = ; 8 1
12 3 7 11 3eqtri 
 |-  ( 3 ^ 4 ) = ; 8 1
13 12 oveq1i 
 |-  ( ( 3 ^ 4 ) mod ; 4 1 ) = ( ; 8 1 mod ; 4 1 )
14 dfdec10 
 |-  ; 8 1 = ( ( ; 1 0 x. 8 ) + 1 )
15 4cn 
 |-  4 e. CC
16 2cn 
 |-  2 e. CC
17 4t2e8 
 |-  ( 4 x. 2 ) = 8
18 15 16 17 mulcomli 
 |-  ( 2 x. 4 ) = 8
19 18 eqcomi 
 |-  8 = ( 2 x. 4 )
20 19 oveq2i 
 |-  ( ; 1 0 x. 8 ) = ( ; 1 0 x. ( 2 x. 4 ) )
21 ax-1cn 
 |-  1 e. CC
22 16 21 negsubi 
 |-  ( 2 + -u 1 ) = ( 2 - 1 )
23 2m1e1 
 |-  ( 2 - 1 ) = 1
24 22 23 eqtri 
 |-  ( 2 + -u 1 ) = 1
25 24 eqcomi 
 |-  1 = ( 2 + -u 1 )
26 20 25 oveq12i 
 |-  ( ( ; 1 0 x. 8 ) + 1 ) = ( ( ; 1 0 x. ( 2 x. 4 ) ) + ( 2 + -u 1 ) )
27 10nn 
 |-  ; 1 0 e. NN
28 27 nncni 
 |-  ; 1 0 e. CC
29 16 15 mulcli 
 |-  ( 2 x. 4 ) e. CC
30 28 29 mulcli 
 |-  ( ; 1 0 x. ( 2 x. 4 ) ) e. CC
31 neg1cn 
 |-  -u 1 e. CC
32 30 16 31 addassi 
 |-  ( ( ( ; 1 0 x. ( 2 x. 4 ) ) + 2 ) + -u 1 ) = ( ( ; 1 0 x. ( 2 x. 4 ) ) + ( 2 + -u 1 ) )
33 28 15 mulcli 
 |-  ( ; 1 0 x. 4 ) e. CC
34 16 33 21 adddii 
 |-  ( 2 x. ( ( ; 1 0 x. 4 ) + 1 ) ) = ( ( 2 x. ( ; 1 0 x. 4 ) ) + ( 2 x. 1 ) )
35 dfdec10 
 |-  ; 4 1 = ( ( ; 1 0 x. 4 ) + 1 )
36 35 eqcomi 
 |-  ( ( ; 1 0 x. 4 ) + 1 ) = ; 4 1
37 36 oveq2i 
 |-  ( 2 x. ( ( ; 1 0 x. 4 ) + 1 ) ) = ( 2 x. ; 4 1 )
38 16 28 15 mul12i 
 |-  ( 2 x. ( ; 1 0 x. 4 ) ) = ( ; 1 0 x. ( 2 x. 4 ) )
39 2t1e2 
 |-  ( 2 x. 1 ) = 2
40 38 39 oveq12i 
 |-  ( ( 2 x. ( ; 1 0 x. 4 ) ) + ( 2 x. 1 ) ) = ( ( ; 1 0 x. ( 2 x. 4 ) ) + 2 )
41 34 37 40 3eqtr3ri 
 |-  ( ( ; 1 0 x. ( 2 x. 4 ) ) + 2 ) = ( 2 x. ; 4 1 )
42 41 oveq1i 
 |-  ( ( ( ; 1 0 x. ( 2 x. 4 ) ) + 2 ) + -u 1 ) = ( ( 2 x. ; 4 1 ) + -u 1 )
43 26 32 42 3eqtr2i 
 |-  ( ( ; 1 0 x. 8 ) + 1 ) = ( ( 2 x. ; 4 1 ) + -u 1 )
44 14 43 eqtri 
 |-  ; 8 1 = ( ( 2 x. ; 4 1 ) + -u 1 )
45 44 oveq1i 
 |-  ( ; 8 1 mod ; 4 1 ) = ( ( ( 2 x. ; 4 1 ) + -u 1 ) mod ; 4 1 )
46 4nn0 
 |-  4 e. NN0
47 1nn 
 |-  1 e. NN
48 46 47 decnncl 
 |-  ; 4 1 e. NN
49 48 nncni 
 |-  ; 4 1 e. CC
50 16 49 mulcli 
 |-  ( 2 x. ; 4 1 ) e. CC
51 50 31 addcomi 
 |-  ( ( 2 x. ; 4 1 ) + -u 1 ) = ( -u 1 + ( 2 x. ; 4 1 ) )
52 51 oveq1i 
 |-  ( ( ( 2 x. ; 4 1 ) + -u 1 ) mod ; 4 1 ) = ( ( -u 1 + ( 2 x. ; 4 1 ) ) mod ; 4 1 )
53 neg1rr 
 |-  -u 1 e. RR
54 nnrp 
 |-  ( ; 4 1 e. NN -> ; 4 1 e. RR+ )
55 48 54 ax-mp 
 |-  ; 4 1 e. RR+
56 2z 
 |-  2 e. ZZ
57 modcyc 
 |-  ( ( -u 1 e. RR /\ ; 4 1 e. RR+ /\ 2 e. ZZ ) -> ( ( -u 1 + ( 2 x. ; 4 1 ) ) mod ; 4 1 ) = ( -u 1 mod ; 4 1 ) )
58 53 55 56 57 mp3an 
 |-  ( ( -u 1 + ( 2 x. ; 4 1 ) ) mod ; 4 1 ) = ( -u 1 mod ; 4 1 )
59 52 58 eqtri 
 |-  ( ( ( 2 x. ; 4 1 ) + -u 1 ) mod ; 4 1 ) = ( -u 1 mod ; 4 1 )
60 13 45 59 3eqtri 
 |-  ( ( 3 ^ 4 ) mod ; 4 1 ) = ( -u 1 mod ; 4 1 )