fzonmapblen

Description: The result of subtracting a nonnegative integer from a positive integer and adding another nonnegative integer which is less than the first one is less than the positive integer. (Contributed by Alexander van der Vekens, 19-May-2018)

		Ref	Expression
	Assertion	fzonmapblen	$⊢ (A \in (0 ..^N) \land B \in (0 ..^N) \land B < A) \to B + N - A < N$

Proof

Step	Hyp	Ref	Expression
1		elfzo0	$⊢ A \in (0 ..^N) \leftrightarrow (A \in ℕ_{0} \land N \in ℕ \land A < N)$
2		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
3		nnre	$⊢ N \in ℕ \to N \in ℝ$
4	2 3	anim12i	$⊢ (A \in ℕ_{0} \land N \in ℕ) \to (A \in ℝ \land N \in ℝ)$
5	4	3adant3	$⊢ (A \in ℕ_{0} \land N \in ℕ \land A < N) \to (A \in ℝ \land N \in ℝ)$
6	1 5	sylbi	$⊢ A \in (0 ..^N) \to (A \in ℝ \land N \in ℝ)$
7		elfzoelz	$⊢ B \in (0 ..^N) \to B \in ℤ$
8	7	zred	$⊢ B \in (0 ..^N) \to B \in ℝ$
9		simpr	$⊢ ((A \in ℝ \land N \in ℝ) \land B \in ℝ) \to B \in ℝ$
10		simpll	$⊢ ((A \in ℝ \land N \in ℝ) \land B \in ℝ) \to A \in ℝ$
11		resubcl	$⊢ (N \in ℝ \land A \in ℝ) \to N - A \in ℝ$
12	11	ancoms	$⊢ (A \in ℝ \land N \in ℝ) \to N - A \in ℝ$
13	12	adantr	$⊢ ((A \in ℝ \land N \in ℝ) \land B \in ℝ) \to N - A \in ℝ$
14	9 10 13	ltadd1d	$⊢ ((A \in ℝ \land N \in ℝ) \land B \in ℝ) \to (B < A \leftrightarrow B + N - A < A + N - A)$
15	14	biimpa	$⊢ (((A \in ℝ \land N \in ℝ) \land B \in ℝ) \land B < A) \to B + N - A < A + N - A$
16		recn	$⊢ A \in ℝ \to A \in ℂ$
17		recn	$⊢ N \in ℝ \to N \in ℂ$
18	16 17	anim12i	$⊢ (A \in ℝ \land N \in ℝ) \to (A \in ℂ \land N \in ℂ)$
19	18	adantr	$⊢ ((A \in ℝ \land N \in ℝ) \land B \in ℝ) \to (A \in ℂ \land N \in ℂ)$
20	19	adantr	$⊢ (((A \in ℝ \land N \in ℝ) \land B \in ℝ) \land B < A) \to (A \in ℂ \land N \in ℂ)$
21		pncan3	$⊢ (A \in ℂ \land N \in ℂ) \to A + N - A = N$
22	20 21	syl	$⊢ (((A \in ℝ \land N \in ℝ) \land B \in ℝ) \land B < A) \to A + N - A = N$
23	15 22	breqtrd	$⊢ (((A \in ℝ \land N \in ℝ) \land B \in ℝ) \land B < A) \to B + N - A < N$
24	23	ex	$⊢ ((A \in ℝ \land N \in ℝ) \land B \in ℝ) \to (B < A \to B + N - A < N)$
25	6 8 24	syl2an	$⊢ (A \in (0 ..^N) \land B \in (0 ..^N)) \to (B < A \to B + N - A < N)$
26	25	3impia	$⊢ (A \in (0 ..^N) \land B \in (0 ..^N) \land B < A) \to B + N - A < N$

Metamath Proof Explorer

Theorem fzonmapblen

Proof