Metamath Proof Explorer

Theorem lediv2aALT

Description: Division of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion lediv2aALT ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C → A ≤ B → C B ≤ C A

Proof

Step Hyp Ref Expression
1 gt0ne0 ⊢ B ∈ ℝ ∧ 0 < B → B ≠ 0
2 rereccl ⊢ B ∈ ℝ ∧ B ≠ 0 → 1 B ∈ ℝ
3 1 2 syldan ⊢ B ∈ ℝ ∧ 0 < B → 1 B ∈ ℝ
4 gt0ne0 ⊢ A ∈ ℝ ∧ 0 < A → A ≠ 0
5 rereccl ⊢ A ∈ ℝ ∧ A ≠ 0 → 1 A ∈ ℝ
6 4 5 syldan ⊢ A ∈ ℝ ∧ 0 < A → 1 A ∈ ℝ
7 3 6 anim12i ⊢ B ∈ ℝ ∧ 0 < B ∧ A ∈ ℝ ∧ 0 < A → 1 B ∈ ℝ ∧ 1 A ∈ ℝ
8 7 ancoms ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 B ∈ ℝ ∧ 1 A ∈ ℝ
9 8 3adant3 ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C → 1 B ∈ ℝ ∧ 1 A ∈ ℝ
10 simp3 ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C → C ∈ ℝ ∧ 0 ≤ C
11 df-3an ⊢ 1 B ∈ ℝ ∧ 1 A ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ↔ 1 B ∈ ℝ ∧ 1 A ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C
12 9 10 11 sylanbrc ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C → 1 B ∈ ℝ ∧ 1 A ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C
13 lemul2a ⊢ 1 B ∈ ℝ ∧ 1 A ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ 1 B ≤ 1 A → C ⁢ 1 B ≤ C ⁢ 1 A
14 13 ex ⊢ 1 B ∈ ℝ ∧ 1 A ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C → 1 B ≤ 1 A → C ⁢ 1 B ≤ C ⁢ 1 A
15 12 14 syl ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C → 1 B ≤ 1 A → C ⁢ 1 B ≤ C ⁢ 1 A
16 lerec ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → A ≤ B ↔ 1 B ≤ 1 A
17 16 3adant3 ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C → A ≤ B ↔ 1 B ≤ 1 A
18 recn ⊢ C ∈ ℝ → C ∈ ℂ
19 18 adantr ⊢ C ∈ ℝ ∧ 0 ≤ C → C ∈ ℂ
20 recn ⊢ B ∈ ℝ → B ∈ ℂ
21 20 adantr ⊢ B ∈ ℝ ∧ 0 < B → B ∈ ℂ
22 21 1 jca ⊢ B ∈ ℝ ∧ 0 < B → B ∈ ℂ ∧ B ≠ 0
23 19 22 anim12i ⊢ C ∈ ℝ ∧ 0 ≤ C ∧ B ∈ ℝ ∧ 0 < B → C ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0
24 3anass ⊢ C ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ↔ C ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0
25 23 24 sylibr ⊢ C ∈ ℝ ∧ 0 ≤ C ∧ B ∈ ℝ ∧ 0 < B → C ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0
26 divrec ⊢ C ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → C B = C ⁢ 1 B
27 25 26 syl ⊢ C ∈ ℝ ∧ 0 ≤ C ∧ B ∈ ℝ ∧ 0 < B → C B = C ⁢ 1 B
28 27 ancoms ⊢ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C → C B = C ⁢ 1 B
29 28 3adant1 ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C → C B = C ⁢ 1 B
30 recn ⊢ A ∈ ℝ → A ∈ ℂ
31 30 adantr ⊢ A ∈ ℝ ∧ 0 < A → A ∈ ℂ
32 31 4 jca ⊢ A ∈ ℝ ∧ 0 < A → A ∈ ℂ ∧ A ≠ 0
33 19 32 anim12i ⊢ C ∈ ℝ ∧ 0 ≤ C ∧ A ∈ ℝ ∧ 0 < A → C ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0
34 3anass ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0 ↔ C ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0
35 33 34 sylibr ⊢ C ∈ ℝ ∧ 0 ≤ C ∧ A ∈ ℝ ∧ 0 < A → C ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0
36 divrec ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0 → C A = C ⁢ 1 A
37 35 36 syl ⊢ C ∈ ℝ ∧ 0 ≤ C ∧ A ∈ ℝ ∧ 0 < A → C A = C ⁢ 1 A
38 37 ancoms ⊢ A ∈ ℝ ∧ 0 < A ∧ C ∈ ℝ ∧ 0 ≤ C → C A = C ⁢ 1 A
39 38 3adant2 ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C → C A = C ⁢ 1 A
40 29 39 breq12d ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C → C B ≤ C A ↔ C ⁢ 1 B ≤ C ⁢ 1 A
41 15 17 40 3imtr4d ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 ≤ C → A ≤ B → C B ≤ C A