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 𝑃 )