Metamath Proof Explorer

Theorem pfxccatin12lem1

Description: Lemma 1 for pfxccatin12 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 9-May-2020)

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

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 elfz2nn0 
 |-  ( M e. ( 0 ... L ) <-> ( M e. NN0 /\ L e. NN0 /\ M <_ L ) )
10 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
11 nn0cn 
 |-  ( L e. NN0 -> L e. CC )
12 elfzelz 
 |-  ( N e. ( L ... X ) -> N e. ZZ )
13 zcn 
 |-  ( N e. ZZ -> N e. CC )
14 subcl 
 |-  ( ( L e. CC /\ M e. CC ) -> ( L - M ) e. CC )
15 14 ancoms 
 |-  ( ( M e. CC /\ L e. CC ) -> ( L - M ) e. CC )
16 15 addridd 
 |-  ( ( M e. CC /\ L e. CC ) -> ( ( L - M ) + 0 ) = ( L - M ) )
17 16 eqcomd 
 |-  ( ( M e. CC /\ L e. CC ) -> ( L - M ) = ( ( L - M ) + 0 ) )
18 17 adantl 
 |-  ( ( N e. CC /\ ( M e. CC /\ L e. CC ) ) -> ( L - M ) = ( ( L - M ) + 0 ) )
19 simprr 
 |-  ( ( N e. CC /\ ( M e. CC /\ L e. CC ) ) -> L e. CC )
20 simpl 
 |-  ( ( M e. CC /\ L e. CC ) -> M e. CC )
21 20 adantl 
 |-  ( ( N e. CC /\ ( M e. CC /\ L e. CC ) ) -> M e. CC )
22 simpl 
 |-  ( ( N e. CC /\ ( M e. CC /\ L e. CC ) ) -> N e. CC )
23 19 21 22 npncan3d 
 |-  ( ( N e. CC /\ ( M e. CC /\ L e. CC ) ) -> ( ( L - M ) + ( N - L ) ) = ( N - M ) )
24 23 eqcomd 
 |-  ( ( N e. CC /\ ( M e. CC /\ L e. CC ) ) -> ( N - M ) = ( ( L - M ) + ( N - L ) ) )
25 18 24 oveq12d 
 |-  ( ( N e. CC /\ ( M e. CC /\ L e. CC ) ) -> ( ( L - M ) ..^ ( N - M ) ) = ( ( ( L - M ) + 0 ) ..^ ( ( L - M ) + ( N - L ) ) ) )
26 25 ex 
 |-  ( N e. CC -> ( ( M e. CC /\ L e. CC ) -> ( ( L - M ) ..^ ( N - M ) ) = ( ( ( L - M ) + 0 ) ..^ ( ( L - M ) + ( N - L ) ) ) ) )
27 12 13 26 3syl 
 |-  ( N e. ( L ... X ) -> ( ( M e. CC /\ L e. CC ) -> ( ( L - M ) ..^ ( N - M ) ) = ( ( ( L - M ) + 0 ) ..^ ( ( L - M ) + ( N - L ) ) ) ) )
28 27 com12 
 |-  ( ( M e. CC /\ L e. CC ) -> ( N e. ( L ... X ) -> ( ( L - M ) ..^ ( N - M ) ) = ( ( ( L - M ) + 0 ) ..^ ( ( L - M ) + ( N - L ) ) ) ) )
29 10 11 28 syl2an 
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( N e. ( L ... X ) -> ( ( L - M ) ..^ ( N - M ) ) = ( ( ( L - M ) + 0 ) ..^ ( ( L - M ) + ( N - L ) ) ) ) )
30 29 3adant3 
 |-  ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( N e. ( L ... X ) -> ( ( L - M ) ..^ ( N - M ) ) = ( ( ( L - M ) + 0 ) ..^ ( ( L - M ) + ( N - L ) ) ) ) )
31 9 30 sylbi 
 |-  ( M e. ( 0 ... L ) -> ( N e. ( L ... X ) -> ( ( L - M ) ..^ ( N - M ) ) = ( ( ( L - M ) + 0 ) ..^ ( ( L - M ) + ( N - L ) ) ) ) )
32 31 imp 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( ( L - M ) ..^ ( N - M ) ) = ( ( ( L - M ) + 0 ) ..^ ( ( L - M ) + ( N - L ) ) ) )
33 32 eleq2d 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( K e. ( ( L - M ) ..^ ( N - M ) ) <-> K e. ( ( ( L - M ) + 0 ) ..^ ( ( L - M ) + ( N - L ) ) ) ) )
34 33 biimpa 
 |-  ( ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) /\ K e. ( ( L - M ) ..^ ( N - M ) ) ) -> K e. ( ( ( L - M ) + 0 ) ..^ ( ( L - M ) + ( N - L ) ) ) )
35 0zd 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> 0 e. ZZ )
36 elfz2 
 |-  ( N e. ( L ... X ) <-> ( ( L e. ZZ /\ X e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ X ) ) )
37 zsubcl 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( N - L ) e. ZZ )
38 37 ancoms 
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> ( N - L ) e. ZZ )
39 38 3adant2 
 |-  ( ( L e. ZZ /\ X e. ZZ /\ N e. ZZ ) -> ( N - L ) e. ZZ )
40 39 adantr 
 |-  ( ( ( L e. ZZ /\ X e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ X ) ) -> ( N - L ) e. ZZ )
41 36 40 sylbi 
 |-  ( N e. ( L ... X ) -> ( N - L ) e. ZZ )
42 41 adantl 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( N - L ) e. ZZ )
43 6 35 42 3jca 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( ( L - M ) e. ZZ /\ 0 e. ZZ /\ ( N - L ) e. ZZ ) )
44 43 adantr 
 |-  ( ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) /\ K e. ( ( L - M ) ..^ ( N - M ) ) ) -> ( ( L - M ) e. ZZ /\ 0 e. ZZ /\ ( N - L ) e. ZZ ) )
45 fzosubel2 
 |-  ( ( K e. ( ( ( L - M ) + 0 ) ..^ ( ( L - M ) + ( N - L ) ) ) /\ ( ( L - M ) e. ZZ /\ 0 e. ZZ /\ ( N - L ) e. ZZ ) ) -> ( K - ( L - M ) ) e. ( 0 ..^ ( N - L ) ) )
46 34 44 45 syl2anc 
 |-  ( ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) /\ K e. ( ( L - M ) ..^ ( N - M ) ) ) -> ( K - ( L - M ) ) e. ( 0 ..^ ( N - L ) ) )
47 46 ex 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( K e. ( ( L - M ) ..^ ( N - M ) ) -> ( K - ( L - M ) ) e. ( 0 ..^ ( N - L ) ) ) )
48 8 47 syld 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> ( K - ( L - M ) ) e. ( 0 ..^ ( N - L ) ) ) )