Theorem 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	⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( - 𝑁 < ( 𝐼 − 𝐽 ) ∧ ( 𝐼 − 𝐽 ) < 𝑁 ) )

Proof

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