Step | Hyp | Ref
| Expression |
1 | | nnnn0 9103 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) |
2 | | nnne0 8867 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ → 𝐾 ≠ 0) |
3 | 1, 2 | jca 304 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ → (𝐾 ∈ ℕ0
∧ 𝐾 ≠
0)) |
4 | | df-ne 2328 |
. . . . . . . . . . . 12
⊢ (𝐾 ≠ 0 ↔ ¬ 𝐾 = 0) |
5 | 4 | anbi2i 453 |
. . . . . . . . . . 11
⊢ ((𝐾 < 𝐷 ∧ 𝐾 ≠ 0) ↔ (𝐾 < 𝐷 ∧ ¬ 𝐾 = 0)) |
6 | | divalg2 11830 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
∃!𝑟 ∈
ℕ0 (𝑟 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) |
7 | | breq1 3970 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = 𝑥 → (𝑟 < 𝐷 ↔ 𝑥 < 𝐷)) |
8 | | oveq2 5835 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟 = 𝑥 → (𝑁 − 𝑟) = (𝑁 − 𝑥)) |
9 | 8 | breq2d 3979 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = 𝑥 → (𝐷 ∥ (𝑁 − 𝑟) ↔ 𝐷 ∥ (𝑁 − 𝑥))) |
10 | 7, 9 | anbi12d 465 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = 𝑥 → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ↔ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥)))) |
11 | 10 | reu4 2906 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃!𝑟 ∈
ℕ0 (𝑟 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ↔ (∃𝑟 ∈ ℕ0 (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ ∀𝑟 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥))) |
12 | 6, 11 | sylib 121 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
(∃𝑟 ∈
ℕ0 (𝑟 <
𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ ∀𝑟 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥))) |
13 | | nngt0 8864 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐷 ∈ ℕ → 0 <
𝐷) |
14 | 13 | 3ad2ant2 1004 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → 0 < 𝐷) |
15 | | zcn 9178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
16 | 15 | subid1d 8180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℤ → (𝑁 − 0) = 𝑁) |
17 | 16 | breq2d 3979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℤ → (𝐷 ∥ (𝑁 − 0) ↔ 𝐷 ∥ 𝑁)) |
18 | 17 | biimpar 295 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∥ 𝑁) → 𝐷 ∥ (𝑁 − 0)) |
19 | 18 | 3adant2 1001 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → 𝐷 ∥ (𝑁 − 0)) |
20 | 14, 19 | jca 304 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0))) |
21 | 20 | 3expa 1185 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) → (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0))) |
22 | 21 | anim2i 340 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁)) → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0)))) |
23 | 22 | ancoms 266 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) ∧ (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0)))) |
24 | | 0nn0 9111 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℕ0 |
25 | | breq1 3970 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 0 → (𝑥 < 𝐷 ↔ 0 < 𝐷)) |
26 | | oveq2 5835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = 0 → (𝑁 − 𝑥) = (𝑁 − 0)) |
27 | 26 | breq2d 3979 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 0 → (𝐷 ∥ (𝑁 − 𝑥) ↔ 𝐷 ∥ (𝑁 − 0))) |
28 | 25, 27 | anbi12d 465 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 0 → ((𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥)) ↔ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0)))) |
29 | 28 | anbi2d 460 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 0 → (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) ↔ ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0))))) |
30 | | eqeq2 2167 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 0 → (𝑟 = 𝑥 ↔ 𝑟 = 0)) |
31 | 29, 30 | imbi12d 233 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 0 → ((((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥) ↔ (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0))) → 𝑟 = 0))) |
32 | 31 | rspcv 2812 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
ℕ0 → (∀𝑥 ∈ ℕ0 (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥) → (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0))) → 𝑟 = 0))) |
33 | 24, 32 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑥 ∈
ℕ0 (((𝑟
< 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥) → (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (0 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 0))) → 𝑟 = 0)) |
34 | 23, 33 | syl5 32 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
ℕ0 (((𝑟
< 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥) → ((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) ∧ (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) → 𝑟 = 0)) |
35 | 34 | expd 256 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
ℕ0 (((𝑟
< 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥) → (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0))) |
36 | 35 | ralimi 2520 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑟 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ∧ (𝑥 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑥))) → 𝑟 = 𝑥) → ∀𝑟 ∈ ℕ0 (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0))) |
37 | 12, 36 | simpl2im 384 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) →
∀𝑟 ∈
ℕ0 (((𝑁
∈ ℤ ∧ 𝐷
∈ ℕ) ∧ 𝐷
∥ 𝑁) → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0))) |
38 | | r19.21v 2534 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑟 ∈
ℕ0 (((𝑁
∈ ℤ ∧ 𝐷
∈ ℕ) ∧ 𝐷
∥ 𝑁) → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0)) ↔ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) → ∀𝑟 ∈ ℕ0 ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0))) |
39 | 37, 38 | sylib 121 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) ∧ 𝐷 ∥ 𝑁) → ∀𝑟 ∈ ℕ0 ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0))) |
40 | 39 | expd 256 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 ∥ 𝑁 → ∀𝑟 ∈ ℕ0 ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0)))) |
41 | 40 | pm2.43i 49 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 ∥ 𝑁 → ∀𝑟 ∈ ℕ0 ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0))) |
42 | 41 | 3impia 1182 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → ∀𝑟 ∈ ℕ0 ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0)) |
43 | | breq1 3970 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝐾 → (𝑟 < 𝐷 ↔ 𝐾 < 𝐷)) |
44 | | oveq2 5835 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝐾 → (𝑁 − 𝑟) = (𝑁 − 𝐾)) |
45 | 44 | breq2d 3979 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝐾 → (𝐷 ∥ (𝑁 − 𝑟) ↔ 𝐷 ∥ (𝑁 − 𝐾))) |
46 | 43, 45 | anbi12d 465 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝐾 → ((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) ↔ (𝐾 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝐾)))) |
47 | | eqeq1 2164 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝐾 → (𝑟 = 0 ↔ 𝐾 = 0)) |
48 | 46, 47 | imbi12d 233 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝐾 → (((𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0) ↔ ((𝐾 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝐾)) → 𝐾 = 0))) |
49 | 48 | rspcv 2812 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ (∀𝑟 ∈
ℕ0 ((𝑟
< 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)) → 𝑟 = 0) → ((𝐾 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝐾)) → 𝐾 = 0))) |
50 | 42, 49 | syl5com 29 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 ∈ ℕ0 → ((𝐾 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝐾)) → 𝐾 = 0))) |
51 | | pm3.37 679 |
. . . . . . . . . . . 12
⊢ (((𝐾 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝐾)) → 𝐾 = 0) → ((𝐾 < 𝐷 ∧ ¬ 𝐾 = 0) → ¬ 𝐷 ∥ (𝑁 − 𝐾))) |
52 | 50, 51 | syl6 33 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 ∈ ℕ0 → ((𝐾 < 𝐷 ∧ ¬ 𝐾 = 0) → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
53 | 5, 52 | syl7bi 164 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 ∈ ℕ0 → ((𝐾 < 𝐷 ∧ 𝐾 ≠ 0) → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
54 | 53 | exp4a 364 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 ∈ ℕ0 → (𝐾 < 𝐷 → (𝐾 ≠ 0 → ¬ 𝐷 ∥ (𝑁 − 𝐾))))) |
55 | 54 | com23 78 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 < 𝐷 → (𝐾 ∈ ℕ0 → (𝐾 ≠ 0 → ¬ 𝐷 ∥ (𝑁 − 𝐾))))) |
56 | 55 | imp4a 347 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 < 𝐷 → ((𝐾 ∈ ℕ0 ∧ 𝐾 ≠ 0) → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
57 | 3, 56 | syl7 69 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 < 𝐷 → (𝐾 ∈ ℕ → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
58 | 57 | com23 78 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → (𝐾 ∈ ℕ → (𝐾 < 𝐷 → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
59 | 58 | impd 252 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁) → ((𝐾 ∈ ℕ ∧ 𝐾 < 𝐷) → ¬ 𝐷 ∥ (𝑁 − 𝐾))) |
60 | 59 | 3expia 1187 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐷 ∥ 𝑁 → ((𝐾 ∈ ℕ ∧ 𝐾 < 𝐷) → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
61 | 60 | com23 78 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ((𝐾 ∈ ℕ ∧ 𝐾 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 − 𝐾)))) |
62 | 61 | 3impia 1182 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐾 < 𝐷)) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 − 𝐾))) |