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 e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( ( M + A ) < N <-> ( M + A ) <_ N ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( M e. ZZ -> M e. RR )
2 1 adantr 
 |-  ( ( M e. ZZ /\ A e. ( 0 (,) 1 ) ) -> M e. RR )
3 elioore 
 |-  ( A e. ( 0 (,) 1 ) -> A e. RR )
4 3 adantl 
 |-  ( ( M e. ZZ /\ A e. ( 0 (,) 1 ) ) -> A e. RR )
5 2 4 readdcld 
 |-  ( ( M e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( M + A ) e. RR )
6 5 3adant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( M + A ) e. RR )
7 zre 
 |-  ( N e. ZZ -> N e. RR )
8 7 3ad2ant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> N e. RR )
9 ltle 
 |-  ( ( ( M + A ) e. RR /\ N e. RR ) -> ( ( M + A ) < N -> ( M + A ) <_ N ) )
10 6 8 9 syl2anc 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( ( M + A ) < N -> ( M + A ) <_ N ) )
11 elioo3g 
 |-  ( A e. ( 0 (,) 1 ) <-> ( ( 0 e. RR* /\ 1 e. RR* /\ A e. RR* ) /\ ( 0 < A /\ A < 1 ) ) )
12 simpl 
 |-  ( ( 0 < A /\ A < 1 ) -> 0 < A )
13 11 12 simplbiim 
 |-  ( A e. ( 0 (,) 1 ) -> 0 < A )
14 3 13 elrpd 
 |-  ( A e. ( 0 (,) 1 ) -> A e. RR+ )
15 addlelt 
 |-  ( ( M e. RR /\ N e. RR /\ A e. RR+ ) -> ( ( M + A ) <_ N -> M < N ) )
16 1 7 14 15 syl3an 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( ( M + A ) <_ N -> M < N ) )
17 zltp1le 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) )
18 17 3adant3 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( M < N <-> ( M + 1 ) <_ N ) )
19 3 3ad2ant3 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> A e. RR )
20 1red 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> 1 e. RR )
21 1 3ad2ant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> M e. RR )
22 simpr 
 |-  ( ( 0 < A /\ A < 1 ) -> A < 1 )
23 11 22 simplbiim 
 |-  ( A e. ( 0 (,) 1 ) -> A < 1 )
24 23 3ad2ant3 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> A < 1 )
25 19 20 21 24 ltadd2dd 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( M + A ) < ( M + 1 ) )
26 peano2z 
 |-  ( M e. ZZ -> ( M + 1 ) e. ZZ )
27 26 zred 
 |-  ( M e. ZZ -> ( M + 1 ) e. RR )
28 27 3ad2ant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( M + 1 ) e. RR )
29 ltletr 
 |-  ( ( ( M + A ) e. RR /\ ( M + 1 ) e. RR /\ N e. RR ) -> ( ( ( M + A ) < ( M + 1 ) /\ ( M + 1 ) <_ N ) -> ( M + A ) < N ) )
30 6 28 8 29 syl3anc 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( ( ( M + A ) < ( M + 1 ) /\ ( M + 1 ) <_ N ) -> ( M + A ) < N ) )
31 25 30 mpand 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( ( M + 1 ) <_ N -> ( M + A ) < N ) )
32 18 31 sylbid 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( M < N -> ( M + A ) < N ) )
33 16 32 syld 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( ( M + A ) <_ N -> ( M + A ) < N ) )
34 10 33 impbid 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( ( M + A ) < N <-> ( M + A ) <_ N ) )