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 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ A ∈ 0 1 → M + A < N ↔ M + A ≤ N

Proof

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