Theorem pfxccatin12lem1

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

	Ref	Expression
Assertion	pfxccatin12lem1	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfz2	⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) ↔ ( ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 0 ≤ 𝑀 ∧ 𝑀 ≤ 𝐿 ) ) )
2		zsubcl	⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
3	2	3adant1	⊢ ( ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
4	3	adantr	⊢ ( ( ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 0 ≤ 𝑀 ∧ 𝑀 ≤ 𝐿 ) ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
5	1 4	sylbi	⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
6	5	adantr	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
7		elfzonelfzo	⊢ ( ( 𝐿 − 𝑀 ) ∈ ℤ → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) )
8	6 7	syl	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) )
9		elfz2nn0	⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) )
10		nn0cn	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ )
11		nn0cn	⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℂ )
12		elfzelz	⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → 𝑁 ∈ ℤ )
13		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
14		subcl	⊢ ( ( 𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐿 − 𝑀 ) ∈ ℂ )
15	14	ancoms	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( 𝐿 − 𝑀 ) ∈ ℂ )
16	15	addridd	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( ( 𝐿 − 𝑀 ) + 0 ) = ( 𝐿 − 𝑀 ) )
17	16	eqcomd	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( 𝐿 − 𝑀 ) = ( ( 𝐿 − 𝑀 ) + 0 ) )
18	17	adantl	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → ( 𝐿 − 𝑀 ) = ( ( 𝐿 − 𝑀 ) + 0 ) )
19		simprr	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → 𝐿 ∈ ℂ )
20		simpl	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → 𝑀 ∈ ℂ )
21	20	adantl	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → 𝑀 ∈ ℂ )
22		simpl	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → 𝑁 ∈ ℂ )
23	19 21 22	npncan3d	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) = ( 𝑁 − 𝑀 ) )
24	23	eqcomd	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → ( 𝑁 − 𝑀 ) = ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) )
25	18 24	oveq12d	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) )
26	25	ex	⊢ ( 𝑁 ∈ ℂ → ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
27	12 13 26	3syl	⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
28	27	com12	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
29	10 11 28	syl2an	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
30	29	3adant3	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
31	9 30	sylbi	⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
32	31	imp	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) )
33	32	eleq2d	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ↔ 𝐾 ∈ ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
34	33	biimpa	⊢ ( ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ∧ 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) → 𝐾 ∈ ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) )
35		0zd	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → 0 ∈ ℤ )
36		elfz2	⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) ↔ ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) )
37		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
38	37	ancoms	⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
39	38	3adant2	⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
40	39	adantr	⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
41	36 40	sylbi	⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
42	41	adantl	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
43	6 35 42	3jca	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐿 − 𝑀 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) )
44	43	adantr	⊢ ( ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ∧ 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝐿 − 𝑀 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) )
45		fzosubel2	⊢ ( ( 𝐾 ∈ ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ∧ ( ( 𝐿 − 𝑀 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) )
46	34 44 45	syl2anc	⊢ ( ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ∧ 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) )
47	46	ex	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) ) )
48	8 47	syld	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) ) )