fsum0diaglem

		Ref	Expression
	Assertion	fsum0diaglem	$⊢ (j \in (0 \dots N) \land k \in (0 \dots N - j)) \to (k \in (0 \dots N) \land j \in (0 \dots N - k))$

Proof

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

Metamath Proof Explorer

Theorem fsum0diaglem

Proof