Metamath Proof Explorer - mmtheorems42

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 - 4101-4200 - Page 42 of 58

Type	Label	Description
Statement
Theorem	1cn 4101	1 is a complex number.
⊢ 1 ∈ ℂ
Theorem	elimne0 4102	Hypothesis for weak deduction theorem to eliminate A ≠ 0.
⊢ if(A ≠ 0, A, 1) ≠ 0
Theorem	adddirt 4103	Distributive law for complex numbers.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) → ((A + B) · C) = ((A · C) + (B · C)))
Theorem	addcl 4104	Closure law for addition.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A + B) ∈ ℂ
Theorem	mulcl 4105	Closure law for multiplication.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A · B) ∈ ℂ
Theorem	addcom 4106	Commutative law for addition.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A + B) = (B + A)
Theorem	mulcom 4107	Commutative law for multiplication.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A · B) = (B · A)
Theorem	addass 4108	Associative law for addition.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((A + B) + C) = (A + (B + C))
Theorem	mulass 4109	Associative law for multiplication.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((A · B) · C) = (A · (B · C))
Theorem	adddi 4110	Distributive law.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ (A · (B + C)) = ((A · B) + (A · C))
Theorem	adddir 4111	Distributive law.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((A + B) · C) = ((A · C) + (B · C))
Theorem	addid1 4112	Identity law for addition.
⊢ A ∈ ℂ    ⇒   ⊢ (A + 0) = A
Theorem	addid2 4113	Identity law for addition.
⊢ A ∈ ℂ    ⇒   ⊢ (0 + A) = A
Theorem	mulid1 4114	Identity law for multiplication.
⊢ A ∈ ℂ    ⇒   ⊢ (A · 1) = A
Theorem	mulid2 4115	Identity law for multiplication.
⊢ A ∈ ℂ    ⇒   ⊢ (1 · A) = A
Theorem	negex 4116	Existence of negatives.
⊢ A ∈ ℂ    ⇒   ⊢ ∃x ∈ ℂ (A + x) = 0
Theorem	recex 4117	Existence of reciprocals.
⊢ A ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ ∃x ∈ ℂ (A · x) = 1
Theorem	readdcl 4118	Closure law for addition of reals.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A + B) ∈ ℝ
Theorem	remulcl 4119	Closure law for multiplication of reals.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A · B) ∈ ℝ
Theorem	addcan 4120	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((A + B) = (A + C) ↔ B = C)
Theorem	addcan2 4121	Cancellation law for addition.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((A + C) = (B + C) ↔ A = B)
Theorem	addcant 4122	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. This proof illustrates how dedth3h 1788 can be used to convert the assumptions of addcan 4120 into antecedents. This general method can be used to convert deductions into theorems as needed.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) → ((A + B) = (A + C) ↔ B = C))
Theorem	addcan2t 4123	Cancellation law for addition.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) → ((A + C) = (B + C) ↔ A = B))
Theorem	negeu 4124	Existential uniqueness of negatives. Theorem I.2 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ∃!x ∈ ℂ (A + x) = B
Theorem	add12t 4125	Commutative/associative law that swaps the first two terms in a triple sum.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) → (A + (B + C)) = (B + (A + C)))
Theorem	add23t 4126	Commutative/associative law that swaps the last two terms in a triple sum.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) → ((A + B) + C) = ((A + C) + B))
Theorem	add4t 4127	Rearrangement of 4 terms in a sum.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ) ∧ (C ∈ ℂ ∧ D ∈ ℂ)) → ((A + B) + (C + D)) = ((A + C) + (B + D)))
Theorem	add12 4128	Commutative/associative law that swaps the first two terms in a triple sum.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ (A + (B + C)) = (B + (A + C))
Theorem	add23 4129	Commutative/associative law that swaps the last two terms in a triple sum.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((A + B) + C) = ((A + C) + B)
Theorem	add4 4130	Rearrangement of 4 terms in a sum.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ D ∈ ℂ    ⇒   ⊢ ((A + B) + (C + D)) = ((A + C) + (B + D))
Theorem	add42 4131	Rearrangement of 4 terms in a sum.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ D ∈ ℂ    ⇒   ⊢ ((A + B) + (C + D)) = ((A + C) + (D + B))
Theorem	addid2t 4132	Identity law for addition.
⊢ (A ∈ ℂ → (0 + A) = A)
Definition	df-sub 4133	Define subtraction. Theorem subval 4134 shows it value (and describes how this definition works), theorem subadd 4143 relates it to addition, and theorems subcl 4139 and resubcl 4174 prove its closure laws.
⊢ − = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℂ) ∧ z = ∪{w ∈ ℂ∣(y + w) = x})}
Theorem	subval 4134	Value of subtraction, which is the (unique) element x such that B + x = A. The notation ∪{x ∈ ℂ∣(B + x) = A} may at first seem cryptic but is actually a way of saying "the element x such that B + x = A" (see Theorem 8.17 of [Quine] p. 56); this works because there is only one such x as shown by negeu 4124, allowing us to exploit eusn 1913 and unisn 1932 (which you will find if you trace back the proof of subcl 4139).
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A − B) = ∪{x ∈ ℂ∣(B + x) = A}
Definition	df-neg 4135	Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction (−) to prevent syntax ambiguity. See cneg 4090 for a discussion of this.
⊢ -A = (0 − A)
Theorem	negeq 4136	Equality theorem for negatives.
⊢ (A = B → -A = -B)
Theorem	negeqi 4137	Equality inference for negatives.
⊢ A = B    ⇒   ⊢ -A = -B
Theorem	negeqd 4138	Equality deduction for negatives.
⊢ (φ → A = B)    ⇒   ⊢ (φ → -A = -B)
Theorem	subcl 4139	Closure law for subtraction.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A − B) ∈ ℂ
Theorem	subclt 4140	Closure law for subtraction.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A − B) ∈ ℂ)
Theorem	negclt 4141	Closure law for negative.
⊢ (A ∈ ℂ → -A ∈ ℂ)
Theorem	negcl 4142	Closure law for negative.
⊢ A ∈ ℂ    ⇒   ⊢ -A ∈ ℂ
Theorem	subadd 4143	Relationship between subtraction and addition.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((A − B) = C ↔ (B + C) = A)
Theorem	subsub 4144	Relationship between subtraction and subtraction.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((A − B) = C ↔ (A − C) = B)
Theorem	subaddt 4145	Relationship between subtraction and addition.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) → ((A − B) = C ↔ (B + C) = A))
Theorem	subaddeq 4146	Subtraction and addition of equals.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A + (B − A)) = B
Theorem	negid 4147	Addition of a number and its negative.
⊢ A ∈ ℂ    ⇒   ⊢ (A + -A) = 0
Theorem	subneg 4148	Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A − B) = (A + -B)
Theorem	subnegt 4149	Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A − B) = (A + -B))
Theorem	addsubasst 4150	Associative-type law for subtraction and addition.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) → ((A + B) − C) = (A + (B − C)))
Theorem	addsubt 4151	Law for subtraction and addition.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) → ((A + B) − C) = ((A − C) + B))
Theorem	addsubass 4152	Associative-type law for subtraction and addition.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((A + B) − C) = (A + (B − C))
Theorem	addsub 4153	Law for subtraction and addition.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((A + B) − C) = ((A − C) + B)
Theorem	negneg 4154	A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18.
⊢ A ∈ ℂ    ⇒   ⊢ --A = A
Theorem	subid 4155	Subtraction of a number from itself.
⊢ A ∈ ℂ    ⇒   ⊢ (A − A) = 0
Theorem	subid1 4156	Identity law for subtraction.
⊢ A ∈ ℂ    ⇒   ⊢ (A − 0) = A
Theorem	negnegt 4157	A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18.
⊢ (A ∈ ℂ → --A = A)
Theorem	subneg2t 4158	Relationship between subtraction and negative.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A − -B) = (A + B))
Theorem	subidt 4159	Subtraction of a number from itself.
⊢ (A ∈ ℂ → (A − A) = 0)
Theorem	subid1t 4160	Identity law for subtraction.
⊢ (A ∈ ℂ → (A − 0) = A)
Theorem	pncant 4161	Cancellation law for subtraction.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A + B) − B) = A)
Theorem	npcant 4162	Cancellation law for subtraction.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A − B) + B) = A)
Theorem	subeq0 4163	If the difference between two numbers is zero, they are equal.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ((A − B) = 0 ↔ A = B)
Theorem	neg11 4164	Negative is one-to-one.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (-A = -B ↔ A = B)
Theorem	negcon1 4165	Negative contraposition law.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (-A = B ↔ -B = A)
Theorem	negcon2 4166	Negative contraposition law.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A = -B ↔ B = -A)
Theorem	negcon1t 4167	Negative contraposition law.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (-A = B ↔ -B = A))
Theorem	negcon2t 4168	Negative contraposition law.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A = -B ↔ B = -A))
Theorem	subeq0t 4169	If the difference between two numbers is zero, they are equal.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A − B) = 0 ↔ A = B))
Theorem	neg0 4170	Minus 0 equals 0.
⊢ -0 = 0
Theorem	renegcl 4171	Closure law for negative of reals.
⊢ A ∈ ℝ    ⇒   ⊢ -A ∈ ℝ
Theorem	renegclt 4172	Closure law for negative of reals.
⊢ (A ∈ ℝ → -A ∈ ℝ)
Theorem	resubclt 4173	Closure law for subtraction of reals.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A − B) ∈ ℝ)
Theorem	resubcl 4174	Closure law for subtraction of reals.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A − B) ∈ ℝ
Theorem	mulid2t 4175	Identity law for multiplication. Note: see ax1id 4077 for commuted version.
⊢ (A ∈ ℂ → (1 · A) = A)
Theorem	mul23t 4176	Commutative/associative law.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) → ((A · B) · C) = ((A · C) · B))
Theorem	mul4t 4177	Rearrangement of 4 factors.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ) ∧ (C ∈ ℂ ∧ D ∈ ℂ)) → ((A · B) · (C · D)) = ((A · C) · (B · D)))
Theorem	mul12 4178	Commutative/associative law that swaps the first two factors in a triple product.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ (A · (B · C)) = (B · (A · C))
Theorem	mul23 4179	Commutative/associative law that swaps the last two factors in a triple product.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((A · B) · C) = ((A · C) · B)
Theorem	mul4 4180	Rearrangement of 4 factors.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ D ∈ ℂ    ⇒   ⊢ ((A · B) · (C · D)) = ((A · C) · (B · D))
Theorem	muladd 4181	Product of sums.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ D ∈ ℂ    ⇒   ⊢ ((A + B) · (C + D)) = (((A · C) + (D · B)) + ((A · D) + (C · B)))
Theorem	subdi 4182	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ (A · (B − C)) = ((A · B) − (A · C))
Theorem	subdir 4183	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ ((A − B) · C) = ((A · C) − (B · C))
Theorem	subdit 4184	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ) → (A · (B − C)) = ((A · B) − (A · C)))
Theorem	mulzer1 4185	Multiplication by 0. Theorem I.6 of [Apostol] p. 18.
⊢ A ∈ ℂ    ⇒   ⊢ (A · 0) = 0
Theorem	mulzer2 4186	Multiplication by 0. Theorem I.6 of [Apostol] p. 18.
⊢ A ∈ ℂ    ⇒   ⊢ (0 · A) = 0
Theorem	1p1times 4187	Two times a number.
⊢ A ∈ ℂ    ⇒   ⊢ ((1 + 1) · A) = (A + A)
Theorem	mulzer1t 4188	Multiplication by 0. Theorem I.6 of [Apostol] p. 18.
⊢ (A ∈ ℂ → (A · 0) = 0)
Theorem	mulzer2t 4189	Multiplication by 0. Theorem I.6 of [Apostol] p. 18.
⊢ (A ∈ ℂ → (0 · A) = 0)
Theorem	mulneg1 4190	Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (-A · B) = -(A · B)
Theorem	mulneg2 4191	Product with negative is negative of product.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (A · -B) = -(A · B)
Theorem	mul2neg 4192	Product of two negatives. Theorem I.12 of [Apostol] p. 18.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (-A · -B) = (A · B)
Theorem	negdi 4193	Distribution of negative over addition.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ -(A + B) = (-A + -B)
Theorem	negdi2 4194	Distribution of negative over subtraction.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ -(A − B) = (-A + B)
Theorem	negdi3 4195	Distribution of negative over subtraction.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ -(A − B) = (B − A)
Theorem	mulneg1t 4196	Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (-A · B) = -(A · B))
Theorem	mulneg2t 4197	The product with a negative is the negative of the product.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A · -B) = -(A · B))
Theorem	mulneg12t 4198	Swap the negative sign in a product.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (-A · B) = (A · -B))
Theorem	mul2negt 4199	Product of two negatives. Theorem I.12 of [Apostol] p. 18.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (-A · -B) = (A · B))
Theorem	negdit 4200	Distribution of negative over addition.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → -(A + B) = (-A + -B))