Proof of Theorem ubmelm1fzo
Step | Hyp | Ref
| Expression |
1 | | elfzo0 13081 |
. 2
⊢ (𝐾 ∈ (0..^𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) |
2 | | nnz 12007 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
3 | 2 | adantr 483 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
4 | | nn0z 12008 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
5 | 4 | adantl 484 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ 𝐾 ∈
ℤ) |
6 | 3, 5 | zsubcld 12095 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ (𝑁 − 𝐾) ∈
ℤ) |
7 | 6 | ancoms 461 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑁 − 𝐾) ∈
ℤ) |
8 | | peano2zm 12028 |
. . . . . 6
⊢ ((𝑁 − 𝐾) ∈ ℤ → ((𝑁 − 𝐾) − 1) ∈
ℤ) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((𝑁 − 𝐾) − 1) ∈
ℤ) |
10 | 9 | 3adant3 1128 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) ∈
ℤ) |
11 | | simp3 1134 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → 𝐾 < 𝑁) |
12 | 4, 2 | anim12i 614 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝐾 ∈ ℤ
∧ 𝑁 ∈
ℤ)) |
13 | 12 | 3adant3 1128 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
14 | | znnsub 12031 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑁 ↔ (𝑁 − 𝐾) ∈ ℕ)) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝐾 < 𝑁 ↔ (𝑁 − 𝐾) ∈ ℕ)) |
16 | 11, 15 | mpbid 234 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝑁 − 𝐾) ∈ ℕ) |
17 | | nnm1ge0 12053 |
. . . . 5
⊢ ((𝑁 − 𝐾) ∈ ℕ → 0 ≤ ((𝑁 − 𝐾) − 1)) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → 0 ≤ ((𝑁 − 𝐾) − 1)) |
19 | | elnn0z 11997 |
. . . 4
⊢ (((𝑁 − 𝐾) − 1) ∈ ℕ0
↔ (((𝑁 − 𝐾) − 1) ∈ ℤ
∧ 0 ≤ ((𝑁 −
𝐾) −
1))) |
20 | 10, 18, 19 | sylanbrc 585 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) ∈
ℕ0) |
21 | | simp2 1133 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → 𝑁 ∈ ℕ) |
22 | | nncn 11649 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
23 | 22 | adantl 484 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑁 ∈
ℂ) |
24 | | nn0cn 11910 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
25 | 24 | adantr 483 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝐾 ∈
ℂ) |
26 | | 1cnd 10639 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 1 ∈ ℂ) |
27 | 23, 25, 26 | subsub4d 11031 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((𝑁 − 𝐾) − 1) = (𝑁 − (𝐾 + 1))) |
28 | | nn0p1gt0 11929 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ 0 < (𝐾 +
1)) |
29 | 28 | adantr 483 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 0 < (𝐾 +
1)) |
30 | | nn0re 11909 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
31 | | peano2re 10816 |
. . . . . . . 8
⊢ (𝐾 ∈ ℝ → (𝐾 + 1) ∈
ℝ) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℝ) |
33 | | nnre 11648 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
34 | | ltsubpos 11135 |
. . . . . . 7
⊢ (((𝐾 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 <
(𝐾 + 1) ↔ (𝑁 − (𝐾 + 1)) < 𝑁)) |
35 | 32, 33, 34 | syl2an 597 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (0 < (𝐾 + 1)
↔ (𝑁 − (𝐾 + 1)) < 𝑁)) |
36 | 29, 35 | mpbid 234 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑁 − (𝐾 + 1)) < 𝑁) |
37 | 27, 36 | eqbrtrd 5091 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((𝑁 − 𝐾) − 1) < 𝑁) |
38 | 37 | 3adant3 1128 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) < 𝑁) |
39 | | elfzo0 13081 |
. . 3
⊢ (((𝑁 − 𝐾) − 1) ∈ (0..^𝑁) ↔ (((𝑁 − 𝐾) − 1) ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ ((𝑁 − 𝐾) − 1) < 𝑁)) |
40 | 20, 21, 38, 39 | syl3anbrc 1339 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) ∈ (0..^𝑁)) |
41 | 1, 40 | sylbi 219 |
1
⊢ (𝐾 ∈ (0..^𝑁) → ((𝑁 − 𝐾) − 1) ∈ (0..^𝑁)) |