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