Metamath Proof Explorer

Theorem difelfznle

Description: The difference of two integers from a finite set of sequential nonnegative integers increased by the upper bound is also element of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 12-Jun-2018)

Ref Expression
Assertion difelfznle ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
2 nn0addcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
3 2 nn0zd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
4 3 3adant3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
5 1 4 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
6 elfzelz ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℤ )
7 zsubcl ⊢ ( ( ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ℤ )
8 5 6 7 syl2anr ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ℤ )
9 8 3adant3 ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ℤ )
10 6 zred ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℝ )
11 10 adantr ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℝ )
12 elfzel2 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℤ )
13 12 zred ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℝ )
14 13 adantr ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
15 nn0readdcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
16 15 3adant3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
17 1 16 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
18 17 adantl ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
19 elfzle2 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ≤ 𝑁 )
20 elfzle1 ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑀 )
21 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
22 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
23 21 22 anim12ci ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
24 23 3adant3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
25 1 24 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
26 addge02 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 0 ≤ 𝑀 ↔ 𝑁 ≤ ( 𝑀 + 𝑁 ) ) )
27 25 26 syl ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 0 ≤ 𝑀 ↔ 𝑁 ≤ ( 𝑀 + 𝑁 ) ) )
28 20 27 mpbid ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑁 ≤ ( 𝑀 + 𝑁 ) )
29 19 28 anim12i ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝐾 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝑀 + 𝑁 ) ) )
30 letr ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑀 + 𝑁 ) ∈ ℝ ) → ( ( 𝐾 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝑀 + 𝑁 ) ) → 𝐾 ≤ ( 𝑀 + 𝑁 ) ) )
31 30 imp ⊢ ( ( ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑀 + 𝑁 ) ∈ ℝ ) ∧ ( 𝐾 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝑀 + 𝑁 ) ) ) → 𝐾 ≤ ( 𝑀 + 𝑁 ) )
32 11 14 18 29 31 syl31anc ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ≤ ( 𝑀 + 𝑁 ) )
33 32 3adant3 ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → 𝐾 ≤ ( 𝑀 + 𝑁 ) )
34 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
35 21 22 anim12i ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
36 35 3adant3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
37 1 36 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
38 readdcl ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
39 37 38 syl ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
40 34 39 anim12ci ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝑁 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) )
41 6 40 sylan ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝑁 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) )
42 41 3adant3 ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → ( ( 𝑀 + 𝑁 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) )
43 subge0 ⊢ ( ( ( 𝑀 + 𝑁 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 0 ≤ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ↔ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) )
44 42 43 syl ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → ( 0 ≤ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ↔ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) )
45 33 44 mpbird ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → 0 ≤ ( ( 𝑀 + 𝑁 ) − 𝐾 ) )
46 elnn0z ⊢ ( ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ℕ0 ↔ ( ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ) )
47 9 45 46 sylanbrc ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ℕ0 )
48 elfz3nn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
49 48 3ad2ant1 ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → 𝑁 ∈ ℕ0 )
50 elfzelz ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℤ )
51 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
52 ltnle ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑀 ) )
53 52 ancoms ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑀 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑀 ) )
54 ltle ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 < 𝐾 → 𝑀 ≤ 𝐾 ) )
55 54 ancoms ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑀 < 𝐾 → 𝑀 ≤ 𝐾 ) )
56 53 55 sylbird ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ¬ 𝐾 ≤ 𝑀 → 𝑀 ≤ 𝐾 ) )
57 34 51 56 syl2an ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ¬ 𝐾 ≤ 𝑀 → 𝑀 ≤ 𝐾 ) )
58 6 50 57 syl2an ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ¬ 𝐾 ≤ 𝑀 → 𝑀 ≤ 𝐾 ) )
59 58 3impia ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → 𝑀 ≤ 𝐾 )
60 50 zred ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℝ )
61 60 adantl ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝑀 ∈ ℝ )
62 61 11 14 leadd1d ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝑀 ≤ 𝐾 ↔ ( 𝑀 + 𝑁 ) ≤ ( 𝐾 + 𝑁 ) ) )
63 62 3adant3 ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → ( 𝑀 ≤ 𝐾 ↔ ( 𝑀 + 𝑁 ) ≤ ( 𝐾 + 𝑁 ) ) )
64 59 63 mpbid ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → ( 𝑀 + 𝑁 ) ≤ ( 𝐾 + 𝑁 ) )
65 18 11 14 lesubadd2d ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑀 + 𝑁 ) − 𝐾 ) ≤ 𝑁 ↔ ( 𝑀 + 𝑁 ) ≤ ( 𝐾 + 𝑁 ) ) )
66 65 3adant3 ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → ( ( ( 𝑀 + 𝑁 ) − 𝐾 ) ≤ 𝑁 ↔ ( 𝑀 + 𝑁 ) ≤ ( 𝐾 + 𝑁 ) ) )
67 64 66 mpbird ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → ( ( 𝑀 + 𝑁 ) − 𝐾 ) ≤ 𝑁 )
68 elfz2nn0 ⊢ ( ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ≤ 𝑁 ) )
69 47 49 67 68 syl3anbrc ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ ¬ 𝐾 ≤ 𝑀 ) → ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 0 ... 𝑁 ) )