subsubelfzo0

Description: Subtracting a difference from a number which is not less than the difference results in a bounded nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018)

		Ref	Expression
	Assertion	subsubelfzo0	$⊢ (A \in (0 ..^N) \land I \in (0 ..^N) \land \neg I < N - A) \to I - (N - A) \in (0 ..^A)$

Proof

Step	Hyp	Ref	Expression
1		elfzo0	$⊢ A \in (0 ..^N) \leftrightarrow (A \in ℕ_{0} \land N \in ℕ \land A < N)$
2		elfzo0	$⊢ I \in (0 ..^N) \leftrightarrow (I \in ℕ_{0} \land N \in ℕ \land I < N)$
3		nnre	$⊢ N \in ℕ \to N \in ℝ$
4	3	3ad2ant2	$⊢ (I \in ℕ_{0} \land N \in ℕ \land I < N) \to N \in ℝ$
5		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
6	5	adantr	$⊢ (A \in ℕ_{0} \land A < N) \to A \in ℝ$
7		resubcl	$⊢ (N \in ℝ \land A \in ℝ) \to N - A \in ℝ$
8	4 6 7	syl2anr	$⊢ ((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \to N - A \in ℝ$
9		nn0re	$⊢ I \in ℕ_{0} \to I \in ℝ$
10	9	3ad2ant1	$⊢ (I \in ℕ_{0} \land N \in ℕ \land I < N) \to I \in ℝ$
11	10	adantl	$⊢ ((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \to I \in ℝ$
12		lenlt	$⊢ (N - A \in ℝ \land I \in ℝ) \to (N - A \leq I \leftrightarrow \neg I < N - A)$
13	12	bicomd	$⊢ (N - A \in ℝ \land I \in ℝ) \to (\neg I < N - A \leftrightarrow N - A \leq I)$
14	8 11 13	syl2anc	$⊢ ((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \to (\neg I < N - A \leftrightarrow N - A \leq I)$
15	14	biimpa	$⊢ (((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \land \neg I < N - A) \to N - A \leq I$
16		nnz	$⊢ N \in ℕ \to N \in ℤ$
17	16	3ad2ant2	$⊢ (I \in ℕ_{0} \land N \in ℕ \land I < N) \to N \in ℤ$
18		nn0z	$⊢ A \in ℕ_{0} \to A \in ℤ$
19	18	adantr	$⊢ (A \in ℕ_{0} \land A < N) \to A \in ℤ$
20		zsubcl	$⊢ (N \in ℤ \land A \in ℤ) \to N - A \in ℤ$
21	17 19 20	syl2anr	$⊢ ((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \to N - A \in ℤ$
22		ltle	$⊢ (A \in ℝ \land N \in ℝ) \to (A < N \to A \leq N)$
23	5 4 22	syl2an	$⊢ (A \in ℕ_{0} \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \to (A < N \to A \leq N)$
24	23	impancom	$⊢ (A \in ℕ_{0} \land A < N) \to ((I \in ℕ_{0} \land N \in ℕ \land I < N) \to A \leq N)$
25	24	imp	$⊢ ((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \to A \leq N$
26		subge0	$⊢ (N \in ℝ \land A \in ℝ) \to (0 \leq N - A \leftrightarrow A \leq N)$
27	4 6 26	syl2anr	$⊢ ((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \to (0 \leq N - A \leftrightarrow A \leq N)$
28	25 27	mpbird	$⊢ ((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \to 0 \leq N - A$
29		elnn0z	$⊢ N - A \in ℕ_{0} \leftrightarrow (N - A \in ℤ \land 0 \leq N - A)$
30	21 28 29	sylanbrc	$⊢ ((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \to N - A \in ℕ_{0}$
31	30	adantr	$⊢ (((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \land \neg I < N - A) \to N - A \in ℕ_{0}$
32		simplr1	$⊢ (((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \land \neg I < N - A) \to I \in ℕ_{0}$
33		nn0sub	$⊢ (N - A \in ℕ_{0} \land I \in ℕ_{0}) \to (N - A \leq I \leftrightarrow I - (N - A) \in ℕ_{0})$
34	31 32 33	syl2anc	$⊢ (((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \land \neg I < N - A) \to (N - A \leq I \leftrightarrow I - (N - A) \in ℕ_{0})$
35	15 34	mpbid	$⊢ (((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \land \neg I < N - A) \to I - (N - A) \in ℕ_{0}$
36		elnn0uz	$⊢ I - (N - A) \in ℕ_{0} \leftrightarrow I - (N - A) \in ℤ_{\geq 0}$
37	35 36	sylib	$⊢ (((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \land \neg I < N - A) \to I - (N - A) \in ℤ_{\geq 0}$
38	19	adantr	$⊢ ((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \to A \in ℤ$
39	38	adantr	$⊢ (((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \land \neg I < N - A) \to A \in ℤ$
40	9	adantr	$⊢ (I \in ℕ_{0} \land N \in ℕ) \to I \in ℝ$
41	40	adantl	$⊢ (A \in ℕ_{0} \land (I \in ℕ_{0} \land N \in ℕ)) \to I \in ℝ$
42	3	adantl	$⊢ (I \in ℕ_{0} \land N \in ℕ) \to N \in ℝ$
43	42	adantl	$⊢ (A \in ℕ_{0} \land (I \in ℕ_{0} \land N \in ℕ)) \to N \in ℝ$
44	42 5 7	syl2anr	$⊢ (A \in ℕ_{0} \land (I \in ℕ_{0} \land N \in ℕ)) \to N - A \in ℝ$
45	41 43 44	ltsub1d	$⊢ (A \in ℕ_{0} \land (I \in ℕ_{0} \land N \in ℕ)) \to (I < N \leftrightarrow I - (N - A) < N - (N - A))$
46		nncn	$⊢ N \in ℕ \to N \in ℂ$
47	46	adantl	$⊢ (I \in ℕ_{0} \land N \in ℕ) \to N \in ℂ$
48		nn0cn	$⊢ A \in ℕ_{0} \to A \in ℂ$
49		nncan	$⊢ (N \in ℂ \land A \in ℂ) \to N - (N - A) = A$
50	47 48 49	syl2anr	$⊢ (A \in ℕ_{0} \land (I \in ℕ_{0} \land N \in ℕ)) \to N - (N - A) = A$
51	50	breq2d	$⊢ (A \in ℕ_{0} \land (I \in ℕ_{0} \land N \in ℕ)) \to (I - (N - A) < N - (N - A) \leftrightarrow I - (N - A) < A)$
52	51	biimpd	$⊢ (A \in ℕ_{0} \land (I \in ℕ_{0} \land N \in ℕ)) \to (I - (N - A) < N - (N - A) \to I - (N - A) < A)$
53	45 52	sylbid	$⊢ (A \in ℕ_{0} \land (I \in ℕ_{0} \land N \in ℕ)) \to (I < N \to I - (N - A) < A)$
54	53	ex	$⊢ A \in ℕ_{0} \to ((I \in ℕ_{0} \land N \in ℕ) \to (I < N \to I - (N - A) < A))$
55	54	adantr	$⊢ (A \in ℕ_{0} \land A < N) \to ((I \in ℕ_{0} \land N \in ℕ) \to (I < N \to I - (N - A) < A))$
56	55	com3l	$⊢ (I \in ℕ_{0} \land N \in ℕ) \to (I < N \to ((A \in ℕ_{0} \land A < N) \to I - (N - A) < A))$
57	56	3impia	$⊢ (I \in ℕ_{0} \land N \in ℕ \land I < N) \to ((A \in ℕ_{0} \land A < N) \to I - (N - A) < A)$
58	57	impcom	$⊢ ((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \to I - (N - A) < A$
59	58	adantr	$⊢ (((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \land \neg I < N - A) \to I - (N - A) < A$
60	37 39 59	3jca	$⊢ (((A \in ℕ_{0} \land A < N) \land (I \in ℕ_{0} \land N \in ℕ \land I < N)) \land \neg I < N - A) \to (I - (N - A) \in ℤ_{\geq 0} \land A \in ℤ \land I - (N - A) < A)$
61	60	exp31	$⊢ (A \in ℕ_{0} \land A < N) \to ((I \in ℕ_{0} \land N \in ℕ \land I < N) \to (\neg I < N - A \to (I - (N - A) \in ℤ_{\geq 0} \land A \in ℤ \land I - (N - A) < A)))$
62	2 61	syl5bi	$⊢ (A \in ℕ_{0} \land A < N) \to (I \in (0 ..^N) \to (\neg I < N - A \to (I - (N - A) \in ℤ_{\geq 0} \land A \in ℤ \land I - (N - A) < A)))$
63	62	3adant2	$⊢ (A \in ℕ_{0} \land N \in ℕ \land A < N) \to (I \in (0 ..^N) \to (\neg I < N - A \to (I - (N - A) \in ℤ_{\geq 0} \land A \in ℤ \land I - (N - A) < A)))$
64	1 63	sylbi	$⊢ A \in (0 ..^N) \to (I \in (0 ..^N) \to (\neg I < N - A \to (I - (N - A) \in ℤ_{\geq 0} \land A \in ℤ \land I - (N - A) < A)))$
65	64	3imp	$⊢ (A \in (0 ..^N) \land I \in (0 ..^N) \land \neg I < N - A) \to (I - (N - A) \in ℤ_{\geq 0} \land A \in ℤ \land I - (N - A) < A)$
66		elfzo2	$⊢ I - (N - A) \in (0 ..^A) \leftrightarrow (I - (N - A) \in ℤ_{\geq 0} \land A \in ℤ \land I - (N - A) < A)$
67	65 66	sylibr	$⊢ (A \in (0 ..^N) \land I \in (0 ..^N) \land \neg I < N - A) \to I - (N - A) \in (0 ..^A)$

Metamath Proof Explorer

Theorem subsubelfzo0

Proof