Metamath Proof Explorer

Theorem 2lgsoddprmlem2

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

Ref Expression
Assertion 2lgsoddprmlem2 ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = ( 𝑁 mod 8 ) ) → ( 2 ∥ ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) ↔ 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) ) )

Proof

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