Metamath Proof Explorer

Theorem ltdiv2

Description: Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005)

Ref Expression
Assertion ltdiv2 ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0<C→A<B↔CB<CA

Proof

Step Hyp Ref Expression
1 ltrec ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B→A<B↔1B<1A
2 1 3adant3 ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0<C→A<B↔1B<1A
3 gt0ne0 ⊢B∈ℝ∧0<B→B≠0
4 rereccl ⊢B∈ℝ∧B≠0→1B∈ℝ
5 3 4 syldan ⊢B∈ℝ∧0<B→1B∈ℝ
6 gt0ne0 ⊢A∈ℝ∧0<A→A≠0
7 rereccl ⊢A∈ℝ∧A≠0→1A∈ℝ
8 6 7 syldan ⊢A∈ℝ∧0<A→1A∈ℝ
9 ltmul2 ⊢1B∈ℝ∧1A∈ℝ∧C∈ℝ∧0<C→1B<1A↔C⁢1B<C⁢1A
10 8 9 syl3an2 ⊢1B∈ℝ∧A∈ℝ∧0<A∧C∈ℝ∧0<C→1B<1A↔C⁢1B<C⁢1A
11 5 10 syl3an1 ⊢B∈ℝ∧0<B∧A∈ℝ∧0<A∧C∈ℝ∧0<C→1B<1A↔C⁢1B<C⁢1A
12 recn ⊢C∈ℝ→C∈ℂ
13 12 adantr ⊢C∈ℝ∧0<C→C∈ℂ
14 recn ⊢B∈ℝ→B∈ℂ
15 14 adantr ⊢B∈ℝ∧0<B→B∈ℂ
16 15 3 jca ⊢B∈ℝ∧0<B→B∈ℂ∧B≠0
17 recn ⊢A∈ℝ→A∈ℂ
18 17 adantr ⊢A∈ℝ∧0<A→A∈ℂ
19 18 6 jca ⊢A∈ℝ∧0<A→A∈ℂ∧A≠0
20 divrec ⊢C∈ℂ∧B∈ℂ∧B≠0→CB=C⁢1B
21 20 3expb ⊢C∈ℂ∧B∈ℂ∧B≠0→CB=C⁢1B
22 21 3adant3 ⊢C∈ℂ∧B∈ℂ∧B≠0∧A∈ℂ∧A≠0→CB=C⁢1B
23 divrec ⊢C∈ℂ∧A∈ℂ∧A≠0→CA=C⁢1A
24 23 3expb ⊢C∈ℂ∧A∈ℂ∧A≠0→CA=C⁢1A
25 24 3adant2 ⊢C∈ℂ∧B∈ℂ∧B≠0∧A∈ℂ∧A≠0→CA=C⁢1A
26 22 25 breq12d ⊢C∈ℂ∧B∈ℂ∧B≠0∧A∈ℂ∧A≠0→CB<CA↔C⁢1B<C⁢1A
27 13 16 19 26 syl3an ⊢C∈ℝ∧0<C∧B∈ℝ∧0<B∧A∈ℝ∧0<A→CB<CA↔C⁢1B<C⁢1A
28 27 3coml ⊢B∈ℝ∧0<B∧A∈ℝ∧0<A∧C∈ℝ∧0<C→CB<CA↔C⁢1B<C⁢1A
29 11 28 bitr4d ⊢B∈ℝ∧0<B∧A∈ℝ∧0<A∧C∈ℝ∧0<C→1B<1A↔CB<CA
30 29 3com12 ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0<C→1B<1A↔CB<CA
31 2 30 bitrd ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B∧C∈ℝ∧0<C→A<B↔CB<CA