Metamath Proof Explorer

Theorem 41prothprmlem1

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

Ref Expression
Hypothesis 41prothprm.p 
|- P = ; 4 1
Assertion 41prothprmlem1 
|- ( ( P - 1 ) / 2 ) = ; 2 0

Proof

Step Hyp Ref Expression
1 41prothprm.p 
 |-  P = ; 4 1
2 dfdec10 
 |-  ; 4 1 = ( ( ; 1 0 x. 4 ) + 1 )
3 1 2 eqtri 
 |-  P = ( ( ; 1 0 x. 4 ) + 1 )
4 3 oveq1i 
 |-  ( P - 1 ) = ( ( ( ; 1 0 x. 4 ) + 1 ) - 1 )
5 10nn 
 |-  ; 1 0 e. NN
6 5 nncni 
 |-  ; 1 0 e. CC
7 4cn 
 |-  4 e. CC
8 6 7 mulcli 
 |-  ( ; 1 0 x. 4 ) e. CC
9 pncan1 
 |-  ( ( ; 1 0 x. 4 ) e. CC -> ( ( ( ; 1 0 x. 4 ) + 1 ) - 1 ) = ( ; 1 0 x. 4 ) )
10 8 9 ax-mp 
 |-  ( ( ( ; 1 0 x. 4 ) + 1 ) - 1 ) = ( ; 1 0 x. 4 )
11 4 10 eqtri 
 |-  ( P - 1 ) = ( ; 1 0 x. 4 )
12 11 oveq1i 
 |-  ( ( P - 1 ) / 2 ) = ( ( ; 1 0 x. 4 ) / 2 )
13 2cn 
 |-  2 e. CC
14 2ne0 
 |-  2 =/= 0
15 6 7 13 14 divassi 
 |-  ( ( ; 1 0 x. 4 ) / 2 ) = ( ; 1 0 x. ( 4 / 2 ) )
16 4d2e2 
 |-  ( 4 / 2 ) = 2
17 16 oveq2i 
 |-  ( ; 1 0 x. ( 4 / 2 ) ) = ( ; 1 0 x. 2 )
18 2nn0 
 |-  2 e. NN0
19 18 dec0u 
 |-  ( ; 1 0 x. 2 ) = ; 2 0
20 17 19 eqtri 
 |-  ( ; 1 0 x. ( 4 / 2 ) ) = ; 2 0
21 15 20 eqtri 
 |-  ( ( ; 1 0 x. 4 ) / 2 ) = ; 2 0
22 12 21 eqtri 
 |-  ( ( P - 1 ) / 2 ) = ; 2 0