This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrid ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝐼 < 𝑁 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( - 𝑁 < ( 𝐼 − 𝐽 ) ∧ ( 𝐼 − 𝐽 ) < 𝑁 ) ) )
65 64 3adant2 ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( - 𝑁 < ( 𝐼 − 𝐽 ) ∧ ( 𝐼 − 𝐽 ) < 𝑁 ) ) )
66 1 65 sylbi ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( - 𝑁 < ( 𝐼 − 𝐽 ) ∧ ( 𝐼 − 𝐽 ) < 𝑁 ) ) )
67 66 imp ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( - 𝑁 < ( 𝐼 − 𝐽 ) ∧ ( 𝐼 − 𝐽 ) < 𝑁 ) )