Proof of Theorem ubmelm1fzo
Step | Hyp | Ref
| Expression |
1 | | elfzo0 13169 |
. 2
⊢ (𝐾 ∈ (0..^𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) |
2 | | nnz 12085 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
3 | 2 | adantr 484 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
4 | | nn0z 12086 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
5 | 4 | adantl 485 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ 𝐾 ∈
ℤ) |
6 | 3, 5 | zsubcld 12173 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ (𝑁 − 𝐾) ∈
ℤ) |
7 | 6 | ancoms 462 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑁 − 𝐾) ∈
ℤ) |
8 | | peano2zm 12106 |
. . . . . 6
⊢ ((𝑁 − 𝐾) ∈ ℤ → ((𝑁 − 𝐾) − 1) ∈
ℤ) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((𝑁 − 𝐾) − 1) ∈
ℤ) |
10 | 9 | 3adant3 1133 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) ∈
ℤ) |
11 | | simp3 1139 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → 𝐾 < 𝑁) |
12 | 4, 2 | anim12i 616 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝐾 ∈ ℤ
∧ 𝑁 ∈
ℤ)) |
13 | 12 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
14 | | znnsub 12109 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑁 ↔ (𝑁 − 𝐾) ∈ ℕ)) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝐾 < 𝑁 ↔ (𝑁 − 𝐾) ∈ ℕ)) |
16 | 11, 15 | mpbid 235 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝑁 − 𝐾) ∈ ℕ) |
17 | | nnm1ge0 12131 |
. . . . 5
⊢ ((𝑁 − 𝐾) ∈ ℕ → 0 ≤ ((𝑁 − 𝐾) − 1)) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → 0 ≤ ((𝑁 − 𝐾) − 1)) |
19 | | elnn0z 12075 |
. . . 4
⊢ (((𝑁 − 𝐾) − 1) ∈ ℕ0
↔ (((𝑁 − 𝐾) − 1) ∈ ℤ
∧ 0 ≤ ((𝑁 −
𝐾) −
1))) |
20 | 10, 18, 19 | sylanbrc 586 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) ∈
ℕ0) |
21 | | simp2 1138 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → 𝑁 ∈ ℕ) |
22 | | nncn 11724 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
23 | 22 | adantl 485 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑁 ∈
ℂ) |
24 | | nn0cn 11986 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
25 | 24 | adantr 484 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝐾 ∈
ℂ) |
26 | | 1cnd 10714 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 1 ∈ ℂ) |
27 | 23, 25, 26 | subsub4d 11106 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((𝑁 − 𝐾) − 1) = (𝑁 − (𝐾 + 1))) |
28 | | nn0p1gt0 12005 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ 0 < (𝐾 +
1)) |
29 | 28 | adantr 484 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 0 < (𝐾 +
1)) |
30 | | nn0re 11985 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
31 | | peano2re 10891 |
. . . . . . . 8
⊢ (𝐾 ∈ ℝ → (𝐾 + 1) ∈
ℝ) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℝ) |
33 | | nnre 11723 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
34 | | ltsubpos 11210 |
. . . . . . 7
⊢ (((𝐾 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 <
(𝐾 + 1) ↔ (𝑁 − (𝐾 + 1)) < 𝑁)) |
35 | 32, 33, 34 | syl2an 599 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (0 < (𝐾 + 1)
↔ (𝑁 − (𝐾 + 1)) < 𝑁)) |
36 | 29, 35 | mpbid 235 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑁 − (𝐾 + 1)) < 𝑁) |
37 | 27, 36 | eqbrtrd 5052 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((𝑁 − 𝐾) − 1) < 𝑁) |
38 | 37 | 3adant3 1133 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) < 𝑁) |
39 | | elfzo0 13169 |
. . 3
⊢ (((𝑁 − 𝐾) − 1) ∈ (0..^𝑁) ↔ (((𝑁 − 𝐾) − 1) ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ ((𝑁 − 𝐾) − 1) < 𝑁)) |
40 | 20, 21, 38, 39 | syl3anbrc 1344 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) ∈ (0..^𝑁)) |
41 | 1, 40 | sylbi 220 |
1
⊢ (𝐾 ∈ (0..^𝑁) → ((𝑁 − 𝐾) − 1) ∈ (0..^𝑁)) |