Metamath Proof Explorer - mmtheorems44

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 4301-4400 - Page 44 of 58

Type	Label	Description
Statement
Theorem	lelt 4301	'Less than or equal to' in terms of 'less than'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A ≤ B ↔ ¬ B < A)
Theorem	ltle 4302	'Less than' implies 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B → A ≤ B)
Theorem	ltlei 4303	'Less than' implies 'less than or equal to' (inference).
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ A < B    ⇒   ⊢ A ≤ B
Theorem	eqle 4304	Equality implies 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A = B → A ≤ B)
Theorem	ltne 4305	'Less than' implies not equal.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B → ¬ A = B)
Theorem	letri 4306	Trichotomy law for 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A ≤ B ∨ B ≤ A)
Theorem	lttr 4307	'Less than' is transitive. Theorem I.17 of [Apostol] p. 20.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A < B ∧ B < C) → A < C)
Theorem	lelttr 4308	'Less than or equal to', 'less than' transitive law.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A ≤ B ∧ B < C) → A < C)
Theorem	ltletr 4309	'Less than', 'less than or equal to' transitive law.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A < B ∧ B ≤ C) → A < C)
Theorem	letr 4310	'Less than or equal to' is transitive.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A ≤ B ∧ B ≤ C) → A ≤ C)
Theorem	le2tri3 4311	Extended trichotomy law for 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A ≤ B ∧ B ≤ C ∧ C ≤ A) ↔ (A = B ∧ B = C ∧ C = A))
Theorem	ltadd2 4312	Addition to both sides of 'less than'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ (A < B ↔ (C + A) < (C + B))
Theorem	ltadd1 4313	Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ (A < B ↔ (A + C) < (B + C))
Theorem	leadd1 4314	Addition to both sides of 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ (A ≤ B ↔ (A + C) ≤ (B + C))
Theorem	leadd2 4315	Addition to both sides of 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ (A ≤ B ↔ (C + A) ≤ (C + B))
Theorem	ltsubadd 4316	'Less than' relationship between subtraction and addition.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A − B) < C ↔ A < (C + B))
Theorem	ltsubadd2 4317	'Less than' relationship between subtraction and addition.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A − B) < C ↔ A < (B + C))
Theorem	lesubadd2 4318	'Less than or equal to' relationship between subtraction and addition.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A − B) ≤ C ↔ A ≤ (B + C))
Theorem	lesubadd 4319	'Less than or equal to' relationship between subtraction and addition.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A − B) ≤ C ↔ A ≤ (C + B))
Theorem	ltaddsub 4320	'Less than' relationship between subtraction and addition.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ ((A + B) < C ↔ A < (C − B))
Theorem	lt2add 4321	Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    &   ⊢ D ∈ ℝ    ⇒   ⊢ ((A < C ∧ B < D) → (A + B) < (C + D))
Theorem	le2add 4322	Adding both side of two inequalities.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    &   ⊢ D ∈ ℝ    ⇒   ⊢ ((A ≤ C ∧ B ≤ D) → (A + B) ≤ (C + D))
Theorem	addgt0 4323	Addition of 2 positive numbers is positive.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 < A ∧ 0 < B) → 0 < (A + B))
Theorem	addge0 4324	Addition of 2 nonnegative numbers is nonnegative.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → 0 ≤ (A + B))
Theorem	addgegt0 4325	Addition of nonnegative and positive numbers is positive.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 < B) → 0 < (A + B))
Theorem	addgt0i 4326	Addition of 2 positive numbers is positive.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 0 < A    &   ⊢ 0 < B    ⇒   ⊢ 0 < (A + B)
Theorem	ltaddpos 4327	Adding a positive number to another number increases it.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (0 < A ↔ B < (B + A))
Theorem	posdif 4328	Comparison of two numbers whose difference is positive.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B ↔ 0 < (B − A))
Theorem	add20 4329	Two nonnegative numbers are zero iff their sum is zero.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → ((A + B) = 0 ↔ (A = 0 ∧ B = 0)))
Theorem	ltneg 4330	Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B ↔ -B < -A)
Theorem	leneg 4331	Negative of both sides of 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A ≤ B ↔ -B ≤ -A)
Theorem	ltnegcon1 4332	Contraposition of negative in 'less than'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (-A < B ↔ -B < A)
Theorem	ltnegcon2 4333	Contraposition of negative in 'less than'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < -B ↔ B < -A)
Theorem	mulgt0 4334	The product of two positive numbers is positive.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 < A ∧ 0 < B) → 0 < (A · B))
Theorem	mulge0 4335	The product of two nonnegative numbers is nonnegative.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → 0 ≤ (A · B))
Theorem	mulgt0i 4336	The product of two positive numbers is positive.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 0 < A    &   ⊢ 0 < B    ⇒   ⊢ 0 < (A · B)
Theorem	ltmullem 4337	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ (0 < C → (A < B → (A · C) < (B · C)))
Theorem	ltnr 4338	'Less than' is irreflexive.
⊢ A ∈ ℝ    ⇒   ⊢ ¬ A < A
Theorem	leid 4339	'Less than or equal to' is reflexive.
⊢ A ∈ ℝ    ⇒   ⊢ A ≤ A
Theorem	gt0ne0 4340	Positive means non-zero (useful for ordering theorems involving division).
⊢ A ∈ ℝ    ⇒   ⊢ (0 < A → A ≠ 0)
Theorem	lesub0 4341	Lemma to show a nonnegative number is zero.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ B ≤ (B − A)) ↔ A = 0)
Theorem	subge0 4342	Nonnegative subtraction.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (0 ≤ (A − B) ↔ B ≤ A)
Theorem	sqgt0 4343	A non-zero square is positive. Theorem I.20 of [Apostol] p. 20.
⊢ A ∈ ℝ    ⇒   ⊢ (¬ A = 0 → 0 < (A · A))
Theorem	sqge0 4344	A square is nonnegative.
⊢ A ∈ ℝ    ⇒   ⊢ 0 ≤ (A · A)
Theorem	gt0ne0i 4345	Positive implies nonzero.
⊢ A ∈ ℝ    &   ⊢ 0 < A    ⇒   ⊢ A ≠ 0
Theorem	gt0ne0t 4346	Positive implies nonzero.
⊢ (A ∈ ℝ → (0 < A → A ≠ 0))
Theorem	letrit 4347	Trichotomy law.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A ≤ B ∨ B ≤ A))
Theorem	ltadd1t 4348	Addition to both sides of 'less than'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → (A < B ↔ (A + C) < (B + C)))
Theorem	ltadd2t 4349	Addition to both sides of 'less than'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → (A < B ↔ (C + A) < (C + B)))
Theorem	leadd1t 4350	Addition to both sides of 'less than or equal to'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → (A ≤ B ↔ (A + C) ≤ (B + C)))
Theorem	leadd2t 4351	Addition to both sides of 'less than or equal to'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → (A ≤ B ↔ (C + A) ≤ (C + B)))
Theorem	lesub1t 4352	Subtraction from both sides of 'less than or equal to'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → (A ≤ B ↔ (A − C) ≤ (B − C)))
Theorem	ltsubaddt 4353	'Less than' relationship between subtraction and addition.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → ((A − B) < C ↔ A < (C + B)))
Theorem	ltsubadd2t 4354	'Less than' relationship between subtraction and addition.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → ((A − B) < C ↔ A < (B + C)))
Theorem	lesubaddt 4355	'Less than or equal to' relationship between subtraction and addition.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → ((A − B) ≤ C ↔ A ≤ (C + B)))
Theorem	lesubadd2t 4356	'Less than or equal to' relationship between subtraction and addition.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → ((A − B) ≤ C ↔ A ≤ (B + C)))
Theorem	ltaddsubt 4357	'Less than' relationship between subtraction and addition.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → ((A + B) < C ↔ A < (C − B)))
Theorem	ltaddsub2t 4358	'Less than' relationship between subtraction and addition.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → ((A + B) < C ↔ B < (C − A)))
Theorem	ltsub23t 4359	'Less than' relationship between subtraction and addition.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → ((A − B) < C ↔ (A − C) < B))
Theorem	ltsub13t 4360	'Less than' relationship between subtraction and addition.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → (A < (B − C) ↔ C < (B − A)))
Theorem	lt2addt 4361	Adding both sides of two 'less than' relations. Theorem I.25 of [Apostol] p. 20.
⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (C ∈ ℝ ∧ D ∈ ℝ)) → ((A < C ∧ B < D) → (A + B) < (C + D)))
Theorem	addge0t 4362	Addition of 2 nonnegative numbers is nonnegative.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((0 ≤ A ∧ 0 ≤ B) → 0 ≤ (A + B)))
Theorem	ltaddpost 4363	Adding a positive number to another number increases it.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (0 < A ↔ B < (B + A)))
Theorem	ltsubpost 4364	Subtracting a positive number from another number decreases it.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (0 < A ↔ (B − A) < B))
Theorem	posdift 4365	Comparison of two numbers whose difference is positive.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A < B ↔ 0 < (B − A)))
Theorem	ltnegt 4366	Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A < B ↔ -B < -A))
Theorem	ltnegcon1t 4367	Contraposition of negative in 'less than'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (-A < B ↔ -B < A))
Theorem	lenegt 4368	Negative of both sides of 'less than or equal to'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A ≤ B ↔ -B ≤ -A))
Theorem	lenegcon1t 4369	Contraposition of negative in 'less than or equal to'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (-A ≤ B ↔ -B ≤ A))
Theorem	lt0neg1t 4370	Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20.
⊢ (A ∈ ℝ → (A < 0 ↔ 0 < -A))
Theorem	lt0neg2t 4371	Comparison of a number and its negative to zero.
⊢ (A ∈ ℝ → (0 < A ↔ -A < 0))
Theorem	le0neg1t 4372	Comparison of a number and its negative to zero.
⊢ (A ∈ ℝ → (A ≤ 0 ↔ 0 ≤ -A))
Theorem	le0neg2t 4373	Comparison of a number and its negative to zero.
⊢ (A ∈ ℝ → (0 ≤ A ↔ -A ≤ 0))
Theorem	lesub0t 4374	Lemma to show a nonnegative number is zero.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((0 ≤ A ∧ B ≤ (B − A)) ↔ A = 0))
Theorem	mulge0t 4375	The product of two nonnegative numbers is nonnegative.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((0 ≤ A ∧ 0 ≤ B) → 0 ≤ (A · B)))
Theorem	ltsqt 4376	A non-zero square is positive. Theorem I.20 of [Apostol] p. 20.
⊢ (A ∈ ℝ → (¬ A = 0 → 0 < (A · A)))
Theorem	lt01 4377	0 is less than 1. Theorem I.21 of [Apostol] p. 20.
⊢ 0 < 1
Theorem	eqneg 4378	A number equal to its negative is zero.
⊢ A ∈ ℂ    ⇒   ⊢ (A = -A ↔ A = 0)
Theorem	negne0 4379	A number is non-zero iff its negative is non-zero.
⊢ A ∈ ℂ    ⇒   ⊢ (A ≠ 0 ↔ -A ≠ 0)
Theorem	negn0 4380	The negative of a non-zero number is non-zero.
⊢ A ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ -A ≠ 0
Theorem	elimgt0 4381	Hypothesis for weak deduction theorem to eliminate 0 < A.
⊢ 0 < if(0 < A, A, 1)
Theorem	elimge0 4382	Hypothesis for weak deduction theorem to eliminate 0 ≤ A.
⊢ 0 ≤ if(0 ≤ A, A, 0)
Theorem	ltplus1t 4383	A number is less than itself plus 1.
⊢ (A ∈ ℝ → A < (A + 1))
Theorem	ltplus1 4384	A number is less than itself plus 1.
⊢ A ∈ ℝ    ⇒   ⊢ A < (A + 1)
Theorem	recgt0i 4385	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21.
⊢ A ∈ ℝ    &   ⊢ 0 < A    ⇒   ⊢ 0 < (1 / A)
Theorem	recgt0 4386	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21.
⊢ A ∈ ℝ    ⇒   ⊢ (0 < A → 0 < (1 / A))
Theorem	prodgt0i 4387	If a number and its product are positive, so is the multiplier.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 0 < A    ⇒   ⊢ (0 < (A · B) → 0 < B)
Theorem	prodgt0 4388	If a number and its product are positive, so is the multiplier.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 < A ∧ 0 < (A · B)) → 0 < B)
Theorem	divgt0lem 4389	The ratio of two positive numbers is positive.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 0 < B    ⇒   ⊢ (0 < A → 0 < (A / B))
Theorem	divgt0 4390	The ratio of two positive numbers is positive.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 < A ∧ 0 < B) → 0 < (A / B))
Theorem	divgt0i 4391	The ratio of two positive numbers is positive.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 0 < A    &   ⊢ 0 < B    ⇒   ⊢ 0 < (A / B)
Theorem	divge0 4392	The ratio of nonnegative and positive numbers is nonnegative.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 < B) → 0 ≤ (A / B))
Theorem	ltmul1i 4393	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    &   ⊢ 0 < C    ⇒   ⊢ (A < B ↔ (A · C) < (B · C))
Theorem	ltmul1 4394	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ (0 < C → (A < B ↔ (A · C) < (B · C)))
Theorem	ltmul2 4395	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ (0 < C → (A < B ↔ (C · A) < (C · B)))
Theorem	lemul2 4396	Multiplication of both sides of 'less than or equal to' by a positive number.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ (0 < C → (A ≤ B ↔ (C · A) ≤ (C · B)))
Theorem	lemul1 4397	Multiplication of both sides of 'less than or equal to' by a positive number.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ (0 < C → (A ≤ B ↔ (A · C) ≤ (B · C)))
Theorem	ltdivi 4398	Division of both sides of 'less than' by a positive number.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    &   ⊢ 0 < C    ⇒   ⊢ (A < B ↔ (A / C) < (B / C))
Theorem	ltdiv 4399	Division of both sides of 'less than' by a positive number.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ (0 < C → (A < B ↔ (A / C) < (B / C)))
Theorem	ltmuldiv 4400	'Less than' relationship between division and multiplication.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ C ∈ ℝ    ⇒   ⊢ (0 < C → ((A · C) < B ↔ A < (B / C)))