Theorem lediv2

Description: Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006)

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

Proof

Step	Hyp	Ref	Expression
1		gt0ne0	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ≠ 0 )
2		rereccl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 1 / 𝐵 ) ∈ ℝ )
3	1 2	syldan	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → ( 1 / 𝐵 ) ∈ ℝ )
4	3	3ad2ant2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 1 / 𝐵 ) ∈ ℝ )
5		gt0ne0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
6		rereccl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℝ )
7	5 6	syldan	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℝ )
8	7	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 1 / 𝐴 ) ∈ ℝ )
9		simp3l	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → 𝐶 ∈ ℝ )
10		simp3r	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → 0 < 𝐶 )
11		lemul2	⊢ ( ( ( 1 / 𝐵 ) ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 1 / 𝐵 ) ≤ ( 1 / 𝐴 ) ↔ ( 𝐶 · ( 1 / 𝐵 ) ) ≤ ( 𝐶 · ( 1 / 𝐴 ) ) ) )
12	4 8 9 10 11	syl112anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 1 / 𝐵 ) ≤ ( 1 / 𝐴 ) ↔ ( 𝐶 · ( 1 / 𝐵 ) ) ≤ ( 𝐶 · ( 1 / 𝐴 ) ) ) )
13		lerec	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 1 / 𝐵 ) ≤ ( 1 / 𝐴 ) ) )
14	13	3adant3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 1 / 𝐵 ) ≤ ( 1 / 𝐴 ) ) )
15		recn	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
16		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
17	16	adantr	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ∈ ℂ )
18	17 1	jca	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
19		divrec	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐶 / 𝐵 ) = ( 𝐶 · ( 1 / 𝐵 ) ) )
20	19	3expb	⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝐶 / 𝐵 ) = ( 𝐶 · ( 1 / 𝐵 ) ) )
21	15 18 20	syl2an	⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐶 / 𝐵 ) = ( 𝐶 · ( 1 / 𝐵 ) ) )
22	21	3adant2	⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐶 / 𝐵 ) = ( 𝐶 · ( 1 / 𝐵 ) ) )
23		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
24	23	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ∈ ℂ )
25	24 5	jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
26		divrec	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐶 / 𝐴 ) = ( 𝐶 · ( 1 / 𝐴 ) ) )
27	26	3expb	⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( 𝐶 / 𝐴 ) = ( 𝐶 · ( 1 / 𝐴 ) ) )
28	15 25 27	syl2an	⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 𝐶 / 𝐴 ) = ( 𝐶 · ( 1 / 𝐴 ) ) )
29	28	3adant3	⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐶 / 𝐴 ) = ( 𝐶 · ( 1 / 𝐴 ) ) )
30	22 29	breq12d	⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) ↔ ( 𝐶 · ( 1 / 𝐵 ) ) ≤ ( 𝐶 · ( 1 / 𝐴 ) ) ) )
31	30	3coml	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) ↔ ( 𝐶 · ( 1 / 𝐵 ) ) ≤ ( 𝐶 · ( 1 / 𝐴 ) ) ) )
32	31	3adant3r	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) ↔ ( 𝐶 · ( 1 / 𝐵 ) ) ≤ ( 𝐶 · ( 1 / 𝐴 ) ) ) )
33	12 14 32	3bitr4d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) ) )