Metamath Proof Explorer

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 ⊢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 3 3ad2ant2 ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0<C→1B∈ℝ
5 gt0ne0 ⊢A∈ℝ∧0<A→A≠0
6 rereccl ⊢A∈ℝ∧A≠0→1A∈ℝ
7 5 6 syldan ⊢A∈ℝ∧0<A→1A∈ℝ
8 7 3ad2ant1 ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0<C→1A∈ℝ
9 simp3l ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0<C→C∈ℝ
10 simp3r ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0<C→0<C
11 lemul2 ⊢1B∈ℝ∧1A∈ℝ∧C∈ℝ∧0<C→1B≤1A↔C⁢1B≤C⁢1A
12 4 8 9 10 11 syl112anc ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0<C→1B≤1A↔C⁢1B≤C⁢1A
13 lerec ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B→A≤B↔1B≤1A
14 13 3adant3 ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0<C→A≤B↔1B≤1A
15 recn ⊢C∈ℝ→C∈ℂ
16 recn ⊢B∈ℝ→B∈ℂ
17 16 adantr ⊢B∈ℝ∧0<B→B∈ℂ
18 17 1 jca ⊢B∈ℝ∧0<B→B∈ℂ∧B≠0
19 divrec ⊢C∈ℂ∧B∈ℂ∧B≠0→CB=C⁢1B
20 19 3expb ⊢C∈ℂ∧B∈ℂ∧B≠0→CB=C⁢1B
21 15 18 20 syl2an ⊢C∈ℝ∧B∈ℝ∧0<B→CB=C⁢1B
22 21 3adant2 ⊢C∈ℝ∧A∈ℝ∧0<A∧B∈ℝ∧0<B→CB=C⁢1B
23 recn ⊢A∈ℝ→A∈ℂ
24 23 adantr ⊢A∈ℝ∧0<A→A∈ℂ
25 24 5 jca ⊢A∈ℝ∧0<A→A∈ℂ∧A≠0
26 divrec ⊢C∈ℂ∧A∈ℂ∧A≠0→CA=C⁢1A
27 26 3expb ⊢C∈ℂ∧A∈ℂ∧A≠0→CA=C⁢1A
28 15 25 27 syl2an ⊢C∈ℝ∧A∈ℝ∧0<A→CA=C⁢1A
29 28 3adant3 ⊢C∈ℝ∧A∈ℝ∧0<A∧B∈ℝ∧0<B→CA=C⁢1A
30 22 29 breq12d ⊢C∈ℝ∧A∈ℝ∧0<A∧B∈ℝ∧0<B→CB≤CA↔C⁢1B≤C⁢1A
31 30 3coml ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ→CB≤CA↔C⁢1B≤C⁢1A
32 31 3adant3r ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0<C→CB≤CA↔C⁢1B≤C⁢1A
33 12 14 32 3bitr4d ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0<C→A≤B↔CB≤CA