Metamath Proof Explorer


Theorem lediv23

Description: Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005)

Ref Expression
Assertion lediv23 ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 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 3adant3 ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
8 simp3 ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
9 simp2 ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
10 lemul1 ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) ≤ 𝐶 ↔ ( ( 𝐴 / 𝐵 ) · 𝐵 ) ≤ ( 𝐶 · 𝐵 ) ) )
11 7 8 9 10 syl3anc ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 / 𝐵 ) ≤ 𝐶 ↔ ( ( 𝐴 / 𝐵 ) · 𝐵 ) ≤ ( 𝐶 · 𝐵 ) ) )
12 11 3adant3r ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 / 𝐵 ) ≤ 𝐶 ↔ ( ( 𝐴 / 𝐵 ) · 𝐵 ) ≤ ( 𝐶 · 𝐵 ) ) )
13 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
14 13 adantr ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 𝐴 ∈ ℂ )
15 recn ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
16 15 ad2antrl ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 𝐵 ∈ ℂ )
17 2 adantl ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 𝐵 ≠ 0 )
18 14 16 17 divcan1d ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) · 𝐵 ) = 𝐴 )
19 18 3adant3 ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 / 𝐵 ) · 𝐵 ) = 𝐴 )
20 19 breq1d ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( ( 𝐴 / 𝐵 ) · 𝐵 ) ≤ ( 𝐶 · 𝐵 ) ↔ 𝐴 ≤ ( 𝐶 · 𝐵 ) ) )
21 remulcl ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 · 𝐵 ) ∈ ℝ )
22 21 ancoms ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 · 𝐵 ) ∈ ℝ )
23 22 adantrr ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐶 · 𝐵 ) ∈ ℝ )
24 23 3adant1 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐶 · 𝐵 ) ∈ ℝ )
25 lediv1 ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 · 𝐵 ) ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ ( 𝐶 · 𝐵 ) ↔ ( 𝐴 / 𝐶 ) ≤ ( ( 𝐶 · 𝐵 ) / 𝐶 ) ) )
26 24 25 syld3an2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ ( 𝐶 · 𝐵 ) ↔ ( 𝐴 / 𝐶 ) ≤ ( ( 𝐶 · 𝐵 ) / 𝐶 ) ) )
27 recn ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
28 27 adantr ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → 𝐶 ∈ ℂ )
29 gt0ne0 ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → 𝐶 ≠ 0 )
30 28 29 jca ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
31 divcan3 ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( ( 𝐶 · 𝐵 ) / 𝐶 ) = 𝐵 )
32 31 3expb ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐵 ) / 𝐶 ) = 𝐵 )
33 15 30 32 syl2an ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐶 · 𝐵 ) / 𝐶 ) = 𝐵 )
34 33 3adant1 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐶 · 𝐵 ) / 𝐶 ) = 𝐵 )
35 34 breq2d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 / 𝐶 ) ≤ ( ( 𝐶 · 𝐵 ) / 𝐶 ) ↔ ( 𝐴 / 𝐶 ) ≤ 𝐵 ) )
36 26 35 bitrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ ( 𝐶 · 𝐵 ) ↔ ( 𝐴 / 𝐶 ) ≤ 𝐵 ) )
37 36 3adant2r ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ ( 𝐶 · 𝐵 ) ↔ ( 𝐴 / 𝐶 ) ≤ 𝐵 ) )
38 12 20 37 3bitrd ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 / 𝐵 ) ≤ 𝐶 ↔ ( 𝐴 / 𝐶 ) ≤ 𝐵 ) )