Metamath Proof Explorer

Theorem 2lgsoddprmlem2

Description: Lemma 2 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021)

Ref Expression
Assertion 2lgsoddprmlem2 
|- ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) ) )

Proof

Step Hyp Ref Expression
1 8nn 
 |-  8 e. NN
2 nnrp 
 |-  ( 8 e. NN -> 8 e. RR+ )
3 1 2 ax-mp 
 |-  8 e. RR+
4 eqcom 
 |-  ( R = ( N mod 8 ) <-> ( N mod 8 ) = R )
5 modmuladdim 
 |-  ( ( N e. ZZ /\ 8 e. RR+ ) -> ( ( N mod 8 ) = R -> E. k e. ZZ N = ( ( k x. 8 ) + R ) ) )
6 4 5 biimtrid 
 |-  ( ( N e. ZZ /\ 8 e. RR+ ) -> ( R = ( N mod 8 ) -> E. k e. ZZ N = ( ( k x. 8 ) + R ) ) )
7 3 6 mpan2 
 |-  ( N e. ZZ -> ( R = ( N mod 8 ) -> E. k e. ZZ N = ( ( k x. 8 ) + R ) ) )
8 7 imp 
 |-  ( ( N e. ZZ /\ R = ( N mod 8 ) ) -> E. k e. ZZ N = ( ( k x. 8 ) + R ) )
9 8 3adant2 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> E. k e. ZZ N = ( ( k x. 8 ) + R ) )
10 zcn 
 |-  ( k e. ZZ -> k e. CC )
11 8cn 
 |-  8 e. CC
12 11 a1i 
 |-  ( k e. ZZ -> 8 e. CC )
13 10 12 mulcomd 
 |-  ( k e. ZZ -> ( k x. 8 ) = ( 8 x. k ) )
14 13 adantl 
 |-  ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) -> ( k x. 8 ) = ( 8 x. k ) )
15 14 oveq1d 
 |-  ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) -> ( ( k x. 8 ) + R ) = ( ( 8 x. k ) + R ) )
16 15 eqeq2d 
 |-  ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) -> ( N = ( ( k x. 8 ) + R ) <-> N = ( ( 8 x. k ) + R ) ) )
17 simpr 
 |-  ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) -> k e. ZZ )
18 17 adantr 
 |-  ( ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) /\ N = ( ( 8 x. k ) + R ) ) -> k e. ZZ )
19 id 
 |-  ( N e. ZZ -> N e. ZZ )
20 1 a1i 
 |-  ( N e. ZZ -> 8 e. NN )
21 19 20 zmodcld 
 |-  ( N e. ZZ -> ( N mod 8 ) e. NN0 )
22 21 nn0zd 
 |-  ( N e. ZZ -> ( N mod 8 ) e. ZZ )
23 22 3ad2ant1 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( N mod 8 ) e. ZZ )
24 eleq1 
 |-  ( R = ( N mod 8 ) -> ( R e. ZZ <-> ( N mod 8 ) e. ZZ ) )
25 24 3ad2ant3 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( R e. ZZ <-> ( N mod 8 ) e. ZZ ) )
26 23 25 mpbird 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> R e. ZZ )
27 26 adantr 
 |-  ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) -> R e. ZZ )
28 27 adantr 
 |-  ( ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) /\ N = ( ( 8 x. k ) + R ) ) -> R e. ZZ )
29 simpr 
 |-  ( ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) /\ N = ( ( 8 x. k ) + R ) ) -> N = ( ( 8 x. k ) + R ) )
30 2lgsoddprmlem1 
 |-  ( ( k e. ZZ /\ R e. ZZ /\ N = ( ( 8 x. k ) + R ) ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) = ( ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) + ( ( ( R ^ 2 ) - 1 ) / 8 ) ) )
31 18 28 29 30 syl3anc 
 |-  ( ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) /\ N = ( ( 8 x. k ) + R ) ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) = ( ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) + ( ( ( R ^ 2 ) - 1 ) / 8 ) ) )
