This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ledivdivd

Description: Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses rpred.1 
|- ( ph -> A e. RR+ )
rpaddcld.1 
|- ( ph -> B e. RR+ )
ltdiv2d.3 
|- ( ph -> C e. RR+ )
ledivdivd.4 
|- ( ph -> D e. RR+ )
ledivdivd.5 
|- ( ph -> ( A / B ) <_ ( C / D ) )
Assertion ledivdivd 
|- ( ph -> ( D / C ) <_ ( B / A ) )

Proof

Step Hyp Ref Expression
1 rpred.1 
 |-  ( ph -> A e. RR+ )
2 rpaddcld.1 
 |-  ( ph -> B e. RR+ )
3 ltdiv2d.3 
 |-  ( ph -> C e. RR+ )
4 ledivdivd.4 
 |-  ( ph -> D e. RR+ )
5 ledivdivd.5 
 |-  ( ph -> ( A / B ) <_ ( C / D ) )
6 1 rpregt0d 
 |-  ( ph -> ( A e. RR /\ 0 < A ) )
7 2 rpregt0d 
 |-  ( ph -> ( B e. RR /\ 0 < B ) )
8 3 rpregt0d 
 |-  ( ph -> ( C e. RR /\ 0 < C ) )
9 4 rpregt0d 
 |-  ( ph -> ( D e. RR /\ 0 < D ) )
10 ledivdiv 
 |-  ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ ( ( C e. RR /\ 0 < C ) /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( A / B ) <_ ( C / D ) <-> ( D / C ) <_ ( B / A ) ) )
11 6 7 8 9 10 syl22anc 
 |-  ( ph -> ( ( A / B ) <_ ( C / D ) <-> ( D / C ) <_ ( B / A ) ) )
12 5 11 mpbid 
 |-  ( ph -> ( D / C ) <_ ( B / A ) )