# Metamath Proof Explorer

## Theorem 2lgsoddprmlem2

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

Ref Expression
Assertion 2lgsoddprmlem2 ${⊢}\left({N}\in ℤ\wedge ¬2\parallel {N}\wedge {R}={N}\mathrm{mod}8\right)\to \left(2\parallel \left(\frac{{{N}}^{2}-1}{8}\right)↔2\parallel \left(\frac{{{R}}^{2}-1}{8}\right)\right)$

### Proof

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