32 31 breq2d 
 |-  ( ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) /\ N = ( ( 8 x. k ) + R ) ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) + ( ( ( R ^ 2 ) - 1 ) / 8 ) ) ) )
33 2z 
 |-  2 e. ZZ
34 simp1 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> N e. ZZ )
35 1 a1i 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> 8 e. NN )
36 34 35 zmodcld 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( N mod 8 ) e. NN0 )
37 36 nn0red 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( N mod 8 ) e. RR )
38 eleq1 
 |-  ( R = ( N mod 8 ) -> ( R e. RR <-> ( N mod 8 ) e. RR ) )
39 38 3ad2ant3 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( R e. RR <-> ( N mod 8 ) e. RR ) )
40 37 39 mpbird 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> R e. RR )
41 resqcl 
 |-  ( R e. RR -> ( R ^ 2 ) e. RR )
42 peano2rem 
 |-  ( ( R ^ 2 ) e. RR -> ( ( R ^ 2 ) - 1 ) e. RR )
43 41 42 syl 
 |-  ( R e. RR -> ( ( R ^ 2 ) - 1 ) e. RR )
44 8re 
 |-  8 e. RR
45 44 a1i 
 |-  ( R e. RR -> 8 e. RR )
46 8pos 
 |-  0 < 8
47 44 46 gt0ne0ii 
 |-  8 =/= 0
48 47 a1i 
 |-  ( R e. RR -> 8 =/= 0 )
49 43 45 48 redivcld 
 |-  ( R e. RR -> ( ( ( R ^ 2 ) - 1 ) / 8 ) e. RR )
50 40 49 syl 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( ( ( R ^ 2 ) - 1 ) / 8 ) e. RR )
51 50 adantr 
 |-  ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) -> ( ( ( R ^ 2 ) - 1 ) / 8 ) e. RR )
52 eleq1 
 |-  ( R = ( N mod 8 ) -> ( R e. NN0 <-> ( N mod 8 ) e. NN0 ) )
53 52 3ad2ant3 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( R e. NN0 <-> ( N mod 8 ) e. NN0 ) )
54 36 53 mpbird 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> R e. NN0 )
55 nn0z 
 |-  ( R e. NN0 -> R e. ZZ )
56 1 nnzi 
 |-  8 e. ZZ
57 56 a1i 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> 8 e. ZZ )
58 zsqcl 
 |-  ( k e. ZZ -> ( k ^ 2 ) e. ZZ )
59 58 adantl 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( k ^ 2 ) e. ZZ )
60 57 59 zmulcld 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( 8 x. ( k ^ 2 ) ) e. ZZ )
61 33 a1i 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> 2 e. ZZ )
62 zmulcl 
 |-  ( ( k e. ZZ /\ R e. ZZ ) -> ( k x. R ) e. ZZ )
63 62 ancoms 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( k x. R ) e. ZZ )
64 61 63 zmulcld 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( 2 x. ( k x. R ) ) e. ZZ )
65 60 64 zaddcld 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) e. ZZ )
66 4z 
 |-  4 e. ZZ
67 66 a1i 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> 4 e. ZZ )
68 67 59 zmulcld 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( 4 x. ( k ^ 2 ) ) e. ZZ )
69 68 63 zaddcld 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( ( 4 x. ( k ^ 2 ) ) + ( k x. R ) ) e. ZZ )
70 61 69 jca 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( 2 e. ZZ /\ ( ( 4 x. ( k ^ 2 ) ) + ( k x. R ) ) e. ZZ ) )
71 dvdsmul1 
 |-  ( ( 2 e. ZZ /\ ( ( 4 x. ( k ^ 2 ) ) + ( k x. R ) ) e. ZZ ) -> 2 || ( 2 x. ( ( 4 x. ( k ^ 2 ) ) + ( k x. R ) ) ) )
72 70 71 syl 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> 2 || ( 2 x. ( ( 4 x. ( k ^ 2 ) ) + ( k x. R ) ) ) )
73 4t2e8 
 |-  ( 4 x. 2 ) = 8
74 4cn 
 |-  4 e. CC
