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 ) = ( - 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 ∈ ℂ
5 2nn0 ⊢ 2 ∈ ℕ0
6 expadd ⊢ ( ( 3 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 3 ↑ ( 2 + 2 ) ) = ( ( 3 ↑ 2 ) · ( 3 ↑ 2 ) ) )
7 4 5 5 6 mp3an ⊢ ( 3 ↑ ( 2 + 2 ) ) = ( ( 3 ↑ 2 ) · ( 3 ↑ 2 ) )
8 sq3 ⊢ ( 3 ↑ 2 ) = 9
9 8 8 oveq12i ⊢ ( ( 3 ↑ 2 ) · ( 3 ↑ 2 ) ) = ( 9 · 9 )
10 9t9e81 ⊢ ( 9 · 9 ) = 8 1
11 9 10 eqtri ⊢ ( ( 3 ↑ 2 ) · ( 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 · 8 ) + 1 )
15 4cn ⊢ 4 ∈ ℂ
16 2cn ⊢ 2 ∈ ℂ
17 4t2e8 ⊢ ( 4 · 2 ) = 8
18 15 16 17 mulcomli ⊢ ( 2 · 4 ) = 8
19 18 eqcomi ⊢ 8 = ( 2 · 4 )
20 19 oveq2i ⊢ ( 1 0 · 8 ) = ( 1 0 · ( 2 · 4 ) )
21 ax-1cn ⊢ 1 ∈ ℂ
22 16 21 negsubi ⊢ ( 2 + - 1 ) = ( 2 − 1 )
23 2m1e1 ⊢ ( 2 − 1 ) = 1
24 22 23 eqtri ⊢ ( 2 + - 1 ) = 1
25 24 eqcomi ⊢ 1 = ( 2 + - 1 )
26 20 25 oveq12i ⊢ ( ( 1 0 · 8 ) + 1 ) = ( ( 1 0 · ( 2 · 4 ) ) + ( 2 + - 1 ) )
27 10nn ⊢ 1 0 ∈ ℕ
28 27 nncni ⊢ 1 0 ∈ ℂ
29 16 15 mulcli ⊢ ( 2 · 4 ) ∈ ℂ
30 28 29 mulcli ⊢ ( 1 0 · ( 2 · 4 ) ) ∈ ℂ
31 neg1cn ⊢ - 1 ∈ ℂ
32 30 16 31 addassi ⊢ ( ( ( 1 0 · ( 2 · 4 ) ) + 2 ) + - 1 ) = ( ( 1 0 · ( 2 · 4 ) ) + ( 2 + - 1 ) )
33 28 15 mulcli ⊢ ( 1 0 · 4 ) ∈ ℂ
34 16 33 21 adddii ⊢ ( 2 · ( ( 1 0 · 4 ) + 1 ) ) = ( ( 2 · ( 1 0 · 4 ) ) + ( 2 · 1 ) )
35 dfdec10 ⊢ 4 1 = ( ( 1 0 · 4 ) + 1 )
36 35 eqcomi ⊢ ( ( 1 0 · 4 ) + 1 ) = 4 1
37 36 oveq2i ⊢ ( 2 · ( ( 1 0 · 4 ) + 1 ) ) = ( 2 · 4 1 )
38 16 28 15 mul12i ⊢ ( 2 · ( 1 0 · 4 ) ) = ( 1 0 · ( 2 · 4 ) )
39 2t1e2 ⊢ ( 2 · 1 ) = 2
40 38 39 oveq12i ⊢ ( ( 2 · ( 1 0 · 4 ) ) + ( 2 · 1 ) ) = ( ( 1 0 · ( 2 · 4 ) ) + 2 )
41 34 37 40 3eqtr3ri ⊢ ( ( 1 0 · ( 2 · 4 ) ) + 2 ) = ( 2 · 4 1 )
42 41 oveq1i ⊢ ( ( ( 1 0 · ( 2 · 4 ) ) + 2 ) + - 1 ) = ( ( 2 · 4 1 ) + - 1 )
43 26 32 42 3eqtr2i ⊢ ( ( 1 0 · 8 ) + 1 ) = ( ( 2 · 4 1 ) + - 1 )
44 14 43 eqtri ⊢ 8 1 = ( ( 2 · 4 1 ) + - 1 )
45 44 oveq1i ⊢ ( 8 1 mod 4 1 ) = ( ( ( 2 · 4 1 ) + - 1 ) mod 4 1 )
46 4nn0 ⊢ 4 ∈ ℕ0
47 1nn ⊢ 1 ∈ ℕ
48 46 47 decnncl ⊢ 4 1 ∈ ℕ
49 48 nncni ⊢ 4 1 ∈ ℂ
50 16 49 mulcli ⊢ ( 2 · 4 1 ) ∈ ℂ
51 50 31 addcomi ⊢ ( ( 2 · 4 1 ) + - 1 ) = ( - 1 + ( 2 · 4 1 ) )
52 51 oveq1i ⊢ ( ( ( 2 · 4 1 ) + - 1 ) mod 4 1 ) = ( ( - 1 + ( 2 · 4 1 ) ) mod 4 1 )
53 neg1rr ⊢ - 1 ∈ ℝ
54 nnrp ⊢ ( 4 1 ∈ ℕ → 4 1 ∈ ℝ+ )
55 48 54 ax-mp ⊢ 4 1 ∈ ℝ+
56 2z ⊢ 2 ∈ ℤ
57 modcyc ⊢ ( ( - 1 ∈ ℝ ∧ 4 1 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( - 1 + ( 2 · 4 1 ) ) mod 4 1 ) = ( - 1 mod 4 1 ) )
58 53 55 56 57 mp3an ⊢ ( ( - 1 + ( 2 · 4 1 ) ) mod 4 1 ) = ( - 1 mod 4 1 )
59 52 58 eqtri ⊢ ( ( ( 2 · 4 1 ) + - 1 ) mod 4 1 ) = ( - 1 mod 4 1 )
60 13 45 59 3eqtri ⊢ ( ( 3 ↑ 4 ) mod 4 1 ) = ( - 1 mod 4 1 )