Metamath Proof Explorer


Theorem 2lgslem3d1

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

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

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 ) = 7 -> E. k e. NN0 P = ( ( k x. 8 ) + 7 ) ) )
7 2 5 6 sylancl
 |-  ( P e. NN -> ( ( P mod 8 ) = 7 -> E. k e. NN0 P = ( ( k x. 8 ) + 7 ) ) )
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 ) + 7 ) = ( ( 8 x. k ) + 7 ) )
15 14 eqeq2d
 |-  ( ( P e. NN /\ k e. NN0 ) -> ( P = ( ( k x. 8 ) + 7 ) <-> P = ( ( 8 x. k ) + 7 ) ) )
16 15 biimpa
 |-  ( ( ( P e. NN /\ k e. NN0 ) /\ P = ( ( k x. 8 ) + 7 ) ) -> P = ( ( 8 x. k ) + 7 ) )
17 1 2lgslem3d
 |-  ( ( k e. NN0 /\ P = ( ( 8 x. k ) + 7 ) ) -> N = ( ( 2 x. k ) + 2 ) )
18 8 16 17 syl2an2r
 |-  ( ( ( P e. NN /\ k e. NN0 ) /\ P = ( ( k x. 8 ) + 7 ) ) -> N = ( ( 2 x. k ) + 2 ) )
19 oveq1
 |-  ( N = ( ( 2 x. k ) + 2 ) -> ( N mod 2 ) = ( ( ( 2 x. k ) + 2 ) mod 2 ) )
20 2t1e2
 |-  ( 2 x. 1 ) = 2
21 20 eqcomi
 |-  2 = ( 2 x. 1 )
22 21 a1i
 |-  ( k e. NN0 -> 2 = ( 2 x. 1 ) )
23 22 oveq2d
 |-  ( k e. NN0 -> ( ( 2 x. k ) + 2 ) = ( ( 2 x. k ) + ( 2 x. 1 ) ) )
24 2cnd
 |-  ( k e. NN0 -> 2 e. CC )
25 1cnd
 |-  ( k e. NN0 -> 1 e. CC )
26 adddi
 |-  ( ( 2 e. CC /\ k e. CC /\ 1 e. CC ) -> ( 2 x. ( k + 1 ) ) = ( ( 2 x. k ) + ( 2 x. 1 ) ) )
27 26 eqcomd
 |-  ( ( 2 e. CC /\ k e. CC /\ 1 e. CC ) -> ( ( 2 x. k ) + ( 2 x. 1 ) ) = ( 2 x. ( k + 1 ) ) )
28 24 9 25 27 syl3anc
 |-  ( k e. NN0 -> ( ( 2 x. k ) + ( 2 x. 1 ) ) = ( 2 x. ( k + 1 ) ) )
29 9 25 addcld
 |-  ( k e. NN0 -> ( k + 1 ) e. CC )
30 24 29 mulcomd
 |-  ( k e. NN0 -> ( 2 x. ( k + 1 ) ) = ( ( k + 1 ) x. 2 ) )
31 23 28 30 3eqtrd
 |-  ( k e. NN0 -> ( ( 2 x. k ) + 2 ) = ( ( k + 1 ) x. 2 ) )
32 31 oveq1d
 |-  ( k e. NN0 -> ( ( ( 2 x. k ) + 2 ) mod 2 ) = ( ( ( k + 1 ) x. 2 ) mod 2 ) )
33 peano2nn0
 |-  ( k e. NN0 -> ( k + 1 ) e. NN0 )
34 33 nn0zd
 |-  ( k e. NN0 -> ( k + 1 ) e. ZZ )
35 2rp
 |-  2 e. RR+
36 mulmod0
 |-  ( ( ( k + 1 ) e. ZZ /\ 2 e. RR+ ) -> ( ( ( k + 1 ) x. 2 ) mod 2 ) = 0 )
37 34 35 36 sylancl
 |-  ( k e. NN0 -> ( ( ( k + 1 ) x. 2 ) mod 2 ) = 0 )
38 32 37 eqtrd
 |-  ( k e. NN0 -> ( ( ( 2 x. k ) + 2 ) mod 2 ) = 0 )
39 19 38 sylan9eqr
 |-  ( ( k e. NN0 /\ N = ( ( 2 x. k ) + 2 ) ) -> ( N mod 2 ) = 0 )
40 8 18 39 syl2an2r
 |-  ( ( ( P e. NN /\ k e. NN0 ) /\ P = ( ( k x. 8 ) + 7 ) ) -> ( N mod 2 ) = 0 )
41 40 rexlimdva2
 |-  ( P e. NN -> ( E. k e. NN0 P = ( ( k x. 8 ) + 7 ) -> ( N mod 2 ) = 0 ) )
42 7 41 syld
 |-  ( P e. NN -> ( ( P mod 8 ) = 7 -> ( N mod 2 ) = 0 ) )
43 42 imp
 |-  ( ( P e. NN /\ ( P mod 8 ) = 7 ) -> ( N mod 2 ) = 0 )