Step | Hyp | Ref
| Expression |
1 | | 4nn 12149 |
. . . . 5
⊢ 4 ∈
ℕ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℤ → 4 ∈
ℕ) |
3 | | 3nn0 12344 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℤ → 3 ∈
ℕ0) |
5 | | 3lt4 12240 |
. . . . 5
⊢ 3 <
4 |
6 | 4, 5 | jctir 521 |
. . . 4
⊢ (𝑁 ∈ ℤ → (3 ∈
ℕ0 ∧ 3 < 4)) |
7 | | modremain 16208 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 4 ∈
ℕ ∧ (3 ∈ ℕ0 ∧ 3 < 4)) → ((𝑁 mod 4) = 3 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 4) + 3) = 𝑁)) |
8 | 2, 6, 7 | mpd3an23 1462 |
. . 3
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 4) = 3 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 4) + 3) = 𝑁)) |
9 | | 2cnd 12144 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 2 ∈
ℂ) |
10 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 𝑧 ∈
ℤ) |
11 | | 4z 12447 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℤ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 4 ∈
ℤ) |
13 | 10, 12 | zmulcld 12525 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑧 · 4) ∈
ℤ) |
14 | 13 | zcnd 12520 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑧 · 4) ∈
ℂ) |
15 | | 3cn 12147 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℂ |
16 | 15 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 3 ∈
ℂ) |
17 | 9, 14, 16 | adddid 11092 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (2
· ((𝑧 · 4) +
3)) = ((2 · (𝑧
· 4)) + (2 · 3))) |
18 | 10 | zcnd 12520 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 𝑧 ∈
ℂ) |
19 | | 4cn 12151 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℂ |
20 | 19 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → 4 ∈
ℂ) |
21 | 9, 18, 20 | mul12d 11277 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (2
· (𝑧 · 4)) =
(𝑧 · (2 ·
4))) |
22 | | 2cn 12141 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
23 | | 4t2e8 12234 |
. . . . . . . . . . . . . 14
⊢ (4
· 2) = 8 |
24 | 19, 22, 23 | mulcomli 11077 |
. . . . . . . . . . . . 13
⊢ (2
· 4) = 8 |
25 | 24 | oveq2i 7340 |
. . . . . . . . . . . 12
⊢ (𝑧 · (2 · 4)) =
(𝑧 ·
8) |
26 | 21, 25 | eqtrdi 2792 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (2
· (𝑧 · 4)) =
(𝑧 ·
8)) |
27 | | 3t2e6 12232 |
. . . . . . . . . . . . 13
⊢ (3
· 2) = 6 |
28 | 15, 22, 27 | mulcomli 11077 |
. . . . . . . . . . . 12
⊢ (2
· 3) = 6 |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (2
· 3) = 6) |
30 | 26, 29 | oveq12d 7347 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((2
· (𝑧 · 4)) +
(2 · 3)) = ((𝑧
· 8) + 6)) |
31 | 17, 30 | eqtrd 2776 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (2
· ((𝑧 · 4) +
3)) = ((𝑧 · 8) +
6)) |
32 | 31 | oveq1d 7344 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((2
· ((𝑧 · 4) +
3)) + 1) = (((𝑧 · 8)
+ 6) + 1)) |
33 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℤ) |
34 | | 8nn 12161 |
. . . . . . . . . . . . . . 15
⊢ 8 ∈
ℕ |
35 | 34 | nnzi 12437 |
. . . . . . . . . . . . . 14
⊢ 8 ∈
ℤ |
36 | 35 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℤ → 8 ∈
ℤ) |
37 | 33, 36 | zmulcld 12525 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℤ → (𝑧 · 8) ∈
ℤ) |
38 | 37 | zcnd 12520 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℤ → (𝑧 · 8) ∈
ℂ) |
39 | | 6cn 12157 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℂ |
40 | 39 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℤ → 6 ∈
ℂ) |
41 | | 1cnd 11063 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℤ → 1 ∈
ℂ) |
42 | 38, 40, 41 | addassd 11090 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℤ → (((𝑧 · 8) + 6) + 1) = ((𝑧 · 8) + (6 +
1))) |
43 | | 6p1e7 12214 |
. . . . . . . . . . . 12
⊢ (6 + 1) =
7 |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℤ → (6 + 1) =
7) |
45 | 44 | oveq2d 7345 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℤ → ((𝑧 · 8) + (6 + 1)) =
((𝑧 · 8) +
7)) |
46 | 42, 45 | eqtrd 2776 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤ → (((𝑧 · 8) + 6) + 1) = ((𝑧 · 8) +
7)) |
47 | 46 | adantl 482 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((𝑧 · 8) + 6) + 1) = ((𝑧 · 8) +
7)) |
48 | 32, 47 | eqtrd 2776 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((2
· ((𝑧 · 4) +
3)) + 1) = ((𝑧 · 8)
+ 7)) |
49 | 48 | oveq1d 7344 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((2
· ((𝑧 · 4) +
3)) + 1) mod 8) = (((𝑧
· 8) + 7) mod 8)) |
50 | | nnrp 12834 |
. . . . . . . . 9
⊢ (8 ∈
ℕ → 8 ∈ ℝ+) |
51 | 34, 50 | mp1i 13 |
. . . . . . . 8
⊢ (𝑧 ∈ ℤ → 8 ∈
ℝ+) |
52 | | 0xr 11115 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
53 | 52 | a1i 11 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤ → 0 ∈
ℝ*) |
54 | | 8re 12162 |
. . . . . . . . . . 11
⊢ 8 ∈
ℝ |
55 | 54 | rexri 11126 |
. . . . . . . . . 10
⊢ 8 ∈
ℝ* |
56 | 55 | a1i 11 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤ → 8 ∈
ℝ*) |
57 | | 7re 12159 |
. . . . . . . . . . 11
⊢ 7 ∈
ℝ |
58 | 57 | rexri 11126 |
. . . . . . . . . 10
⊢ 7 ∈
ℝ* |
59 | 58 | a1i 11 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤ → 7 ∈
ℝ*) |
60 | | 0re 11070 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
61 | | 7pos 12177 |
. . . . . . . . . . 11
⊢ 0 <
7 |
62 | 60, 57, 61 | ltleii 11191 |
. . . . . . . . . 10
⊢ 0 ≤
7 |
63 | 62 | a1i 11 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤ → 0 ≤
7) |
64 | | 7lt8 12258 |
. . . . . . . . . 10
⊢ 7 <
8 |
65 | 64 | a1i 11 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤ → 7 <
8) |
66 | 53, 56, 59, 63, 65 | elicod 13222 |
. . . . . . . 8
⊢ (𝑧 ∈ ℤ → 7 ∈
(0[,)8)) |
67 | | muladdmodid 13724 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℤ ∧ 8 ∈
ℝ+ ∧ 7 ∈ (0[,)8)) → (((𝑧 · 8) + 7) mod 8) =
7) |
68 | 51, 66, 67 | mpd3an23 1462 |
. . . . . . 7
⊢ (𝑧 ∈ ℤ → (((𝑧 · 8) + 7) mod 8) =
7) |
69 | 68 | adantl 482 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((𝑧 · 8) + 7) mod 8) =
7) |
70 | 49, 69 | eqtrd 2776 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((2
· ((𝑧 · 4) +
3)) + 1) mod 8) = 7) |
71 | | oveq2 7337 |
. . . . . . . 8
⊢ (((𝑧 · 4) + 3) = 𝑁 → (2 · ((𝑧 · 4) + 3)) = (2 ·
𝑁)) |
72 | 71 | oveq1d 7344 |
. . . . . . 7
⊢ (((𝑧 · 4) + 3) = 𝑁 → ((2 · ((𝑧 · 4) + 3)) + 1) = ((2
· 𝑁) +
1)) |
73 | 72 | oveq1d 7344 |
. . . . . 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 244 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((𝑧 · 4) + 3) = 𝑁 → (((2 · 𝑁) + 1) mod 8) =
7)) |
76 | 75 | rexlimdva 3148 |
. . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑧 ∈ ℤ
((𝑧 · 4) + 3) =
𝑁 → (((2 ·
𝑁) + 1) mod 8) =
7)) |
77 | 8, 76 | sylbid 239 |
. 2
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 4) = 3 → (((2 ·
𝑁) + 1) mod 8) =
7)) |
78 | 77 | imp 407 |
1
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 mod 4) = 3) → (((2
· 𝑁) + 1) mod 8) =
7) |