75 2cn 
 |-  2 e. CC
76 74 75 mulcomi 
 |-  ( 4 x. 2 ) = ( 2 x. 4 )
77 73 76 eqtr3i 
 |-  8 = ( 2 x. 4 )
78 77 a1i 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> 8 = ( 2 x. 4 ) )
79 78 oveq1d 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( 8 x. ( k ^ 2 ) ) = ( ( 2 x. 4 ) x. ( k ^ 2 ) ) )
80 75 a1i 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> 2 e. CC )
81 74 a1i 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> 4 e. CC )
82 58 zcnd 
 |-  ( k e. ZZ -> ( k ^ 2 ) e. CC )
83 82 adantl 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( k ^ 2 ) e. CC )
84 80 81 83 mulassd 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( ( 2 x. 4 ) x. ( k ^ 2 ) ) = ( 2 x. ( 4 x. ( k ^ 2 ) ) ) )
85 79 84 eqtrd 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( 8 x. ( k ^ 2 ) ) = ( 2 x. ( 4 x. ( k ^ 2 ) ) ) )
86 85 oveq1d 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) = ( ( 2 x. ( 4 x. ( k ^ 2 ) ) ) + ( 2 x. ( k x. R ) ) ) )
87 68 zcnd 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( 4 x. ( k ^ 2 ) ) e. CC )
88 62 zcnd 
 |-  ( ( k e. ZZ /\ R e. ZZ ) -> ( k x. R ) e. CC )
89 88 ancoms 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( k x. R ) e. CC )
90 80 87 89 adddid 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( 2 x. ( ( 4 x. ( k ^ 2 ) ) + ( k x. R ) ) ) = ( ( 2 x. ( 4 x. ( k ^ 2 ) ) ) + ( 2 x. ( k x. R ) ) ) )
91 86 90 eqtr4d 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) = ( 2 x. ( ( 4 x. ( k ^ 2 ) ) + ( k x. R ) ) ) )
92 72 91 breqtrrd 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> 2 || ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) )
93 65 92 jca 
 |-  ( ( R e. ZZ /\ k e. ZZ ) -> ( ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) e. ZZ /\ 2 || ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) ) )
94 93 ex 
 |-  ( R e. ZZ -> ( k e. ZZ -> ( ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) e. ZZ /\ 2 || ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) ) ) )
95 55 94 syl 
 |-  ( R e. NN0 -> ( k e. ZZ -> ( ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) e. ZZ /\ 2 || ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) ) ) )
96 54 95 syl 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( k e. ZZ -> ( ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) e. ZZ /\ 2 || ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) ) ) )
97 96 imp 
 |-  ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) -> ( ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) e. ZZ /\ 2 || ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) ) )
98 97 adantr 
 |-  ( ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) /\ N = ( ( 8 x. k ) + R ) ) -> ( ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) e. ZZ /\ 2 || ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) ) )
99 dvdsaddre2b 
 |-  ( ( 2 e. ZZ /\ ( ( ( R ^ 2 ) - 1 ) / 8 ) e. RR /\ ( ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) e. ZZ /\ 2 || ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) ) ) -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) + ( ( ( R ^ 2 ) - 1 ) / 8 ) ) ) )
100 33 51 98 99 mp3an2ani 
 |-  ( ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) /\ N = ( ( 8 x. k ) + R ) ) -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( 8 x. ( k ^ 2 ) ) + ( 2 x. ( k x. R ) ) ) + ( ( ( R ^ 2 ) - 1 ) / 8 ) ) ) )
101 32 100 bitr4d 
 |-  ( ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) /\ N = ( ( 8 x. k ) + R ) ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) ) )
102 101 ex 
 |-  ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) -> ( N = ( ( 8 x. k ) + R ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) ) ) )
103 16 102 sylbid 
 |-  ( ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) /\ k e. ZZ ) -> ( N = ( ( k x. 8 ) + R ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) ) ) )
104 103 rexlimdva 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( E. k e. ZZ N = ( ( k x. 8 ) + R ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) ) ) )
105 9 104 mpd 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) ) )