Metamath Proof Explorer

Theorem ledivdiv

Description: Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006)

Ref Expression
Assertion ledivdiv ( ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐴 / 𝐵 ) ≤ ( 𝐶 / 𝐷 ) ↔ ( 𝐷 / 𝐶 ) ≤ ( 𝐵 / 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ∈ ℝ )
2 gt0ne0 ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ≠ 0 )
3 1 2 jca ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) )
4 redivcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
5 4 3expb ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
6 3 5 sylan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
7 6 adantlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
8 divgt0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 / 𝐵 ) )
9 7 8 jca ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 / 𝐵 ) ) )
10 simpl ⊢ ( ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) → 𝐷 ∈ ℝ )
11 gt0ne0 ⊢ ( ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) → 𝐷 ≠ 0 )
12 10 11 jca ⊢ ( ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) → ( 𝐷 ∈ ℝ ∧ 𝐷 ≠ 0 ) )
13 redivcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ 𝐷 ≠ 0 ) → ( 𝐶 / 𝐷 ) ∈ ℝ )
14 13 3expb ⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 / 𝐷 ) ∈ ℝ )
15 12 14 sylan2 ⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) → ( 𝐶 / 𝐷 ) ∈ ℝ )
16 15 adantlr ⊢ ( ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) → ( 𝐶 / 𝐷 ) ∈ ℝ )
17 divgt0 ⊢ ( ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) → 0 < ( 𝐶 / 𝐷 ) )
18 16 17 jca ⊢ ( ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) → ( ( 𝐶 / 𝐷 ) ∈ ℝ ∧ 0 < ( 𝐶 / 𝐷 ) ) )
19 lerec ⊢ ( ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 / 𝐵 ) ) ∧ ( ( 𝐶 / 𝐷 ) ∈ ℝ ∧ 0 < ( 𝐶 / 𝐷 ) ) ) → ( ( 𝐴 / 𝐵 ) ≤ ( 𝐶 / 𝐷 ) ↔ ( 1 / ( 𝐶 / 𝐷 ) ) ≤ ( 1 / ( 𝐴 / 𝐵 ) ) ) )
20 9 18 19 syl2an ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐴 / 𝐵 ) ≤ ( 𝐶 / 𝐷 ) ↔ ( 1 / ( 𝐶 / 𝐷 ) ) ≤ ( 1 / ( 𝐴 / 𝐵 ) ) ) )
21 recn ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
22 21 adantr ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → 𝐶 ∈ ℂ )
23 gt0ne0 ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → 𝐶 ≠ 0 )
24 22 23 jca ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
25 recn ⊢ ( 𝐷 ∈ ℝ → 𝐷 ∈ ℂ )
26 25 adantr ⊢ ( ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) → 𝐷 ∈ ℂ )
27 26 11 jca ⊢ ( ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) → ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) )
28 recdiv ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 1 / ( 𝐶 / 𝐷 ) ) = ( 𝐷 / 𝐶 ) )
29 24 27 28 syl2an ⊢ ( ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) → ( 1 / ( 𝐶 / 𝐷 ) ) = ( 𝐷 / 𝐶 ) )
30 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
31 30 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ∈ ℂ )
32 gt0ne0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
33 31 32 jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
34 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
35 34 adantr ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ∈ ℂ )
36 35 2 jca ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
37 recdiv ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 1 / ( 𝐴 / 𝐵 ) ) = ( 𝐵 / 𝐴 ) )
38 33 36 37 syl2an ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 1 / ( 𝐴 / 𝐵 ) ) = ( 𝐵 / 𝐴 ) )
39 29 38 breqan12rd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 1 / ( 𝐶 / 𝐷 ) ) ≤ ( 1 / ( 𝐴 / 𝐵 ) ) ↔ ( 𝐷 / 𝐶 ) ≤ ( 𝐵 / 𝐴 ) ) )
40 20 39 bitrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐴 / 𝐵 ) ≤ ( 𝐶 / 𝐷 ) ↔ ( 𝐷 / 𝐶 ) ≤ ( 𝐵 / 𝐴 ) ) )