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

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 < 𝐶 ) ) → ( ( 𝐴 / 𝐵 ) ≤ 𝐶 ↔ ( 𝐴 / 𝐶 ) ≤ 𝐵 ) )