Metamath Proof Explorer

Theorem 41prothprm

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

Ref Expression
Hypothesis 41prothprm.p ⊢ 𝑃 = 4 1
Assertion 41prothprm ( 𝑃 = ( ( 5 · ( 2 ↑ 3 ) ) + 1 ) ∧ 𝑃 ∈ ℙ )

Proof

Step Hyp Ref Expression
1 41prothprm.p ⊢ 𝑃 = 4 1
2 1 41prothprmlem2 ⊢ ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 )
3 dfdec10 ⊢ 4 1 = ( ( 1 0 · 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 ) = 1 0
13 12 oveq1i ⊢ ( ( 5 · 2 ) · 4 ) = ( 1 0 · 4 )
14 9 11 13 3eqtr2i ⊢ ( 5 · 8 ) = ( 1 0 · 4 )
15 cu2 ⊢ ( 2 ↑ 3 ) = 8
16 15 eqcomi ⊢ 8 = ( 2 ↑ 3 )
17 16 oveq2i ⊢ ( 5 · 8 ) = ( 5 · ( 2 ↑ 3 ) )
18 14 17 eqtr3i ⊢ ( 1 0 · 4 ) = ( 5 · ( 2 ↑ 3 ) )
19 18 oveq1i ⊢ ( ( 1 0 · 4 ) + 1 ) = ( ( 5 · ( 2 ↑ 3 ) ) + 1 )
20 1 3 19 3eqtri ⊢ 𝑃 = ( ( 5 · ( 2 ↑ 3 ) ) + 1 )
21 simpr ⊢ ( ( ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ∧ 𝑃 = ( ( 5 · ( 2 ↑ 3 ) ) + 1 ) ) → 𝑃 = ( ( 5 · ( 2 ↑ 3 ) ) + 1 ) )
22 3nn ⊢ 3 ∈ ℕ
23 22 a1i ⊢ ( ( ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ∧ 𝑃 = ( ( 5 · ( 2 ↑ 3 ) ) + 1 ) ) → 3 ∈ ℕ )
24 5nn ⊢ 5 ∈ ℕ
25 24 a1i ⊢ ( ( ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ∧ 𝑃 = ( ( 5 · ( 2 ↑ 3 ) ) + 1 ) ) → 5 ∈ ℕ )
26 5lt8 ⊢ 5 < 8
27 26 15 breqtrri ⊢ 5 < ( 2 ↑ 3 )
28 27 a1i ⊢ ( ( ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ∧ 𝑃 = ( ( 5 · ( 2 ↑ 3 ) ) + 1 ) ) → 5 < ( 2 ↑ 3 ) )
29 3z ⊢ 3 ∈ ℤ
30 29 a1i ⊢ ( ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) → 3 ∈ ℤ )
31 oveq1 ⊢ ( 𝑥 = 3 → ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) = ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) )
32 31 oveq1d ⊢ ( 𝑥 = 3 → ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) )
33 32 eqeq1d ⊢ ( 𝑥 = 3 → ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
34 33 adantl ⊢ ( ( ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ∧ 𝑥 = 3 ) → ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
35 id ⊢ ( ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) → ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
36 30 34 35 rspcedvd ⊢ ( ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) → ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
37 36 adantr ⊢ ( ( ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ∧ 𝑃 = ( ( 5 · ( 2 ↑ 3 ) ) + 1 ) ) → ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
38 23 25 21 28 37 proththd ⊢ ( ( ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ∧ 𝑃 = ( ( 5 · ( 2 ↑ 3 ) ) + 1 ) ) → 𝑃 ∈ ℙ )
39 21 38 jca ⊢ ( ( ( ( 3 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ∧ 𝑃 = ( ( 5 · ( 2 ↑ 3 ) ) + 1 ) ) → ( 𝑃 = ( ( 5 · ( 2 ↑ 3 ) ) + 1 ) ∧ 𝑃 ∈ ℙ ) )
40 2 20 39 mp2an ⊢ ( 𝑃 = ( ( 5 · ( 2 ↑ 3 ) ) + 1 ) ∧ 𝑃 ∈ ℙ )