Metamath Proof Explorer

Theorem ledivge1le

Description: If a number is less than or equal to another number, the number divided by a positive number greater than or equal to one is less than or equal to the other number. (Contributed by AV, 29-Jun-2021)

Ref Expression
Assertion ledivge1le ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 / 𝐶 ) ≤ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 divle1le ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) ≤ 1 ↔ 𝐴 ≤ 𝐵 ) )
2 1 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) ≤ 1 ↔ 𝐴 ≤ 𝐵 ) )
3 rerpdivcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
4 3 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
5 1red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝐶 ∈ ℝ+ ) → 1 ∈ ℝ )
6 rpre ⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ∈ ℝ )
7 6 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
8 letr ⊢ ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 / 𝐵 ) ≤ 1 ∧ 1 ≤ 𝐶 ) → ( 𝐴 / 𝐵 ) ≤ 𝐶 ) )
9 4 5 7 8 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 / 𝐵 ) ≤ 1 ∧ 1 ≤ 𝐶 ) → ( 𝐴 / 𝐵 ) ≤ 𝐶 ) )
10 9 expd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) ≤ 1 → ( 1 ≤ 𝐶 → ( 𝐴 / 𝐵 ) ≤ 𝐶 ) ) )
11 2 10 sylbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 → ( 1 ≤ 𝐶 → ( 𝐴 / 𝐵 ) ≤ 𝐶 ) ) )
12 11 com23 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝐶 ∈ ℝ+ ) → ( 1 ≤ 𝐶 → ( 𝐴 ≤ 𝐵 → ( 𝐴 / 𝐵 ) ≤ 𝐶 ) ) )
13 12 expimpd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 / 𝐵 ) ≤ 𝐶 ) ) )
14 13 ex ⊢ ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ℝ+ → ( ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 / 𝐵 ) ≤ 𝐶 ) ) ) )
15 14 3imp1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 / 𝐵 ) ≤ 𝐶 )
16 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) ) → 𝐴 ∈ ℝ )
17 6 adantr ⊢ ( ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) → 𝐶 ∈ ℝ )
18 0lt1 ⊢ 0 < 1
19 0red ⊢ ( 𝐶 ∈ ℝ+ → 0 ∈ ℝ )
20 1red ⊢ ( 𝐶 ∈ ℝ+ → 1 ∈ ℝ )
21 ltletr ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 0 < 1 ∧ 1 ≤ 𝐶 ) → 0 < 𝐶 ) )
22 19 20 6 21 syl3anc ⊢ ( 𝐶 ∈ ℝ+ → ( ( 0 < 1 ∧ 1 ≤ 𝐶 ) → 0 < 𝐶 ) )
23 18 22 mpani ⊢ ( 𝐶 ∈ ℝ+ → ( 1 ≤ 𝐶 → 0 < 𝐶 ) )
24 23 imp ⊢ ( ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) → 0 < 𝐶 )
25 17 24 jca ⊢ ( ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) → ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) )
26 25 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) ) → ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) )
27 rpregt0 ⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
28 27 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) ) → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
29 16 26 28 3jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) ) → ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) )
30 29 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) )
31 lediv23 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐶 ) ≤ 𝐵 ↔ ( 𝐴 / 𝐵 ) ≤ 𝐶 ) )
32 30 31 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 / 𝐶 ) ≤ 𝐵 ↔ ( 𝐴 / 𝐵 ) ≤ 𝐶 ) )
33 15 32 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 / 𝐶 ) ≤ 𝐵 )
34 33 ex ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ ( 𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶 ) ) → ( 𝐴 ≤ 𝐵 → ( 𝐴 / 𝐶 ) ≤ 𝐵 ) )