Metamath Proof Explorer

Theorem 41prothprmlem2

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

Ref Expression
Hypothesis 41prothprm.p ⊢ P = 41
Assertion 41prothprmlem2 ⊢ 3 P − 1 2 mod P = -1 mod P

Proof

Step Hyp Ref Expression
1 41prothprm.p ⊢ P = 41
2 1 41prothprmlem1 ⊢ P − 1 2 = 20
3 2 oveq2i ⊢ 3 P − 1 2 = 3 20
4 3 oveq1i ⊢ 3 P − 1 2 mod P = 3 20 mod P
5 5cn ⊢ 5 ∈ ℂ
6 4cn ⊢ 4 ∈ ℂ
7 5t4e20 ⊢ 5 ⋅ 4 = 20
8 5 6 7 mulcomli ⊢ 4 ⋅ 5 = 20
9 8 eqcomi ⊢ 20 = 4 ⋅ 5
10 9 oveq2i ⊢ 3 20 = 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 20 = 3 4 5
17 16 oveq1i ⊢ 3 20 mod 41 = 3 4 5 mod 41
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 ⊢ 41 ∈ ℕ
25 nnrp ⊢ 41 ∈ ℕ → 41 ∈ ℝ +
26 24 25 ax-mp ⊢ 41 ∈ ℝ +
27 13 26 pm3.2i ⊢ 5 ∈ ℕ 0 ∧ 41 ∈ ℝ +
28 3exp4mod41 ⊢ 3 4 mod 41 = -1 mod 41
29 modexp ⊢ 3 4 ∈ ℤ ∧ − 1 ∈ ℤ ∧ 5 ∈ ℕ 0 ∧ 41 ∈ ℝ + ∧ 3 4 mod 41 = -1 mod 41 → 3 4 5 mod 41 = − 1 5 mod 41
30 22 27 28 29 mp3an ⊢ 3 4 5 mod 41 = − 1 5 mod 41
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 41 = -1 mod 41
49 17 30 48 3eqtri ⊢ 3 20 mod 41 = -1 mod 41
50 1 oveq2i ⊢ 3 20 mod P = 3 20 mod 41
51 1 oveq2i ⊢ -1 mod P = -1 mod 41
52 49 50 51 3eqtr4i ⊢ 3 20 mod P = -1 mod P
53 4 52 eqtri ⊢ 3 P − 1 2 mod P = -1 mod P