Metamath Proof Explorer


Theorem 41prothprmlem2

Description: Lemma 2 for 41prothprm . (Contributed by AV, 5-Jul-2020)

Ref Expression
Hypothesis 41prothprm.p 𝑃 = 4 1
Assertion 41prothprmlem2 ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 )

Proof

Step Hyp Ref Expression
1 41prothprm.p 𝑃 = 4 1
2 1 41prothprmlem1 ( ( 𝑃 − 1 ) / 2 ) = 2 0
3 2 oveq2i ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) = ( 3 ↑ 2 0 )
4 3 oveq1i ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( ( 3 ↑ 2 0 ) mod 𝑃 )
5 5cn 5 ∈ ℂ
6 4cn 4 ∈ ℂ
7 5t4e20 ( 5 · 4 ) = 2 0
8 5 6 7 mulcomli ( 4 · 5 ) = 2 0
9 8 eqcomi 2 0 = ( 4 · 5 )
10 9 oveq2i ( 3 ↑ 2 0 ) = ( 3 ↑ ( 4 · 5 ) )
11 3cn 3 ∈ ℂ
12 4nn0 4 ∈ ℕ0
13 5nn0 5 ∈ ℕ0
14 expmul ( ( 3 ∈ ℂ ∧ 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) → ( 3 ↑ ( 4 · 5 ) ) = ( ( 3 ↑ 4 ) ↑ 5 ) )
15 11 12 13 14 mp3an ( 3 ↑ ( 4 · 5 ) ) = ( ( 3 ↑ 4 ) ↑ 5 )
16 10 15 eqtri ( 3 ↑ 2 0 ) = ( ( 3 ↑ 4 ) ↑ 5 )
17 16 oveq1i ( ( 3 ↑ 2 0 ) mod 4 1 ) = ( ( ( 3 ↑ 4 ) ↑ 5 ) mod 4 1 )
18 3z 3 ∈ ℤ
19 zexpcl ( ( 3 ∈ ℤ ∧ 4 ∈ ℕ0 ) → ( 3 ↑ 4 ) ∈ ℤ )
20 18 12 19 mp2an ( 3 ↑ 4 ) ∈ ℤ
21 neg1z - 1 ∈ ℤ
22 20 21 pm3.2i ( ( 3 ↑ 4 ) ∈ ℤ ∧ - 1 ∈ ℤ )
23 1nn 1 ∈ ℕ
24 12 23 decnncl 4 1 ∈ ℕ
25 nnrp ( 4 1 ∈ ℕ → 4 1 ∈ ℝ+ )
26 24 25 ax-mp 4 1 ∈ ℝ+
27 13 26 pm3.2i ( 5 ∈ ℕ0 4 1 ∈ ℝ+ )
28 3exp4mod41 ( ( 3 ↑ 4 ) mod 4 1 ) = ( - 1 mod 4 1 )
29 modexp ( ( ( ( 3 ↑ 4 ) ∈ ℤ ∧ - 1 ∈ ℤ ) ∧ ( 5 ∈ ℕ0 4 1 ∈ ℝ+ ) ∧ ( ( 3 ↑ 4 ) mod 4 1 ) = ( - 1 mod 4 1 ) ) → ( ( ( 3 ↑ 4 ) ↑ 5 ) mod 4 1 ) = ( ( - 1 ↑ 5 ) mod 4 1 ) )
30 22 27 28 29 mp3an ( ( ( 3 ↑ 4 ) ↑ 5 ) mod 4 1 ) = ( ( - 1 ↑ 5 ) mod 4 1 )
31 3p2e5 ( 3 + 2 ) = 5
32 31 eqcomi 5 = ( 3 + 2 )
33 32 oveq2i ( - 1 ↑ 5 ) = ( - 1 ↑ ( 3 + 2 ) )
34 2z 2 ∈ ℤ
35 m1expaddsub ( ( 3 ∈ ℤ ∧ 2 ∈ ℤ ) → ( - 1 ↑ ( 3 − 2 ) ) = ( - 1 ↑ ( 3 + 2 ) ) )
36 18 34 35 mp2an ( - 1 ↑ ( 3 − 2 ) ) = ( - 1 ↑ ( 3 + 2 ) )
37 36 eqcomi ( - 1 ↑ ( 3 + 2 ) ) = ( - 1 ↑ ( 3 − 2 ) )
38 2cn 2 ∈ ℂ
39 ax-1cn 1 ∈ ℂ
40 2p1e3 ( 2 + 1 ) = 3
41 11 38 39 40 subaddrii ( 3 − 2 ) = 1
42 41 oveq2i ( - 1 ↑ ( 3 − 2 ) ) = ( - 1 ↑ 1 )
43 neg1cn - 1 ∈ ℂ
44 exp1 ( - 1 ∈ ℂ → ( - 1 ↑ 1 ) = - 1 )
45 43 44 ax-mp ( - 1 ↑ 1 ) = - 1
46 42 45 eqtri ( - 1 ↑ ( 3 − 2 ) ) = - 1
47 33 37 46 3eqtri ( - 1 ↑ 5 ) = - 1
48 47 oveq1i ( ( - 1 ↑ 5 ) mod 4 1 ) = ( - 1 mod 4 1 )
49 17 30 48 3eqtri ( ( 3 ↑ 2 0 ) mod 4 1 ) = ( - 1 mod 4 1 )
50 1 oveq2i ( ( 3 ↑ 2 0 ) mod 𝑃 ) = ( ( 3 ↑ 2 0 ) mod 4 1 )
51 1 oveq2i ( - 1 mod 𝑃 ) = ( - 1 mod 4 1 )
52 49 50 51 3eqtr4i ( ( 3 ↑ 2 0 ) mod 𝑃 ) = ( - 1 mod 𝑃 )
53 4 52 eqtri ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 )