Metamath Proof Explorer

Theorem ltdiv23

Description: Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999)

Ref Expression
Assertion ltdiv23 ⊢A∈ℝ∧B∈ℝ∧0<B∧C∈ℝ∧0<C→AB<C↔AC<B

Proof

Step Hyp Ref Expression
1 simpl ⊢B∈ℝ∧0<B→B∈ℝ
2 gt0ne0 ⊢B∈ℝ∧0<B→B≠0
3 1 2 jca ⊢B∈ℝ∧0<B→B∈ℝ∧B≠0
4 redivcl ⊢A∈ℝ∧B∈ℝ∧B≠0→AB∈ℝ
5 4 3expb ⊢A∈ℝ∧B∈ℝ∧B≠0→AB∈ℝ
6 3 5 sylan2 ⊢A∈ℝ∧B∈ℝ∧0<B→AB∈ℝ
7 6 3adant3 ⊢A∈ℝ∧B∈ℝ∧0<B∧C∈ℝ→AB∈ℝ
8 simp3 ⊢A∈ℝ∧B∈ℝ∧0<B∧C∈ℝ→C∈ℝ
9 simp2 ⊢A∈ℝ∧B∈ℝ∧0<B∧C∈ℝ→B∈ℝ∧0<B
10 ltmul1 ⊢AB∈ℝ∧C∈ℝ∧B∈ℝ∧0<B→AB<C↔AB⁢B<C⁢B
11 7 8 9 10 syl3anc ⊢A∈ℝ∧B∈ℝ∧0<B∧C∈ℝ→AB<C↔AB⁢B<C⁢B
12 11 3adant3r ⊢A∈ℝ∧B∈ℝ∧0<B∧C∈ℝ∧0<C→AB<C↔AB⁢B<C⁢B
13 recn ⊢A∈ℝ→A∈ℂ
14 13 adantr ⊢A∈ℝ∧B∈ℝ∧0<B→A∈ℂ
15 recn ⊢B∈ℝ→B∈ℂ
16 15 ad2antrl ⊢A∈ℝ∧B∈ℝ∧0<B→B∈ℂ
17 2 adantl ⊢A∈ℝ∧B∈ℝ∧0<B→B≠0
18 14 16 17 divcan1d ⊢A∈ℝ∧B∈ℝ∧0<B→AB⁢B=A
19 18 3adant3 ⊢A∈ℝ∧B∈ℝ∧0<B∧C∈ℝ∧0<C→AB⁢B=A
20 19 breq1d ⊢A∈ℝ∧B∈ℝ∧0<B∧C∈ℝ∧0<C→AB⁢B<C⁢B↔A<C⁢B
21 remulcl ⊢C∈ℝ∧B∈ℝ→C⁢B∈ℝ
22 21 ancoms ⊢B∈ℝ∧C∈ℝ→C⁢B∈ℝ
23 22 adantrr ⊢B∈ℝ∧C∈ℝ∧0<C→C⁢B∈ℝ
24 23 3adant1 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→C⁢B∈ℝ
25 ltdiv1 ⊢A∈ℝ∧C⁢B∈ℝ∧C∈ℝ∧0<C→A<C⁢B↔AC<C⁢BC
26 24 25 syld3an2 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→A<C⁢B↔AC<C⁢BC
27 recn ⊢C∈ℝ→C∈ℂ
28 27 adantr ⊢C∈ℝ∧0<C→C∈ℂ
29 gt0ne0 ⊢C∈ℝ∧0<C→C≠0
30 28 29 jca ⊢C∈ℝ∧0<C→C∈ℂ∧C≠0
31 divcan3 ⊢B∈ℂ∧C∈ℂ∧C≠0→C⁢BC=B
32 31 3expb ⊢B∈ℂ∧C∈ℂ∧C≠0→C⁢BC=B
33 15 30 32 syl2an ⊢B∈ℝ∧C∈ℝ∧0<C→C⁢BC=B
34 33 3adant1 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→C⁢BC=B
35 34 breq2d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→AC<C⁢BC↔AC<B
36 26 35 bitrd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0<C→A<C⁢B↔AC<B
37 36 3adant2r ⊢A∈ℝ∧B∈ℝ∧0<B∧C∈ℝ∧0<C→A<C⁢B↔AC<B
38 12 20 37 3bitrd ⊢A∈ℝ∧B∈ℝ∧0<B∧C∈ℝ∧0<C→AB<C↔AC<B