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	nnn1suc 42301*	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	nnadd1com 42302	Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) = (1 + 𝐴))
Theorem	nnaddcom 42303	Addition is commutative for natural numbers. Uses fewer axioms than addcom 11447. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	nnaddcomli 42304	Version of addcomli 11453 for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ (𝐴 + 𝐵) = 𝐶    ⇒   ⊢ (𝐵 + 𝐴) = 𝐶
Theorem	nnadddir 42305	Right-distributivity for natural numbers without ax-mulcom 11219. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	nnmul1com 42306	Multiplication with 1 is commutative for natural numbers, without ax-mulcom 11219. Since (𝐴 · 1) is 𝐴 by ax-1rid 11225, this is equivalent to remullid 42463 for natural numbers, but using fewer axioms (avoiding ax-resscn 11212, ax-addass 11220, ax-mulass 11221, ax-rnegex 11226, ax-pre-lttri 11229, ax-pre-lttrn 11230, ax-pre-ltadd 11231). (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1))
Theorem	nnmulcom 42307	Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	readdrcl2d 42308	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 42309	Move a subtraction in the RHS to a right-addition in the LHS. Converse of mvlraddd 11673. EDITORIAL: Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → (𝐴 + 𝐶) = 𝐵)
Theorem	laddrotrd 42310	Rotate the variables right in an equation with addition on the left, converting it into a subtraction. Version of mvlladdd 11674 with a commuted consequent, and of mvrladdd 11676 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 33607. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐶 − 𝐴) = 𝐵)
Theorem	raddswap12d 42311	Swap the first two variables in an equation with addition on the right, converting it into a subtraction. Version of mvrraddd 11675 with a commuted consequent, and of mvlraddd 11673 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 42312	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 42313	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 42314	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 42315	Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵)))
Theorem	sqsumi 42316	A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵)))
Theorem	negn0nposznnd 42317	Lemma for dffltz 42644. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → ¬ 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℕ)
Theorem	sqmid3api 42318	Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝑁 ∈ ℂ    &   ⊢ (𝐴 + 𝑁) = 𝐵    &   ⊢ (𝐵 + 𝑁) = 𝐶    ⇒   ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁))
Theorem	decaddcom 42319	Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵)
Theorem	sqn5i 42320	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 42321	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 42322	Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11714. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐸    &   ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹    &   ⊢ (𝐵 · 𝐷) = 𝐺    ⇒   ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐸𝐹𝐺
Theorem	decpmul 42323	Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐸    &   ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹    &   ⊢ (𝐵 · 𝐷) = ;𝐺𝐻    &   ⊢ (;𝐸𝐺 + 𝐹) = 𝐼    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;𝐼𝐻
Theorem	sqdeccom12 42324	The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
Theorem	sq3deccom12 42325	Variant of sqdeccom12 42324 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ (𝐴 + 𝐶) = 𝐷    ⇒   ⊢ ((;;𝐴𝐵𝐶 · ;;𝐴𝐵𝐶) − (;𝐷𝐵 · ;𝐷𝐵)) = (;99 · ((;𝐴𝐵 · ;𝐴𝐵) − (𝐶 · 𝐶)))
Theorem	4t5e20 42326	4 times 5 equals 20. (Contributed by SN, 30-Mar-2025.)
⊢ (4 · 5) = ;20
Theorem	sq4 42327	The square of 4 is 16. (Contributed by SN, 26-Aug-2025.)
⊢ (4↑2) = ;16
Theorem	sq5 42328	The square of 5 is 25. (Contributed by SN, 26-Aug-2025.)
⊢ (5↑2) = ;25
Theorem	sq6 42329	The square of 6 is 36. (Contributed by SN, 26-Aug-2025.)
⊢ (6↑2) = ;36
Theorem	sq7 42330	The square of 7 is 49. (Contributed by SN, 26-Aug-2025.)
⊢ (7↑2) = ;49
Theorem	sq8 42331	The square of 8 is 64. (Contributed by SN, 26-Aug-2025.)
⊢ (8↑2) = ;64
Theorem	sq9 42332	The square of 9 is 81. (Contributed by SN, 30-Mar-2025.)
⊢ (9↑2) = ;81
Theorem	rpsscn 42333	The positive reals are a subset of the complex numbers. (Contributed by SN, 1-Oct-2025.)
⊢ ℝ+ ⊆ ℂ
Theorem	4rp 42334	4 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 4 ∈ ℝ+
Theorem	6rp 42335	6 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 6 ∈ ℝ+
Theorem	7rp 42336	7 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 7 ∈ ℝ+
Theorem	8rp 42337	8 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 8 ∈ ℝ+
Theorem	9rp 42338	9 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 9 ∈ ℝ+
Theorem	235t711 42339	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 11270 saving the lower level uses of mulcomli 11270 within 235 · 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12842 are added then this proof would benefit more than ex-decpmul 42340. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 12401 or 8t7e56 12853. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.)
⊢ (;;235 · ;;711) = ;;;;;167085
Theorem	ex-decpmul 42340	Example usage of decpmul 42323. This proof is significantly longer than 235t711 42339. There is more unnecessary carrying compared to 235t711 42339. Although saving 5 visual steps, using mulcomli 11270 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 42341	Membership in a successor upper set of integers. (Contributed by SN, 5-Jul-2025.)
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ↔ (𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)))
Theorem	sn-eluzp1l 42342	Shorter proof of eluzp1l 12905. (Contributed by NM, 12-Sep-2005.) (Revised by SN, 5-Jul-2025.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁)
Theorem	fz1sumconst 42343*	The sum of 𝑁 constant terms (𝑘 is not free in 𝐶). (Contributed by SN, 21-Mar-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (1...𝑁)𝐶 = (𝑁 · 𝐶))
Theorem	fz1sump1 42344*	Add one more term to a sum. Special case of fsump1 15792 generalized to 𝑁 ∈ ℕ0. (Contributed by SN, 22-Mar-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (1...𝑁)𝐴 + 𝐵))
Theorem	oddnumth 42345*	The Odd Number Theorem. The sum of the first 𝑁 odd numbers is 𝑁↑2. A corollary of arisum 15896. (Contributed by SN, 21-Mar-2025.)
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)((2 · 𝑘) − 1) = (𝑁↑2))
Theorem	nicomachus 42346*	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 42347*	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	pine0 42348	π is nonzero. (Contributed by SN, 25-Apr-2025.)
⊢ π ≠ 0
Theorem	ine1 42349	i is not 1. (Contributed by SN, 25-Apr-2025.)
⊢ i ≠ 1
Theorem	0tie0 42350	0 times i equals 0. (Contributed by SN, 25-Apr-2025.)
⊢ (0 · i) = 0
Theorem	it1ei 42351	i times 1 equals i. (Contributed by SN, 25-Apr-2025.)
⊢ (i · 1) = i
Theorem	1tiei 42352	1 times i equals i. (Contributed by SN, 25-Apr-2025.)
⊢ (1 · i) = i
Theorem	itrere 42353	i times a real is real iff the real is zero. (Contributed by SN, 25-Apr-2025.)
⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0))
Theorem	retire 42354	A real times i is real iff the real is zero. (Contributed by SN, 25-Apr-2025.)
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0))
Theorem	iocioodisjd 42355	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 42356	A positive real is its own absolute value. (Contributed by SN, 1-Oct-2025.)
⊢ (𝑅 ∈ ℝ+ → (abs‘𝑅) = 𝑅)
21.30.3  Exponents and divisibility
Theorem	oexpreposd 42357	Lemma for dffltz 42644. For a more standard version, see expgt0b 32818. TODO-SN?: This can be used to show exp11d 42361 holds for all integers when the exponent is odd. (Contributed by SN, 4-Mar-2023.)
⊢ (𝜑 → 𝑁 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (𝑀 / 2) ∈ ℕ)    ⇒   ⊢ (𝜑 → (0 < 𝑁 ↔ 0 < (𝑁↑𝑀)))
Theorem	explt1d 42358	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 42359	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 42360	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 42361	exp11nnd 14300 for nonzero integer exponents. (Contributed by SN, 14-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ≠ 0)    &   ⊢ (𝜑 → (𝐴↑𝑁) = (𝐵↑𝑁))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	0dvds0 42362	0 divides 0. (Contributed by SN, 15-Sep-2024.)
⊢ 0 ∥ 0
Theorem	absdvdsabsb 42363	Divisibility is invariant under taking the absolute value on both sides. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁)))
Theorem	gcdnn0id 42364	The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024.)
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 𝑁) = 𝑁)
Theorem	gcdle1d 42365	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 42366	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 42367	Deduction associated with dvdsexpim 16592. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∥ (𝐵↑𝑁))
Theorem	dvdsexpnn 42368	dvdssqlem 16603 generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	dvdsexpnn0 42369	dvdsexpnn 42368 generalized to include zero bases. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	dvdsexpb 42370	dvdssq 16604 generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	posqsqznn 42371	When a positive rational squared is an integer, the rational is a positive integer. zsqrtelqelz 16795 with all terms squared and positive. (Contributed by SN, 23-Aug-2024.)
⊢ (𝜑 → (𝐴↑2) ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℚ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℕ)
Theorem	zdivgd 42372*	Two ways to express "𝑁 is an integer multiple of 𝑀". Originally a subproof of zdiv 12688. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    ⇒   ⊢ (𝜑 → (∃𝑘 ∈ ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))
Theorem	efne0d 42373	The exponential of a complex number is nonzero, deduction form. EDITORIAL: Using efne0d 42373 in efne0 16133 is shorter than vice versa. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ≠ 0)
Theorem	efsubd 42374	Difference of exponents law for exponential function, deduction form. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵)))
Theorem	ef11d 42375*	General condition for the exponential function to be one-to-one. efper 26521 shows that exponentiation is periodic. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((exp‘𝐴) = (exp‘𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + ((i · (2 · π)) · 𝑛))))
Theorem	logccne0d 42376	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 42377*	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 42378*	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 42379*	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 42380	Deduction form of logne0 26621. See logccne0d 42376 for a more general version. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ≠ 1)    ⇒   ⊢ (𝜑 → (log‘𝐴) ≠ 0)
Theorem	rxp112d 42381	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 42382	The natural logarithm is one-to-one. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	rplog11d 42383	The natural logarithm is one-to-one on positive reals. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	rxp11d 42384	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 42385	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	tan3rdpi 42386	The tangent of π / 3 is √3. (Contributed by SN, 2-Sep-2025.)
⊢ (tan‘(π / 3)) = (√‘3)
Theorem	asin1half 42387	The arcsine of 1 / 2 is π / 6. (Contributed by SN, 31-Aug-2025.)
⊢ (arcsin‘(1 / 2)) = (π / 6)
Theorem	acos1half 42388	The arccosine of 1 / 2 is π / 3. (Contributed by SN, 31-Aug-2024.)
⊢ (arccos‘(1 / 2)) = (π / 3)
Theorem	dvun 42389	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 23090. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐺:𝐵⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → (((int‘𝐽)‘𝐴) ∪ ((int‘𝐽)‘𝐵)) = ((int‘𝐽)‘(𝐴 ∪ 𝐵)))    ⇒   ⊢ (𝜑 → ((𝑆 D 𝐹) ∪ (𝑆 D 𝐺)) = (𝑆 D (𝐹 ∪ 𝐺)))
Theorem	redvmptabs 42390*	The derivative of the absolute value, for real numbers. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐷 = (ℝ ∖ {0})    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1))
Theorem	readvrec2 42391*	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 42392*	For real numbers, the antiderivative of 1/x is ln|x|. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐷 = (ℝ ∖ {0})    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))
Theorem	resuppsinopn 42393	The support of sin (df-supp 8186) restricted to the reals is an open set. (Contributed by SN, 7-Oct-2025.)
⊢ 𝐷 = {𝑦 ∈ ℝ ∣ (sin‘𝑦) ≠ 0}    ⇒   ⊢ 𝐷 ∈ (topGen‘ran (,))
Theorem	readvcot 42394*	Real antiderivative of cotangent. (Contributed by SN, 7-Oct-2025.)
⊢ 𝐷 = {𝑦 ∈ ℝ ∣ (sin‘𝑦) ≠ 0}    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘(sin‘𝑥))))) = (𝑥 ∈ 𝐷 ↦ ((cos‘𝑥) / (sin‘𝑥)))
21.30.5  Real subtraction
Syntax	cresub 42395	Real number subtraction.
class −ℝ
Definition	df-resub 42396*	Define subtraction between real numbers. This operator saves a few axioms over df-sub 11494 in certain situations. Theorem resubval 42397 shows its value, resubadd 42409 relates it to addition, and rersubcl 42408 proves its closure. It is the restriction of df-sub 11494 to the reals: subresre 42460. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥))
Theorem	resubval 42397*	Value of real subtraction, which is the (unique) real 𝑥 such that 𝐵 + 𝑥 = 𝐴. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴))
Theorem	renegeulemv 42398*	Lemma for renegeu 42400 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴)
Theorem	renegeulem 42399*	Lemma for renegeu 42400 and similar. Remove a change in bound variables from renegeulemv 42398. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)    ⇒   ⊢ (𝜑 → ∃!𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)
Theorem	renegeu 42400*	Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)