P. 431 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43001-43100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lttrii 43001	'Less than' is transitive. (Contributed by SN, 26-Aug-2025.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ 𝐴 < 𝐶
Theorem	remulcan2d 43002	mulcan2d 11849 for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵))
Theorem	readdridaddlidd 43003	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 11385, 𝐴 is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐵 + 𝐴) = 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) = 𝐶)
Theorem	1p3e4 43004	1 + 3 = 4. (Contributed by SN, 19-Nov-2025.)
⊢ (1 + 3) = 4
Theorem	5ne0 43005	The number 5 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 5 ≠ 0
Theorem	6ne0 43006	The number 6 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 6 ≠ 0
Theorem	7ne0 43007	The number 7 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 7 ≠ 0
Theorem	8ne0 43008	The number 8 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 8 ≠ 0
Theorem	9ne0 43009	The number 9 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 9 ≠ 0
Theorem	sn-1ne2 43010	A proof of 1ne2 12452 without using ax-mulcom 11165, ax-mulass 11167, ax-pre-mulgt0 11178. Based on mul02lem2 11388. (Contributed by SN, 13-Dec-2023.)
⊢ 1 ≠ 2
Theorem	nnn1suc 43011*	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 43012	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	mvrrsubd 43013	Move a subtraction in the RHS to a right-addition in the LHS. Converse of mvlraddd 11625. EDITORIAL: Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → (𝐴 + 𝐶) = 𝐵)
Theorem	laddrotrd 43014	Rotate the variables right in an equation with addition on the left, converting it into a subtraction. Version of mvlladdd 11626 with a commuted consequent, and of mvrladdd 11628 with a commuted hypothesis. EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: ply1dg3rt0irred 33852. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐶 − 𝐴) = 𝐵)
Theorem	raddswap12d 43015	Swap the first two variables in an equation with addition on the right, converting it into a subtraction. Version of mvrraddd 11627 with a commuted consequent, and of mvlraddd 11625 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 43016	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 43017	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 43018	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 43019	Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵)))
Theorem	sqsumi 43020	A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵)))
Theorem	negn0nposznnd 43021	Lemma for dffltz 43346. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → ¬ 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℕ)
Theorem	sqmid3api 43022	Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝑁 ∈ ℂ    &   ⊢ (𝐴 + 𝑁) = 𝐵    &   ⊢ (𝐵 + 𝑁) = 𝐶    ⇒   ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁))
Theorem	decaddcom 43023	Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵)
Theorem	sqn5i 43024	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 43025	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 43026	Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11666. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐸    &   ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹    &   ⊢ (𝐵 · 𝐷) = 𝐺    ⇒   ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐸𝐹𝐺
Theorem	decpmul 43027	Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐸    &   ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹    &   ⊢ (𝐵 · 𝐷) = ;𝐺𝐻    &   ⊢ (;𝐸𝐺 + 𝐹) = 𝐼    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;𝐼𝐻
Theorem	sqdeccom12 43028	The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
Theorem	sq3deccom12 43029	Variant of sqdeccom12 43028 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ (𝐴 + 𝐶) = 𝐷    ⇒   ⊢ ((;;𝐴𝐵𝐶 · ;;𝐴𝐵𝐶) − (;𝐷𝐵 · ;𝐷𝐵)) = (;99 · ((;𝐴𝐵 · ;𝐴𝐵) − (𝐶 · 𝐶)))
Theorem	4t5e20 43030	4 times 5 equals 20. (Contributed by SN, 30-Mar-2025.)
⊢ (4 · 5) = ;20
Theorem	3rdpwhole 43031	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 43032	The square of 4 is 16. (Contributed by SN, 26-Aug-2025.)
⊢ (4↑2) = ;16
Theorem	sq5 43033	The square of 5 is 25. (Contributed by SN, 26-Aug-2025.)
⊢ (5↑2) = ;25
Theorem	sq6 43034	The square of 6 is 36. (Contributed by SN, 26-Aug-2025.)
⊢ (6↑2) = ;36
Theorem	sq7 43035	The square of 7 is 49. (Contributed by SN, 26-Aug-2025.)
⊢ (7↑2) = ;49
Theorem	sq8 43036	The square of 8 is 64. (Contributed by SN, 26-Aug-2025.)
⊢ (8↑2) = ;64
Theorem	sq9 43037	The square of 9 is 81. (Contributed by SN, 30-Mar-2025.)
⊢ (9↑2) = ;81
Theorem	rpsscn 43038	The positive reals are a subset of the complex numbers. (Contributed by SN, 1-Oct-2025.)
⊢ ℝ+ ⊆ ℂ
Theorem	4rp 43039	4 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 4 ∈ ℝ+
Theorem	6rp 43040	6 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 6 ∈ ℝ+
Theorem	7rp 43041	7 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 7 ∈ ℝ+
Theorem	8rp 43042	8 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 8 ∈ ℝ+
Theorem	9rp 43043	9 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 9 ∈ ℝ+
Theorem	235t711 43044	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 11219 saving the lower level uses of mulcomli 11219 within 235 · 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12826 are added then this proof would benefit more than ex-decpmul 43045. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 12376 or 8t7e56 12837. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.)
⊢ (;;235 · ;;711) = ;;;;;167085
Theorem	ex-decpmul 43045	Example usage of decpmul 43027. This proof is significantly longer than 235t711 43044. There is more unnecessary carrying compared to 235t711 43044. Although saving 5 visual steps, using mulcomli 11219 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 43046	Membership in a successor upper set of integers. (Contributed by SN, 5-Jul-2025.)
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ↔ (𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)))
Theorem	sn-eluzp1l 43047	Shorter proof of eluzp1l 12890. (Contributed by NM, 12-Sep-2005.) (Revised by SN, 5-Jul-2025.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁)
Theorem	fz1sumconst 43048*	The sum of 𝑁 constant terms (𝑘 is not free in 𝐶). (Contributed by SN, 21-Mar-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (1...𝑁)𝐶 = (𝑁 · 𝐶))
Theorem	fz1sump1 43049*	Add one more term to a sum. Special case of fsump1 15809 generalized to 𝑁 ∈ ℕ0. (Contributed by SN, 22-Mar-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (1...𝑁)𝐴 + 𝐵))
Theorem	oddnumth 43050*	The Odd Number Theorem. The sum of the first 𝑁 odd numbers is 𝑁↑2. A corollary of arisum 15916. (Contributed by SN, 21-Mar-2025.)
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)((2 · 𝑘) − 1) = (𝑁↑2))
Theorem	nicomachus 43051*	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 43052*	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 43053	i is not 1. (Contributed by SN, 25-Apr-2025.)
⊢ i ≠ 1
Theorem	0tie0 43054	0 times i equals 0. (Contributed by SN, 25-Apr-2025.)
⊢ (0 · i) = 0
Theorem	it1ei 43055	i times 1 equals i. (Contributed by SN, 25-Apr-2025.)
⊢ (i · 1) = i
Theorem	1tiei 43056	1 times i equals i. (Contributed by SN, 25-Apr-2025.)
⊢ (1 · i) = i
Theorem	itrere 43057	i times a real is real iff the real is zero. (Contributed by SN, 25-Apr-2025.)
⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0))
Theorem	retire 43058	A real times i is real iff the real is zero. (Contributed by SN, 25-Apr-2025.)
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0))
Theorem	iocioodisjd 43059	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 43060	A positive real is its own absolute value. (Contributed by SN, 1-Oct-2025.)
⊢ (𝑅 ∈ ℝ+ → (abs‘𝑅) = 𝑅)
21.31.3  Exponents and divisibility
Theorem	oexpreposd 43061	Lemma for dffltz 43346. For a more standard version, see expgt0b 33139. TODO-SN?: This can be used to show exp11d 43065 holds for all integers when the exponent is odd. (Contributed by SN, 4-Mar-2023.)
⊢ (𝜑 → 𝑁 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (𝑀 / 2) ∈ ℕ)    ⇒   ⊢ (𝜑 → (0 < 𝑁 ↔ 0 < (𝑁↑𝑀)))
Theorem	explt1d 43062	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 43063	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 43064	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 43065	exp11nnd 14299 for nonzero integer exponents. (Contributed by SN, 14-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ≠ 0)    &   ⊢ (𝜑 → (𝐴↑𝑁) = (𝐵↑𝑁))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	0dvds0 43066	0 divides 0. (Contributed by SN, 15-Sep-2024.)
⊢ 0 ∥ 0
Theorem	absdvdsabsb 43067	Divisibility is invariant under taking the absolute value on both sides. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁)))
Theorem	gcdnn0id 43068	The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024.)
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 𝑁) = 𝑁)
Theorem	gcdle1d 43069	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 43070	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 43071	Deduction associated with dvdsexpim 16614. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∥ (𝐵↑𝑁))
Theorem	dvdsexpnn 43072	dvdssqlem 16625 generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	dvdsexpnn0 43073	dvdsexpnn 43072 generalized to include zero bases. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	dvdsexpb 43074	dvdssq 16626 generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	posqsqznn 43075	When a positive rational squared is an integer, the rational is a positive integer. zsqrtelqelz 16818 with all terms squared and positive. (Contributed by SN, 23-Aug-2024.)
⊢ (𝜑 → (𝐴↑2) ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℚ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℕ)
Theorem	zdivgd 43076*	Two ways to express "𝑁 is an integer multiple of 𝑀". Originally a subproof of zdiv 12667. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    ⇒   ⊢ (𝜑 → (∃𝑘 ∈ ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))
Theorem	efsubd 43077	Difference of exponents law for exponential function, deduction form. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵)))
Theorem	ef11d 43078*	General condition for the exponential function to be one-to-one. efper 26622 shows that exponentiation is periodic. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((exp‘𝐴) = (exp‘𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + ((i · (2 · π)) · 𝑛))))
Theorem	logccne0d 43079	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 43080*	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 43081*	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 43082*	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 43083	Deduction form of logne0 26722. See logccne0d 43079 for a more general version. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ≠ 1)    ⇒   ⊢ (𝜑 → (log‘𝐴) ≠ 0)
Theorem	rxp112d 43084	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 43085	The natural logarithm is one-to-one. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	rplog11d 43086	The natural logarithm is one-to-one on positive reals. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	rxp11d 43087	Real exponentiation is one-to-one with respect to the first argument. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → (𝐴↑𝑐𝐶) = (𝐵↑𝑐𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
21.31.4  Trigonometry and Calculus
Theorem	tanhalfpim 43088	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 43089	Sine of a number subtracted from π. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → (sin‘(π − 𝐴)) = (sin‘𝐴))
Theorem	cospim 43090	Cosine of a number subtracted from π. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → (cos‘(π − 𝐴)) = -(cos‘𝐴))
Theorem	tan3rdpi 43091	The tangent of π / 3 is √3. (Contributed by SN, 2-Sep-2025.)
⊢ (tan‘(π / 3)) = (√‘3)
Theorem	sin2t3rdpi 43092	The sine of 2 · (π / 3) is (√3) / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (sin‘(2 · (π / 3))) = ((√‘3) / 2)
Theorem	cos2t3rdpi 43093	The cosine of 2 · (π / 3) is -1 / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (cos‘(2 · (π / 3))) = -(1 / 2)
Theorem	sin4t3rdpi 43094	The sine of 4 · (π / 3) is -(√3) / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (sin‘(4 · (π / 3))) = -((√‘3) / 2)
Theorem	cos4t3rdpi 43095	The cosine of 4 · (π / 3) is -1 / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (cos‘(4 · (π / 3))) = -(1 / 2)
Theorem	asin1half 43096	The arcsine of 1 / 2 is π / 6. (Contributed by SN, 31-Aug-2025.)
⊢ (arcsin‘(1 / 2)) = (π / 6)
Theorem	acos1half 43097	The arccosine of 1 / 2 is π / 3. (Contributed by SN, 31-Aug-2024.)
⊢ (arccos‘(1 / 2)) = (π / 3)
Theorem	dvun 43098	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 23220. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐺:𝐵⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → (((int‘𝐽)‘𝐴) ∪ ((int‘𝐽)‘𝐵)) = ((int‘𝐽)‘(𝐴 ∪ 𝐵)))    ⇒   ⊢ (𝜑 → ((𝑆 D 𝐹) ∪ (𝑆 D 𝐺)) = (𝑆 D (𝐹 ∪ 𝐺)))
Theorem	redvmptabs 43099*	The derivative of the absolute value, for real numbers. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐷 = (ℝ ∖ {0})    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1))
Theorem	readvrec2 43100*	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 / 𝑥))