Step |
Hyp |
Ref |
Expression |
1 |
|
elfzo0 |
⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) ) |
2 |
|
nnz |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ ) |
3 |
2
|
adantr |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ ℤ ) |
4 |
|
nn0z |
⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℤ ) |
5 |
4
|
adantl |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℤ ) |
6 |
3 5
|
zsubcld |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 − 𝐾 ) ∈ ℤ ) |
7 |
6
|
ancoms |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 𝐾 ) ∈ ℤ ) |
8 |
|
peano2zm |
⊢ ( ( 𝑁 − 𝐾 ) ∈ ℤ → ( ( 𝑁 − 𝐾 ) − 1 ) ∈ ℤ ) |
9 |
7 8
|
syl |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 𝐾 ) − 1 ) ∈ ℤ ) |
10 |
9
|
3adant3 |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( ( 𝑁 − 𝐾 ) − 1 ) ∈ ℤ ) |
11 |
|
simp3 |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → 𝐾 < 𝑁 ) |
12 |
4 2
|
anim12i |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) |
13 |
12
|
3adant3 |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) |
14 |
|
znnsub |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 ↔ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) |
15 |
13 14
|
syl |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( 𝐾 < 𝑁 ↔ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) |
16 |
11 15
|
mpbid |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ ) |
17 |
|
nnm1ge0 |
⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ → 0 ≤ ( ( 𝑁 − 𝐾 ) − 1 ) ) |
18 |
16 17
|
syl |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → 0 ≤ ( ( 𝑁 − 𝐾 ) − 1 ) ) |
19 |
|
elnn0z |
⊢ ( ( ( 𝑁 − 𝐾 ) − 1 ) ∈ ℕ0 ↔ ( ( ( 𝑁 − 𝐾 ) − 1 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑁 − 𝐾 ) − 1 ) ) ) |
20 |
10 18 19
|
sylanbrc |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( ( 𝑁 − 𝐾 ) − 1 ) ∈ ℕ0 ) |
21 |
|
simp2 |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → 𝑁 ∈ ℕ ) |
22 |
|
nncn |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ ) |
23 |
22
|
adantl |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ ) |
24 |
|
nn0cn |
⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℂ ) |
25 |
24
|
adantr |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ℂ ) |
26 |
|
1cnd |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → 1 ∈ ℂ ) |
27 |
23 25 26
|
subsub4d |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 𝐾 ) − 1 ) = ( 𝑁 − ( 𝐾 + 1 ) ) ) |
28 |
|
nn0p1gt0 |
⊢ ( 𝐾 ∈ ℕ0 → 0 < ( 𝐾 + 1 ) ) |
29 |
28
|
adantr |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → 0 < ( 𝐾 + 1 ) ) |
30 |
|
nn0re |
⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ ) |
31 |
|
peano2re |
⊢ ( 𝐾 ∈ ℝ → ( 𝐾 + 1 ) ∈ ℝ ) |
32 |
30 31
|
syl |
⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℝ ) |
33 |
|
nnre |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ ) |
34 |
|
ltsubpos |
⊢ ( ( ( 𝐾 + 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 < ( 𝐾 + 1 ) ↔ ( 𝑁 − ( 𝐾 + 1 ) ) < 𝑁 ) ) |
35 |
32 33 34
|
syl2an |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 0 < ( 𝐾 + 1 ) ↔ ( 𝑁 − ( 𝐾 + 1 ) ) < 𝑁 ) ) |
36 |
29 35
|
mpbid |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − ( 𝐾 + 1 ) ) < 𝑁 ) |
37 |
27 36
|
eqbrtrd |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 𝐾 ) − 1 ) < 𝑁 ) |
38 |
37
|
3adant3 |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( ( 𝑁 − 𝐾 ) − 1 ) < 𝑁 ) |
39 |
|
elfzo0 |
⊢ ( ( ( 𝑁 − 𝐾 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) ↔ ( ( ( 𝑁 − 𝐾 ) − 1 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ ( ( 𝑁 − 𝐾 ) − 1 ) < 𝑁 ) ) |
40 |
20 21 38 39
|
syl3anbrc |
⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( ( 𝑁 − 𝐾 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) ) |
41 |
1 40
|
sylbi |
⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑁 − 𝐾 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) ) |