Step |
Hyp |
Ref |
Expression |
1 |
|
peano2z |
|- ( B e. ZZ -> ( B + 1 ) e. ZZ ) |
2 |
1
|
ad2antrl |
|- ( ( A e. ZZ /\ ( B e. ZZ /\ A <_ B ) ) -> ( B + 1 ) e. ZZ ) |
3 |
|
zre |
|- ( A e. ZZ -> A e. RR ) |
4 |
|
zre |
|- ( B e. ZZ -> B e. RR ) |
5 |
|
lep1 |
|- ( B e. RR -> B <_ ( B + 1 ) ) |
6 |
5
|
adantl |
|- ( ( A e. RR /\ B e. RR ) -> B <_ ( B + 1 ) ) |
7 |
|
peano2re |
|- ( B e. RR -> ( B + 1 ) e. RR ) |
8 |
7
|
ancli |
|- ( B e. RR -> ( B e. RR /\ ( B + 1 ) e. RR ) ) |
9 |
|
letr |
|- ( ( A e. RR /\ B e. RR /\ ( B + 1 ) e. RR ) -> ( ( A <_ B /\ B <_ ( B + 1 ) ) -> A <_ ( B + 1 ) ) ) |
10 |
9
|
3expb |
|- ( ( A e. RR /\ ( B e. RR /\ ( B + 1 ) e. RR ) ) -> ( ( A <_ B /\ B <_ ( B + 1 ) ) -> A <_ ( B + 1 ) ) ) |
11 |
8 10
|
sylan2 |
|- ( ( A e. RR /\ B e. RR ) -> ( ( A <_ B /\ B <_ ( B + 1 ) ) -> A <_ ( B + 1 ) ) ) |
12 |
6 11
|
mpan2d |
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> A <_ ( B + 1 ) ) ) |
13 |
3 4 12
|
syl2an |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A <_ B -> A <_ ( B + 1 ) ) ) |
14 |
13
|
impr |
|- ( ( A e. ZZ /\ ( B e. ZZ /\ A <_ B ) ) -> A <_ ( B + 1 ) ) |
15 |
2 14
|
jca |
|- ( ( A e. ZZ /\ ( B e. ZZ /\ A <_ B ) ) -> ( ( B + 1 ) e. ZZ /\ A <_ ( B + 1 ) ) ) |
16 |
|
breq2 |
|- ( x = B -> ( A <_ x <-> A <_ B ) ) |
17 |
16
|
elrab |
|- ( B e. { x e. ZZ | A <_ x } <-> ( B e. ZZ /\ A <_ B ) ) |
18 |
17
|
anbi2i |
|- ( ( A e. ZZ /\ B e. { x e. ZZ | A <_ x } ) <-> ( A e. ZZ /\ ( B e. ZZ /\ A <_ B ) ) ) |
19 |
|
breq2 |
|- ( x = ( B + 1 ) -> ( A <_ x <-> A <_ ( B + 1 ) ) ) |
20 |
19
|
elrab |
|- ( ( B + 1 ) e. { x e. ZZ | A <_ x } <-> ( ( B + 1 ) e. ZZ /\ A <_ ( B + 1 ) ) ) |
21 |
15 18 20
|
3imtr4i |
|- ( ( A e. ZZ /\ B e. { x e. ZZ | A <_ x } ) -> ( B + 1 ) e. { x e. ZZ | A <_ x } ) |