Metamath Proof Explorer

Theorem zltaddlt1le

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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( ( 𝑀 + 𝐴 ) < 𝑁 ↔ ( 𝑀 + 𝐴 ) ≤ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
2 1 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → 𝑀 ∈ ℝ )
3 elioore ⊢ ( 𝐴 ∈ ( 0 (,) 1 ) → 𝐴 ∈ ℝ )
4 3 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → 𝐴 ∈ ℝ )
5 2 4 readdcld ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( 𝑀 + 𝐴 ) ∈ ℝ )
6 5 3adant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( 𝑀 + 𝐴 ) ∈ ℝ )
7 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
8 7 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ℝ )
9 ltle ⊢ ( ( ( 𝑀 + 𝐴 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 + 𝐴 ) < 𝑁 → ( 𝑀 + 𝐴 ) ≤ 𝑁 ) )
10 6 8 9 syl2anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( ( 𝑀 + 𝐴 ) < 𝑁 → ( 𝑀 + 𝐴 ) ≤ 𝑁 ) )
11 elioo3g ⊢ ( 𝐴 ∈ ( 0 (,) 1 ) ↔ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) ∧ ( 0 < 𝐴 ∧ 𝐴 < 1 ) ) )
12 simpl ⊢ ( ( 0 < 𝐴 ∧ 𝐴 < 1 ) → 0 < 𝐴 )
13 11 12 simplbiim ⊢ ( 𝐴 ∈ ( 0 (,) 1 ) → 0 < 𝐴 )
14 3 13 elrpd ⊢ ( 𝐴 ∈ ( 0 (,) 1 ) → 𝐴 ∈ ℝ+ )
15 addlelt ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → ( ( 𝑀 + 𝐴 ) ≤ 𝑁 → 𝑀 < 𝑁 ) )
16 1 7 14 15 syl3an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( ( 𝑀 + 𝐴 ) ≤ 𝑁 → 𝑀 < 𝑁 ) )
17 zltp1le ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 + 1 ) ≤ 𝑁 ) )
18 17 3adant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 + 1 ) ≤ 𝑁 ) )
19 3 3ad2ant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → 𝐴 ∈ ℝ )
20 1red ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → 1 ∈ ℝ )
21 1 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → 𝑀 ∈ ℝ )
22 simpr ⊢ ( ( 0 < 𝐴 ∧ 𝐴 < 1 ) → 𝐴 < 1 )
23 11 22 simplbiim ⊢ ( 𝐴 ∈ ( 0 (,) 1 ) → 𝐴 < 1 )
24 23 3ad2ant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → 𝐴 < 1 )
25 19 20 21 24 ltadd2dd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( 𝑀 + 𝐴 ) < ( 𝑀 + 1 ) )
26 peano2z ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 + 1 ) ∈ ℤ )
27 26 zred ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 + 1 ) ∈ ℝ )
28 27 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( 𝑀 + 1 ) ∈ ℝ )
29 ltletr ⊢ ( ( ( 𝑀 + 𝐴 ) ∈ ℝ ∧ ( 𝑀 + 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝑀 + 𝐴 ) < ( 𝑀 + 1 ) ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) → ( 𝑀 + 𝐴 ) < 𝑁 ) )
30 6 28 8 29 syl3anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( ( ( 𝑀 + 𝐴 ) < ( 𝑀 + 1 ) ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) → ( 𝑀 + 𝐴 ) < 𝑁 ) )
31 25 30 mpand ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( ( 𝑀 + 1 ) ≤ 𝑁 → ( 𝑀 + 𝐴 ) < 𝑁 ) )
32 18 31 sylbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( 𝑀 < 𝑁 → ( 𝑀 + 𝐴 ) < 𝑁 ) )
33 16 32 syld ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( ( 𝑀 + 𝐴 ) ≤ 𝑁 → ( 𝑀 + 𝐴 ) < 𝑁 ) )
34 10 33 impbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 0 (,) 1 ) ) → ( ( 𝑀 + 𝐴 ) < 𝑁 ↔ ( 𝑀 + 𝐴 ) ≤ 𝑁 ) )