Metamath Proof Explorer

Theorem 2lgslem3a1

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

Ref Expression
Hypothesis 2lgslem2.n โŠข ๐‘ = ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) )
Assertion 2lgslem3a1 ( ( ๐‘ƒ โˆˆ โ„• โˆง ( ๐‘ƒ mod 8 ) = 1 ) โ†’ ( ๐‘ mod 2 ) = 0 )

Proof

Step Hyp Ref Expression
1 2lgslem2.n โŠข ๐‘ = ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) )
2 nnnn0 โŠข ( ๐‘ƒ โˆˆ โ„• โ†’ ๐‘ƒ โˆˆ โ„•0 )
3 8nn โŠข 8 โˆˆ โ„•
4 nnrp โŠข ( 8 โˆˆ โ„• โ†’ 8 โˆˆ โ„+ )
5 3 4 ax-mp โŠข 8 โˆˆ โ„+
6 modmuladdnn0 โŠข ( ( ๐‘ƒ โˆˆ โ„•0 โˆง 8 โˆˆ โ„+ ) โ†’ ( ( ๐‘ƒ mod 8 ) = 1 โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ƒ = ( ( ๐‘˜ ยท 8 ) + 1 ) ) )
7 2 5 6 sylancl โŠข ( ๐‘ƒ โˆˆ โ„• โ†’ ( ( ๐‘ƒ mod 8 ) = 1 โ†’ โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ƒ = ( ( ๐‘˜ ยท 8 ) + 1 ) ) )
8 simpr โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ๐‘˜ โˆˆ โ„•0 )
9 nn0cn โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„‚ )
10 8cn โŠข 8 โˆˆ โ„‚
11 10 a1i โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ 8 โˆˆ โ„‚ )
12 9 11 mulcomd โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ๐‘˜ ยท 8 ) = ( 8 ยท ๐‘˜ ) )
13 12 adantl โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘˜ ยท 8 ) = ( 8 ยท ๐‘˜ ) )
14 13 oveq1d โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘˜ ยท 8 ) + 1 ) = ( ( 8 ยท ๐‘˜ ) + 1 ) )
15 14 eqeq2d โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘ƒ = ( ( ๐‘˜ ยท 8 ) + 1 ) โ†” ๐‘ƒ = ( ( 8 ยท ๐‘˜ ) + 1 ) ) )
16 15 biimpa โŠข ( ( ( ๐‘ƒ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘ƒ = ( ( ๐‘˜ ยท 8 ) + 1 ) ) โ†’ ๐‘ƒ = ( ( 8 ยท ๐‘˜ ) + 1 ) )
17 1 2lgslem3a โŠข ( ( ๐‘˜ โˆˆ โ„•0 โˆง ๐‘ƒ = ( ( 8 ยท ๐‘˜ ) + 1 ) ) โ†’ ๐‘ = ( 2 ยท ๐‘˜ ) )
18 8 16 17 syl2an2r โŠข ( ( ( ๐‘ƒ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘ƒ = ( ( ๐‘˜ ยท 8 ) + 1 ) ) โ†’ ๐‘ = ( 2 ยท ๐‘˜ ) )
19 oveq1 โŠข ( ๐‘ = ( 2 ยท ๐‘˜ ) โ†’ ( ๐‘ mod 2 ) = ( ( 2 ยท ๐‘˜ ) mod 2 ) )
20 2cnd โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ 2 โˆˆ โ„‚ )
21 20 9 mulcomd โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( 2 ยท ๐‘˜ ) = ( ๐‘˜ ยท 2 ) )
22 21 oveq1d โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ( 2 ยท ๐‘˜ ) mod 2 ) = ( ( ๐‘˜ ยท 2 ) mod 2 ) )
23 nn0z โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„ค )
24 2rp โŠข 2 โˆˆ โ„+
25 mulmod0 โŠข ( ( ๐‘˜ โˆˆ โ„ค โˆง 2 โˆˆ โ„+ ) โ†’ ( ( ๐‘˜ ยท 2 ) mod 2 ) = 0 )
26 23 24 25 sylancl โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ( ๐‘˜ ยท 2 ) mod 2 ) = 0 )
27 22 26 eqtrd โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ( 2 ยท ๐‘˜ ) mod 2 ) = 0 )
28 19 27 sylan9eqr โŠข ( ( ๐‘˜ โˆˆ โ„•0 โˆง ๐‘ = ( 2 ยท ๐‘˜ ) ) โ†’ ( ๐‘ mod 2 ) = 0 )
29 8 18 28 syl2an2r โŠข ( ( ( ๐‘ƒ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘ƒ = ( ( ๐‘˜ ยท 8 ) + 1 ) ) โ†’ ( ๐‘ mod 2 ) = 0 )
30 29 rexlimdva2 โŠข ( ๐‘ƒ โˆˆ โ„• โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„•0 ๐‘ƒ = ( ( ๐‘˜ ยท 8 ) + 1 ) โ†’ ( ๐‘ mod 2 ) = 0 ) )
31 7 30 syld โŠข ( ๐‘ƒ โˆˆ โ„• โ†’ ( ( ๐‘ƒ mod 8 ) = 1 โ†’ ( ๐‘ mod 2 ) = 0 ) )
32 31 imp โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ( ๐‘ƒ mod 8 ) = 1 ) โ†’ ( ๐‘ mod 2 ) = 0 )