Metamath Proof Explorer

Theorem pfxccatin12lem2a

Description: Lemma for pfxccatin12lem2 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 27-May-2018)

Ref Expression
Assertion pfxccatin12lem2a 
|- ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> ( K + M ) e. ( L ..^ X ) ) )

Proof

Step Hyp Ref Expression
1 elfz2 
 |-  ( M e. ( 0 ... L ) <-> ( ( 0 e. ZZ /\ L e. ZZ /\ M e. ZZ ) /\ ( 0 <_ M /\ M <_ L ) ) )
2 zsubcl 
 |-  ( ( L e. ZZ /\ M e. ZZ ) -> ( L - M ) e. ZZ )
3 2 3adant1 
 |-  ( ( 0 e. ZZ /\ L e. ZZ /\ M e. ZZ ) -> ( L - M ) e. ZZ )
4 3 adantr 
 |-  ( ( ( 0 e. ZZ /\ L e. ZZ /\ M e. ZZ ) /\ ( 0 <_ M /\ M <_ L ) ) -> ( L - M ) e. ZZ )
5 1 4 sylbi 
 |-  ( M e. ( 0 ... L ) -> ( L - M ) e. ZZ )
6 5 adantr 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( L - M ) e. ZZ )
7 elfzonelfzo 
 |-  ( ( L - M ) e. ZZ -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> K e. ( ( L - M ) ..^ ( N - M ) ) ) )
8 6 7 syl 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> K e. ( ( L - M ) ..^ ( N - M ) ) ) )
9 elfzoelz 
 |-  ( K e. ( ( L - M ) ..^ ( N - M ) ) -> K e. ZZ )
10 elfzelz 
 |-  ( N e. ( L ... X ) -> N e. ZZ )
11 simpl 
 |-  ( ( L e. ZZ /\ M e. ZZ ) -> L e. ZZ )
12 simpl 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> N e. ZZ )
13 11 12 anim12i 
 |-  ( ( ( L e. ZZ /\ M e. ZZ ) /\ ( N e. ZZ /\ K e. ZZ ) ) -> ( L e. ZZ /\ N e. ZZ ) )
14 simpr 
 |-  ( ( L e. ZZ /\ M e. ZZ ) -> M e. ZZ )
15 simpr 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> K e. ZZ )
16 14 15 anim12ci 
 |-  ( ( ( L e. ZZ /\ M e. ZZ ) /\ ( N e. ZZ /\ K e. ZZ ) ) -> ( K e. ZZ /\ M e. ZZ ) )
17 13 16 jca 
 |-  ( ( ( L e. ZZ /\ M e. ZZ ) /\ ( N e. ZZ /\ K e. ZZ ) ) -> ( ( L e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) )
18 17 exp32 
 |-  ( ( L e. ZZ /\ M e. ZZ ) -> ( N e. ZZ -> ( K e. ZZ -> ( ( L e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) ) ) )
19 10 18 syl5 
 |-  ( ( L e. ZZ /\ M e. ZZ ) -> ( N e. ( L ... X ) -> ( K e. ZZ -> ( ( L e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) ) ) )
20 19 3adant1 
 |-  ( ( 0 e. ZZ /\ L e. ZZ /\ M e. ZZ ) -> ( N e. ( L ... X ) -> ( K e. ZZ -> ( ( L e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) ) ) )
21 20 adantr 
 |-  ( ( ( 0 e. ZZ /\ L e. ZZ /\ M e. ZZ ) /\ ( 0 <_ M /\ M <_ L ) ) -> ( N e. ( L ... X ) -> ( K e. ZZ -> ( ( L e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) ) ) )
22 1 21 sylbi 
 |-  ( M e. ( 0 ... L ) -> ( N e. ( L ... X ) -> ( K e. ZZ -> ( ( L e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) ) ) )
23 22 imp 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( K e. ZZ -> ( ( L e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) ) )
24 23 impcom 
 |-  ( ( K e. ZZ /\ ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) ) -> ( ( L e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) )
25 elfzomelpfzo 
 |-  ( ( ( L e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( K e. ( ( L - M ) ..^ ( N - M ) ) <-> ( K + M ) e. ( L ..^ N ) ) )
26 24 25 syl 
 |-  ( ( K e. ZZ /\ ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) ) -> ( K e. ( ( L - M ) ..^ ( N - M ) ) <-> ( K + M ) e. ( L ..^ N ) ) )
27 elfz2 
 |-  ( N e. ( L ... X ) <-> ( ( L e. ZZ /\ X e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ X ) ) )
28 simpl3 
 |-  ( ( ( L e. ZZ /\ X e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ X ) ) -> N e. ZZ )
29 simpl2 
 |-  ( ( ( L e. ZZ /\ X e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ X ) ) -> X e. ZZ )
30 simpr 
 |-  ( ( L <_ N /\ N <_ X ) -> N <_ X )
31 30 adantl 
 |-  ( ( ( L e. ZZ /\ X e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ X ) ) -> N <_ X )
32 28 29 31 3jca 
 |-  ( ( ( L e. ZZ /\ X e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ X ) ) -> ( N e. ZZ /\ X e. ZZ /\ N <_ X ) )
33 27 32 sylbi 
 |-  ( N e. ( L ... X ) -> ( N e. ZZ /\ X e. ZZ /\ N <_ X ) )
34 33 adantl 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( N e. ZZ /\ X e. ZZ /\ N <_ X ) )
35 34 adantl 
 |-  ( ( K e. ZZ /\ ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) ) -> ( N e. ZZ /\ X e. ZZ /\ N <_ X ) )
36 eluz2 
 |-  ( X e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ X e. ZZ /\ N <_ X ) )
37 35 36 sylibr 
 |-  ( ( K e. ZZ /\ ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) ) -> X e. ( ZZ>= ` N ) )
38 fzoss2 
 |-  ( X e. ( ZZ>= ` N ) -> ( L ..^ N ) C_ ( L ..^ X ) )
39 37 38 syl 
 |-  ( ( K e. ZZ /\ ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) ) -> ( L ..^ N ) C_ ( L ..^ X ) )
40 39 sseld 
 |-  ( ( K e. ZZ /\ ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) ) -> ( ( K + M ) e. ( L ..^ N ) -> ( K + M ) e. ( L ..^ X ) ) )
41 26 40 sylbid 
 |-  ( ( K e. ZZ /\ ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) ) -> ( K e. ( ( L - M ) ..^ ( N - M ) ) -> ( K + M ) e. ( L ..^ X ) ) )
42 41 ex 
 |-  ( K e. ZZ -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( K e. ( ( L - M ) ..^ ( N - M ) ) -> ( K + M ) e. ( L ..^ X ) ) ) )
43 42 com23 
 |-  ( K e. ZZ -> ( K e. ( ( L - M ) ..^ ( N - M ) ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( K + M ) e. ( L ..^ X ) ) ) )
44 9 43 mpcom 
 |-  ( K e. ( ( L - M ) ..^ ( N - M ) ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( K + M ) e. ( L ..^ X ) ) )
45 44 com12 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( K e. ( ( L - M ) ..^ ( N - M ) ) -> ( K + M ) e. ( L ..^ X ) ) )
46 8 45 syld 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> ( K + M ) e. ( L ..^ X ) ) )