pfxccatin12lem1

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

		Ref	Expression
	Assertion	pfxccatin12lem1	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to ((K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to K - (L - M) \in (0 ..^N - L))$

Proof

Step	Hyp	Ref	Expression
1		elfz2	$⊢ M \in (0 \dots L) \leftrightarrow ((0 \in ℤ \land L \in ℤ \land M \in ℤ) \land (0 \leq M \land M \leq L))$
2		zsubcl	$⊢ (L \in ℤ \land M \in ℤ) \to L - M \in ℤ$
3	2	3adant1	$⊢ (0 \in ℤ \land L \in ℤ \land M \in ℤ) \to L - M \in ℤ$
4	3	adantr	$⊢ ((0 \in ℤ \land L \in ℤ \land M \in ℤ) \land (0 \leq M \land M \leq L)) \to L - M \in ℤ$
5	1 4	sylbi	$⊢ M \in (0 \dots L) \to L - M \in ℤ$
6	5	adantr	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to L - M \in ℤ$
7		elfzonelfzo	$⊢ L - M \in ℤ \to ((K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to K \in (L - M ..^N - M))$
8	6 7	syl	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to ((K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to K \in (L - M ..^N - M))$
9		elfz2nn0	$⊢ M \in (0 \dots L) \leftrightarrow (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L)$
10		nn0cn	$⊢ M \in ℕ_{0} \to M \in ℂ$
11		nn0cn	$⊢ L \in ℕ_{0} \to L \in ℂ$
12		elfzelz	$⊢ N \in (L \dots X) \to N \in ℤ$
13		zcn	$⊢ N \in ℤ \to N \in ℂ$
14		subcl	$⊢ (L \in ℂ \land M \in ℂ) \to L - M \in ℂ$
15	14	ancoms	$⊢ (M \in ℂ \land L \in ℂ) \to L - M \in ℂ$
16	15	addid1d	$⊢ (M \in ℂ \land L \in ℂ) \to L - M + 0 = L - M$
17	16	eqcomd	$⊢ (M \in ℂ \land L \in ℂ) \to L - M = L - M + 0$
18	17	adantl	$⊢ (N \in ℂ \land (M \in ℂ \land L \in ℂ)) \to L - M = L - M + 0$
19		simprr	$⊢ (N \in ℂ \land (M \in ℂ \land L \in ℂ)) \to L \in ℂ$
20		simpl	$⊢ (M \in ℂ \land L \in ℂ) \to M \in ℂ$
21	20	adantl	$⊢ (N \in ℂ \land (M \in ℂ \land L \in ℂ)) \to M \in ℂ$
22		simpl	$⊢ (N \in ℂ \land (M \in ℂ \land L \in ℂ)) \to N \in ℂ$
23	19 21 22	npncan3d	$⊢ (N \in ℂ \land (M \in ℂ \land L \in ℂ)) \to (L - M) + N - L = N - M$
24	23	eqcomd	$⊢ (N \in ℂ \land (M \in ℂ \land L \in ℂ)) \to N - M = (L - M) + N - L$
25	18 24	oveq12d	$⊢ (N \in ℂ \land (M \in ℂ \land L \in ℂ)) \to (L - M ..^N - M) = (L - M + 0 ..^(L - M) + N - L)$
26	25	ex	$⊢ N \in ℂ \to ((M \in ℂ \land L \in ℂ) \to (L - M ..^N - M) = (L - M + 0 ..^(L - M) + N - L))$
27	12 13 26	3syl	$⊢ N \in (L \dots X) \to ((M \in ℂ \land L \in ℂ) \to (L - M ..^N - M) = (L - M + 0 ..^(L - M) + N - L))$
28	27	com12	$⊢ (M \in ℂ \land L \in ℂ) \to (N \in (L \dots X) \to (L - M ..^N - M) = (L - M + 0 ..^(L - M) + N - L))$
29	10 11 28	syl2an	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (N \in (L \dots X) \to (L - M ..^N - M) = (L - M + 0 ..^(L - M) + N - L))$
30	29	3adant3	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (N \in (L \dots X) \to (L - M ..^N - M) = (L - M + 0 ..^(L - M) + N - L))$
31	9 30	sylbi	$⊢ M \in (0 \dots L) \to (N \in (L \dots X) \to (L - M ..^N - M) = (L - M + 0 ..^(L - M) + N - L))$
32	31	imp	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to (L - M ..^N - M) = (L - M + 0 ..^(L - M) + N - L)$
33	32	eleq2d	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to (K \in (L - M ..^N - M) \leftrightarrow K \in (L - M + 0 ..^(L - M) + N - L))$
34	33	biimpa	$⊢ ((M \in (0 \dots L) \land N \in (L \dots X)) \land K \in (L - M ..^N - M)) \to K \in (L - M + 0 ..^(L - M) + N - L)$
35		0zd	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to 0 \in ℤ$
36		elfz2	$⊢ N \in (L \dots X) \leftrightarrow ((L \in ℤ \land X \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq X))$
37		zsubcl	$⊢ (N \in ℤ \land L \in ℤ) \to N - L \in ℤ$
38	37	ancoms	$⊢ (L \in ℤ \land N \in ℤ) \to N - L \in ℤ$
39	38	3adant2	$⊢ (L \in ℤ \land X \in ℤ \land N \in ℤ) \to N - L \in ℤ$
40	39	adantr	$⊢ ((L \in ℤ \land X \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq X)) \to N - L \in ℤ$
41	36 40	sylbi	$⊢ N \in (L \dots X) \to N - L \in ℤ$
42	41	adantl	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to N - L \in ℤ$
43	6 35 42	3jca	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to (L - M \in ℤ \land 0 \in ℤ \land N - L \in ℤ)$
44	43	adantr	$⊢ ((M \in (0 \dots L) \land N \in (L \dots X)) \land K \in (L - M ..^N - M)) \to (L - M \in ℤ \land 0 \in ℤ \land N - L \in ℤ)$
45		fzosubel2	$⊢ (K \in (L - M + 0 ..^(L - M) + N - L) \land (L - M \in ℤ \land 0 \in ℤ \land N - L \in ℤ)) \to K - (L - M) \in (0 ..^N - L)$
46	34 44 45	syl2anc	$⊢ ((M \in (0 \dots L) \land N \in (L \dots X)) \land K \in (L - M ..^N - M)) \to K - (L - M) \in (0 ..^N - L)$
47	46	ex	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to (K \in (L - M ..^N - M) \to K - (L - M) \in (0 ..^N - L))$
48	8 47	syld	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to ((K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to K - (L - M) \in (0 ..^N - L))$

Metamath Proof Explorer

Theorem pfxccatin12lem1

Proof