Metamath Proof Explorer

Theorem pfxccatin12lem4

Description: Lemma 4 for pfxccatin12 . (Contributed by Alexander van der Vekens, 30-Mar-2018) (Revised by Alexander van der Vekens, 23-May-2018)

Ref Expression
Assertion pfxccatin12lem4 
|- ( ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> K e. ( ( L - M ) ..^ ( ( L - M ) + ( N - L ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( L e. NN0 -> L e. ZZ )
2 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
3 zsubcl 
 |-  ( ( L e. ZZ /\ M e. ZZ ) -> ( L - M ) e. ZZ )
4 1 2 3 syl2an 
 |-  ( ( L e. NN0 /\ M e. NN0 ) -> ( L - M ) e. ZZ )
5 4 3adant3 
 |-  ( ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) -> ( L - M ) e. ZZ )
6 elfzonelfzo 
 |-  ( ( L - M ) e. ZZ -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> K e. ( ( L - M ) ..^ ( N - M ) ) ) )
7 6 imp 
 |-  ( ( ( L - M ) e. ZZ /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> K e. ( ( L - M ) ..^ ( N - M ) ) )
8 5 7 sylan 
 |-  ( ( ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> K e. ( ( L - M ) ..^ ( N - M ) ) )
9 nn0cn 
 |-  ( L e. NN0 -> L e. CC )
10 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
11 zcn 
 |-  ( N e. ZZ -> N e. CC )
12 npncan3 
 |-  ( ( L e. CC /\ M e. CC /\ N e. CC ) -> ( ( L - M ) + ( N - L ) ) = ( N - M ) )
13 9 10 11 12 syl3an 
 |-  ( ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) -> ( ( L - M ) + ( N - L ) ) = ( N - M ) )
14 13 oveq2d 
 |-  ( ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) -> ( ( L - M ) ..^ ( ( L - M ) + ( N - L ) ) ) = ( ( L - M ) ..^ ( N - M ) ) )
15 14 eleq2d 
 |-  ( ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) -> ( K e. ( ( L - M ) ..^ ( ( L - M ) + ( N - L ) ) ) <-> K e. ( ( L - M ) ..^ ( N - M ) ) ) )
16 15 adantr 
 |-  ( ( ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( K e. ( ( L - M ) ..^ ( ( L - M ) + ( N - L ) ) ) <-> K e. ( ( L - M ) ..^ ( N - M ) ) ) )
17 8 16 mpbird 
 |-  ( ( ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> K e. ( ( L - M ) ..^ ( ( L - M ) + ( N - L ) ) ) )
18 17 ex 
 |-  ( ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> K e. ( ( L - M ) ..^ ( ( L - M ) + ( N - L ) ) ) ) )