# 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 ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to \left({k}\in \left(0\dots {N}\right)\wedge {j}\in \left(0\dots {N}-{k}\right)\right)$

### Proof

Step Hyp Ref Expression
1 elfzle1 ${⊢}{j}\in \left(0\dots {N}\right)\to 0\le {j}$
2 1 adantr ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to 0\le {j}$
3 elfz3nn0 ${⊢}{j}\in \left(0\dots {N}\right)\to {N}\in {ℕ}_{0}$
4 3 adantr ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {N}\in {ℕ}_{0}$
5 4 nn0zd ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {N}\in ℤ$
6 5 zred ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {N}\in ℝ$
7 elfzelz ${⊢}{j}\in \left(0\dots {N}\right)\to {j}\in ℤ$
8 7 adantr ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {j}\in ℤ$
9 8 zred ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {j}\in ℝ$
10 6 9 subge02d ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to \left(0\le {j}↔{N}-{j}\le {N}\right)$
11 2 10 mpbid ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {N}-{j}\le {N}$
12 5 8 zsubcld ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {N}-{j}\in ℤ$
13 eluz ${⊢}\left({N}-{j}\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\in {ℤ}_{\ge \left({N}-{j}\right)}↔{N}-{j}\le {N}\right)$
14 12 5 13 syl2anc ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to \left({N}\in {ℤ}_{\ge \left({N}-{j}\right)}↔{N}-{j}\le {N}\right)$
15 11 14 mpbird ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {N}\in {ℤ}_{\ge \left({N}-{j}\right)}$
16 fzss2 ${⊢}{N}\in {ℤ}_{\ge \left({N}-{j}\right)}\to \left(0\dots {N}-{j}\right)\subseteq \left(0\dots {N}\right)$
17 15 16 syl ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to \left(0\dots {N}-{j}\right)\subseteq \left(0\dots {N}\right)$
18 simpr ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {k}\in \left(0\dots {N}-{j}\right)$
19 17 18 sseldd ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {k}\in \left(0\dots {N}\right)$
20 elfzelz ${⊢}{k}\in \left(0\dots {N}-{j}\right)\to {k}\in ℤ$
21 20 adantl ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {k}\in ℤ$
22 21 zred ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {k}\in ℝ$
23 elfzle2 ${⊢}{k}\in \left(0\dots {N}-{j}\right)\to {k}\le {N}-{j}$
24 23 adantl ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {k}\le {N}-{j}$
25 22 6 9 24 lesubd ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {j}\le {N}-{k}$
26 elfzuz ${⊢}{j}\in \left(0\dots {N}\right)\to {j}\in {ℤ}_{\ge 0}$
27 26 adantr ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {j}\in {ℤ}_{\ge 0}$
28 5 21 zsubcld ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {N}-{k}\in ℤ$
29 elfz5 ${⊢}\left({j}\in {ℤ}_{\ge 0}\wedge {N}-{k}\in ℤ\right)\to \left({j}\in \left(0\dots {N}-{k}\right)↔{j}\le {N}-{k}\right)$
30 27 28 29 syl2anc ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to \left({j}\in \left(0\dots {N}-{k}\right)↔{j}\le {N}-{k}\right)$
31 25 30 mpbird ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to {j}\in \left(0\dots {N}-{k}\right)$
32 19 31 jca ${⊢}\left({j}\in \left(0\dots {N}\right)\wedge {k}\in \left(0\dots {N}-{j}\right)\right)\to \left({k}\in \left(0\dots {N}\right)\wedge {j}\in \left(0\dots {N}-{k}\right)\right)$