Step | Hyp | Ref
| Expression |
1 | | nnnn0 11176 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) |
2 | | nnne0 10930 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ → 𝐾 ≠ 0) |
3 | 1, 2 | jca 553 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ → (𝐾 ∈ ℕ0
∧ 𝐾 ≠
0)) |
4 | | df-ne 2782 |
. . . . . . . . . . . 12
⊢ (𝐾 ≠ 0 ↔ ¬ 𝐾 = 0) |
5 | 4 | anbi2i 726 |
. . . . . . . . . . 11
⊢ ((𝐾 < 𝐷 ∧ 𝐾 ≠ 0) ↔ (𝐾 < 𝐷 ∧ ¬ 𝐾 = 0)) |
6 | | divalg2 14966 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
∃!𝑟 ∈
ℕ0 (𝑟 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) |
7 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟 = 𝑥 → (𝑟 < 𝐷 ↔ 𝑥 < 𝐷)) |
8 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑟 = 𝑥 → (𝑁 − 𝑟) = (𝑁 − 𝑥)) |
9 | 8 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟 = 𝑥 → (𝐷 ∥ (𝑁 − 𝑟) ↔ 𝐷 ∥ (𝑁 − 𝑥))) |
10 | 7, 9 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = 𝑥 → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ↔ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥)))) |
11 | 10 | reu4 3367 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃!𝑟 ∈
ℕ0 (𝑟 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ↔ (∃𝑟 ∈ ℕ0 (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ ∀𝑟 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥))) |
12 | 6, 11 | sylib 207 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(∃𝑟 ∈
ℕ0 (𝑟 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ ∀𝑟 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥))) |
13 | 12 | simprd 478 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
∀𝑟 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥)) |
14 | | nngt0 10926 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐷 ∈ ℕ → 0 <
𝐷) |
15 | 14 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → 0 < 𝐷) |
16 | | zcn 11259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
17 | 16 | subid1d 10260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℤ → (𝑁 − 0) = 𝑁) |
18 | 17 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℤ → (𝐷 ∥ (𝑁 − 0) ↔ 𝐷 ∥ 𝑁)) |
19 | 18 | biimpar 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∥ 𝑁) → 𝐷 ∥ (𝑁 − 0)) |
20 | 19 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → 𝐷 ∥ (𝑁 − 0)) |
21 | 15, 20 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0))) |
22 | 21 | 3expa 1257 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) → (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0))) |
23 | 22 | anim2i 591 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁)) → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0)))) |
24 | 23 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) ∧ (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0)))) |
25 | | 0nn0 11184 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℕ0 |
26 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 0 → (𝑥 < 𝐷 ↔ 0 < 𝐷)) |
27 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = 0 → (𝑁 − 𝑥) = (𝑁 − 0)) |
28 | 27 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 0 → (𝐷 ∥ (𝑁 − 𝑥) ↔ 𝐷 ∥ (𝑁 − 0))) |
29 | 26, 28 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 0 → ((𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥)) ↔ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0)))) |
30 | 29 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 0 → (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) ↔ ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0))))) |
31 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 0 → (𝑟 = 𝑥 ↔ 𝑟 = 0)) |
32 | 30, 31 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 0 → ((((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥) ↔ (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0))) → 𝑟 = 0))) |
33 | 32 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
ℕ0 → (∀𝑥 ∈ ℕ0 (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥) → (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0))) → 𝑟 = 0))) |
34 | 25, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑥 ∈
ℕ0 (((𝑟
< 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥) → (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0))) → 𝑟 = 0)) |
35 | 24, 34 | syl5 33 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
ℕ0 (((𝑟
< 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥) → ((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) ∧ (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) → 𝑟 = 0)) |
36 | 35 | expd 451 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
ℕ0 (((𝑟
< 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥) → (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0))) |
37 | 36 | ralimi 2936 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑟 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥) → ∀𝑟 ∈ ℕ0 (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0))) |
38 | 13, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
∀𝑟 ∈
ℕ0 (((𝑁
∈ ℤ ∧ 𝐷
∈ ℕ) ∧ 𝐷
∥ 𝑁) → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0))) |
39 | | r19.21v 2943 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑟 ∈
ℕ0 (((𝑁
∈ ℤ ∧ 𝐷
∈ ℕ) ∧ 𝐷
∥ 𝑁) → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0)) ↔ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) → ∀𝑟 ∈ ℕ0 ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0))) |
40 | 38, 39 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) → ∀𝑟 ∈ ℕ0 ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0))) |
41 | 40 | expd 451 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 ∥ 𝑁 → ∀𝑟 ∈ ℕ0 ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0)))) |
42 | 41 | pm2.43i 50 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 ∥ 𝑁 → ∀𝑟 ∈ ℕ0 ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0))) |
43 | 42 | 3impia 1253 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → ∀𝑟 ∈ ℕ0 ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0)) |
44 | | breq1 4586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝐾 → (𝑟 < 𝐷 ↔ 𝐾 < 𝐷)) |
45 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝐾 → (𝑁 − 𝑟) = (𝑁 − 𝐾)) |
46 | 45 | breq2d 4595 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝐾 → (𝐷 ∥ (𝑁 − 𝑟) ↔ 𝐷 ∥ (𝑁 − 𝐾))) |
47 | 44, 46 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝐾 → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ↔ (𝐾 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝐾)))) |
48 | | eqeq1 2614 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝐾 → (𝑟 = 0 ↔ 𝐾 = 0)) |
49 | 47, 48 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝐾 → (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0) ↔ ((𝐾 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝐾)) → 𝐾 = 0))) |
50 | 49 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ (∀𝑟 ∈
ℕ0 ((𝑟
< 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0) → ((𝐾 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝐾)) → 𝐾 = 0))) |
51 | 43, 50 | syl5com 31 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 ∈ ℕ0 → ((𝐾 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝐾)) → 𝐾 = 0))) |
52 | | pm4.14 600 |
. . . . . . . . . . . 12
⊢ (((𝐾 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝐾)) → 𝐾 = 0) ↔ ((𝐾 < 𝐷 ∧ ¬ 𝐾 = 0) → ¬ 𝐷 ∥ (𝑁 − 𝐾))) |
53 | 51, 52 | syl6ib 240 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 ∈ ℕ0 → ((𝐾 < 𝐷 ∧ ¬ 𝐾 = 0) → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
54 | 5, 53 | syl7bi 244 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 ∈ ℕ0 → ((𝐾 < 𝐷 ∧ 𝐾 ≠ 0) → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
55 | 54 | exp4a 631 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 ∈ ℕ0 → (𝐾 < 𝐷 → (𝐾 ≠ 0 → ¬ 𝐷 ∥ (𝑁 − 𝐾))))) |
56 | 55 | com23 84 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 < 𝐷 → (𝐾 ∈ ℕ0 → (𝐾 ≠ 0 → ¬ 𝐷 ∥ (𝑁 − 𝐾))))) |
57 | 56 | imp4a 612 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 < 𝐷 → ((𝐾 ∈ ℕ0 ∧ 𝐾 ≠ 0) → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
58 | 3, 57 | syl7 72 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 < 𝐷 → (𝐾 ∈ ℕ → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
59 | 58 | com23 84 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 ∈ ℕ → (𝐾 < 𝐷 → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
60 | 59 | impd 446 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → ((𝐾 ∈ ℕ ∧ 𝐾 < 𝐷) → ¬ 𝐷 ∥ (𝑁 − 𝐾))) |
61 | 60 | 3expia 1259 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 ∥ 𝑁 → ((𝐾 ∈ ℕ ∧ 𝐾 < 𝐷) → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
62 | 61 | com23 84 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ((𝐾 ∈ ℕ ∧ 𝐾 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
63 | 62 | 3impia 1253 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐾 < 𝐷)) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 − 𝐾))) |