Proof of Theorem ubmelm1fzo
Step | Hyp | Ref
| Expression |
1 | | elfzo0 13428 |
. 2
⊢ (𝐾 ∈ (0..^𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) |
2 | | nnz 12342 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
3 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
4 | | nn0z 12343 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
5 | 4 | adantl 482 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ 𝐾 ∈
ℤ) |
6 | 3, 5 | zsubcld 12431 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ (𝑁 − 𝐾) ∈
ℤ) |
7 | 6 | ancoms 459 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑁 − 𝐾) ∈
ℤ) |
8 | | peano2zm 12363 |
. . . . . 6
⊢ ((𝑁 − 𝐾) ∈ ℤ → ((𝑁 − 𝐾) − 1) ∈
ℤ) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((𝑁 − 𝐾) − 1) ∈
ℤ) |
10 | 9 | 3adant3 1131 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) ∈
ℤ) |
11 | | simp3 1137 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → 𝐾 < 𝑁) |
12 | 4, 2 | anim12i 613 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝐾 ∈ ℤ
∧ 𝑁 ∈
ℤ)) |
13 | 12 | 3adant3 1131 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
14 | | znnsub 12366 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑁 ↔ (𝑁 − 𝐾) ∈ ℕ)) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝐾 < 𝑁 ↔ (𝑁 − 𝐾) ∈ ℕ)) |
16 | 11, 15 | mpbid 231 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝑁 − 𝐾) ∈ ℕ) |
17 | | nnm1ge0 12388 |
. . . . 5
⊢ ((𝑁 − 𝐾) ∈ ℕ → 0 ≤ ((𝑁 − 𝐾) − 1)) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → 0 ≤ ((𝑁 − 𝐾) − 1)) |
19 | | elnn0z 12332 |
. . . 4
⊢ (((𝑁 − 𝐾) − 1) ∈ ℕ0
↔ (((𝑁 − 𝐾) − 1) ∈ ℤ
∧ 0 ≤ ((𝑁 −
𝐾) −
1))) |
20 | 10, 18, 19 | sylanbrc 583 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) ∈
ℕ0) |
21 | | simp2 1136 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → 𝑁 ∈ ℕ) |
22 | | nncn 11981 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
23 | 22 | adantl 482 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑁 ∈
ℂ) |
24 | | nn0cn 12243 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
25 | 24 | adantr 481 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝐾 ∈
ℂ) |
26 | | 1cnd 10970 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 1 ∈ ℂ) |
27 | 23, 25, 26 | subsub4d 11363 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((𝑁 − 𝐾) − 1) = (𝑁 − (𝐾 + 1))) |
28 | | nn0p1gt0 12262 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ 0 < (𝐾 +
1)) |
29 | 28 | adantr 481 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 0 < (𝐾 +
1)) |
30 | | nn0re 12242 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
31 | | peano2re 11148 |
. . . . . . . 8
⊢ (𝐾 ∈ ℝ → (𝐾 + 1) ∈
ℝ) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℝ) |
33 | | nnre 11980 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
34 | | ltsubpos 11467 |
. . . . . . 7
⊢ (((𝐾 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 <
(𝐾 + 1) ↔ (𝑁 − (𝐾 + 1)) < 𝑁)) |
35 | 32, 33, 34 | syl2an 596 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (0 < (𝐾 + 1)
↔ (𝑁 − (𝐾 + 1)) < 𝑁)) |
36 | 29, 35 | mpbid 231 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑁 − (𝐾 + 1)) < 𝑁) |
37 | 27, 36 | eqbrtrd 5096 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((𝑁 − 𝐾) − 1) < 𝑁) |
38 | 37 | 3adant3 1131 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) < 𝑁) |
39 | | elfzo0 13428 |
. . 3
⊢ (((𝑁 − 𝐾) − 1) ∈ (0..^𝑁) ↔ (((𝑁 − 𝐾) − 1) ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ ((𝑁 − 𝐾) − 1) < 𝑁)) |
40 | 20, 21, 38, 39 | syl3anbrc 1342 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) ∈ (0..^𝑁)) |
41 | 1, 40 | sylbi 216 |
1
⊢ (𝐾 ∈ (0..^𝑁) → ((𝑁 − 𝐾) − 1) ∈ (0..^𝑁)) |