Proof of Theorem ubmelm1fzo
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfzo0 13740 | . 2
⊢ (𝐾 ∈ (0..^𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) | 
| 2 |  | nnz 12634 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) | 
| 3 | 2 | adantr 480 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ 𝑁 ∈
ℤ) | 
| 4 |  | nn0z 12638 | . . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) | 
| 5 | 4 | adantl 481 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ 𝐾 ∈
ℤ) | 
| 6 | 3, 5 | zsubcld 12727 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ (𝑁 − 𝐾) ∈
ℤ) | 
| 7 | 6 | ancoms 458 | . . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑁 − 𝐾) ∈
ℤ) | 
| 8 |  | peano2zm 12660 | . . . . . 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 613 | . . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝐾 ∈ ℤ
∧ 𝑁 ∈
ℤ)) | 
| 13 | 12 | 3adant3 1133 | . . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 14 |  | znnsub 12663 | . . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑁 ↔ (𝑁 − 𝐾) ∈ ℕ)) | 
| 15 | 13, 14 | syl 17 | . . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝐾 < 𝑁 ↔ (𝑁 − 𝐾) ∈ ℕ)) | 
| 16 | 11, 15 | mpbid 232 | . . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝑁 − 𝐾) ∈ ℕ) | 
| 17 |  | nnm1ge0 12686 | . . . . 5
⊢ ((𝑁 − 𝐾) ∈ ℕ → 0 ≤ ((𝑁 − 𝐾) − 1)) | 
| 18 | 16, 17 | syl 17 | . . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → 0 ≤ ((𝑁 − 𝐾) − 1)) | 
| 19 |  | elnn0z 12626 | . . . 4
⊢ (((𝑁 − 𝐾) − 1) ∈ ℕ0
↔ (((𝑁 − 𝐾) − 1) ∈ ℤ
∧ 0 ≤ ((𝑁 −
𝐾) −
1))) | 
| 20 | 10, 18, 19 | sylanbrc 583 | . . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) ∈
ℕ0) | 
| 21 |  | simp2 1138 | . . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → 𝑁 ∈ ℕ) | 
| 22 |  | nncn 12274 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 23 | 22 | adantl 481 | . . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑁 ∈
ℂ) | 
| 24 |  | nn0cn 12536 | . . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) | 
| 25 | 24 | adantr 480 | . . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝐾 ∈
ℂ) | 
| 26 |  | 1cnd 11256 | . . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 1 ∈ ℂ) | 
| 27 | 23, 25, 26 | subsub4d 11651 | . . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((𝑁 − 𝐾) − 1) = (𝑁 − (𝐾 + 1))) | 
| 28 |  | nn0p1gt0 12555 | . . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ 0 < (𝐾 +
1)) | 
| 29 | 28 | adantr 480 | . . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 0 < (𝐾 +
1)) | 
| 30 |  | nn0re 12535 | . . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) | 
| 31 |  | peano2re 11434 | . . . . . . . 8
⊢ (𝐾 ∈ ℝ → (𝐾 + 1) ∈
ℝ) | 
| 32 | 30, 31 | syl 17 | . . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℝ) | 
| 33 |  | nnre 12273 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 34 |  | ltsubpos 11755 | . . . . . . 7
⊢ (((𝐾 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 <
(𝐾 + 1) ↔ (𝑁 − (𝐾 + 1)) < 𝑁)) | 
| 35 | 32, 33, 34 | syl2an 596 | . . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (0 < (𝐾 + 1)
↔ (𝑁 − (𝐾 + 1)) < 𝑁)) | 
| 36 | 29, 35 | mpbid 232 | . . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑁 − (𝐾 + 1)) < 𝑁) | 
| 37 | 27, 36 | eqbrtrd 5165 | . . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((𝑁 − 𝐾) − 1) < 𝑁) | 
| 38 | 37 | 3adant3 1133 | . . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) < 𝑁) | 
| 39 |  | elfzo0 13740 | . . 3
⊢ (((𝑁 − 𝐾) − 1) ∈ (0..^𝑁) ↔ (((𝑁 − 𝐾) − 1) ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ ((𝑁 − 𝐾) − 1) < 𝑁)) | 
| 40 | 20, 21, 38, 39 | syl3anbrc 1344 | . 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → ((𝑁 − 𝐾) − 1) ∈ (0..^𝑁)) | 
| 41 | 1, 40 | sylbi 217 | 1
⊢ (𝐾 ∈ (0..^𝑁) → ((𝑁 − 𝐾) − 1) ∈ (0..^𝑁)) |