Theorem lediv2aALT

Description: Division of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	lediv2aALT	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 ≤ 𝐵 → ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gt0ne0	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ≠ 0 )
2		rereccl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 1 / 𝐵 ) ∈ ℝ )
3	1 2	syldan	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → ( 1 / 𝐵 ) ∈ ℝ )
4		gt0ne0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
5		rereccl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℝ )
6	4 5	syldan	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℝ )
7	3 6	anim12i	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( 1 / 𝐵 ) ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ) )
8	7	ancoms	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 1 / 𝐵 ) ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ) )
9	8	3adant3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( ( 1 / 𝐵 ) ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ) )
10		simp3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
11		df-3an	⊢ ( ( ( 1 / 𝐵 ) ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ↔ ( ( ( 1 / 𝐵 ) ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) )
12	9 10 11	sylanbrc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( ( 1 / 𝐵 ) ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) )
13		lemul2a	⊢ ( ( ( ( 1 / 𝐵 ) ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ∧ ( 1 / 𝐵 ) ≤ ( 1 / 𝐴 ) ) → ( 𝐶 · ( 1 / 𝐵 ) ) ≤ ( 𝐶 · ( 1 / 𝐴 ) ) )
14	13	ex	⊢ ( ( ( 1 / 𝐵 ) ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( ( 1 / 𝐵 ) ≤ ( 1 / 𝐴 ) → ( 𝐶 · ( 1 / 𝐵 ) ) ≤ ( 𝐶 · ( 1 / 𝐴 ) ) ) )
15	12 14	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( ( 1 / 𝐵 ) ≤ ( 1 / 𝐴 ) → ( 𝐶 · ( 1 / 𝐵 ) ) ≤ ( 𝐶 · ( 1 / 𝐴 ) ) ) )
16		lerec	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 1 / 𝐵 ) ≤ ( 1 / 𝐴 ) ) )
17	16	3adant3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 1 / 𝐵 ) ≤ ( 1 / 𝐴 ) ) )
18		recn	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
19	18	adantr	⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) → 𝐶 ∈ ℂ )
20		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
21	20	adantr	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ∈ ℂ )
22	21 1	jca	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
23	19 22	anim12i	⊢ ( ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐶 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) )
24		3anass	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ↔ ( 𝐶 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) )
25	23 24	sylibr	⊢ ( ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
26		divrec	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐶 / 𝐵 ) = ( 𝐶 · ( 1 / 𝐵 ) ) )
27	25 26	syl	⊢ ( ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐶 / 𝐵 ) = ( 𝐶 · ( 1 / 𝐵 ) ) )
28	27	ancoms	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐶 / 𝐵 ) = ( 𝐶 · ( 1 / 𝐵 ) ) )
29	28	3adant1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐶 / 𝐵 ) = ( 𝐶 · ( 1 / 𝐵 ) ) )
30		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
31	30	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ∈ ℂ )
32	31 4	jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
33	19 32	anim12i	⊢ ( ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 𝐶 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) )
34		3anass	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ↔ ( 𝐶 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) )
35	33 34	sylibr	⊢ ( ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
36		divrec	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐶 / 𝐴 ) = ( 𝐶 · ( 1 / 𝐴 ) ) )
37	35 36	syl	⊢ ( ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 𝐶 / 𝐴 ) = ( 𝐶 · ( 1 / 𝐴 ) ) )
38	37	ancoms	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐶 / 𝐴 ) = ( 𝐶 · ( 1 / 𝐴 ) ) )
39	38	3adant2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐶 / 𝐴 ) = ( 𝐶 · ( 1 / 𝐴 ) ) )
40	29 39	breq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) ↔ ( 𝐶 · ( 1 / 𝐵 ) ) ≤ ( 𝐶 · ( 1 / 𝐴 ) ) ) )
41	15 17 40	3imtr4d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 ≤ 𝐵 → ( 𝐶 / 𝐵 ) ≤ ( 𝐶 / 𝐴 ) ) )