Step |
Hyp |
Ref |
Expression |
1 |
|
nnnn0 |
⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ0 ) |
2 |
|
nnne0 |
⊢ ( 𝐾 ∈ ℕ → 𝐾 ≠ 0 ) |
3 |
1 2
|
jca |
⊢ ( 𝐾 ∈ ℕ → ( 𝐾 ∈ ℕ0 ∧ 𝐾 ≠ 0 ) ) |
4 |
|
df-ne |
⊢ ( 𝐾 ≠ 0 ↔ ¬ 𝐾 = 0 ) |
5 |
4
|
anbi2i |
⊢ ( ( 𝐾 < 𝐷 ∧ 𝐾 ≠ 0 ) ↔ ( 𝐾 < 𝐷 ∧ ¬ 𝐾 = 0 ) ) |
6 |
|
divalg2 |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ∃! 𝑟 ∈ ℕ0 ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) |
7 |
|
breq1 |
⊢ ( 𝑟 = 𝑥 → ( 𝑟 < 𝐷 ↔ 𝑥 < 𝐷 ) ) |
8 |
|
oveq2 |
⊢ ( 𝑟 = 𝑥 → ( 𝑁 − 𝑟 ) = ( 𝑁 − 𝑥 ) ) |
9 |
8
|
breq2d |
⊢ ( 𝑟 = 𝑥 → ( 𝐷 ∥ ( 𝑁 − 𝑟 ) ↔ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ) |
10 |
7 9
|
anbi12d |
⊢ ( 𝑟 = 𝑥 → ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ↔ ( 𝑥 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ) ) |
11 |
10
|
reu4 |
⊢ ( ∃! 𝑟 ∈ ℕ0 ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ↔ ( ∃ 𝑟 ∈ ℕ0 ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ∀ 𝑟 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 𝑥 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ) → 𝑟 = 𝑥 ) ) ) |
12 |
6 11
|
sylib |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ∃ 𝑟 ∈ ℕ0 ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ∀ 𝑟 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 𝑥 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ) → 𝑟 = 𝑥 ) ) ) |
13 |
|
nngt0 |
⊢ ( 𝐷 ∈ ℕ → 0 < 𝐷 ) |
14 |
13
|
3ad2ant2 |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁 ) → 0 < 𝐷 ) |
15 |
|
zcn |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ ) |
16 |
15
|
subid1d |
⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 0 ) = 𝑁 ) |
17 |
16
|
breq2d |
⊢ ( 𝑁 ∈ ℤ → ( 𝐷 ∥ ( 𝑁 − 0 ) ↔ 𝐷 ∥ 𝑁 ) ) |
18 |
17
|
biimpar |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∥ 𝑁 ) → 𝐷 ∥ ( 𝑁 − 0 ) ) |
19 |
18
|
3adant2 |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁 ) → 𝐷 ∥ ( 𝑁 − 0 ) ) |
20 |
14 19
|
jca |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁 ) → ( 0 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 0 ) ) ) |
21 |
20
|
3expa |
⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷 ∥ 𝑁 ) → ( 0 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 0 ) ) ) |
22 |
21
|
anim1ci |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷 ∥ 𝑁 ) ∧ ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) → ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 0 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 0 ) ) ) ) |
23 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
24 |
|
breq1 |
⊢ ( 𝑥 = 0 → ( 𝑥 < 𝐷 ↔ 0 < 𝐷 ) ) |
25 |
|
oveq2 |
⊢ ( 𝑥 = 0 → ( 𝑁 − 𝑥 ) = ( 𝑁 − 0 ) ) |
26 |
25
|
breq2d |
⊢ ( 𝑥 = 0 → ( 𝐷 ∥ ( 𝑁 − 𝑥 ) ↔ 𝐷 ∥ ( 𝑁 − 0 ) ) ) |
27 |
24 26
|
anbi12d |
⊢ ( 𝑥 = 0 → ( ( 𝑥 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ↔ ( 0 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 0 ) ) ) ) |
28 |
27
|
anbi2d |
⊢ ( 𝑥 = 0 → ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 𝑥 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ) ↔ ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 0 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 0 ) ) ) ) ) |
29 |
|
eqeq2 |
⊢ ( 𝑥 = 0 → ( 𝑟 = 𝑥 ↔ 𝑟 = 0 ) ) |
30 |
28 29
|
imbi12d |
⊢ ( 𝑥 = 0 → ( ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 𝑥 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ) → 𝑟 = 𝑥 ) ↔ ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 0 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 0 ) ) ) → 𝑟 = 0 ) ) ) |
31 |
30
|
rspcv |
⊢ ( 0 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 𝑥 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ) → 𝑟 = 𝑥 ) → ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 0 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 0 ) ) ) → 𝑟 = 0 ) ) ) |
32 |
23 31
|
ax-mp |
⊢ ( ∀ 𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 𝑥 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ) → 𝑟 = 𝑥 ) → ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 0 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 0 ) ) ) → 𝑟 = 0 ) ) |
33 |
22 32
|
syl5 |
⊢ ( ∀ 𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 𝑥 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ) → 𝑟 = 𝑥 ) → ( ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷 ∥ 𝑁 ) ∧ ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) → 𝑟 = 0 ) ) |
34 |
33
|
expd |
⊢ ( ∀ 𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 𝑥 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ) → 𝑟 = 𝑥 ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷 ∥ 𝑁 ) → ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) → 𝑟 = 0 ) ) ) |
35 |
34
|
ralimi |
⊢ ( ∀ 𝑟 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ∧ ( 𝑥 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ) → 𝑟 = 𝑥 ) → ∀ 𝑟 ∈ ℕ0 ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷 ∥ 𝑁 ) → ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) → 𝑟 = 0 ) ) ) |
36 |
12 35
|
simpl2im |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ∀ 𝑟 ∈ ℕ0 ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷 ∥ 𝑁 ) → ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) → 𝑟 = 0 ) ) ) |
37 |
|
r19.21v |
⊢ ( ∀ 𝑟 ∈ ℕ0 ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷 ∥ 𝑁 ) → ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) → 𝑟 = 0 ) ) ↔ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷 ∥ 𝑁 ) → ∀ 𝑟 ∈ ℕ0 ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) → 𝑟 = 0 ) ) ) |
38 |
36 37
|
sylib |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷 ∥ 𝑁 ) → ∀ 𝑟 ∈ ℕ0 ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) → 𝑟 = 0 ) ) ) |
39 |
38
|
expd |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐷 ∥ 𝑁 → ∀ 𝑟 ∈ ℕ0 ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) → 𝑟 = 0 ) ) ) ) |
40 |
39
|
pm2.43i |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐷 ∥ 𝑁 → ∀ 𝑟 ∈ ℕ0 ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) → 𝑟 = 0 ) ) ) |
41 |
40
|
3impia |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁 ) → ∀ 𝑟 ∈ ℕ0 ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) → 𝑟 = 0 ) ) |
42 |
|
breq1 |
⊢ ( 𝑟 = 𝐾 → ( 𝑟 < 𝐷 ↔ 𝐾 < 𝐷 ) ) |
43 |
|
oveq2 |
⊢ ( 𝑟 = 𝐾 → ( 𝑁 − 𝑟 ) = ( 𝑁 − 𝐾 ) ) |
44 |
43
|
breq2d |
⊢ ( 𝑟 = 𝐾 → ( 𝐷 ∥ ( 𝑁 − 𝑟 ) ↔ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) |
45 |
42 44
|
anbi12d |
⊢ ( 𝑟 = 𝐾 → ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ↔ ( 𝐾 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) ) |
46 |
|
eqeq1 |
⊢ ( 𝑟 = 𝐾 → ( 𝑟 = 0 ↔ 𝐾 = 0 ) ) |
47 |
45 46
|
imbi12d |
⊢ ( 𝑟 = 𝐾 → ( ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) → 𝑟 = 0 ) ↔ ( ( 𝐾 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) → 𝐾 = 0 ) ) ) |
48 |
47
|
rspcv |
⊢ ( 𝐾 ∈ ℕ0 → ( ∀ 𝑟 ∈ ℕ0 ( ( 𝑟 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) → 𝑟 = 0 ) → ( ( 𝐾 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) → 𝐾 = 0 ) ) ) |
49 |
41 48
|
syl5com |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁 ) → ( 𝐾 ∈ ℕ0 → ( ( 𝐾 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) → 𝐾 = 0 ) ) ) |
50 |
|
pm4.14 |
⊢ ( ( ( 𝐾 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) → 𝐾 = 0 ) ↔ ( ( 𝐾 < 𝐷 ∧ ¬ 𝐾 = 0 ) → ¬ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) |
51 |
49 50
|
syl6ib |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁 ) → ( 𝐾 ∈ ℕ0 → ( ( 𝐾 < 𝐷 ∧ ¬ 𝐾 = 0 ) → ¬ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) ) |
52 |
5 51
|
syl7bi |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁 ) → ( 𝐾 ∈ ℕ0 → ( ( 𝐾 < 𝐷 ∧ 𝐾 ≠ 0 ) → ¬ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) ) |
53 |
52
|
exp4a |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁 ) → ( 𝐾 ∈ ℕ0 → ( 𝐾 < 𝐷 → ( 𝐾 ≠ 0 → ¬ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) ) ) |
54 |
53
|
com23 |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁 ) → ( 𝐾 < 𝐷 → ( 𝐾 ∈ ℕ0 → ( 𝐾 ≠ 0 → ¬ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) ) ) |
55 |
54
|
imp4a |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁 ) → ( 𝐾 < 𝐷 → ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 ≠ 0 ) → ¬ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) ) |
56 |
3 55
|
syl7 |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁 ) → ( 𝐾 < 𝐷 → ( 𝐾 ∈ ℕ → ¬ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) ) |
57 |
56
|
impcomd |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∥ 𝑁 ) → ( ( 𝐾 ∈ ℕ ∧ 𝐾 < 𝐷 ) → ¬ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) |
58 |
57
|
3expia |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐷 ∥ 𝑁 → ( ( 𝐾 ∈ ℕ ∧ 𝐾 < 𝐷 ) → ¬ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) ) |
59 |
58
|
com23 |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ( 𝐾 ∈ ℕ ∧ 𝐾 < 𝐷 ) → ( 𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) ) |
60 |
59
|
3impia |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐾 < 𝐷 ) ) → ( 𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ ( 𝑁 − 𝐾 ) ) ) |