Theorem lediv1

Description: Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004)

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

Proof

Step	Hyp	Ref	Expression
1		ltdiv1	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐵 < 𝐴 ↔ ( 𝐵 / 𝐶 ) < ( 𝐴 / 𝐶 ) ) )
2	1	3com12	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐵 < 𝐴 ↔ ( 𝐵 / 𝐶 ) < ( 𝐴 / 𝐶 ) ) )
3	2	notbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ¬ 𝐵 < 𝐴 ↔ ¬ ( 𝐵 / 𝐶 ) < ( 𝐴 / 𝐶 ) ) )
4		lenlt	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
5	4	3adant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
6		gt0ne0	⊢ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → 𝐶 ≠ 0 )
7	6	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → 𝐶 ≠ 0 )
8		redivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) → ( 𝐴 / 𝐶 ) ∈ ℝ )
9	7 8	syld3an3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → ( 𝐴 / 𝐶 ) ∈ ℝ )
10	9	3expb	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 / 𝐶 ) ∈ ℝ )
11	10	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 / 𝐶 ) ∈ ℝ )
12	6	3adant1	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → 𝐶 ≠ 0 )
13		redivcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) → ( 𝐵 / 𝐶 ) ∈ ℝ )
14	12 13	syld3an3	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → ( 𝐵 / 𝐶 ) ∈ ℝ )
15	14	3expb	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐵 / 𝐶 ) ∈ ℝ )
16	15	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐵 / 𝐶 ) ∈ ℝ )
17	11 16	lenltd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 / 𝐶 ) ≤ ( 𝐵 / 𝐶 ) ↔ ¬ ( 𝐵 / 𝐶 ) < ( 𝐴 / 𝐶 ) ) )
18	3 5 17	3bitr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 / 𝐶 ) ≤ ( 𝐵 / 𝐶 ) ) )