Step |
Hyp |
Ref |
Expression |
1 |
|
lep1 |
|- ( A e. RR -> A <_ ( A + 1 ) ) |
2 |
1
|
adantr |
|- ( ( A e. RR /\ B e. RR ) -> A <_ ( A + 1 ) ) |
3 |
|
peano2re |
|- ( A e. RR -> ( A + 1 ) e. RR ) |
4 |
3
|
ancli |
|- ( A e. RR -> ( A e. RR /\ ( A + 1 ) e. RR ) ) |
5 |
|
letr |
|- ( ( A e. RR /\ ( A + 1 ) e. RR /\ B e. RR ) -> ( ( A <_ ( A + 1 ) /\ ( A + 1 ) <_ B ) -> A <_ B ) ) |
6 |
5
|
3expa |
|- ( ( ( A e. RR /\ ( A + 1 ) e. RR ) /\ B e. RR ) -> ( ( A <_ ( A + 1 ) /\ ( A + 1 ) <_ B ) -> A <_ B ) ) |
7 |
4 6
|
sylan |
|- ( ( A e. RR /\ B e. RR ) -> ( ( A <_ ( A + 1 ) /\ ( A + 1 ) <_ B ) -> A <_ B ) ) |
8 |
2 7
|
mpand |
|- ( ( A e. RR /\ B e. RR ) -> ( ( A + 1 ) <_ B -> A <_ B ) ) |
9 |
8
|
3impia |
|- ( ( A e. RR /\ B e. RR /\ ( A + 1 ) <_ B ) -> A <_ B ) |