Step | Hyp | Ref
| Expression |
1 | | divalglem8.4 |
. . . . . . . . . . . . 13
⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} |
2 | | ssrab2 3650 |
. . . . . . . . . . . . 13
⊢ {𝑟 ∈ ℕ0
∣ 𝐷 ∥ (𝑁 − 𝑟)} ⊆
ℕ0 |
3 | 1, 2 | eqsstri 3598 |
. . . . . . . . . . . 12
⊢ 𝑆 ⊆
ℕ0 |
4 | | nn0sscn 11174 |
. . . . . . . . . . . 12
⊢
ℕ0 ⊆ ℂ |
5 | 3, 4 | sstri 3577 |
. . . . . . . . . . 11
⊢ 𝑆 ⊆
ℂ |
6 | 5 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑌 ∈ 𝑆 → 𝑌 ∈ ℂ) |
7 | 5 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ ℂ) |
8 | | divalglem8.2 |
. . . . . . . . . . . . . 14
⊢ 𝐷 ∈ ℤ |
9 | | divalglem8.3 |
. . . . . . . . . . . . . 14
⊢ 𝐷 ≠ 0 |
10 | | nnabscl 13913 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (abs‘𝐷) ∈
ℕ) |
11 | 8, 9, 10 | mp2an 704 |
. . . . . . . . . . . . 13
⊢
(abs‘𝐷) ∈
ℕ |
12 | 11 | nnzi 11278 |
. . . . . . . . . . . 12
⊢
(abs‘𝐷) ∈
ℤ |
13 | | zmulcl 11303 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℤ ∧
(abs‘𝐷) ∈
ℤ) → (𝐾 ·
(abs‘𝐷)) ∈
ℤ) |
14 | 12, 13 | mpan2 703 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℤ → (𝐾 · (abs‘𝐷)) ∈
ℤ) |
15 | 14 | zcnd 11359 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → (𝐾 · (abs‘𝐷)) ∈
ℂ) |
16 | | subadd 10163 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ (𝐾 · (abs‘𝐷)) ∈ ℂ) →
((𝑌 − 𝑋) = (𝐾 · (abs‘𝐷)) ↔ (𝑋 + (𝐾 · (abs‘𝐷))) = 𝑌)) |
17 | 6, 7, 15, 16 | syl3an 1360 |
. . . . . . . . 9
⊢ ((𝑌 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆 ∧ 𝐾 ∈ ℤ) → ((𝑌 − 𝑋) = (𝐾 · (abs‘𝐷)) ↔ (𝑋 + (𝐾 · (abs‘𝐷))) = 𝑌)) |
18 | 17 | 3com12 1261 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ∧ 𝐾 ∈ ℤ) → ((𝑌 − 𝑋) = (𝐾 · (abs‘𝐷)) ↔ (𝑋 + (𝐾 · (abs‘𝐷))) = 𝑌)) |
19 | | eqcom 2617 |
. . . . . . . 8
⊢ ((𝑌 − 𝑋) = (𝐾 · (abs‘𝐷)) ↔ (𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋)) |
20 | | eqcom 2617 |
. . . . . . . 8
⊢ ((𝑋 + (𝐾 · (abs‘𝐷))) = 𝑌 ↔ 𝑌 = (𝑋 + (𝐾 · (abs‘𝐷)))) |
21 | 18, 19, 20 | 3bitr3g 301 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ∧ 𝐾 ∈ ℤ) → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) ↔ 𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))))) |
22 | 21 | 3adant1r 1311 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ 𝑌 ∈ 𝑆 ∧ 𝐾 ∈ ℤ) → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) ↔ 𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))))) |
23 | 22 | 3adant2r 1313 |
. . . . 5
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ (𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) ↔ 𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))))) |
24 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑌 → (𝑧 < (abs‘𝐷) ↔ 𝑌 < (abs‘𝐷))) |
25 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑌 → (𝑧 ∈ (0...((abs‘𝐷) − 1)) ↔ 𝑌 ∈ (0...((abs‘𝐷) − 1)))) |
26 | 24, 25 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑌 → ((𝑧 < (abs‘𝐷) → 𝑧 ∈ (0...((abs‘𝐷) − 1))) ↔ (𝑌 < (abs‘𝐷) → 𝑌 ∈ (0...((abs‘𝐷) − 1))))) |
27 | 3 | sseli 3564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ℕ0) |
28 | | elnn0z 11267 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ℕ0
↔ (𝑧 ∈ ℤ
∧ 0 ≤ 𝑧)) |
29 | 27, 28 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → (𝑧 ∈ ℤ ∧ 0 ≤ 𝑧)) |
30 | 29 | anim1i 590 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑧 < (abs‘𝐷)) → ((𝑧 ∈ ℤ ∧ 0 ≤ 𝑧) ∧ 𝑧 < (abs‘𝐷))) |
31 | | df-3an 1033 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℤ ∧ 0 ≤
𝑧 ∧ 𝑧 < (abs‘𝐷)) ↔ ((𝑧 ∈ ℤ ∧ 0 ≤ 𝑧) ∧ 𝑧 < (abs‘𝐷))) |
32 | 30, 31 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑧 < (abs‘𝐷)) → (𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ∧ 𝑧 < (abs‘𝐷))) |
33 | | 0z 11265 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ |
34 | | elfzm11 12280 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℤ ∧ (abs‘𝐷) ∈ ℤ) → (𝑧 ∈ (0...((abs‘𝐷) − 1)) ↔ (𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ∧ 𝑧 < (abs‘𝐷)))) |
35 | 33, 12, 34 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (0...((abs‘𝐷) − 1)) ↔ (𝑧 ∈ ℤ ∧ 0 ≤
𝑧 ∧ 𝑧 < (abs‘𝐷))) |
36 | 32, 35 | sylibr 223 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑧 < (abs‘𝐷)) → 𝑧 ∈ (0...((abs‘𝐷) − 1))) |
37 | 36 | ex 449 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑆 → (𝑧 < (abs‘𝐷) → 𝑧 ∈ (0...((abs‘𝐷) − 1)))) |
38 | 26, 37 | vtoclga 3245 |
. . . . . . . . . 10
⊢ (𝑌 ∈ 𝑆 → (𝑌 < (abs‘𝐷) → 𝑌 ∈ (0...((abs‘𝐷) − 1)))) |
39 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))) → (𝑌 ∈ (0...((abs‘𝐷) − 1)) ↔ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)))) |
40 | 39 | biimpd 218 |
. . . . . . . . . 10
⊢ (𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))) → (𝑌 ∈ (0...((abs‘𝐷) − 1)) → (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)))) |
41 | 38, 40 | sylan9 687 |
. . . . . . . . 9
⊢ ((𝑌 ∈ 𝑆 ∧ 𝑌 = (𝑋 + (𝐾 · (abs‘𝐷)))) → (𝑌 < (abs‘𝐷) → (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)))) |
42 | 41 | impancom 455 |
. . . . . . . 8
⊢ ((𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷)) → (𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))) → (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)))) |
43 | 42 | 3ad2ant2 1076 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ (𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → (𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))) → (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)))) |
44 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑋 → (𝑧 < (abs‘𝐷) ↔ 𝑋 < (abs‘𝐷))) |
45 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑋 → (𝑧 ∈ (0...((abs‘𝐷) − 1)) ↔ 𝑋 ∈ (0...((abs‘𝐷) − 1)))) |
46 | 44, 45 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑋 → ((𝑧 < (abs‘𝐷) → 𝑧 ∈ (0...((abs‘𝐷) − 1))) ↔ (𝑋 < (abs‘𝐷) → 𝑋 ∈ (0...((abs‘𝐷) − 1))))) |
47 | 46, 37 | vtoclga 3245 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑆 → (𝑋 < (abs‘𝐷) → 𝑋 ∈ (0...((abs‘𝐷) − 1)))) |
48 | 47 | imp 444 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) → 𝑋 ∈ (0...((abs‘𝐷) − 1))) |
49 | 8, 9 | divalglem7 14960 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (0...((abs‘𝐷) − 1)) ∧ 𝐾 ∈ ℤ) → (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)))) |
50 | 48, 49 | sylan 487 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)))) |
51 | 50 | 3adant2 1073 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ (𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)))) |
52 | 51 | con2d 128 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ (𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → ((𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)) → ¬ 𝐾 ≠ 0)) |
53 | 43, 52 | syld 46 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ (𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → (𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))) → ¬ 𝐾 ≠ 0)) |
54 | | df-ne 2782 |
. . . . . . 7
⊢ (𝐾 ≠ 0 ↔ ¬ 𝐾 = 0) |
55 | 54 | con2bii 346 |
. . . . . 6
⊢ (𝐾 = 0 ↔ ¬ 𝐾 ≠ 0) |
56 | 53, 55 | syl6ibr 241 |
. . . . 5
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ (𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → (𝑌 = (𝑋 + (𝐾 · (abs‘𝐷))) → 𝐾 = 0)) |
57 | 23, 56 | sylbid 229 |
. . . 4
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ (𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) → 𝐾 = 0)) |
58 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝐾 = 0 → (𝐾 · (abs‘𝐷)) = (0 · (abs‘𝐷))) |
59 | 11 | nncni 10907 |
. . . . . . . . . . . 12
⊢
(abs‘𝐷) ∈
ℂ |
60 | 59 | mul02i 10104 |
. . . . . . . . . . 11
⊢ (0
· (abs‘𝐷)) =
0 |
61 | 58, 60 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝐾 = 0 → (𝐾 · (abs‘𝐷)) = 0) |
62 | 61 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝐾 = 0 → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) ↔ 0 = (𝑌 − 𝑋))) |
63 | 62 | biimpac 502 |
. . . . . . . 8
⊢ (((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) ∧ 𝐾 = 0) → 0 = (𝑌 − 𝑋)) |
64 | | subeq0 10186 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((𝑌 − 𝑋) = 0 ↔ 𝑌 = 𝑋)) |
65 | 6, 7, 64 | syl2anr 494 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → ((𝑌 − 𝑋) = 0 ↔ 𝑌 = 𝑋)) |
66 | | eqcom 2617 |
. . . . . . . . 9
⊢ ((𝑌 − 𝑋) = 0 ↔ 0 = (𝑌 − 𝑋)) |
67 | | eqcom 2617 |
. . . . . . . . 9
⊢ (𝑌 = 𝑋 ↔ 𝑋 = 𝑌) |
68 | 65, 66, 67 | 3bitr3g 301 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (0 = (𝑌 − 𝑋) ↔ 𝑋 = 𝑌)) |
69 | 63, 68 | syl5ib 233 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) ∧ 𝐾 = 0) → 𝑋 = 𝑌)) |
70 | 69 | ad2ant2r 779 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ (𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷))) → (((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) ∧ 𝐾 = 0) → 𝑋 = 𝑌)) |
71 | 70 | 3adant3 1074 |
. . . . 5
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ (𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → (((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) ∧ 𝐾 = 0) → 𝑋 = 𝑌)) |
72 | 71 | expd 451 |
. . . 4
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ (𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) → (𝐾 = 0 → 𝑋 = 𝑌))) |
73 | 57, 72 | mpdd 42 |
. . 3
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ (𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷)) ∧ 𝐾 ∈ ℤ) → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) → 𝑋 = 𝑌)) |
74 | 73 | 3expia 1259 |
. 2
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑋 < (abs‘𝐷)) ∧ (𝑌 ∈ 𝑆 ∧ 𝑌 < (abs‘𝐷))) → (𝐾 ∈ ℤ → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) → 𝑋 = 𝑌))) |
75 | 74 | an4s 865 |
1
⊢ (((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝑋 < (abs‘𝐷) ∧ 𝑌 < (abs‘𝐷))) → (𝐾 ∈ ℤ → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) → 𝑋 = 𝑌))) |