Proof of Theorem fsum0diaglem
Step | Hyp | Ref
| Expression |
1 | | elfzle1 9970 |
. . . . . . 7
⊢ (𝑗 ∈ (0...𝑁) → 0 ≤ 𝑗) |
2 | 1 | adantr 274 |
. . . . . 6
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 0 ≤ 𝑗) |
3 | | elfz3nn0 10058 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (0...𝑁) → 𝑁 ∈
ℕ0) |
4 | 3 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑁 ∈
ℕ0) |
5 | 4 | nn0zd 9319 |
. . . . . . . 8
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑁 ∈ ℤ) |
6 | 5 | zred 9321 |
. . . . . . 7
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑁 ∈ ℝ) |
7 | | elfzelz 9968 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ) |
8 | 7 | adantr 274 |
. . . . . . . 8
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑗 ∈ ℤ) |
9 | 8 | zred 9321 |
. . . . . . 7
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑗 ∈ ℝ) |
10 | 6, 9 | subge02d 8443 |
. . . . . 6
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (0 ≤ 𝑗 ↔ (𝑁 − 𝑗) ≤ 𝑁)) |
11 | 2, 10 | mpbid 146 |
. . . . 5
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (𝑁 − 𝑗) ≤ 𝑁) |
12 | 5, 8 | zsubcld 9326 |
. . . . . 6
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (𝑁 − 𝑗) ∈ ℤ) |
13 | | eluz 9487 |
. . . . . 6
⊢ (((𝑁 − 𝑗) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘(𝑁 − 𝑗)) ↔ (𝑁 − 𝑗) ≤ 𝑁)) |
14 | 12, 5, 13 | syl2anc 409 |
. . . . 5
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (𝑁 ∈ (ℤ≥‘(𝑁 − 𝑗)) ↔ (𝑁 − 𝑗) ≤ 𝑁)) |
15 | 11, 14 | mpbird 166 |
. . . 4
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑁 ∈ (ℤ≥‘(𝑁 − 𝑗))) |
16 | | fzss2 10007 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 𝑗)) → (0...(𝑁 − 𝑗)) ⊆ (0...𝑁)) |
17 | 15, 16 | syl 14 |
. . 3
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (0...(𝑁 − 𝑗)) ⊆ (0...𝑁)) |
18 | | simpr 109 |
. . 3
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑘 ∈ (0...(𝑁 − 𝑗))) |
19 | 17, 18 | sseldd 3148 |
. 2
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑘 ∈ (0...𝑁)) |
20 | | elfzelz 9968 |
. . . . . 6
⊢ (𝑘 ∈ (0...(𝑁 − 𝑗)) → 𝑘 ∈ ℤ) |
21 | 20 | adantl 275 |
. . . . 5
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑘 ∈ ℤ) |
22 | 21 | zred 9321 |
. . . 4
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑘 ∈ ℝ) |
23 | | elfzle2 9971 |
. . . . 5
⊢ (𝑘 ∈ (0...(𝑁 − 𝑗)) → 𝑘 ≤ (𝑁 − 𝑗)) |
24 | 23 | adantl 275 |
. . . 4
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑘 ≤ (𝑁 − 𝑗)) |
25 | 22, 6, 9, 24 | lesubd 8455 |
. . 3
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑗 ≤ (𝑁 − 𝑘)) |
26 | | elfzuz 9964 |
. . . . 5
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈
(ℤ≥‘0)) |
27 | 26 | adantr 274 |
. . . 4
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑗 ∈
(ℤ≥‘0)) |
28 | 5, 21 | zsubcld 9326 |
. . . 4
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (𝑁 − 𝑘) ∈ ℤ) |
29 | | elfz5 9960 |
. . . 4
⊢ ((𝑗 ∈
(ℤ≥‘0) ∧ (𝑁 − 𝑘) ∈ ℤ) → (𝑗 ∈ (0...(𝑁 − 𝑘)) ↔ 𝑗 ≤ (𝑁 − 𝑘))) |
30 | 27, 28, 29 | syl2anc 409 |
. . 3
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (𝑗 ∈ (0...(𝑁 − 𝑘)) ↔ 𝑗 ≤ (𝑁 − 𝑘))) |
31 | 25, 30 | mpbird 166 |
. 2
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → 𝑗 ∈ (0...(𝑁 − 𝑘))) |
32 | 19, 31 | jca 304 |
1
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (𝑘 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 𝑘)))) |