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→CB≤CA

Proof

Step Hyp Ref Expression
1 gt0ne0 ⊢B∈ℝ∧0<B→B≠0
2 rereccl ⊢B∈ℝ∧B≠0→1B∈ℝ
3 1 2 syldan ⊢B∈ℝ∧0<B→1B∈ℝ
4 gt0ne0 ⊢A∈ℝ∧0<A→A≠0
5 rereccl ⊢A∈ℝ∧A≠0→1A∈ℝ
6 4 5 syldan ⊢A∈ℝ∧0<A→1A∈ℝ
7 3 6 anim12i ⊢B∈ℝ∧0<B∧A∈ℝ∧0<A→1B∈ℝ∧1A∈ℝ
8 7 ancoms ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B→1B∈ℝ∧1A∈ℝ
9 8 3adant3 ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0≤C→1B∈ℝ∧1A∈ℝ
10 simp3 ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0≤C→C∈ℝ∧0≤C
11 df-3an ⊢1B∈ℝ∧1A∈ℝ∧C∈ℝ∧0≤C↔1B∈ℝ∧1A∈ℝ∧C∈ℝ∧0≤C
12 9 10 11 sylanbrc ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0≤C→1B∈ℝ∧1A∈ℝ∧C∈ℝ∧0≤C
13 lemul2a ⊢1B∈ℝ∧1A∈ℝ∧C∈ℝ∧0≤C∧1B≤1A→C⁢1B≤C⁢1A
14 13 ex ⊢1B∈ℝ∧1A∈ℝ∧C∈ℝ∧0≤C→1B≤1A→C⁢1B≤C⁢1A
15 12 14 syl ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0≤C→1B≤1A→C⁢1B≤C⁢1A
16 lerec ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B→A≤B↔1B≤1A
17 16 3adant3 ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0≤C→A≤B↔1B≤1A
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→CB=C⁢1B
27 25 26 syl ⊢C∈ℝ∧0≤C∧B∈ℝ∧0<B→CB=C⁢1B
28 27 ancoms ⊢B∈ℝ∧0<B∧C∈ℝ∧0≤C→CB=C⁢1B
29 28 3adant1 ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0≤C→CB=C⁢1B
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→CA=C⁢1A
37 35 36 syl ⊢C∈ℝ∧0≤C∧A∈ℝ∧0<A→CA=C⁢1A
38 37 ancoms ⊢A∈ℝ∧0<A∧C∈ℝ∧0≤C→CA=C⁢1A
39 38 3adant2 ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0≤C→CA=C⁢1A
40 29 39 breq12d ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0≤C→CB≤CA↔C⁢1B≤C⁢1A
41 15 17 40 3imtr4d ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0≤C→A≤B→CB≤CA