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

Metamath Proof Explorer

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

Proof

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