Step |
Hyp |
Ref |
Expression |
1 |
|
pm3.2 |
|- ( C e. RR -> ( C e. RR -> ( C e. RR /\ C e. RR ) ) ) |
2 |
1
|
pm2.43i |
|- ( C e. RR -> ( C e. RR /\ C e. RR ) ) |
3 |
2
|
adantr |
|- ( ( C e. RR /\ 0 <_ C ) -> ( C e. RR /\ C e. RR ) ) |
4 |
|
leid |
|- ( C e. RR -> C <_ C ) |
5 |
4
|
anim1ci |
|- ( ( C e. RR /\ 0 <_ C ) -> ( 0 <_ C /\ C <_ C ) ) |
6 |
3 5
|
jca |
|- ( ( C e. RR /\ 0 <_ C ) -> ( ( C e. RR /\ C e. RR ) /\ ( 0 <_ C /\ C <_ C ) ) ) |
7 |
6
|
ad2antlr |
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( ( C e. RR /\ C e. RR ) /\ ( 0 <_ C /\ C <_ C ) ) ) |
8 |
7
|
3adantl2 |
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( ( C e. RR /\ C e. RR ) /\ ( 0 <_ C /\ C <_ C ) ) ) |
9 |
|
id |
|- ( ( A e. RR /\ B e. RR ) -> ( A e. RR /\ B e. RR ) ) |
10 |
9
|
ad2ant2r |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A e. RR /\ B e. RR ) ) |
11 |
10
|
adantr |
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ A <_ B ) -> ( A e. RR /\ B e. RR ) ) |
12 |
|
simplr |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < A ) |
13 |
12
|
anim1i |
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ A <_ B ) -> ( 0 < A /\ A <_ B ) ) |
14 |
11 13
|
jca |
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ A <_ B ) -> ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ A <_ B ) ) ) |
15 |
14
|
3adantl3 |
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ A <_ B ) ) ) |
16 |
|
lediv12a |
|- ( ( ( ( C e. RR /\ C e. RR ) /\ ( 0 <_ C /\ C <_ C ) ) /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ A <_ B ) ) ) -> ( C / B ) <_ ( C / A ) ) |
17 |
8 15 16
|
syl2anc |
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( C / B ) <_ ( C / A ) ) |