Metamath Proof Explorer

Theorem 41prothprm

Description: 41 is aProth prime. (Contributed by AV, 5-Jul-2020)

Ref Expression
Hypothesis 41prothprm.p ⊢ P = 41
Assertion 41prothprm ⊢ P = 5 ⁢ 2 3 + 1 ∧ P ∈ ℙ

Proof

Step Hyp Ref Expression
1 41prothprm.p ⊢ P = 41
2 1 41prothprmlem2 ⊢ 3 P − 1 2 mod P = -1 mod P
3 dfdec10 ⊢ 41 = 10 ⋅ 4 + 1
4 4t2e8 ⊢ 4 ⋅ 2 = 8
5 4cn ⊢ 4 ∈ ℂ
6 2cn ⊢ 2 ∈ ℂ
7 5 6 mulcomi ⊢ 4 ⋅ 2 = 2 ⋅ 4
8 4 7 eqtr3i ⊢ 8 = 2 ⋅ 4
9 8 oveq2i ⊢ 5 ⋅ 8 = 5 ⁢ 2 ⋅ 4
10 5cn ⊢ 5 ∈ ℂ
11 10 6 5 mulassi ⊢ 5 ⋅ 2 ⋅ 4 = 5 ⁢ 2 ⋅ 4
12 5t2e10 ⊢ 5 ⋅ 2 = 10
13 12 oveq1i ⊢ 5 ⋅ 2 ⋅ 4 = 10 ⋅ 4
14 9 11 13 3eqtr2i ⊢ 5 ⋅ 8 = 10 ⋅ 4
15 cu2 ⊢ 2 3 = 8
16 15 eqcomi ⊢ 8 = 2 3
17 16 oveq2i ⊢ 5 ⋅ 8 = 5 ⁢ 2 3
18 14 17 eqtr3i ⊢ 10 ⋅ 4 = 5 ⁢ 2 3
19 18 oveq1i ⊢ 10 ⋅ 4 + 1 = 5 ⁢ 2 3 + 1
20 1 3 19 3eqtri ⊢ P = 5 ⁢ 2 3 + 1
21 simpr ⊢ 3 P − 1 2 mod P = -1 mod P ∧ P = 5 ⁢ 2 3 + 1 → P = 5 ⁢ 2 3 + 1
22 3nn ⊢ 3 ∈ ℕ
23 22 a1i ⊢ 3 P − 1 2 mod P = -1 mod P ∧ P = 5 ⁢ 2 3 + 1 → 3 ∈ ℕ
24 5nn ⊢ 5 ∈ ℕ
25 24 a1i ⊢ 3 P − 1 2 mod P = -1 mod P ∧ P = 5 ⁢ 2 3 + 1 → 5 ∈ ℕ
26 5lt8 ⊢ 5 < 8
27 26 15 breqtrri ⊢ 5 < 2 3
28 27 a1i ⊢ 3 P − 1 2 mod P = -1 mod P ∧ P = 5 ⁢ 2 3 + 1 → 5 < 2 3
29 3z ⊢ 3 ∈ ℤ
30 29 a1i ⊢ 3 P − 1 2 mod P = -1 mod P → 3 ∈ ℤ
31 oveq1 ⊢ x = 3 → x P − 1 2 = 3 P − 1 2
32 31 oveq1d ⊢ x = 3 → x P − 1 2 mod P = 3 P − 1 2 mod P
33 32 eqeq1d ⊢ x = 3 → x P − 1 2 mod P = -1 mod P ↔ 3 P − 1 2 mod P = -1 mod P
34 33 adantl ⊢ 3 P − 1 2 mod P = -1 mod P ∧ x = 3 → x P − 1 2 mod P = -1 mod P ↔ 3 P − 1 2 mod P = -1 mod P
35 id ⊢ 3 P − 1 2 mod P = -1 mod P → 3 P − 1 2 mod P = -1 mod P
36 30 34 35 rspcedvd ⊢ 3 P − 1 2 mod P = -1 mod P → ∃ x ∈ ℤ x P − 1 2 mod P = -1 mod P
37 36 adantr ⊢ 3 P − 1 2 mod P = -1 mod P ∧ P = 5 ⁢ 2 3 + 1 → ∃ x ∈ ℤ x P − 1 2 mod P = -1 mod P
38 23 25 21 28 37 proththd ⊢ 3 P − 1 2 mod P = -1 mod P ∧ P = 5 ⁢ 2 3 + 1 → P ∈ ℙ
39 21 38 jca ⊢ 3 P − 1 2 mod P = -1 mod P ∧ P = 5 ⁢ 2 3 + 1 → P = 5 ⁢ 2 3 + 1 ∧ P ∈ ℙ
40 2 20 39 mp2an ⊢ P = 5 ⁢ 2 3 + 1 ∧ P ∈ ℙ