# 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 ${⊢}\left({A}\in \left(0..^{N}\right)\wedge {B}\in \left(0..^{N}\right)\wedge {B}<{A}\right)\to {B}+{N}-{A}<{N}$

### Proof

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