Metamath Proof Explorer

Theorem 2lgslem3c1

Description: Lemma 3 for 2lgslem3 . (Contributed by AV, 16-Jul-2021)

Ref Expression
Hypothesis 2lgslem2.n 
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )
Assertion 2lgslem3c1 
|- ( ( P e. NN /\ ( P mod 8 ) = 5 ) -> ( N mod 2 ) = 1 )

Proof

Step Hyp Ref Expression
1 2lgslem2.n 
 |-  N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )
2 nnnn0 
 |-  ( P e. NN -> P e. NN0 )
3 8nn 
 |-  8 e. NN
4 nnrp 
 |-  ( 8 e. NN -> 8 e. RR+ )
5 3 4 ax-mp 
 |-  8 e. RR+
6 modmuladdnn0 
 |-  ( ( P e. NN0 /\ 8 e. RR+ ) -> ( ( P mod 8 ) = 5 -> E. k e. NN0 P = ( ( k x. 8 ) + 5 ) ) )
7 2 5 6 sylancl 
 |-  ( P e. NN -> ( ( P mod 8 ) = 5 -> E. k e. NN0 P = ( ( k x. 8 ) + 5 ) ) )
8 simpr 
 |-  ( ( P e. NN /\ k e. NN0 ) -> k e. NN0 )
9 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
10 8cn 
 |-  8 e. CC
11 10 a1i 
 |-  ( k e. NN0 -> 8 e. CC )
12 9 11 mulcomd 
 |-  ( k e. NN0 -> ( k x. 8 ) = ( 8 x. k ) )
13 12 adantl 
 |-  ( ( P e. NN /\ k e. NN0 ) -> ( k x. 8 ) = ( 8 x. k ) )
14 13 oveq1d 
 |-  ( ( P e. NN /\ k e. NN0 ) -> ( ( k x. 8 ) + 5 ) = ( ( 8 x. k ) + 5 ) )
15 14 eqeq2d 
 |-  ( ( P e. NN /\ k e. NN0 ) -> ( P = ( ( k x. 8 ) + 5 ) <-> P = ( ( 8 x. k ) + 5 ) ) )
16 15 biimpa 
 |-  ( ( ( P e. NN /\ k e. NN0 ) /\ P = ( ( k x. 8 ) + 5 ) ) -> P = ( ( 8 x. k ) + 5 ) )
17 1 2lgslem3c 
 |-  ( ( k e. NN0 /\ P = ( ( 8 x. k ) + 5 ) ) -> N = ( ( 2 x. k ) + 1 ) )
18 8 16 17 syl2an2r 
 |-  ( ( ( P e. NN /\ k e. NN0 ) /\ P = ( ( k x. 8 ) + 5 ) ) -> N = ( ( 2 x. k ) + 1 ) )
19 oveq1 
 |-  ( N = ( ( 2 x. k ) + 1 ) -> ( N mod 2 ) = ( ( ( 2 x. k ) + 1 ) mod 2 ) )
20 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
21 eqidd 
 |-  ( k e. NN0 -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. k ) + 1 ) )
22 2tp1odd 
 |-  ( ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = ( ( 2 x. k ) + 1 ) ) -> -. 2 || ( ( 2 x. k ) + 1 ) )
23 20 21 22 syl2anc 
 |-  ( k e. NN0 -> -. 2 || ( ( 2 x. k ) + 1 ) )
24 2z 
 |-  2 e. ZZ
25 24 a1i 
 |-  ( k e. NN0 -> 2 e. ZZ )
26 25 20 zmulcld 
 |-  ( k e. NN0 -> ( 2 x. k ) e. ZZ )
27 26 peano2zd 
 |-  ( k e. NN0 -> ( ( 2 x. k ) + 1 ) e. ZZ )
28 mod2eq1n2dvds 
 |-  ( ( ( 2 x. k ) + 1 ) e. ZZ -> ( ( ( ( 2 x. k ) + 1 ) mod 2 ) = 1 <-> -. 2 || ( ( 2 x. k ) + 1 ) ) )
29 27 28 syl 
 |-  ( k e. NN0 -> ( ( ( ( 2 x. k ) + 1 ) mod 2 ) = 1 <-> -. 2 || ( ( 2 x. k ) + 1 ) ) )
30 23 29 mpbird 
 |-  ( k e. NN0 -> ( ( ( 2 x. k ) + 1 ) mod 2 ) = 1 )
31 19 30 sylan9eqr 
 |-  ( ( k e. NN0 /\ N = ( ( 2 x. k ) + 1 ) ) -> ( N mod 2 ) = 1 )
32 8 18 31 syl2an2r 
 |-  ( ( ( P e. NN /\ k e. NN0 ) /\ P = ( ( k x. 8 ) + 5 ) ) -> ( N mod 2 ) = 1 )
33 32 rexlimdva2 
 |-  ( P e. NN -> ( E. k e. NN0 P = ( ( k x. 8 ) + 5 ) -> ( N mod 2 ) = 1 ) )
34 7 33 syld 
 |-  ( P e. NN -> ( ( P mod 8 ) = 5 -> ( N mod 2 ) = 1 ) )
35 34 imp 
 |-  ( ( P e. NN /\ ( P mod 8 ) = 5 ) -> ( N mod 2 ) = 1 )