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 ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) ) )

Proof

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