P. 436 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43501-43600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	readdridaddlidd 43501	Given some real number 𝐵 where 𝐴 acts like a right additive identity, derive that 𝐴 is a left additive identity. Note that the hypothesis is weaker than proving that 𝐴 is a right additive identity (for all numbers). Although, if there is a right additive identity, then by readdcan 11511, 𝐴 is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐵 + 𝐴) = 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) = 𝐶)
Theorem	4p4e8ALT 43502	A shorter proof of 4p4e8 12524 if 6p2e8 12528 was moved up. The most clean way to do this would be to start with 7p2e9 12530, then go 6p2e8 12528, 6p3e9 12529, etc., which is still inelegant. The idea here is that using 4 = 2 + 2 and 2cn 12445 is shorter than using 4 = 3 + 1, 3cn 12451, and ax-1cn 11285. This also works with 5p4e9 12527. (Contributed by SN, 24-Aug-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (4 + 4) = 8
Theorem	1p3e4 43503	1 + 3 = 4. (Contributed by SN, 19-Nov-2025.)
⊢ (1 + 3) = 4
Theorem	1p4e5 43504	1 + 4 = 5. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 4) = 5
Theorem	1p5e6 43505	1 + 5 = 6. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 5) = 6
Theorem	1p6e7 43506	1 + 6 = 7. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 6) = 7
Theorem	1p7e8 43507	1 + 7 = 8. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 7) = 8
Theorem	1p8e9 43508	1 + 8 = 9. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 8) = 9
Theorem	2p3e5 43509	2 + 3 = 5. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 3) = 5
Theorem	2p4e6 43510	2 + 4 = 6. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 4) = 6
Theorem	2p5e7 43511	2 + 5 = 7. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 5) = 7
Theorem	2p6e8 43512	2 + 6 = 8. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 6) = 8
Theorem	2p7e9 43513	2 + 7 = 9. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 7) = 9
Theorem	3p4e7 43514	3 + 4 = 7. (Contributed by SN, 24-Aug-2026.)
⊢ (3 + 4) = 7
Theorem	3p5e8 43515	3 + 5 = 8. (Contributed by SN, 24-Aug-2026.)
⊢ (3 + 5) = 8
Theorem	3p6e9 43516	3 + 6 = 9. (Contributed by SN, 24-Aug-2026.)
⊢ (3 + 6) = 9
Theorem	4p5e9 43517	4 + 5 = 9. (Contributed by SN, 24-Aug-2026.)
⊢ (4 + 5) = 9
Theorem	5ne0 43518	The number 5 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 5 ≠ 0
Theorem	6ne0 43519	The number 6 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 6 ≠ 0
Theorem	7ne0 43520	The number 7 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 7 ≠ 0
Theorem	8ne0 43521	The number 8 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 8 ≠ 0
Theorem	9ne0 43522	The number 9 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 9 ≠ 0
Theorem	sn-1ne2 43523	A proof of 1ne2 12580 without using ax-mulcom 11291, ax-mulass 11293, ax-pre-mulgt0 11304. Based on mul02lem2 11514. (Contributed by SN, 13-Dec-2023.)
⊢ 1 ≠ 2
Theorem	nnn1suc 43524*	A positive integer that is not 1 is a successor of some other positive integer. (Contributed by Steven Nguyen, 19-Aug-2023.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ≠ 1) → ∃𝑥 ∈ ℕ (𝑥 + 1) = 𝐴)
Theorem	readdrcl2d 43525	Reverse closure for addition: the second addend is real if the first addend is real and the sum is real. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐵 ∈ ℝ)
Theorem	raddswap12d 43526	Swap the first two variables in an equation with addition on the right, converting it into a subtraction. Version of mvrraddd 11754 with a commuted consequent, and of mvlraddd 11751 with a commuted hypothesis. EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶))    ⇒   ⊢ (𝜑 → 𝐵 = (𝐴 − 𝐶))
Theorem	lsubrotld 43527	Rotate the variables left in an equation with subtraction on the left, converting it into an addition. EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐶) = 𝐴)
Theorem	rsubrotld 43528	Rotate the variables left in an equation with subtraction on the right, converting it into an addition. EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 4-Jul-2025.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 + 𝐴))
Theorem	lsubswap23d 43529	Swap the second and third variables in an equation with subtraction on the left, converting it into an addition. EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 23-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐶) = 𝐵)
Theorem	addsubeq4com 43530	Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵)))
Theorem	sqsumi 43531	A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵)))
Theorem	negn0nposznnd 43532	Lemma for dffltz 43863. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → ¬ 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℕ)
Theorem	sqmid3api 43533	Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝑁 ∈ ℂ    &   ⊢ (𝐴 + 𝑁) = 𝐵    &   ⊢ (𝐵 + 𝑁) = 𝐶    ⇒   ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁))
Theorem	decaddcom 43534	Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵)
Theorem	sqn5i 43535	The square of a number ending in 5. This shortcut only works because 5 is half of 10. (Contributed by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (;𝐴5 · ;𝐴5) = ;;(𝐴 · (𝐴 + 1))25
Theorem	sqn5ii 43536	The square of a number ending in 5. This shortcut only works because 5 is half of 10. (Contributed by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ (𝐴 + 1) = 𝐵    &   ⊢ (𝐴 · 𝐵) = 𝐶    ⇒   ⊢ (;𝐴5 · ;𝐴5) = ;;𝐶25
Theorem	decpmulnc 43537	Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11794. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐸    &   ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹    &   ⊢ (𝐵 · 𝐷) = 𝐺    ⇒   ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐸𝐹𝐺
Theorem	decpmul 43538	Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐸    &   ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹    &   ⊢ (𝐵 · 𝐷) = ;𝐺𝐻    &   ⊢ (;𝐸𝐺 + 𝐹) = 𝐼    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;𝐼𝐻
Theorem	sqdeccom12 43539	The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
Theorem	sq3deccom12 43540	Variant of sqdeccom12 43539 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ (𝐴 + 𝐶) = 𝐷    ⇒   ⊢ ((;;𝐴𝐵𝐶 · ;;𝐴𝐵𝐶) − (;𝐷𝐵 · ;𝐷𝐵)) = (;99 · ((;𝐴𝐵 · ;𝐴𝐵) − (𝐶 · 𝐶)))
Theorem	4t5e20 43541	4 times 5 equals 20. (Contributed by SN, 30-Mar-2025.)
⊢ (4 · 5) = ;20
Theorem	3rdpwhole 43542	A third of a number plus the number is four thirds of the number. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → ((𝐴 / 3) + 𝐴) = (4 · (𝐴 / 3)))
Theorem	sq4 43543	The square of 4 is 16. (Contributed by SN, 26-Aug-2025.)
⊢ (4↑2) = ;16
Theorem	sq5 43544	The square of 5 is 25. (Contributed by SN, 26-Aug-2025.)
⊢ (5↑2) = ;25
Theorem	sq6 43545	The square of 6 is 36. (Contributed by SN, 26-Aug-2025.)
⊢ (6↑2) = ;36
Theorem	sq7 43546	The square of 7 is 49. (Contributed by SN, 26-Aug-2025.)
⊢ (7↑2) = ;49
Theorem	sq8 43547	The square of 8 is 64. (Contributed by SN, 26-Aug-2025.)
⊢ (8↑2) = ;64
Theorem	sq9 43548	The square of 9 is 81. (Contributed by SN, 30-Mar-2025.)
⊢ (9↑2) = ;81
Theorem	rpsscn 43549	The positive reals are a subset of the complex numbers. (Contributed by SN, 1-Oct-2025.)
⊢ ℝ+ ⊆ ℂ
Theorem	4rp 43550	4 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 4 ∈ ℝ+
Theorem	6rp 43551	6 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 6 ∈ ℝ+
Theorem	7rp 43552	7 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 7 ∈ ℝ+
Theorem	8rp 43553	8 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 8 ∈ ℝ+
Theorem	9rp 43554	9 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 9 ∈ ℝ+
Theorem	235t711 43555	Calculate a product by long multiplication as a base comparison with other multiplication algorithms. Conveniently, 711 has two ones which greatly simplifies calculations like 235 · 1. There isn't a higher level mulcomli 11345 saving the lower level uses of mulcomli 11345 within 235 · 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12955 are added then this proof would benefit more than ex-decpmul 43556. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 12504 or 8t7e56 12966. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.)
⊢ (;;235 · ;;711) = ;;;;;167085
Theorem	ex-decpmul 43556	Example usage of decpmul 43538. This proof is significantly longer than 235t711 43555. There is more unnecessary carrying compared to 235t711 43555. Although saving 5 visual steps, using mulcomli 11345 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 43557	Membership in a successor upper set of integers. (Contributed by SN, 5-Jul-2025.)
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ↔ (𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)))
Theorem	sn-eluzp1l 43558	Shorter proof of eluzp1l 13019. (Contributed by NM, 12-Sep-2005.) (Revised by SN, 5-Jul-2025.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁)
Theorem	fz1sumconst 43559*	The sum of 𝑁 constant terms (𝑘 is not free in 𝐶). (Contributed by SN, 21-Mar-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (1...𝑁)𝐶 = (𝑁 · 𝐶))
Theorem	fz1sump1 43560*	Add one more term to a sum. Special case of fsump1 15951 generalized to 𝑁 ∈ ℕ0. (Contributed by SN, 22-Mar-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (1...𝑁)𝐴 + 𝐵))
Theorem	oddnumth 43561*	The Odd Number Theorem. The sum of the first 𝑁 odd numbers is 𝑁↑2. A corollary of arisum 16058. (Contributed by SN, 21-Mar-2025.)
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)((2 · 𝑘) − 1) = (𝑁↑2))
Theorem	nicomachus 43562*	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 43563*	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 43564	i is not 1. (Contributed by SN, 25-Apr-2025.)
⊢ i ≠ 1
Theorem	0tie0 43565	0 times i equals 0. (Contributed by SN, 25-Apr-2025.)
⊢ (0 · i) = 0
Theorem	it1ei 43566	i times 1 equals i. (Contributed by SN, 25-Apr-2025.)
⊢ (i · 1) = i
Theorem	1tiei 43567	1 times i equals i. (Contributed by SN, 25-Apr-2025.)
⊢ (1 · i) = i
Theorem	itrere 43568	i times a real is real iff the real is zero. (Contributed by SN, 25-Apr-2025.)
⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0))
Theorem	retire 43569	A real times i is real iff the real is zero. (Contributed by SN, 25-Apr-2025.)
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0))
Theorem	iocioodisjd 43570	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 43571	A positive real is its own absolute value. (Contributed by SN, 1-Oct-2025.)
⊢ (𝑅 ∈ ℝ+ → (abs‘𝑅) = 𝑅)
21.33.3  Exponents and divisibility
Theorem	oexpreposd 43572	Lemma for dffltz 43863. For a more standard version, see expgt0b 33478. TODO-SN?: This can be used to show exp11d 43576 holds for all integers when the exponent is odd. (Contributed by SN, 4-Mar-2023.)
⊢ (𝜑 → 𝑁 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (𝑀 / 2) ∈ ℕ)    ⇒   ⊢ (𝜑 → (0 < 𝑁 ↔ 0 < (𝑁↑𝑀)))
Theorem	explt1d 43573	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 43574	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 43575	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 43576	exp11nnd 14432 for nonzero integer exponents. (Contributed by SN, 14-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ≠ 0)    &   ⊢ (𝜑 → (𝐴↑𝑁) = (𝐵↑𝑁))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	0dvds0 43577	0 divides 0. (Contributed by SN, 15-Sep-2024.)
⊢ 0 ∥ 0
Theorem	absdvdsabsb 43578	Divisibility is invariant under taking the absolute value on both sides. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁)))
Theorem	dvdsexpnn0 43579	dvdsexpnn 16769 generalized to include zero bases. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	dvdsexpb 43580	dvdssq 16771 generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	zdivgd 43581*	Two ways to express "𝑁 is an integer multiple of 𝑀". Originally a subproof of zdiv 12796. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    ⇒   ⊢ (𝜑 → (∃𝑘 ∈ ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))
Theorem	efsubd 43582	Difference of exponents law for exponential function, deduction form. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵)))
Theorem	ef11d 43583*	General condition for the exponential function to be one-to-one. efper 26838 shows that exponentiation is periodic. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((exp‘𝐴) = (exp‘𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + ((i · (2 · π)) · 𝑛))))
Theorem	logccne0d 43584	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 43585*	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 43586*	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 43587*	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 43588	Deduction form of logne0 26937. See logccne0d 43584 for a more general version. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ≠ 1)    ⇒   ⊢ (𝜑 → (log‘𝐴) ≠ 0)
Theorem	rxp112d 43589	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 43590	The natural logarithm is one-to-one. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	rplog11d 43591	The natural logarithm is one-to-one on positive reals. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	rxp11d 43592	Real exponentiation is one-to-one with respect to the first argument. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → (𝐴↑𝑐𝐶) = (𝐵↑𝑐𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
21.33.4  Trigonometry and Calculus
Theorem	tanhalfpim 43593	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 43594	Sine of a number subtracted from π. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → (sin‘(π − 𝐴)) = (sin‘𝐴))
Theorem	cospim 43595	Cosine of a number subtracted from π. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → (cos‘(π − 𝐴)) = -(cos‘𝐴))
Theorem	tan3rdpi 43596	The tangent of π / 3 is √3. (Contributed by SN, 2-Sep-2025.)
⊢ (tan‘(π / 3)) = (√‘3)
Theorem	sin2t3rdpi 43597	The sine of 2 · (π / 3) is (√3) / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (sin‘(2 · (π / 3))) = ((√‘3) / 2)
Theorem	cos2t3rdpi 43598	The cosine of 2 · (π / 3) is -1 / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (cos‘(2 · (π / 3))) = -(1 / 2)
Theorem	sin4t3rdpi 43599	The sine of 4 · (π / 3) is -(√3) / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (sin‘(4 · (π / 3))) = -((√‘3) / 2)
Theorem	cos4t3rdpi 43600	The cosine of 4 · (π / 3) is -1 / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (cos‘(4 · (π / 3))) = -(1 / 2)