Step |
Hyp |
Ref |
Expression |
1 |
|
ltle |
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) ) |
2 |
|
ltne |
|- ( ( A e. RR /\ A < B ) -> B =/= A ) |
3 |
2
|
ex |
|- ( A e. RR -> ( A < B -> B =/= A ) ) |
4 |
3
|
adantr |
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> B =/= A ) ) |
5 |
1 4
|
jcad |
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> ( A <_ B /\ B =/= A ) ) ) |
6 |
|
leloe |
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( A < B \/ A = B ) ) ) |
7 |
|
df-ne |
|- ( B =/= A <-> -. B = A ) |
8 |
|
pm2.24 |
|- ( B = A -> ( -. B = A -> A < B ) ) |
9 |
8
|
eqcoms |
|- ( A = B -> ( -. B = A -> A < B ) ) |
10 |
7 9
|
syl5bi |
|- ( A = B -> ( B =/= A -> A < B ) ) |
11 |
10
|
jao1i |
|- ( ( A < B \/ A = B ) -> ( B =/= A -> A < B ) ) |
12 |
6 11
|
syl6bi |
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> ( B =/= A -> A < B ) ) ) |
13 |
12
|
impd |
|- ( ( A e. RR /\ B e. RR ) -> ( ( A <_ B /\ B =/= A ) -> A < B ) ) |
14 |
5 13
|
impbid |
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( A <_ B /\ B =/= A ) ) ) |