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