Metamath Proof Explorer

Theorem fsum0diaglem

Description: Lemma for fsum0diag . (Contributed by Mario Carneiro, 28-Apr-2014) (Revised by Mario Carneiro, 8-Apr-2016)

Ref Expression
Assertion fsum0diaglem ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → k ∈ 0 … N ∧ j ∈ 0 … N − k

Proof

Step Hyp Ref Expression
1 elfzle1 ⊢ j ∈ 0 … N → 0 ≤ j
2 1 adantr ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → 0 ≤ j
3 elfz3nn0 ⊢ j ∈ 0 … N → N ∈ ℕ 0
4 3 adantr ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → N ∈ ℕ 0
5 4 nn0zd ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → N ∈ ℤ
6 5 zred ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → N ∈ ℝ
7 elfzelz ⊢ j ∈ 0 … N → j ∈ ℤ
8 7 adantr ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → j ∈ ℤ
9 8 zred ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → j ∈ ℝ
10 6 9 subge02d ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → 0 ≤ j ↔ N − j ≤ N
11 2 10 mpbid ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → N − j ≤ N
12 5 8 zsubcld ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → N − j ∈ ℤ
13 eluz ⊢ N − j ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ ≥ N − j ↔ N − j ≤ N
14 12 5 13 syl2anc ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → N ∈ ℤ ≥ N − j ↔ N − j ≤ N
15 11 14 mpbird ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → N ∈ ℤ ≥ N − j
16 fzss2 ⊢ N ∈ ℤ ≥ N − j → 0 … N − j ⊆ 0 … N
17 15 16 syl ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → 0 … N − j ⊆ 0 … N
18 simpr ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → k ∈ 0 … N − j
19 17 18 sseldd ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → k ∈ 0 … N
20 elfzelz ⊢ k ∈ 0 … N − j → k ∈ ℤ
21 20 adantl ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → k ∈ ℤ
22 21 zred ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → k ∈ ℝ
23 elfzle2 ⊢ k ∈ 0 … N − j → k ≤ N − j
24 23 adantl ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → k ≤ N − j
25 22 6 9 24 lesubd ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → j ≤ N − k
26 elfzuz ⊢ j ∈ 0 … N → j ∈ ℤ ≥ 0
27 26 adantr ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → j ∈ ℤ ≥ 0
28 5 21 zsubcld ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → N − k ∈ ℤ
29 elfz5 ⊢ j ∈ ℤ ≥ 0 ∧ N − k ∈ ℤ → j ∈ 0 … N − k ↔ j ≤ N − k
30 27 28 29 syl2anc ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → j ∈ 0 … N − k ↔ j ≤ N − k
31 25 30 mpbird ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → j ∈ 0 … N − k
32 19 31 jca ⊢ j ∈ 0 … N ∧ k ∈ 0 … N − j → k ∈ 0 … N ∧ j ∈ 0 … N − k