| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 4nn 12350 | . . . . 5
⊢ 4 ∈
ℕ | 
| 2 | 1 | a1i 11 | . . . 4
⊢ (𝑁 ∈ ℤ → 4 ∈
ℕ) | 
| 3 |  | 3nn0 12546 | . . . . . 6
⊢ 3 ∈
ℕ0 | 
| 4 | 3 | a1i 11 | . . . . 5
⊢ (𝑁 ∈ ℤ → 3 ∈
ℕ0) | 
| 5 |  | 3lt4 12441 | . . . . 5
⊢ 3 <
4 | 
| 6 | 4, 5 | jctir 520 | . . . 4
⊢ (𝑁 ∈ ℤ → (3 ∈
ℕ0 ∧ 3 < 4)) | 
| 7 |  | modremain 16446 | . . . 4
⊢ ((𝑁 ∈ ℤ ∧ 4 ∈
ℕ ∧ (3 ∈ ℕ0 ∧ 3 < 4)) → ((𝑁 mod 4) = 3 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 4) + 3) = 𝑁)) | 
| 8 | 2, 6, 7 | mpd3an23 1464 | . . 3
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 4) = 3 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 4) + 3) = 𝑁)) | 
| 9 |  | 2cnd 12345 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 2 ∈
ℂ) | 
| 10 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 𝑧 ∈
ℤ) | 
| 11 |  | 4z 12653 | . . . . . . . . . . . . . 14
⊢ 4 ∈
ℤ | 
| 12 | 11 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 4 ∈
ℤ) | 
| 13 | 10, 12 | zmulcld 12730 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑧 · 4) ∈
ℤ) | 
| 14 | 13 | zcnd 12725 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑧 · 4) ∈
ℂ) | 
| 15 |  | 3cn 12348 | . . . . . . . . . . . 12
⊢ 3 ∈
ℂ | 
| 16 | 15 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 3 ∈
ℂ) | 
| 17 | 9, 14, 16 | adddid 11286 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (2
· ((𝑧 · 4) +
3)) = ((2 · (𝑧
· 4)) + (2 · 3))) | 
| 18 | 10 | zcnd 12725 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 𝑧 ∈
ℂ) | 
| 19 |  | 4cn 12352 | . . . . . . . . . . . . . 14
⊢ 4 ∈
ℂ | 
| 20 | 19 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 4 ∈
ℂ) | 
| 21 | 9, 18, 20 | mul12d 11471 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (2
· (𝑧 · 4)) =
(𝑧 · (2 ·
4))) | 
| 22 |  | 2cn 12342 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ | 
| 23 |  | 4t2e8 12435 | . . . . . . . . . . . . . 14
⊢ (4
· 2) = 8 | 
| 24 | 19, 22, 23 | mulcomli 11271 | . . . . . . . . . . . . 13
⊢ (2
· 4) = 8 | 
| 25 | 24 | oveq2i 7443 | . . . . . . . . . . . 12
⊢ (𝑧 · (2 · 4)) =
(𝑧 ·
8) | 
| 26 | 21, 25 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (2
· (𝑧 · 4)) =
(𝑧 ·
8)) | 
| 27 |  | 3t2e6 12433 | . . . . . . . . . . . . 13
⊢ (3
· 2) = 6 | 
| 28 | 15, 22, 27 | mulcomli 11271 | . . . . . . . . . . . 12
⊢ (2
· 3) = 6 | 
| 29 | 28 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (2
· 3) = 6) | 
| 30 | 26, 29 | oveq12d 7450 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((2
· (𝑧 · 4)) +
(2 · 3)) = ((𝑧
· 8) + 6)) | 
| 31 | 17, 30 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (2
· ((𝑧 · 4) +
3)) = ((𝑧 · 8) +
6)) | 
| 32 | 31 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((2
· ((𝑧 · 4) +
3)) + 1) = (((𝑧 · 8)
+ 6) + 1)) | 
| 33 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℤ) | 
| 34 |  | 8nn 12362 | . . . . . . . . . . . . . . 15
⊢ 8 ∈
ℕ | 
| 35 | 34 | nnzi 12643 | . . . . . . . . . . . . . 14
⊢ 8 ∈
ℤ | 
| 36 | 35 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℤ → 8 ∈
ℤ) | 
| 37 | 33, 36 | zmulcld 12730 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ ℤ → (𝑧 · 8) ∈
ℤ) | 
| 38 | 37 | zcnd 12725 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℤ → (𝑧 · 8) ∈
ℂ) | 
| 39 |  | 6cn 12358 | . . . . . . . . . . . 12
⊢ 6 ∈
ℂ | 
| 40 | 39 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℤ → 6 ∈
ℂ) | 
| 41 |  | 1cnd 11257 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℤ → 1 ∈
ℂ) | 
| 42 | 38, 40, 41 | addassd 11284 | . . . . . . . . . 10
⊢ (𝑧 ∈ ℤ → (((𝑧 · 8) + 6) + 1) = ((𝑧 · 8) + (6 +
1))) | 
| 43 |  | 6p1e7 12415 | . . . . . . . . . . . 12
⊢ (6 + 1) =
7 | 
| 44 | 43 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℤ → (6 + 1) =
7) | 
| 45 | 44 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑧 ∈ ℤ → ((𝑧 · 8) + (6 + 1)) =
((𝑧 · 8) +
7)) | 
| 46 | 42, 45 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝑧 ∈ ℤ → (((𝑧 · 8) + 6) + 1) = ((𝑧 · 8) +
7)) | 
| 47 | 46 | adantl 481 | . . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((𝑧 · 8) + 6) + 1) = ((𝑧 · 8) +
7)) | 
| 48 | 32, 47 | eqtrd 2776 | . . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((2
· ((𝑧 · 4) +
3)) + 1) = ((𝑧 · 8)
+ 7)) | 
| 49 | 48 | oveq1d 7447 | . . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((2
· ((𝑧 · 4) +
3)) + 1) mod 8) = (((𝑧
· 8) + 7) mod 8)) | 
| 50 |  | nnrp 13047 | . . . . . . . . 9
⊢ (8 ∈
ℕ → 8 ∈ ℝ+) | 
| 51 | 34, 50 | mp1i 13 | . . . . . . . 8
⊢ (𝑧 ∈ ℤ → 8 ∈
ℝ+) | 
| 52 |  | 0xr 11309 | . . . . . . . . . 10
⊢ 0 ∈
ℝ* | 
| 53 | 52 | a1i 11 | . . . . . . . . 9
⊢ (𝑧 ∈ ℤ → 0 ∈
ℝ*) | 
| 54 |  | 8re 12363 | . . . . . . . . . . 11
⊢ 8 ∈
ℝ | 
| 55 | 54 | rexri 11320 | . . . . . . . . . 10
⊢ 8 ∈
ℝ* | 
| 56 | 55 | a1i 11 | . . . . . . . . 9
⊢ (𝑧 ∈ ℤ → 8 ∈
ℝ*) | 
| 57 |  | 7re 12360 | . . . . . . . . . . 11
⊢ 7 ∈
ℝ | 
| 58 | 57 | rexri 11320 | . . . . . . . . . 10
⊢ 7 ∈
ℝ* | 
| 59 | 58 | a1i 11 | . . . . . . . . 9
⊢ (𝑧 ∈ ℤ → 7 ∈
ℝ*) | 
| 60 |  | 0re 11264 | . . . . . . . . . . 11
⊢ 0 ∈
ℝ | 
| 61 |  | 7pos 12378 | . . . . . . . . . . 11
⊢ 0 <
7 | 
| 62 | 60, 57, 61 | ltleii 11385 | . . . . . . . . . 10
⊢ 0 ≤
7 | 
| 63 | 62 | a1i 11 | . . . . . . . . 9
⊢ (𝑧 ∈ ℤ → 0 ≤
7) | 
| 64 |  | 7lt8 12459 | . . . . . . . . . 10
⊢ 7 <
8 | 
| 65 | 64 | a1i 11 | . . . . . . . . 9
⊢ (𝑧 ∈ ℤ → 7 <
8) | 
| 66 | 53, 56, 59, 63, 65 | elicod 13438 | . . . . . . . 8
⊢ (𝑧 ∈ ℤ → 7 ∈
(0[,)8)) | 
| 67 |  | muladdmodid 13952 | . . . . . . . 8
⊢ ((𝑧 ∈ ℤ ∧ 8 ∈
ℝ+ ∧ 7 ∈ (0[,)8)) → (((𝑧 · 8) + 7) mod 8) =
7) | 
| 68 | 51, 66, 67 | mpd3an23 1464 | . . . . . . 7
⊢ (𝑧 ∈ ℤ → (((𝑧 · 8) + 7) mod 8) =
7) | 
| 69 | 68 | adantl 481 | . . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((𝑧 · 8) + 7) mod 8) =
7) | 
| 70 | 49, 69 | eqtrd 2776 | . . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((2
· ((𝑧 · 4) +
3)) + 1) mod 8) = 7) | 
| 71 |  | oveq2 7440 | . . . . . . . 8
⊢ (((𝑧 · 4) + 3) = 𝑁 → (2 · ((𝑧 · 4) + 3)) = (2 ·
𝑁)) | 
| 72 | 71 | oveq1d 7447 | . . . . . . 7
⊢ (((𝑧 · 4) + 3) = 𝑁 → ((2 · ((𝑧 · 4) + 3)) + 1) = ((2
· 𝑁) +
1)) | 
| 73 | 72 | oveq1d 7447 | . . . . . 6
⊢ (((𝑧 · 4) + 3) = 𝑁 → (((2 · ((𝑧 · 4) + 3)) + 1) mod 8) =
(((2 · 𝑁) + 1) mod
8)) | 
| 74 | 73 | eqeq1d 2738 | . . . . 5
⊢ (((𝑧 · 4) + 3) = 𝑁 → ((((2 · ((𝑧 · 4) + 3)) + 1) mod 8) =
7 ↔ (((2 · 𝑁) +
1) mod 8) = 7)) | 
| 75 | 70, 74 | syl5ibcom 245 | . . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((𝑧 · 4) + 3) = 𝑁 → (((2 · 𝑁) + 1) mod 8) =
7)) | 
| 76 | 75 | rexlimdva 3154 | . . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑧 ∈ ℤ
((𝑧 · 4) + 3) =
𝑁 → (((2 ·
𝑁) + 1) mod 8) =
7)) | 
| 77 | 8, 76 | sylbid 240 | . 2
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 4) = 3 → (((2 ·
𝑁) + 1) mod 8) =
7)) | 
| 78 | 77 | imp 406 | 1
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 mod 4) = 3) → (((2
· 𝑁) + 1) mod 8) =
7) |