Metamath Proof Explorer

Theorem fzonmapblen

Description: The result of subtracting a nonnegative integer from a positive integer and adding another nonnegative integer which is less than the first one is less than the positive integer. (Contributed by Alexander van der Vekens, 19-May-2018)

Ref Expression
Assertion fzonmapblen ⊢ A ∈ 0 ..^ N ∧ B ∈ 0 ..^ N ∧ B < A → B + N - A < N

Proof

Step Hyp Ref Expression
1 elfzo0 ⊢ A ∈ 0 ..^ N ↔ A ∈ ℕ 0 ∧ N ∈ ℕ ∧ A < N
2 nn0re ⊢ A ∈ ℕ 0 → A ∈ ℝ
3 nnre ⊢ N ∈ ℕ → N ∈ ℝ
4 2 3 anim12i ⊢ A ∈ ℕ 0 ∧ N ∈ ℕ → A ∈ ℝ ∧ N ∈ ℝ
5 4 3adant3 ⊢ A ∈ ℕ 0 ∧ N ∈ ℕ ∧ A < N → A ∈ ℝ ∧ N ∈ ℝ
6 1 5 sylbi ⊢ A ∈ 0 ..^ N → A ∈ ℝ ∧ N ∈ ℝ
7 elfzoelz ⊢ B ∈ 0 ..^ N → B ∈ ℤ
8 7 zred ⊢ B ∈ 0 ..^ N → B ∈ ℝ
9 simpr ⊢ A ∈ ℝ ∧ N ∈ ℝ ∧ B ∈ ℝ → B ∈ ℝ
10 simpll ⊢ A ∈ ℝ ∧ N ∈ ℝ ∧ B ∈ ℝ → A ∈ ℝ
11 resubcl ⊢ N ∈ ℝ ∧ A ∈ ℝ → N − A ∈ ℝ
12 11 ancoms ⊢ A ∈ ℝ ∧ N ∈ ℝ → N − A ∈ ℝ
13 12 adantr ⊢ A ∈ ℝ ∧ N ∈ ℝ ∧ B ∈ ℝ → N − A ∈ ℝ
14 9 10 13 ltadd1d ⊢ A ∈ ℝ ∧ N ∈ ℝ ∧ B ∈ ℝ → B < A ↔ B + N - A < A + N - A
15 14 biimpa ⊢ A ∈ ℝ ∧ N ∈ ℝ ∧ B ∈ ℝ ∧ B < A → B + N - A < A + N - A
16 recn ⊢ A ∈ ℝ → A ∈ ℂ
17 recn ⊢ N ∈ ℝ → N ∈ ℂ
18 16 17 anim12i ⊢ A ∈ ℝ ∧ N ∈ ℝ → A ∈ ℂ ∧ N ∈ ℂ
19 18 adantr ⊢ A ∈ ℝ ∧ N ∈ ℝ ∧ B ∈ ℝ → A ∈ ℂ ∧ N ∈ ℂ
20 19 adantr ⊢ A ∈ ℝ ∧ N ∈ ℝ ∧ B ∈ ℝ ∧ B < A → A ∈ ℂ ∧ N ∈ ℂ
21 pncan3 ⊢ A ∈ ℂ ∧ N ∈ ℂ → A + N - A = N
22 20 21 syl ⊢ A ∈ ℝ ∧ N ∈ ℝ ∧ B ∈ ℝ ∧ B < A → A + N - A = N
23 15 22 breqtrd ⊢ A ∈ ℝ ∧ N ∈ ℝ ∧ B ∈ ℝ ∧ B < A → B + N - A < N
24 23 ex ⊢ A ∈ ℝ ∧ N ∈ ℝ ∧ B ∈ ℝ → B < A → B + N - A < N
25 6 8 24 syl2an ⊢ A ∈ 0 ..^ N ∧ B ∈ 0 ..^ N → B < A → B + N - A < N
26 25 3impia ⊢ A ∈ 0 ..^ N ∧ B ∈ 0 ..^ N ∧ B < A → B + N - A < N