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 e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> ( k e. ( 0 ... N ) /\ j e. ( 0 ... ( N - k ) ) ) )

Proof

Step Hyp Ref Expression
1 elfzle1 
 |-  ( j e. ( 0 ... N ) -> 0 <_ j )
2 1 adantr 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> 0 <_ j )
3 elfz3nn0 
 |-  ( j e. ( 0 ... N ) -> N e. NN0 )
4 3 adantr 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> N e. NN0 )
5 4 nn0zd 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> N e. ZZ )
6 5 zred 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> N e. RR )
7 elfzelz 
 |-  ( j e. ( 0 ... N ) -> j e. ZZ )
8 7 adantr 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> j e. ZZ )
9 8 zred 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> j e. RR )
10 6 9 subge02d 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> ( 0 <_ j <-> ( N - j ) <_ N ) )
11 2 10 mpbid 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> ( N - j ) <_ N )
12 5 8 zsubcld 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> ( N - j ) e. ZZ )
13 eluz 
 |-  ( ( ( N - j ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( N - j ) ) <-> ( N - j ) <_ N ) )
14 12 5 13 syl2anc 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> ( N e. ( ZZ>= ` ( N - j ) ) <-> ( N - j ) <_ N ) )
15 11 14 mpbird 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> N e. ( ZZ>= ` ( N - j ) ) )
16 fzss2 
 |-  ( N e. ( ZZ>= ` ( N - j ) ) -> ( 0 ... ( N - j ) ) C_ ( 0 ... N ) )
17 15 16 syl 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> ( 0 ... ( N - j ) ) C_ ( 0 ... N ) )
18 simpr 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> k e. ( 0 ... ( N - j ) ) )
19 17 18 sseldd 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> k e. ( 0 ... N ) )
20 elfzelz 
 |-  ( k e. ( 0 ... ( N - j ) ) -> k e. ZZ )
21 20 adantl 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> k e. ZZ )
22 21 zred 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> k e. RR )
23 elfzle2 
 |-  ( k e. ( 0 ... ( N - j ) ) -> k <_ ( N - j ) )
24 23 adantl 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> k <_ ( N - j ) )
25 22 6 9 24 lesubd 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> j <_ ( N - k ) )
26 elfzuz 
 |-  ( j e. ( 0 ... N ) -> j e. ( ZZ>= ` 0 ) )
27 26 adantr 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> j e. ( ZZ>= ` 0 ) )
28 5 21 zsubcld 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> ( N - k ) e. ZZ )
29 elfz5 
 |-  ( ( j e. ( ZZ>= ` 0 ) /\ ( N - k ) e. ZZ ) -> ( j e. ( 0 ... ( N - k ) ) <-> j <_ ( N - k ) ) )
30 27 28 29 syl2anc 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> ( j e. ( 0 ... ( N - k ) ) <-> j <_ ( N - k ) ) )
31 25 30 mpbird 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> j e. ( 0 ... ( N - k ) ) )
32 19 31 jca 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> ( k e. ( 0 ... N ) /\ j e. ( 0 ... ( N - k ) ) ) )