This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 < 𝐵 ↔ ( 𝐶 / 𝐵 ) < ( 𝐶 / 𝐴 ) ) )

Proof

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