subfzo0

Description: The difference between two elements in a half-open range of nonnegative integers is greater than the negation of the upper bound and less than the upper bound of the range. (Contributed by AV, 20-Mar-2021)

		Ref	Expression
	Assertion	subfzo0	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (- N < I - J \land I - J < N)$

Proof

Step	Hyp	Ref	Expression
1		elfzo0	$⊢ I \in (0 ..^N) \leftrightarrow (I \in ℕ_{0} \land N \in ℕ \land I < N)$
2		elfzo0	$⊢ J \in (0 ..^N) \leftrightarrow (J \in ℕ_{0} \land N \in ℕ \land J < N)$
3		nn0re	$⊢ I \in ℕ_{0} \to I \in ℝ$
4	3	adantr	$⊢ (I \in ℕ_{0} \land I < N) \to I \in ℝ$
5		nnre	$⊢ N \in ℕ \to N \in ℝ$
6		nn0re	$⊢ J \in ℕ_{0} \to J \in ℝ$
7		resubcl	$⊢ (N \in ℝ \land J \in ℝ) \to N - J \in ℝ$
8	5 6 7	syl2an	$⊢ (N \in ℕ \land J \in ℕ_{0}) \to N - J \in ℝ$
9	8	ancoms	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to N - J \in ℝ$
10	9	3adant3	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to N - J \in ℝ$
11	4 10	anim12i	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (I \in ℝ \land N - J \in ℝ)$
12		nn0ge0	$⊢ I \in ℕ_{0} \to 0 \leq I$
13	12	adantr	$⊢ (I \in ℕ_{0} \land I < N) \to 0 \leq I$
14		posdif	$⊢ (J \in ℝ \land N \in ℝ) \to (J < N \leftrightarrow 0 < N - J)$
15	6 5 14	syl2an	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to (J < N \leftrightarrow 0 < N - J)$
16	15	biimp3a	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to 0 < N - J$
17	13 16	anim12i	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (0 \leq I \land 0 < N - J)$
18		addgegt0	$⊢ ((I \in ℝ \land N - J \in ℝ) \land (0 \leq I \land 0 < N - J)) \to 0 < I + N - J$
19	11 17 18	syl2anc	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to 0 < I + N - J$
20		nn0cn	$⊢ I \in ℕ_{0} \to I \in ℂ$
21	20	adantr	$⊢ (I \in ℕ_{0} \land I < N) \to I \in ℂ$
22	21	adantr	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to I \in ℂ$
23		nn0cn	$⊢ J \in ℕ_{0} \to J \in ℂ$
24	23	3ad2ant1	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to J \in ℂ$
25	24	adantl	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to J \in ℂ$
26		nncn	$⊢ N \in ℕ \to N \in ℂ$
27	26	3ad2ant2	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to N \in ℂ$
28	27	adantl	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to N \in ℂ$
29	22 25 28	subadd23d	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to I - J + N = I + N - J$
30	19 29	breqtrrd	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to 0 < I - J + N$
31	6	3ad2ant1	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to J \in ℝ$
32		resubcl	$⊢ (I \in ℝ \land J \in ℝ) \to I - J \in ℝ$
33	4 31 32	syl2an	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to I - J \in ℝ$
34	5	3ad2ant2	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to N \in ℝ$
35	34	adantl	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to N \in ℝ$
36	33 35	possumd	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (0 < I - J + N \leftrightarrow - N < I - J)$
37	30 36	mpbid	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to - N < I - J$
38	3	adantr	$⊢ (I \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to I \in ℝ$
39	34	adantl	$⊢ (I \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to N \in ℝ$
40		readdcl	$⊢ (J \in ℝ \land N \in ℝ) \to J + N \in ℝ$
41	6 5 40	syl2an	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to J + N \in ℝ$
42	41	3adant3	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to J + N \in ℝ$
43	42	adantl	$⊢ (I \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to J + N \in ℝ$
44	38 39 43	3jca	$⊢ (I \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (I \in ℝ \land N \in ℝ \land J + N \in ℝ)$
45		nn0ge0	$⊢ J \in ℕ_{0} \to 0 \leq J$
46	45	3ad2ant1	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to 0 \leq J$
47	46	adantl	$⊢ (I \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to 0 \leq J$
48	5 6	anim12i	$⊢ (N \in ℕ \land J \in ℕ_{0}) \to (N \in ℝ \land J \in ℝ)$
49	48	ancoms	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to (N \in ℝ \land J \in ℝ)$
50	49	3adant3	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (N \in ℝ \land J \in ℝ)$
51	50	adantl	$⊢ (I \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (N \in ℝ \land J \in ℝ)$
52		addge02	$⊢ (N \in ℝ \land J \in ℝ) \to (0 \leq J \leftrightarrow N \leq J + N)$
53	51 52	syl	$⊢ (I \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (0 \leq J \leftrightarrow N \leq J + N)$
54	47 53	mpbid	$⊢ (I \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to N \leq J + N$
55	44 54	lelttrdi	$⊢ (I \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (I < N \to I < J + N)$
56	55	impancom	$⊢ (I \in ℕ_{0} \land I < N) \to ((J \in ℕ_{0} \land N \in ℕ \land J < N) \to I < J + N)$
57	56	imp	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to I < J + N$
58	4	adantr	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to I \in ℝ$
59	31	adantl	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to J \in ℝ$
60	58 59 35	ltsubadd2d	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (I - J < N \leftrightarrow I < J + N)$
61	57 60	mpbird	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to I - J < N$
62	37 61	jca	$⊢ ((I \in ℕ_{0} \land I < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (- N < I - J \land I - J < N)$
63	62	ex	$⊢ (I \in ℕ_{0} \land I < N) \to ((J \in ℕ_{0} \land N \in ℕ \land J < N) \to (- N < I - J \land I - J < N))$
64	2 63	biimtrid	$⊢ (I \in ℕ_{0} \land I < N) \to (J \in (0 ..^N) \to (- N < I - J \land I - J < N))$
65	64	3adant2	$⊢ (I \in ℕ_{0} \land N \in ℕ \land I < N) \to (J \in (0 ..^N) \to (- N < I - J \land I - J < N))$
66	1 65	sylbi	$⊢ I \in (0 ..^N) \to (J \in (0 ..^N) \to (- N < I - J \land I - J < N))$
67	66	imp	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (- N < I - J \land I - J < N)$

Metamath Proof Explorer

Theorem subfzo0

Proof