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 ) ) )