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