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 ⊢3P−12modP=-1modP

Proof

Step Hyp Ref Expression
1 41prothprm.p ⊢P=41
2 1 41prothprmlem1 ⊢P−12=20
3 2 oveq2i ⊢3P−12=320
4 3 oveq1i ⊢3P−12modP=320modP
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 ⊢320=34⋅5
11 3cn ⊢3∈ℂ
12 4nn0 ⊢4∈ℕ0
13 5nn0 ⊢5∈ℕ0
14 expmul ⊢3∈ℂ∧4∈ℕ0∧5∈ℕ0→34⋅5=345
15 11 12 13 14 mp3an ⊢34⋅5=345
16 10 15 eqtri ⊢320=345
17 16 oveq1i ⊢320mod41=345mod41
18 3z ⊢3∈ℤ
19 zexpcl ⊢3∈ℤ∧4∈ℕ0→34∈ℤ
20 18 12 19 mp2an ⊢34∈ℤ
21 neg1z ⊢−1∈ℤ
22 20 21 pm3.2i ⊢34∈ℤ∧−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 ⊢34mod41=-1mod41
29 modexp ⊢34∈ℤ∧−1∈ℤ∧5∈ℕ0∧41∈ℝ+∧34mod41=-1mod41→345mod41=−15mod41
30 22 27 28 29 mp3an ⊢345mod41=−15mod41
31 3p2e5 ⊢3+2=5
32 31 eqcomi ⊢5=3+2
33 32 oveq2i ⊢−15=−13+2
34 2z ⊢2∈ℤ
35 m1expaddsub ⊢3∈ℤ∧2∈ℤ→−13−2=−13+2
36 18 34 35 mp2an ⊢−13−2=−13+2
37 36 eqcomi ⊢−13+2=−13−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 ⊢−13−2=−11
43 neg1cn ⊢−1∈ℂ
44 exp1 ⊢−1∈ℂ→−11=−1
45 43 44 ax-mp ⊢−11=−1
46 42 45 eqtri ⊢−13−2=−1
47 33 37 46 3eqtri ⊢−15=−1
48 47 oveq1i ⊢−15mod41=-1mod41
49 17 30 48 3eqtri ⊢320mod41=-1mod41
50 1 oveq2i ⊢320modP=320mod41
51 1 oveq2i ⊢-1modP=-1mod41
52 49 50 51 3eqtr4i ⊢320modP=-1modP
53 4 52 eqtri ⊢3P−12modP=-1modP