Theorem ltdiv23

Description: Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999)

	Ref	Expression
Assertion	ltdiv23	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 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		ltmul1	⊢ ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 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		ltdiv1	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 · 𝐵 ) ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 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 < 𝐶 ) ) → ( ( 𝐴 / 𝐵 ) < 𝐶 ↔ ( 𝐴 / 𝐶 ) < 𝐵 ) )