Theorem pfxccatin12lem2a

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

	Ref	Expression
Assertion	pfxccatin12lem2a	⊢ ( ( 𝑀 ∈ ( 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		elfzoelz	⊢ ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → 𝐾 ∈ ℤ )
10		elfzelz	⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → 𝑁 ∈ ℤ )
11		simpl	⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝐿 ∈ ℤ )
12		simpl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℤ )
13	11 12	anim12i	⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
14		simpr	⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
15		simpr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℤ )
16	14 15	anim12ci	⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
17	13 16	jca	⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) )
18	17	exp32	⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ∈ ℤ → ( 𝐾 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ) ) )
19	10 18	syl5	⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝐾 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ) ) )
20	19	3adant1	⊢ ( ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝐾 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ) ) )
21	20	adantr	⊢ ( ( ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 0 ≤ 𝑀 ∧ 𝑀 ≤ 𝐿 ) ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝐾 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ) ) )
22	1 21	sylbi	⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝐾 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ) ) )
23	22	imp	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ) )
24	23	impcom	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) )
25		elfzomelpfzo	⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ↔ ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑁 ) ) )
26	24 25	syl	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ↔ ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑁 ) ) )
27		elfz2	⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) ↔ ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) )
28		simpl3	⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) → 𝑁 ∈ ℤ )
29		simpl2	⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) → 𝑋 ∈ ℤ )
30		simpr	⊢ ( ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) → 𝑁 ≤ 𝑋 )
31	30	adantl	⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) → 𝑁 ≤ 𝑋 )
32	28 29 31	3jca	⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) → ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋 ) )
33	27 32	sylbi	⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋 ) )
34	33	adantl	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋 ) )
35	34	adantl	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋 ) )
36		eluz2	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋 ) )
37	35 36	sylibr	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → 𝑋 ∈ ( ℤ≥ ‘ 𝑁 ) )
38		fzoss2	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐿 ..^ 𝑁 ) ⊆ ( 𝐿 ..^ 𝑋 ) )
39	37 38	syl	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → ( 𝐿 ..^ 𝑁 ) ⊆ ( 𝐿 ..^ 𝑋 ) )
40	39	sseld	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → ( ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑁 ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) )
41	26 40	sylbid	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) )
42	41	ex	⊢ ( 𝐾 ∈ ℤ → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) ) )
43	42	com23	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) ) )
44	9 43	mpcom	⊢ ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) )
45	44	com12	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) )
46	8 45	syld	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) )