P. 424 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42301-42400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ex-decpmul 42301	Example usage of decpmul 42283. This proof is significantly longer than 235t711 42300. There is more unnecessary carrying compared to 235t711 42300. Although saving 5 visual steps, using mulcomli 11190 early on increases the compressed proof length. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (;;235 · ;;711) = ;;;;;167085
Theorem	eluzp1 42302	Membership in a successor upper set of integers. (Contributed by SN, 5-Jul-2025.)
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ↔ (𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)))
Theorem	sn-eluzp1l 42303	Shorter proof of eluzp1l 12827. (Contributed by NM, 12-Sep-2005.) (Revised by SN, 5-Jul-2025.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁)
Theorem	fz1sumconst 42304*	The sum of 𝑁 constant terms (𝑘 is not free in 𝐶). (Contributed by SN, 21-Mar-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (1...𝑁)𝐶 = (𝑁 · 𝐶))
Theorem	fz1sump1 42305*	Add one more term to a sum. Special case of fsump1 15729 generalized to 𝑁 ∈ ℕ0. (Contributed by SN, 22-Mar-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (1...𝑁)𝐴 + 𝐵))
Theorem	oddnumth 42306*	The Odd Number Theorem. The sum of the first 𝑁 odd numbers is 𝑁↑2. A corollary of arisum 15833. (Contributed by SN, 21-Mar-2025.)
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)((2 · 𝑘) − 1) = (𝑁↑2))
Theorem	nicomachus 42307*	Nicomachus's Theorem. The sum of the odd numbers from 𝑁↑2 − 𝑁 + 1 to 𝑁↑2 + 𝑁 − 1 is 𝑁↑3. Proof 2 from https://proofwiki.org/wiki/Nicomachus%27s_Theorem. (Contributed by SN, 21-Mar-2025.)
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)(((𝑁↑2) − 𝑁) + ((2 · 𝑘) − 1)) = (𝑁↑3))
Theorem	sumcubes 42308*	The sum of the first 𝑁 perfect cubes is the sum of the first 𝑁 nonnegative integers, squared. This is the Proof by Nicomachus from https://proofwiki.org/wiki/Sum_of_Sequence_of_Cubes using induction and index shifting to collect all the odd numbers. (Contributed by SN, 22-Mar-2025.)
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)(𝑘↑3) = (Σ𝑘 ∈ (1...𝑁)𝑘↑2))
Theorem	ine1 42309	i is not 1. (Contributed by SN, 25-Apr-2025.)
⊢ i ≠ 1
Theorem	0tie0 42310	0 times i equals 0. (Contributed by SN, 25-Apr-2025.)
⊢ (0 · i) = 0
Theorem	it1ei 42311	i times 1 equals i. (Contributed by SN, 25-Apr-2025.)
⊢ (i · 1) = i
Theorem	1tiei 42312	1 times i equals i. (Contributed by SN, 25-Apr-2025.)
⊢ (1 · i) = i
Theorem	itrere 42313	i times a real is real iff the real is zero. (Contributed by SN, 25-Apr-2025.)
⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0))
Theorem	retire 42314	A real times i is real iff the real is zero. (Contributed by SN, 25-Apr-2025.)
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0))
Theorem	iocioodisjd 42315	Adjacent intervals where the lower interval is right-closed and the upper interval is open are disjoint. (Contributed by SN, 1-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    ⇒   ⊢ (𝜑 → ((𝐴(,]𝐵) ∩ (𝐵(,)𝐶)) = ∅)
Theorem	rpabsid 42316	A positive real is its own absolute value. (Contributed by SN, 1-Oct-2025.)
⊢ (𝑅 ∈ ℝ+ → (abs‘𝑅) = 𝑅)
21.30.3  Exponents and divisibility
Theorem	oexpreposd 42317	Lemma for dffltz 42629. For a more standard version, see expgt0b 32748. TODO-SN?: This can be used to show exp11d 42321 holds for all integers when the exponent is odd. (Contributed by SN, 4-Mar-2023.)
⊢ (𝜑 → 𝑁 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (𝑀 / 2) ∈ ℕ)    ⇒   ⊢ (𝜑 → (0 < 𝑁 ↔ 0 < (𝑁↑𝑀)))
Theorem	explt1d 42318	A nonnegative real number less than one raised to a positive integer is less than one. (Contributed by SN, 3-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 < 1)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) < 1)
Theorem	expeq1d 42319	A nonnegative real number is one if and only if it is one when raised to a positive integer. (Contributed by SN, 3-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑁) = 1 ↔ 𝐴 = 1))
Theorem	expeqidd 42320	A nonnegative real number is zero or one if and only if it is itself when raised to an integer greater than one. (Contributed by SN, 3-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑁) = 𝐴 ↔ (𝐴 = 0 ∨ 𝐴 = 1)))
Theorem	exp11d 42321	exp11nnd 14233 for nonzero integer exponents. (Contributed by SN, 14-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ≠ 0)    &   ⊢ (𝜑 → (𝐴↑𝑁) = (𝐵↑𝑁))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	0dvds0 42322	0 divides 0. (Contributed by SN, 15-Sep-2024.)
⊢ 0 ∥ 0
Theorem	absdvdsabsb 42323	Divisibility is invariant under taking the absolute value on both sides. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁)))
Theorem	gcdnn0id 42324	The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024.)
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 𝑁) = 𝑁)
Theorem	gcdle1d 42325	The greatest common divisor of a positive integer and another integer is less than or equal to the positive integer. (Contributed by SN, 25-Aug-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 gcd 𝑁) ≤ 𝑀)
Theorem	gcdle2d 42326	The greatest common divisor of a positive integer and another integer is less than or equal to the positive integer. (Contributed by SN, 25-Aug-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝑀 gcd 𝑁) ≤ 𝑁)
Theorem	dvdsexpad 42327	Deduction associated with dvdsexpim 16532. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∥ (𝐵↑𝑁))
Theorem	dvdsexpnn 42328	dvdssqlem 16543 generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	dvdsexpnn0 42329	dvdsexpnn 42328 generalized to include zero bases. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	dvdsexpb 42330	dvdssq 16544 generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	posqsqznn 42331	When a positive rational squared is an integer, the rational is a positive integer. zsqrtelqelz 16735 with all terms squared and positive. (Contributed by SN, 23-Aug-2024.)
⊢ (𝜑 → (𝐴↑2) ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℚ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℕ)
Theorem	zdivgd 42332*	Two ways to express "𝑁 is an integer multiple of 𝑀". Originally a subproof of zdiv 12611. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    ⇒   ⊢ (𝜑 → (∃𝑘 ∈ ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))
Theorem	efsubd 42333	Difference of exponents law for exponential function, deduction form. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵)))
Theorem	ef11d 42334*	General condition for the exponential function to be one-to-one. efper 26395 shows that exponentiation is periodic. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((exp‘𝐴) = (exp‘𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + ((i · (2 · π)) · 𝑛))))
Theorem	logccne0d 42335	The logarithm isn't 0 if its argument isn't 0 or 1, deduction form. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐴 ≠ 1)    ⇒   ⊢ (𝜑 → (log‘𝐴) ≠ 0)
Theorem	cxp112d 42336*	General condition for complex exponentiation to be one-to-one with respect to the second argument. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 1)    ⇒   ⊢ (𝜑 → ((𝐶↑𝑐𝐴) = (𝐶↑𝑐𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + (((i · (2 · π)) · 𝑛) / (log‘𝐶)))))
Theorem	cxp111d 42337*	General condition for complex exponentiation to be one-to-one with respect to the first argument. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑐𝐶) = (𝐵↑𝑐𝐶) ↔ ∃𝑛 ∈ ℤ (log‘𝐴) = ((log‘𝐵) + (((i · (2 · π)) · 𝑛) / 𝐶))))
Theorem	cxpi11d 42338*	i to the powers of 𝐴 and 𝐵 are equal iff 𝐴 and 𝐵 are a multiple of 4 apart. EDITORIAL: This theorem may be revised to a more convenient form. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((i↑𝑐𝐴) = (i↑𝑐𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + (4 · 𝑛))))
Theorem	logne0d 42339	Deduction form of logne0 26495. See logccne0d 42335 for a more general version. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ≠ 1)    ⇒   ⊢ (𝜑 → (log‘𝐴) ≠ 0)
Theorem	rxp112d 42340	Real exponentiation is one-to-one with respect to the second argument. (TODO: Note that the base 𝐶 must be positive since -𝐶↑𝐴 is 𝐶↑𝐴 · e↑iπ𝐴, so in the negative case 𝐴 = 𝐵 + 2𝑘). (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 1)    &   ⊢ (𝜑 → (𝐶↑𝑐𝐴) = (𝐶↑𝑐𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	log11d 42341	The natural logarithm is one-to-one. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	rplog11d 42342	The natural logarithm is one-to-one on positive reals. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	rxp11d 42343	Real exponentiation is one-to-one with respect to the first argument. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → (𝐴↑𝑐𝐶) = (𝐵↑𝑐𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
21.30.4  Trigonometry and Calculus
Theorem	tanhalfpim 42344	The tangent of π / 2 minus a number is the cotangent, here represented by cos𝐴 / sin𝐴. (Contributed by SN, 2-Sep-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (sin‘𝐴) ≠ 0)    ⇒   ⊢ (𝜑 → (tan‘((π / 2) − 𝐴)) = ((cos‘𝐴) / (sin‘𝐴)))
Theorem	sinpim 42345	Sine of a number subtracted from π. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → (sin‘(π − 𝐴)) = (sin‘𝐴))
Theorem	cospim 42346	Cosine of a number subtracted from π. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → (cos‘(π − 𝐴)) = -(cos‘𝐴))
Theorem	tan3rdpi 42347	The tangent of π / 3 is √3. (Contributed by SN, 2-Sep-2025.)
⊢ (tan‘(π / 3)) = (√‘3)
Theorem	sin2t3rdpi 42348	The sine of 2 · (π / 3) is (√3) / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (sin‘(2 · (π / 3))) = ((√‘3) / 2)
Theorem	cos2t3rdpi 42349	The cosine of 2 · (π / 3) is -1 / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (cos‘(2 · (π / 3))) = -(1 / 2)
Theorem	sin4t3rdpi 42350	The sine of 4 · (π / 3) is -(√3) / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (sin‘(4 · (π / 3))) = -((√‘3) / 2)
Theorem	cos4t3rdpi 42351	The cosine of 4 · (π / 3) is -1 / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (cos‘(4 · (π / 3))) = -(1 / 2)
Theorem	asin1half 42352	The arcsine of 1 / 2 is π / 6. (Contributed by SN, 31-Aug-2025.)
⊢ (arcsin‘(1 / 2)) = (π / 6)
Theorem	acos1half 42353	The arccosine of 1 / 2 is π / 3. (Contributed by SN, 31-Aug-2024.)
⊢ (arccos‘(1 / 2)) = (π / 3)
Theorem	dvun 42354	Condition for the union of the derivatives of two disjoint functions to be equal to the derivative of the union of the two functions. If 𝐴 and 𝐵 are open sets, this condition (dvun.n) is satisfied by isopn3i 22976. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐺:𝐵⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → (((int‘𝐽)‘𝐴) ∪ ((int‘𝐽)‘𝐵)) = ((int‘𝐽)‘(𝐴 ∪ 𝐵)))    ⇒   ⊢ (𝜑 → ((𝑆 D 𝐹) ∪ (𝑆 D 𝐺)) = (𝑆 D (𝐹 ∪ 𝐺)))
Theorem	redvmptabs 42355*	The derivative of the absolute value, for real numbers. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐷 = (ℝ ∖ {0})    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1))
Theorem	readvrec2 42356*	The antiderivative of 1/x in real numbers, without using the absolute value function. (Contributed by SN, 1-Oct-2025.)
⊢ 𝐷 = (ℝ ∖ {0})    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ ((log‘(𝑥↑2)) / 2))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))
Theorem	readvrec 42357*	For real numbers, the antiderivative of 1/x is ln|x|. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐷 = (ℝ ∖ {0})    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))
Theorem	resuppsinopn 42358	The support of sin (df-supp 8143) restricted to the reals is an open set. (Contributed by SN, 7-Oct-2025.)
⊢ 𝐷 = {𝑦 ∈ ℝ ∣ (sin‘𝑦) ≠ 0}    ⇒   ⊢ 𝐷 ∈ (topGen‘ran (,))
Theorem	readvcot 42359*	Real antiderivative of cotangent. (Contributed by SN, 7-Oct-2025.)
⊢ 𝐷 = {𝑦 ∈ ℝ ∣ (sin‘𝑦) ≠ 0}    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘(sin‘𝑥))))) = (𝑥 ∈ 𝐷 ↦ ((cos‘𝑥) / (sin‘𝑥)))
21.30.5  Independence of ax-mulcom This section mainly concerns the independence of ax-mulcom 11139, which is the only real and complex number axiom whose independence is open ( https://us.metamath.org/mpeuni/mmcomplex.html 11139). In particular, this is a combination of attempts to prove more and more properties of real and complex numbers without ax-mulcom 11139. Completing this direction would show that ax-mulcom 11139 is not independent. Alternatively, one could search for a model satisfying all axioms except ax-mulcom 11139, thus showing it is independent. A few models satisfying non-commutativity which only violate one other axiom are provided at https://gist.github.com/icecream17/933f95d820e0b8f1cab0d4293b68eaf9 11139. I conjecture that if it is possible to prove ax-mulcom 11139 from the other axioms, then all the other axioms are needed. In abstract terms, the symbol ℝ would have to correspond to an infinite non-commutative left-near-field with a Dedekind-complete order compatible with its ring operations. (Note: https://en.wikipedia.org/wiki/Near-field_(mathematics) 11139 does not require commutativity despite having "field" in the name.) Needless to say, this is a very undeveloped area of math. In addition, such a structure for ℝ would have to, together with the structure for the symbol ℂ, satisfy ax-resscn 11132, ax-icn 11134, ax-i2m1 11143, and most crucially ax-cnre 11148. None of the theorems in this section should be moved to main. If there is a naming conflict, feel free to add the prefix "sn-".
Syntax	cresub 42360	Real number subtraction.
class −ℝ
Definition	df-resub 42361*	Define subtraction between real numbers. This operator saves a few axioms over df-sub 11414 in certain situations. Theorem resubval 42362 shows its value, resubadd 42374 relates it to addition, and rersubcl 42373 proves its closure. It is the restriction of df-sub 11414 to the reals: subresre 42426. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥))
Theorem	resubval 42362*	Value of real subtraction, which is the (unique) real 𝑥 such that 𝐵 + 𝑥 = 𝐴. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴))
Theorem	renegeulemv 42363*	Lemma for renegeu 42365 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴)
Theorem	renegeulem 42364*	Lemma for renegeu 42365 and similar. Remove a change in bound variables from renegeulemv 42363. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)    ⇒   ⊢ (𝜑 → ∃!𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)
Theorem	renegeu 42365*	Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Theorem	rernegcl 42366	Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → (0 −ℝ 𝐴) ∈ ℝ)
Theorem	renegadd 42367	Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 −ℝ 𝐴) = 𝐵 ↔ (𝐴 + 𝐵) = 0))
Theorem	renegid 42368	Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → (𝐴 + (0 −ℝ 𝐴)) = 0)
Theorem	reneg0addlid 42369	Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 0) + 𝐴) = 𝐴)
Theorem	resubeulem1 42370	Lemma for resubeu 42372. A value which when added to zero, results in negative zero. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → (0 + (0 −ℝ (0 + 0))) = (0 −ℝ 0))
Theorem	resubeulem2 42371	Lemma for resubeu 42372. A value which when added to 𝐴, results in 𝐵. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + ((0 −ℝ 𝐴) + ((0 −ℝ (0 + 0)) + 𝐵))) = 𝐵)
Theorem	resubeu 42372*	Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 𝐵)
Theorem	rersubcl 42373	Closure for real subtraction. Based on subcl 11427. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) ∈ ℝ)
Theorem	resubadd 42374	Relation between real subtraction and addition. Based on subadd 11431. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴))
Theorem	resubaddd 42375	Relationship between subtraction and addition. Based on subaddd 11558. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴))
Theorem	resubf 42376	Real subtraction is an operation on the real numbers. Based on subf 11430. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ −ℝ :(ℝ × ℝ)⟶ℝ
Theorem	repncan2 42377	Addition and subtraction of equals. Compare pncan2 11435. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐴) = 𝐵)
Theorem	repncan3 42378	Addition and subtraction of equals. Based on pncan3 11436. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (𝐵 −ℝ 𝐴)) = 𝐵)
Theorem	readdsub 42379	Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐶) = ((𝐴 −ℝ 𝐶) + 𝐵))
Theorem	reladdrsub 42380	Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11596 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 −ℝ 𝐴))
Theorem	reltsub1 42381	Subtraction from both sides of 'less than'. Compare ltsub1 11681. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 −ℝ 𝐶) < (𝐵 −ℝ 𝐶)))
Theorem	reltsubadd2 42382	'Less than' relationship between addition and subtraction. Compare ltsubadd2 11656. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶)))
Theorem	resubcan2 42383	Cancellation law for real subtraction. Compare subcan2 11454. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) = (𝐵 −ℝ 𝐶) ↔ 𝐴 = 𝐵))
Theorem	resubsub4 42384	Law for double subtraction. Compare subsub4 11462. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) −ℝ 𝐶) = (𝐴 −ℝ (𝐵 + 𝐶)))
Theorem	rennncan2 42385	Cancellation law for real subtraction. Compare nnncan2 11466. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) −ℝ (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐵))
Theorem	renpncan3 42386	Cancellation law for real subtraction. Compare npncan3 11467. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) + (𝐶 −ℝ 𝐴)) = (𝐶 −ℝ 𝐵))
Theorem	repnpcan 42387	Cancellation law for addition and real subtraction. Compare pnpcan 11468. (Contributed by Steven Nguyen, 19-May-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ (𝐴 + 𝐶)) = (𝐵 −ℝ 𝐶))
Theorem	reppncan 42388	Cancellation law for mixed addition and real subtraction. Compare ppncan 11471. (Contributed by SN, 3-Sep-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) + (𝐵 −ℝ 𝐶)) = (𝐴 + 𝐵))
Theorem	resubidaddlidlem 42389	Lemma for resubidaddlid 42390. A special case of npncan 11450. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 −ℝ 𝐵) = (𝐵 −ℝ 𝐶))    ⇒   ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) + (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐶))
Theorem	resubidaddlid 42390	Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 −ℝ 𝐴) + 𝐵) = 𝐵)
Theorem	resubdi 42391	Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 −ℝ 𝐶)) = ((𝐴 · 𝐵) −ℝ (𝐴 · 𝐶)))
Theorem	re1m1e0m0 42392	Equality of two left-additive identities. See resubidaddlid 42390. Uses ax-i2m1 11143. (Contributed by SN, 25-Dec-2023.)
⊢ (1 −ℝ 1) = (0 −ℝ 0)
Theorem	sn-00idlem1 42393	Lemma for sn-00id 42396. (Contributed by SN, 25-Dec-2023.)
⊢ (𝐴 ∈ ℝ → (𝐴 · (0 −ℝ 0)) = (𝐴 −ℝ 𝐴))
Theorem	sn-00idlem2 42394	Lemma for sn-00id 42396. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) ≠ 0 → (0 −ℝ 0) = 1)
Theorem	sn-00idlem3 42395	Lemma for sn-00id 42396. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) = 1 → (0 + 0) = 0)
Theorem	sn-00id 42396	00id 11356 proven without ax-mulcom 11139 but using ax-1ne0 11144. (Though note that the current version of 00id 11356 can be changed to avoid ax-icn 11134, ax-addcl 11135, ax-mulcl 11137, ax-i2m1 11143, ax-cnre 11148. Most of this is by using 0cnALT3 42248 instead of 0cn 11173). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.)
⊢ (0 + 0) = 0
Theorem	re0m0e0 42397	Real number version of 0m0e0 12308 proven without ax-mulcom 11139. (Contributed by SN, 23-Jan-2024.)
⊢ (0 −ℝ 0) = 0
Theorem	readdlid 42398	Real number version of addlid 11364. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 + 𝐴) = 𝐴)
Theorem	sn-addlid 42399	addlid 11364 without ax-mulcom 11139. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
Theorem	remul02 42400	Real number version of mul02 11359 proven without ax-mulcom 11139. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0)