pfxccatin12lem2a

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

		Ref	Expression
	Assertion	pfxccatin12lem2a	$⊢ (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 + M \in (L ..^X))$

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		elfzoelz	$⊢ K \in (L - M ..^N - M) \to K \in ℤ$
10		elfzelz	$⊢ N \in (L \dots X) \to N \in ℤ$
11		simpl	$⊢ (L \in ℤ \land M \in ℤ) \to L \in ℤ$
12		simpl	$⊢ (N \in ℤ \land K \in ℤ) \to N \in ℤ$
13	11 12	anim12i	$⊢ ((L \in ℤ \land M \in ℤ) \land (N \in ℤ \land K \in ℤ)) \to (L \in ℤ \land N \in ℤ)$
14		simpr	$⊢ (L \in ℤ \land M \in ℤ) \to M \in ℤ$
15		simpr	$⊢ (N \in ℤ \land K \in ℤ) \to K \in ℤ$
16	14 15	anim12ci	$⊢ ((L \in ℤ \land M \in ℤ) \land (N \in ℤ \land K \in ℤ)) \to (K \in ℤ \land M \in ℤ)$
17	13 16	jca	$⊢ ((L \in ℤ \land M \in ℤ) \land (N \in ℤ \land K \in ℤ)) \to ((L \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \in ℤ))$
18	17	exp32	$⊢ (L \in ℤ \land M \in ℤ) \to (N \in ℤ \to (K \in ℤ \to ((L \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \in ℤ))))$
19	10 18	syl5	$⊢ (L \in ℤ \land M \in ℤ) \to (N \in (L \dots X) \to (K \in ℤ \to ((L \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \in ℤ))))$
20	19	3adant1	$⊢ (0 \in ℤ \land L \in ℤ \land M \in ℤ) \to (N \in (L \dots X) \to (K \in ℤ \to ((L \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \in ℤ))))$
21	20	adantr	$⊢ ((0 \in ℤ \land L \in ℤ \land M \in ℤ) \land (0 \leq M \land M \leq L)) \to (N \in (L \dots X) \to (K \in ℤ \to ((L \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \in ℤ))))$
22	1 21	sylbi	$⊢ M \in (0 \dots L) \to (N \in (L \dots X) \to (K \in ℤ \to ((L \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \in ℤ))))$
23	22	imp	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to (K \in ℤ \to ((L \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)))$
24	23	impcom	$⊢ (K \in ℤ \land (M \in (0 \dots L) \land N \in (L \dots X))) \to ((L \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \in ℤ))$
25		elfzomelpfzo	$⊢ ((L \in ℤ \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to (K \in (L - M ..^N - M) \leftrightarrow K + M \in (L ..^N))$
26	24 25	syl	$⊢ (K \in ℤ \land (M \in (0 \dots L) \land N \in (L \dots X))) \to (K \in (L - M ..^N - M) \leftrightarrow K + M \in (L ..^N))$
27		elfz2	$⊢ N \in (L \dots X) \leftrightarrow ((L \in ℤ \land X \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq X))$
28		simpl3	$⊢ ((L \in ℤ \land X \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq X)) \to N \in ℤ$
29		simpl2	$⊢ ((L \in ℤ \land X \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq X)) \to X \in ℤ$
30		simpr	$⊢ (L \leq N \land N \leq X) \to N \leq X$
31	30	adantl	$⊢ ((L \in ℤ \land X \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq X)) \to N \leq X$
32	28 29 31	3jca	$⊢ ((L \in ℤ \land X \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq X)) \to (N \in ℤ \land X \in ℤ \land N \leq X)$
33	27 32	sylbi	$⊢ N \in (L \dots X) \to (N \in ℤ \land X \in ℤ \land N \leq X)$
34	33	adantl	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to (N \in ℤ \land X \in ℤ \land N \leq X)$
35	34	adantl	$⊢ (K \in ℤ \land (M \in (0 \dots L) \land N \in (L \dots X))) \to (N \in ℤ \land X \in ℤ \land N \leq X)$
36		eluz2	$⊢ X \in ℤ_{\geq N} \leftrightarrow (N \in ℤ \land X \in ℤ \land N \leq X)$
37	35 36	sylibr	$⊢ (K \in ℤ \land (M \in (0 \dots L) \land N \in (L \dots X))) \to X \in ℤ_{\geq N}$
38		fzoss2	$⊢ X \in ℤ_{\geq N} \to (L ..^N) \subseteq (L ..^X)$
39	37 38	syl	$⊢ (K \in ℤ \land (M \in (0 \dots L) \land N \in (L \dots X))) \to (L ..^N) \subseteq (L ..^X)$
40	39	sseld	$⊢ (K \in ℤ \land (M \in (0 \dots L) \land N \in (L \dots X))) \to (K + M \in (L ..^N) \to K + M \in (L ..^X))$
41	26 40	sylbid	$⊢ (K \in ℤ \land (M \in (0 \dots L) \land N \in (L \dots X))) \to (K \in (L - M ..^N - M) \to K + M \in (L ..^X))$
42	41	ex	$⊢ K \in ℤ \to ((M \in (0 \dots L) \land N \in (L \dots X)) \to (K \in (L - M ..^N - M) \to K + M \in (L ..^X)))$
43	42	com23	$⊢ K \in ℤ \to (K \in (L - M ..^N - M) \to ((M \in (0 \dots L) \land N \in (L \dots X)) \to K + M \in (L ..^X)))$
44	9 43	mpcom	$⊢ K \in (L - M ..^N - M) \to ((M \in (0 \dots L) \land N \in (L \dots X)) \to K + M \in (L ..^X))$
45	44	com12	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to (K \in (L - M ..^N - M) \to K + M \in (L ..^X))$
46	8 45	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 + M \in (L ..^X))$

Metamath Proof Explorer

Theorem pfxccatin12lem2a

Proof