Step |
Hyp |
Ref |
Expression |
1 |
|
zltlesub.n |
|- ( ph -> N e. ZZ ) |
2 |
|
zltlesub.a |
|- ( ph -> A e. RR ) |
3 |
|
zltlesub.nlea |
|- ( ph -> N <_ A ) |
4 |
|
zltlesub.b |
|- ( ph -> B e. RR ) |
5 |
|
zltlesub.blt1 |
|- ( ph -> B < 1 ) |
6 |
|
zltlesub.asb |
|- ( ph -> ( A - B ) e. ZZ ) |
7 |
1
|
zred |
|- ( ph -> N e. RR ) |
8 |
6
|
zred |
|- ( ph -> ( A - B ) e. RR ) |
9 |
8 4
|
readdcld |
|- ( ph -> ( ( A - B ) + B ) e. RR ) |
10 |
|
peano2re |
|- ( ( A - B ) e. RR -> ( ( A - B ) + 1 ) e. RR ) |
11 |
8 10
|
syl |
|- ( ph -> ( ( A - B ) + 1 ) e. RR ) |
12 |
2
|
recnd |
|- ( ph -> A e. CC ) |
13 |
4
|
recnd |
|- ( ph -> B e. CC ) |
14 |
12 13
|
npcand |
|- ( ph -> ( ( A - B ) + B ) = A ) |
15 |
3 14
|
breqtrrd |
|- ( ph -> N <_ ( ( A - B ) + B ) ) |
16 |
|
1red |
|- ( ph -> 1 e. RR ) |
17 |
4 16 8 5
|
ltadd2dd |
|- ( ph -> ( ( A - B ) + B ) < ( ( A - B ) + 1 ) ) |
18 |
7 9 11 15 17
|
lelttrd |
|- ( ph -> N < ( ( A - B ) + 1 ) ) |
19 |
|
zleltp1 |
|- ( ( N e. ZZ /\ ( A - B ) e. ZZ ) -> ( N <_ ( A - B ) <-> N < ( ( A - B ) + 1 ) ) ) |
20 |
1 6 19
|
syl2anc |
|- ( ph -> ( N <_ ( A - B ) <-> N < ( ( A - B ) + 1 ) ) ) |
21 |
18 20
|
mpbird |
|- ( ph -> N <_ ( A - B ) ) |