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 \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ) \to ((K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to K \in (L - M ..^(L - M) + N - L))$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$⊢ L \in ℕ_{0} \to L \in ℤ$
2		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
3		zsubcl	$⊢ (L \in ℤ \land M \in ℤ) \to L - M \in ℤ$
4	1 2 3	syl2an	$⊢ (L \in ℕ_{0} \land M \in ℕ_{0}) \to L - M \in ℤ$
5	4	3adant3	$⊢ (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ) \to L - M \in ℤ$
6		elfzonelfzo	$⊢ L - M \in ℤ \to ((K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to K \in (L - M ..^N - M))$
7	6	imp	$⊢ (L - M \in ℤ \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K \in (L - M ..^N - M)$
8	5 7	sylan	$⊢ ((L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K \in (L - M ..^N - M)$
9		nn0cn	$⊢ L \in ℕ_{0} \to L \in ℂ$
10		nn0cn	$⊢ M \in ℕ_{0} \to M \in ℂ$
11		zcn	$⊢ N \in ℤ \to N \in ℂ$
12		npncan3	$⊢ (L \in ℂ \land M \in ℂ \land N \in ℂ) \to (L - M) + N - L = N - M$
13	9 10 11 12	syl3an	$⊢ (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ) \to (L - M) + N - L = N - M$
14	13	oveq2d	$⊢ (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ) \to (L - M ..^(L - M) + N - L) = (L - M ..^N - M)$
15	14	eleq2d	$⊢ (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ) \to (K \in (L - M ..^(L - M) + N - L) \leftrightarrow K \in (L - M ..^N - M))$
16	15	adantr	$⊢ ((L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to (K \in (L - M ..^(L - M) + N - L) \leftrightarrow K \in (L - M ..^N - M))$
17	8 16	mpbird	$⊢ ((L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ) \land (K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M))) \to K \in (L - M ..^(L - M) + N - L)$
18	17	ex	$⊢ (L \in ℕ_{0} \land M \in ℕ_{0} \land N \in ℤ) \to ((K \in (0 ..^N - M) \land \neg K \in (0 ..^L - M)) \to K \in (L - M ..^(L - M) + N - L))$