# Metamath Proof Explorer

Description: The sum of an integer and a real number between 0 and 1 is less than or equal to a second integer iff the sum is less than the second integer. (Contributed by AV, 1-Jul-2021)

Ref Expression
Assertion zltaddlt1le ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to \left({M}+{A}<{N}↔{M}+{A}\le {N}\right)$

### Proof

Step Hyp Ref Expression
1 zre ${⊢}{M}\in ℤ\to {M}\in ℝ$
2 1 adantr ${⊢}\left({M}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to {M}\in ℝ$
3 elioore ${⊢}{A}\in \left(0,1\right)\to {A}\in ℝ$
4 3 adantl ${⊢}\left({M}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to {A}\in ℝ$
5 2 4 readdcld ${⊢}\left({M}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to {M}+{A}\in ℝ$
6 5 3adant2 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to {M}+{A}\in ℝ$
7 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
8 7 3ad2ant2 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to {N}\in ℝ$
9 ltle ${⊢}\left({M}+{A}\in ℝ\wedge {N}\in ℝ\right)\to \left({M}+{A}<{N}\to {M}+{A}\le {N}\right)$
10 6 8 9 syl2anc ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to \left({M}+{A}<{N}\to {M}+{A}\le {N}\right)$
11 elioo3g ${⊢}{A}\in \left(0,1\right)↔\left(\left(0\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\wedge \left(0<{A}\wedge {A}<1\right)\right)$
12 simpl ${⊢}\left(0<{A}\wedge {A}<1\right)\to 0<{A}$
13 11 12 simplbiim ${⊢}{A}\in \left(0,1\right)\to 0<{A}$
14 3 13 elrpd ${⊢}{A}\in \left(0,1\right)\to {A}\in {ℝ}^{+}$
15 addlelt ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\wedge {A}\in {ℝ}^{+}\right)\to \left({M}+{A}\le {N}\to {M}<{N}\right)$
16 1 7 14 15 syl3an ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to \left({M}+{A}\le {N}\to {M}<{N}\right)$
17 zltp1le ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}<{N}↔{M}+1\le {N}\right)$
18 17 3adant3 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to \left({M}<{N}↔{M}+1\le {N}\right)$
19 3 3ad2ant3 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to {A}\in ℝ$
20 1red ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to 1\in ℝ$
21 1 3ad2ant1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to {M}\in ℝ$
22 simpr ${⊢}\left(0<{A}\wedge {A}<1\right)\to {A}<1$
23 11 22 simplbiim ${⊢}{A}\in \left(0,1\right)\to {A}<1$
24 23 3ad2ant3 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to {A}<1$
25 19 20 21 24 ltadd2dd ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to {M}+{A}<{M}+1$
26 peano2z ${⊢}{M}\in ℤ\to {M}+1\in ℤ$
27 26 zred ${⊢}{M}\in ℤ\to {M}+1\in ℝ$
28 27 3ad2ant1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to {M}+1\in ℝ$
29 ltletr ${⊢}\left({M}+{A}\in ℝ\wedge {M}+1\in ℝ\wedge {N}\in ℝ\right)\to \left(\left({M}+{A}<{M}+1\wedge {M}+1\le {N}\right)\to {M}+{A}<{N}\right)$
30 6 28 8 29 syl3anc ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to \left(\left({M}+{A}<{M}+1\wedge {M}+1\le {N}\right)\to {M}+{A}<{N}\right)$
31 25 30 mpand ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to \left({M}+1\le {N}\to {M}+{A}<{N}\right)$
32 18 31 sylbid ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to \left({M}<{N}\to {M}+{A}<{N}\right)$
33 16 32 syld ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to \left({M}+{A}\le {N}\to {M}+{A}<{N}\right)$
34 10 33 impbid ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {A}\in \left(0,1\right)\right)\to \left({M}+{A}<{N}↔{M}+{A}\le {N}\right)$