Metamath Proof Explorer

Theorem 41prothprmlem1

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

Ref Expression
Hypothesis 41prothprm.p ⊢ 𝑃 = 4 1
Assertion 41prothprmlem1 ( ( 𝑃 − 1 ) / 2 ) = 2 0

Proof

Step Hyp Ref Expression
1 41prothprm.p ⊢ 𝑃 = 4 1
2 dfdec10 ⊢ 4 1 = ( ( 1 0 · 4 ) + 1 )
3 1 2 eqtri ⊢ 𝑃 = ( ( 1 0 · 4 ) + 1 )
4 3 oveq1i ⊢ ( 𝑃 − 1 ) = ( ( ( 1 0 · 4 ) + 1 ) − 1 )
5 10nn ⊢ 1 0 ∈ ℕ
6 5 nncni ⊢ 1 0 ∈ ℂ
7 4cn ⊢ 4 ∈ ℂ
8 6 7 mulcli ⊢ ( 1 0 · 4 ) ∈ ℂ
9 pncan1 ⊢ ( ( 1 0 · 4 ) ∈ ℂ → ( ( ( 1 0 · 4 ) + 1 ) − 1 ) = ( 1 0 · 4 ) )
10 8 9 ax-mp ⊢ ( ( ( 1 0 · 4 ) + 1 ) − 1 ) = ( 1 0 · 4 )
11 4 10 eqtri ⊢ ( 𝑃 − 1 ) = ( 1 0 · 4 )
12 11 oveq1i ⊢ ( ( 𝑃 − 1 ) / 2 ) = ( ( 1 0 · 4 ) / 2 )
13 2cn ⊢ 2 ∈ ℂ
14 2ne0 ⊢ 2 ≠ 0
15 6 7 13 14 divassi ⊢ ( ( 1 0 · 4 ) / 2 ) = ( 1 0 · ( 4 / 2 ) )
16 4d2e2 ⊢ ( 4 / 2 ) = 2
17 16 oveq2i ⊢ ( 1 0 · ( 4 / 2 ) ) = ( 1 0 · 2 )
18 2nn0 ⊢ 2 ∈ ℕ0
19 18 dec0u ⊢ ( 1 0 · 2 ) = 2 0
20 17 19 eqtri ⊢ ( 1 0 · ( 4 / 2 ) ) = 2 0
21 15 20 eqtri ⊢ ( ( 1 0 · 4 ) / 2 ) = 2 0
22 12 21 eqtri ⊢ ( ( 𝑃 − 1 ) / 2 ) = 2 0