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 ↔ C B < C A

Proof

Step Hyp Ref Expression
1 ltrec ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → A < B ↔ 1 B < 1 A
2 1 3adant3 ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ 1 B < 1 A
3 gt0ne0 ⊢ B ∈ ℝ ∧ 0 < B → B ≠ 0
4 rereccl ⊢ B ∈ ℝ ∧ B ≠ 0 → 1 B ∈ ℝ
5 3 4 syldan ⊢ B ∈ ℝ ∧ 0 < B → 1 B ∈ ℝ
6 gt0ne0 ⊢ A ∈ ℝ ∧ 0 < A → A ≠ 0
7 rereccl ⊢ A ∈ ℝ ∧ A ≠ 0 → 1 A ∈ ℝ
8 6 7 syldan ⊢ A ∈ ℝ ∧ 0 < A → 1 A ∈ ℝ
9 ltmul2 ⊢ 1 B ∈ ℝ ∧ 1 A ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → 1 B < 1 A ↔ C ⁢ 1 B < C ⁢ 1 A
10 8 9 syl3an2 ⊢ 1 B ∈ ℝ ∧ A ∈ ℝ ∧ 0 < A ∧ C ∈ ℝ ∧ 0 < C → 1 B < 1 A ↔ C ⁢ 1 B < C ⁢ 1 A
11 5 10 syl3an1 ⊢ B ∈ ℝ ∧ 0 < B ∧ A ∈ ℝ ∧ 0 < A ∧ C ∈ ℝ ∧ 0 < C → 1 B < 1 A ↔ C ⁢ 1 B < C ⁢ 1 A
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 → C B = C ⁢ 1 B
21 20 3expb ⊢ C ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → C B = C ⁢ 1 B
22 21 3adant3 ⊢ C ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ A ∈ ℂ ∧ A ≠ 0 → C B = C ⁢ 1 B
23 divrec ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0 → C A = C ⁢ 1 A
24 23 3expb ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0 → C A = C ⁢ 1 A
25 24 3adant2 ⊢ C ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ A ∈ ℂ ∧ A ≠ 0 → C A = C ⁢ 1 A
26 22 25 breq12d ⊢ C ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ A ∈ ℂ ∧ A ≠ 0 → C B < C A ↔ C ⁢ 1 B < C ⁢ 1 A
27 13 16 19 26 syl3an ⊢ C ∈ ℝ ∧ 0 < C ∧ B ∈ ℝ ∧ 0 < B ∧ A ∈ ℝ ∧ 0 < A → C B < C A ↔ C ⁢ 1 B < C ⁢ 1 A
28 27 3coml ⊢ B ∈ ℝ ∧ 0 < B ∧ A ∈ ℝ ∧ 0 < A ∧ C ∈ ℝ ∧ 0 < C → C B < C A ↔ C ⁢ 1 B < C ⁢ 1 A
29 11 28 bitr4d ⊢ B ∈ ℝ ∧ 0 < B ∧ A ∈ ℝ ∧ 0 < A ∧ C ∈ ℝ ∧ 0 < C → 1 B < 1 A ↔ C B < C A
30 29 3com12 ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 < C → 1 B < 1 A ↔ C B < C A
31 2 30 bitrd ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ C B < C A