| Step | Hyp | Ref
| Expression |
| 1 | | 8nn 12361 |
. . . . . 6
⊢ 8 ∈
ℕ |
| 2 | | nnrp 13046 |
. . . . . 6
⊢ (8 ∈
ℕ → 8 ∈ ℝ+) |
| 3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ 8 ∈
ℝ+ |
| 4 | | eqcom 2744 |
. . . . . 6
⊢ (𝑅 = (𝑁 mod 8) ↔ (𝑁 mod 8) = 𝑅) |
| 5 | | modmuladdim 13955 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 8 ∈
ℝ+) → ((𝑁 mod 8) = 𝑅 → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅))) |
| 6 | 4, 5 | biimtrid 242 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 8 ∈
ℝ+) → (𝑅 = (𝑁 mod 8) → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅))) |
| 7 | 3, 6 | mpan2 691 |
. . . 4
⊢ (𝑁 ∈ ℤ → (𝑅 = (𝑁 mod 8) → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅))) |
| 8 | 7 | imp 406 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑅 = (𝑁 mod 8)) → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅)) |
| 9 | 8 | 3adant2 1132 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅)) |
| 10 | | zcn 12618 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℂ) |
| 11 | | 8cn 12363 |
. . . . . . . . 9
⊢ 8 ∈
ℂ |
| 12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ → 8 ∈
ℂ) |
| 13 | 10, 12 | mulcomd 11282 |
. . . . . . 7
⊢ (𝑘 ∈ ℤ → (𝑘 · 8) = (8 · 𝑘)) |
| 14 | 13 | adantl 481 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (𝑘 · 8) = (8 · 𝑘)) |
| 15 | 14 | oveq1d 7446 |
. . . . 5
⊢ (((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → ((𝑘 · 8) + 𝑅) = ((8 · 𝑘) + 𝑅)) |
| 16 | 15 | eqeq2d 2748 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (𝑁 = ((𝑘 · 8) + 𝑅) ↔ 𝑁 = ((8 · 𝑘) + 𝑅))) |
| 17 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℤ) |
| 18 | 17 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → 𝑘 ∈ ℤ) |
| 19 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℤ) |
| 20 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → 8 ∈
ℕ) |
| 21 | 19, 20 | zmodcld 13932 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → (𝑁 mod 8) ∈
ℕ0) |
| 22 | 21 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑁 mod 8) ∈
ℤ) |
| 23 | 22 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑁 mod 8) ∈ ℤ) |
| 24 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑅 = (𝑁 mod 8) → (𝑅 ∈ ℤ ↔ (𝑁 mod 8) ∈ ℤ)) |
| 25 | 24 | 3ad2ant3 1136 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑅 ∈ ℤ ↔ (𝑁 mod 8) ∈ ℤ)) |
| 26 | 23, 25 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 𝑅 ∈ ℤ) |
| 27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → 𝑅 ∈ ℤ) |
| 28 | 27 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → 𝑅 ∈ ℤ) |
| 29 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → 𝑁 = ((8 · 𝑘) + 𝑅)) |
| 30 | | 2lgsoddprmlem1 27452 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (((𝑁↑2) − 1) / 8) = (((8 ·
(𝑘↑2)) + (2 ·
(𝑘 · 𝑅))) + (((𝑅↑2) − 1) / 8))) |
| 31 | 18, 28, 29, 30 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (((𝑁↑2) − 1) / 8) = (((8 ·
(𝑘↑2)) + (2 ·
(𝑘 · 𝑅))) + (((𝑅↑2) − 1) / 8))) |
| 32 | 31 | breq2d 5155 |
. . . . . 6
⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥
(((8 · (𝑘↑2)) +
(2 · (𝑘 ·
𝑅))) + (((𝑅↑2) − 1) / 8)))) |
| 33 | | 2z 12649 |
. . . . . . 7
⊢ 2 ∈
ℤ |
| 34 | | simp1 1137 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 𝑁 ∈ ℤ) |
| 35 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 8 ∈
ℕ) |
| 36 | 34, 35 | zmodcld 13932 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑁 mod 8) ∈
ℕ0) |
| 37 | 36 | nn0red 12588 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑁 mod 8) ∈ ℝ) |
| 38 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑅 = (𝑁 mod 8) → (𝑅 ∈ ℝ ↔ (𝑁 mod 8) ∈ ℝ)) |
| 39 | 38 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑅 ∈ ℝ ↔ (𝑁 mod 8) ∈ ℝ)) |
| 40 | 37, 39 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 𝑅 ∈ ℝ) |
| 41 | | resqcl 14164 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈
ℝ) |
| 42 | | peano2rem 11576 |
. . . . . . . . . . 11
⊢ ((𝑅↑2) ∈ ℝ →
((𝑅↑2) − 1)
∈ ℝ) |
| 43 | 41, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ → ((𝑅↑2) − 1) ∈
ℝ) |
| 44 | | 8re 12362 |
. . . . . . . . . . 11
⊢ 8 ∈
ℝ |
| 45 | 44 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ → 8 ∈
ℝ) |
| 46 | | 8pos 12378 |
. . . . . . . . . . . 12
⊢ 0 <
8 |
| 47 | 44, 46 | gt0ne0ii 11799 |
. . . . . . . . . . 11
⊢ 8 ≠
0 |
| 48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ → 8 ≠
0) |
| 49 | 43, 45, 48 | redivcld 12095 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ → (((𝑅↑2) − 1) / 8) ∈
ℝ) |
| 50 | 40, 49 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (((𝑅↑2) − 1) / 8) ∈
ℝ) |
| 51 | 50 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (((𝑅↑2) − 1) / 8) ∈
ℝ) |
| 52 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑅 = (𝑁 mod 8) → (𝑅 ∈ ℕ0 ↔ (𝑁 mod 8) ∈
ℕ0)) |
| 53 | 52 | 3ad2ant3 1136 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑅 ∈ ℕ0 ↔ (𝑁 mod 8) ∈
ℕ0)) |
| 54 | 36, 53 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 𝑅 ∈
ℕ0) |
| 55 | | nn0z 12638 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℕ0
→ 𝑅 ∈
ℤ) |
| 56 | 1 | nnzi 12641 |
. . . . . . . . . . . . . . . 16
⊢ 8 ∈
ℤ |
| 57 | 56 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 8 ∈
ℤ) |
| 58 | | zsqcl 14169 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℤ → (𝑘↑2) ∈
ℤ) |
| 59 | 58 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘↑2) ∈
ℤ) |
| 60 | 57, 59 | zmulcld 12728 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (8
· (𝑘↑2)) ∈
ℤ) |
| 61 | 33 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2 ∈
ℤ) |
| 62 | | zmulcl 12666 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑘 · 𝑅) ∈ ℤ) |
| 63 | 62 | ancoms 458 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑅) ∈ ℤ) |
| 64 | 61, 63 | zmulcld 12728 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2
· (𝑘 · 𝑅)) ∈
ℤ) |
| 65 | 60, 64 | zaddcld 12726 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((8
· (𝑘↑2)) + (2
· (𝑘 · 𝑅))) ∈
ℤ) |
| 66 | | 4z 12651 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ∈
ℤ |
| 67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 4 ∈
ℤ) |
| 68 | 67, 59 | zmulcld 12728 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (4
· (𝑘↑2)) ∈
ℤ) |
| 69 | 68, 63 | zaddcld 12726 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((4
· (𝑘↑2)) +
(𝑘 · 𝑅)) ∈
ℤ) |
| 70 | 61, 69 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2
∈ ℤ ∧ ((4 · (𝑘↑2)) + (𝑘 · 𝑅)) ∈ ℤ)) |
| 71 | | dvdsmul1 16315 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℤ ∧ ((4 · (𝑘↑2)) + (𝑘 · 𝑅)) ∈ ℤ) → 2 ∥ (2
· ((4 · (𝑘↑2)) + (𝑘 · 𝑅)))) |
| 72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2
∥ (2 · ((4 · (𝑘↑2)) + (𝑘 · 𝑅)))) |
| 73 | | 4t2e8 12434 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (4
· 2) = 8 |
| 74 | | 4cn 12351 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 4 ∈
ℂ |
| 75 | | 2cn 12341 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℂ |
| 76 | 74, 75 | mulcomi 11269 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (4
· 2) = (2 · 4) |
| 77 | 73, 76 | eqtr3i 2767 |
. . . . . . . . . . . . . . . . . . 19
⊢ 8 = (2
· 4) |
| 78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 8 = (2
· 4)) |
| 79 | 78 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (8
· (𝑘↑2)) = ((2
· 4) · (𝑘↑2))) |
| 80 | 75 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2 ∈
ℂ) |
| 81 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 4 ∈
ℂ) |
| 82 | 58 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℤ → (𝑘↑2) ∈
ℂ) |
| 83 | 82 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘↑2) ∈
ℂ) |
| 84 | 80, 81, 83 | mulassd 11284 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((2
· 4) · (𝑘↑2)) = (2 · (4 · (𝑘↑2)))) |
| 85 | 79, 84 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (8
· (𝑘↑2)) = (2
· (4 · (𝑘↑2)))) |
| 86 | 85 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((8
· (𝑘↑2)) + (2
· (𝑘 · 𝑅))) = ((2 · (4 ·
(𝑘↑2))) + (2 ·
(𝑘 · 𝑅)))) |
| 87 | 68 | zcnd 12723 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (4
· (𝑘↑2)) ∈
ℂ) |
| 88 | 62 | zcnd 12723 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑘 · 𝑅) ∈ ℂ) |
| 89 | 88 | ancoms 458 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑅) ∈ ℂ) |
| 90 | 80, 87, 89 | adddid 11285 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2
· ((4 · (𝑘↑2)) + (𝑘 · 𝑅))) = ((2 · (4 · (𝑘↑2))) + (2 · (𝑘 · 𝑅)))) |
| 91 | 86, 90 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((8
· (𝑘↑2)) + (2
· (𝑘 · 𝑅))) = (2 · ((4 ·
(𝑘↑2)) + (𝑘 · 𝑅)))) |
| 92 | 72, 91 | breqtrrd 5171 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2
∥ ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅)))) |
| 93 | 65, 92 | jca 511 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((8
· (𝑘↑2)) + (2
· (𝑘 · 𝑅))) ∈ ℤ ∧ 2
∥ ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))))) |
| 94 | 93 | ex 412 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℤ → (𝑘 ∈ ℤ → (((8
· (𝑘↑2)) + (2
· (𝑘 · 𝑅))) ∈ ℤ ∧ 2
∥ ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅)))))) |
| 95 | 55, 94 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℕ0
→ (𝑘 ∈ ℤ
→ (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) ∈ ℤ ∧ 2 ∥ ((8
· (𝑘↑2)) + (2
· (𝑘 · 𝑅)))))) |
| 96 | 54, 95 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑘 ∈ ℤ → (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) ∈ ℤ ∧ 2 ∥ ((8
· (𝑘↑2)) + (2
· (𝑘 · 𝑅)))))) |
| 97 | 96 | imp 406 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) ∈ ℤ ∧ 2 ∥ ((8
· (𝑘↑2)) + (2
· (𝑘 · 𝑅))))) |
| 98 | 97 | adantr 480 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) ∈ ℤ ∧ 2 ∥ ((8
· (𝑘↑2)) + (2
· (𝑘 · 𝑅))))) |
| 99 | | dvdsaddre2b 16344 |
. . . . . . 7
⊢ ((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 1470 |
. . . . . 6
⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (2 ∥ (((𝑅↑2) − 1) / 8) ↔ 2 ∥
(((8 · (𝑘↑2)) +
(2 · (𝑘 ·
𝑅))) + (((𝑅↑2) − 1) / 8)))) |
| 101 | 32, 100 | bitr4d 282 |
. . . . 5
⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥
(((𝑅↑2) − 1) /
8))) |
| 102 | 101 | ex 412 |
. . . 4
⊢ (((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (𝑁 = ((8 · 𝑘) + 𝑅) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥
(((𝑅↑2) − 1) /
8)))) |
| 103 | 16, 102 | sylbid 240 |
. . 3
⊢ (((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (𝑁 = ((𝑘 · 8) + 𝑅) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥
(((𝑅↑2) − 1) /
8)))) |
| 104 | 103 | rexlimdva 3155 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥
(((𝑅↑2) − 1) /
8)))) |
| 105 | 9, 104 | mpd 15 |
1
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔
2 ∥ (((𝑅↑2)
− 1) / 8))) |