Metamath Proof Explorer - mmtheorems43

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 - 4201-4300 - Page 43 of 58

Type	Label	Description
Statement
Theorem	negdi2t 4201	Distribution of negative over subtraction.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → -(A − B) = (-A + B))
Theorem	negdi3t 4202	Distribution of negative over subtraction.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → -(A − B) = (B − A))
Theorem	subsubt 4203	Law for double subtraction.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) → (A − (B − C)) = ((A − B) + C))
Theorem	mulm1t 4204	Product with minus one is negative.
⊢ (A ∈ ℂ → (-1 · A) = -A)
Theorem	mulm1 4205	Product with minus one is negative.
⊢ A ∈ ℂ    ⇒   ⊢ (-1 · A) = -A
Theorem	sub4 4206	Rearrangement of 4 terms in a mixed addition and subtraction.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ D ∈ ℂ    ⇒   ⊢ ((A + B) − (C + D)) = ((A − C) + (B − D))
Theorem	mulcan 4207	Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ ((A · B) = (A · C) ↔ B = C)
Theorem	mulcant 4208	Cancellation law for multiplication (theorem form). Theorem I.7 of [Apostol] p. 18. Illustrates use of keephyp 1794.
⊢ A ≠ 0    ⇒   ⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) → ((A · B) = (A · C) ↔ B = C))
Theorem	mulcant2 4209	Cancellation law for multiplication (full theorem form). Theorem I.7 of [Apostol] p. 18. Illustrates use of dedth 1784 and elimne0 4102.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) ∧ A ≠ 0) → ((A · B) = (A · C) ↔ B = C))
Theorem	mul0or 4210	If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ((A · B) = 0 ↔ (A = 0 ∨ B = 0))
Theorem	sq0 4211	A number is zero iff its square is zero.
⊢ A ∈ ℂ    ⇒   ⊢ ((A · A) = 0 ↔ A = 0)
Theorem	mul0ort 4212	If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A · B) = 0 ↔ (A = 0 ∨ B = 0)))
Theorem	muln0bt 4213	The product of two non-zero numbers is non-zero.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A ≠ 0 ∧ B ≠ 0) ↔ (A · B) ≠ 0))
Theorem	muln0 4214	The product of two non-zero numbers is non-zero.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ A ≠ 0    &   ⊢ B ≠ 0    ⇒   ⊢ (A · B) ≠ 0
Theorem	receu 4215	Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ ∃!x ∈ ℂ (A · x) = B
Definition	df-div 4216	Define division. Theorem divmul 4218 relates it to multiplication, and divcl 4221 and redivcl 4274 prove its closure laws.
⊢ / = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ (ℂ ∖ {0})) ∧ z = ∪{w ∈ ℂ∣(y · w) = x})}
Theorem	divval 4217	Value of division: the (unique) element x such that (B · x) = A. This is meaningful only when B is nonzero.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ B ≠ 0    ⇒   ⊢ (A / B) = ∪{x ∈ ℂ∣(B · x) = A}
Theorem	divmul 4218	Relationship between division and multiplication.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ B ≠ 0    ⇒   ⊢ ((A / B) = C ↔ (B · C) = A)
Theorem	divmulz 4219	Relationship between division and multiplication.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ (B ≠ 0 → ((A / B) = C ↔ (B · C) = A))
Theorem	divmult 4220	Relationship between division and multiplication.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) ∧ B ≠ 0) → ((A / B) = C ↔ (B · C) = A))
Theorem	divcl 4221	Closure law for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ B ≠ 0    ⇒   ⊢ (A / B) ∈ ℂ
Theorem	divclz 4222	Closure law for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (B ≠ 0 → (A / B) ∈ ℂ)
Theorem	divclt 4223	Closure law for division.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ) ∧ B ≠ 0) → (A / B) ∈ ℂ)
Theorem	divcan2 4224	A cancellation law for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ (A · (B / A)) = B
Theorem	divcan1 4225	A cancellation law for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ ((B / A) · A) = B
Theorem	divcan1z 4226	A cancellation law for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A ≠ 0 → ((B / A) · A) = B)
Theorem	divcan2z 4227	A cancellation law for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A ≠ 0 → (A · (B / A)) = B)
Theorem	divcan1t 4228	A cancellation law for division.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ) ∧ A ≠ 0) → ((B / A) · A) = B)
Theorem	divcan2t 4229	A cancellation law for division.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ) ∧ A ≠ 0) → (A · (B / A)) = B)
Theorem	divneq0bt 4230	The ratio of non-zero numbers is non-zero.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ) ∧ B ≠ 0) → (A ≠ 0 ↔ (A / B) ≠ 0))
Theorem	divneq0 4231	The ratio of non-zero numbers is non-zero.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ A ≠ 0    &   ⊢ B ≠ 0    ⇒   ⊢ (A / B) ≠ 0
Theorem	recneq0z 4232	The reciprocal of a non-zero number is non-zero.
⊢ A ∈ ℂ    ⇒   ⊢ (A ≠ 0 → (1 / A) ≠ 0)
Theorem	recid 4233	Multiplication of a number and its reciprocal.
⊢ A ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ (A · (1 / A)) = 1
Theorem	recidz 4234	Multiplication of a number and its reciprocal.
⊢ A ∈ ℂ    ⇒   ⊢ (A ≠ 0 → (A · (1 / A)) = 1)
Theorem	recidt 4235	Multiplication of a number and its reciprocal.
⊢ ((A ∈ ℂ ∧ A ≠ 0) → (A · (1 / A)) = 1)
Theorem	divrec 4236	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ B ≠ 0    ⇒   ⊢ (A / B) = (A · (1 / B))
Theorem	divrecz 4237	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (B ≠ 0 → (A / B) = (A · (1 / B)))
Theorem	divrect 4238	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ) ∧ B ≠ 0) → (A / B) = (A · (1 / B)))
Theorem	divasst 4239	An associative law for division.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) ∧ C ≠ 0) → ((A · B) / C) = (A · (B / C)))
Theorem	div23t 4240	An associative/distributive law for division.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) ∧ C ≠ 0) → ((A · B) / C) = ((A / C) · B))
Theorem	divassz 4241	An associative law for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ (C ≠ 0 → ((A · B) / C) = (A · (B / C)))
Theorem	divass 4242	An associative law for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ C ≠ 0    ⇒   ⊢ ((A · B) / C) = (A · (B / C))
Theorem	divdistr 4243	Distribution of division over addition.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ C ≠ 0    ⇒   ⊢ ((A + B) / C) = ((A / C) + (B / C))
Theorem	div23 4244	An associative/distributive law for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ C ≠ 0    ⇒   ⊢ ((A · B) / C) = ((A / C) · B)
Theorem	divdistrz 4245	Distribution of division over addition.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ (C ≠ 0 → ((A + B) / C) = ((A / C) + (B / C)))
Theorem	divdistrt 4246	Distribution of division over addition.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) ∧ C ≠ 0) → ((A + B) / C) = ((A / C) + (B / C)))
Theorem	divcan3 4247	A cancellation law for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ ((A · B) / A) = B
Theorem	divcan4 4248	A cancellation law for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ ((B · A) / A) = B
Theorem	divcan3z 4249	A cancellation law for division. (Eliminates a hypothesis of divcan3 4247 with the weak deduction theorem.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A ≠ 0 → ((A · B) / A) = B)
Theorem	divcan4z 4250	A cancellation law for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A ≠ 0 → ((B · A) / A) = B)
Theorem	divcan3t 4251	A cancellation law for division.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ) ∧ A ≠ 0) → ((A · B) / A) = B)
Theorem	div11 4252	One-to-one relationship for division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ C ≠ 0    ⇒   ⊢ ((A / C) = (B / C) ↔ A = B)
Theorem	recrec 4253	A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ (1 / (1 / A)) = A
Theorem	divid 4254	A number divided by itself is one.
⊢ A ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ (A / A) = 1
Theorem	divzer 4255	Division into zero is zero.
⊢ A ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ (0 / A) = 0
Theorem	dividt 4256	A number divided by itself is one.
⊢ ((A ∈ ℂ ∧ A ≠ 0) → (A / A) = 1)
Theorem	div1 4257	A number divided by 1 is itself.
⊢ A ∈ ℂ    ⇒   ⊢ (A / 1) = A
Theorem	div1t 4258	A number divided by 1 is itself.
⊢ (A ∈ ℂ → (A / 1) = A)
Theorem	divnegt 4259	Move negative sign inside of a division.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ) ∧ B ≠ 0) → -(A / B) = (-A / B))
Theorem	recrect 4260	A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18.
⊢ ((A ∈ ℂ ∧ A ≠ 0) → (1 / (1 / A)) = A)
Theorem	rec11i 4261	Reciprocal is one-to-one.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ A ≠ 0    &   ⊢ B ≠ 0    ⇒   ⊢ ((1 / A) = (1 / B) ↔ A = B)
Theorem	rec11 4262	Reciprocal is one-to-one.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ((A ≠ 0 ∧ B ≠ 0) → ((1 / A) = (1 / B) ↔ A = B))
Theorem	divmuldivt 4263	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18.
⊢ ((((A ∈ ℂ ∧ B ∈ ℂ) ∧ (C ∈ ℂ ∧ D ∈ ℂ)) ∧ (B ≠ 0 ∧ D ≠ 0)) → ((A / B) · (C / D)) = ((A · C) / (B · D)))
Theorem	divadddivt 4264	Addition of two ratios. Theorem I.13 of [Apostol] p. 18.
⊢ ((((A ∈ ℂ ∧ B ∈ ℂ) ∧ (C ∈ ℂ ∧ D ∈ ℂ)) ∧ (B ≠ 0 ∧ D ≠ 0)) → ((A / B) + (C / D)) = (((A · D) + (B · C)) / (B · D)))
Theorem	divdivdivt 4265	Division of two ratios. Theorem I.15 of [Apostol] p. 18.
⊢ ((((A ∈ ℂ ∧ B ∈ ℂ) ∧ (C ∈ ℂ ∧ D ∈ ℂ)) ∧ (B ≠ 0 ∧ C ≠ 0 ∧ D ≠ 0)) → ((A / B) / (C / D)) = ((A · D) / (B · C)))
Theorem	divmuldiv 4266	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ D ∈ ℂ    &   ⊢ B ≠ 0    &   ⊢ D ≠ 0    ⇒   ⊢ ((A / B) · (C / D)) = ((A · C) / (B · D))
Theorem	divmul13 4267	Swap denominators of two ratios.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ D ∈ ℂ    &   ⊢ B ≠ 0    &   ⊢ D ≠ 0    ⇒   ⊢ ((A / B) · (C / D)) = ((C / B) · (A / D))
Theorem	divadddiv 4268	Addition of two ratios. Theorem I.13 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ D ∈ ℂ    &   ⊢ B ≠ 0    &   ⊢ D ≠ 0    ⇒   ⊢ ((A / B) + (C / D)) = (((A · D) + (B · C)) / (B · D))
Theorem	divdivdiv 4269	Division of two ratios. Theorem I.15 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ D ∈ ℂ    &   ⊢ B ≠ 0    &   ⊢ D ≠ 0    &   ⊢ C ≠ 0    ⇒   ⊢ ((A / B) / (C / D)) = ((A · D) / (B · C))
Theorem	recdivt 4270	The reciprocal of a ratio.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ) ∧ (A ≠ 0 ∧ B ≠ 0)) → (1 / (A / B)) = (B / A))
Theorem	divdiv23t 4271	Swap denominators in a division.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) ∧ (B ≠ 0 ∧ C ≠ 0)) → ((A / B) / C) = ((A / C) / B))
Theorem	divdiv23 4272	Swap denominators in a division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ B ≠ 0    &   ⊢ C ≠ 0    ⇒   ⊢ ((A / B) / C) = ((A / C) / B)
Theorem	divdiv23z 4273	Swap denominators in a division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((B ≠ 0 ∧ C ≠ 0) → ((A / B) / C) = ((A / C) / B))
Theorem	redivcl 4274	Closure law for division of reals.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ B ≠ 0    ⇒   ⊢ (A / B) ∈ ℝ
Theorem	redivclz 4275	Closure law for division of reals.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (B ≠ 0 → (A / B) ∈ ℝ)
Theorem	redivclt 4276	Closure law for division of reals.
⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ B ≠ 0) → (A / B) ∈ ℝ)
Definition	df-le 4277	Define 'less than or equal to' on real subset of complex numbers. Theorem leloet 4284 relates it to 'less than'.
⊢ ≤ = ((ℝ × ℝ) ∖ ◡ < )
Theorem	leltt 4278	'Less than or equal to' expressed in terms of 'less than'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A ≤ B ↔ ¬ B < A))
Theorem	ltso 4279	'Less than' is a strict ordering. Note: do not shorten this with ltsor 4055, and do not use ltsor 4055 in complex number proofs, in order to maintain a "clean" derivation of all complex number proofs directly from postulates.
⊢ < Or ℝ
Theorem	lttri2t 4280	Consequence of trichotomy.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (¬ A = B ↔ (A < B ∨ B < A)))
Theorem	lttri3t 4281	Trichotomy law for 'less than'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A = B ↔ (¬ A < B ∧ ¬ B < A)))
Theorem	ltnet 4282	'Less than' implies not equal.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A < B → ¬ A = B))
Theorem	letri3t 4283	Trichotomy law.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A = B ↔ (A ≤ B ∧ B ≤ A)))
Theorem	leloet 4284	'Less than or equal to' expressed in terms of 'less than' or 'equals'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A ≤ B ↔ (A < B ∨ A = B)))
Theorem	lenltt 4285	Equality in terms of 'less than or equal to', 'less than'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A = B ↔ (A ≤ B ∧ ¬ A < B)))
Theorem	ltlet 4286	'Less than' implies 'less than or equal to'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A < B → A ≤ B))
Theorem	leltnet 4287	'Less than or equal to' implies 'less than' is not 'equals'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A ≤ B → (A < B ↔ ¬ A = B)))
Theorem	ltlent 4288	'Less than' expressed in terms of 'less than or equal to'.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A < B ↔ (A ≤ B ∧ ¬ A = B)))
Theorem	lelttrt 4289	Transitive law.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → ((A ≤ B ∧ B < C) → A < C))
Theorem	ltletrt 4290	Transitive law.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → ((A < B ∧ B ≤ C) → A < C))
Theorem	letrt 4291	Transitive law.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ) → ((A ≤ B ∧ B ≤ C) → A ≤ C))
Theorem	ltnrt 4292	'Less than' is irreflexive.
⊢ (A ∈ ℝ → ¬ A < A)
Theorem	leidt 4293	'Less than or equal to' is reflexive.
⊢ (A ∈ ℝ → A ≤ A)
Theorem	ltnsymt 4294	'Less than' is not symmetric.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A < B → ¬ B < A))
Theorem	lttri2 4295	Consequence of trichotomy.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (¬ A = B ↔ (A < B ∨ B < A))
Theorem	lttri3 4296	Consequence of trichotomy.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A = B ↔ (¬ A < B ∧ ¬ B < A))
Theorem	letri3 4297	Consequence of trichotomy.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A = B ↔ (A ≤ B ∧ B ≤ A))
Theorem	leloe 4298	'Less than or equal to' in terms of 'less than'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A ≤ B ↔ (A < B ∨ A = B))
Theorem	ltlen 4299	'Less than' expressed in terms of 'less than or equal to'.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B ↔ (A ≤ B ∧ ¬ A = B))
Theorem	ltnsym 4300	'Less than' is not symmetric.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B → ¬ B < A)