P. 402 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40101-40200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	aks4d1p8d3 40101	The remainder of a division with its maximal prime power is coprime with that prime power. (Contributed by metakunt, 13-Nov-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑃 ∥ 𝑁)    ⇒   ⊢ (𝜑 → ((𝑁 / (𝑃↑(𝑃 pCnt 𝑁))) gcd (𝑃↑(𝑃 pCnt 𝑁))) = 1)
Theorem	aks4d1p8 40102*	Show that 𝑁 and 𝑅 are coprime for AKS existence theorem, with eliminated hypothesis. (Contributed by metakunt, 10-Nov-2024.) (Proof sketch by Thierry Arnoux.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1))    &   ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   ⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < )    ⇒   ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)
Theorem	aks4d1p9 40103*	Show that the order is bound by the squared binary logarithm. (Contributed by metakunt, 14-Nov-2024.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1))    &   ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   ⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < )    ⇒   ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁))
Theorem	aks4d1 40104*	Lemma 4.1 from https://www3.nd.edu/%7eandyp/notes/AKS.pdf, existence of a polynomially bounded number by the digit size of 𝑁 that asserts the polynomial subspace that we need to search to guarantee that 𝑁 is prime. Eventually we want to show that the polynomial searching space is bounded by degree 𝐵. (Contributed by metakunt, 14-Nov-2024.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5))    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ (1...𝐵)((𝑁 gcd 𝑟) = 1 ∧ ((2 logb 𝑁)↑2) < ((odℤ‘𝑟)‘𝑁)))
Theorem	5bc2eq10 40105	The value of 5 choose 2. (Contributed by metakunt, 8-Jun-2024.)
⊢ (5C2) = ;10
Theorem	facp2 40106	The factorial of a successor's successor. (Contributed by metakunt, 19-Apr-2024.)
⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 2)) = ((!‘𝑁) · ((𝑁 + 1) · (𝑁 + 2))))
Theorem	2np3bcnp1 40107	Part of induction step for 2ap1caineq 40108. (Contributed by metakunt, 8-Jun-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (((2 · (𝑁 + 1)) + 1)C(𝑁 + 1)) = ((((2 · 𝑁) + 1)C𝑁) · (2 · (((2 · 𝑁) + 3) / (𝑁 + 2)))))
Theorem	2ap1caineq 40108	Inequality for Theorem 6.6 for AKS. (Contributed by metakunt, 8-Jun-2024.)
⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 2 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (2↑(𝑁 + 1)) < (((2 · 𝑁) + 1)C𝑁))
20.25.6  Sticks and stones
Theorem	sticksstones1 40109*	Different strictly monotone functions have different ranges. (Contributed by metakunt, 27-Sep-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < )    ⇒   ⊢ (𝜑 → ran 𝑋 ≠ ran 𝑌)
Theorem	sticksstones2 40110*	The range function on strictly monotone functions with finite domain and codomain is an injective mapping onto 𝐾-elemental sets. (Contributed by metakunt, 27-Sep-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    &   ⊢ 𝐹 = (𝑧 ∈ 𝐴 ↦ ran 𝑧)    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵)
Theorem	sticksstones3 40111*	The range function on strictly monotone functions with finite domain and codomain is an surjective mapping onto 𝐾-elemental sets. (Contributed by metakunt, 28-Sep-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    &   ⊢ 𝐹 = (𝑧 ∈ 𝐴 ↦ ran 𝑧)    ⇒   ⊢ (𝜑 → 𝐹:𝐴–onto→𝐵)
Theorem	sticksstones4 40112*	Equinumerosity lemma for sticks and stones. (Contributed by metakunt, 28-Sep-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐴 ≈ 𝐵)
Theorem	sticksstones5 40113*	Count the number of strictly monotonely increasing functions on finite domains and codomains. (Contributed by metakunt, 28-Sep-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = (𝑁C𝐾))
Theorem	sticksstones6 40114*	Function induces an order isomorphism for sticks and stones theorem. (Contributed by metakunt, 1-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐺:(1...(𝐾 + 1))⟶ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝐾))    &   ⊢ (𝜑 → 𝑌 ∈ (1...𝐾))    &   ⊢ (𝜑 → 𝑋 < 𝑌)    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) < (𝐹‘𝑌))
Theorem	sticksstones7 40115*	Closure property of sticks and stones function. (Contributed by metakunt, 1-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐺:(1...(𝐾 + 1))⟶ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝐾))    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖)))    &   ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺‘𝑖) = 𝑁)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ∈ (1...(𝑁 + 𝐾)))
Theorem	sticksstones8 40116*	Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 1-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
Theorem	sticksstones9 40117*	Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 = 0)    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
Theorem	sticksstones10 40118*	Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
Theorem	sticksstones11 40119*	Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 = 0)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	sticksstones12a 40120*	Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 11-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → ∀𝑑 ∈ 𝐵 (𝐹‘(𝐺‘𝑑)) = 𝑑)
Theorem	sticksstones12 40121*	Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	sticksstones13 40122*	Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	sticksstones14 40123*	Sticks and stones with definitions as hypotheses. (Contributed by metakunt, 7-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + 𝐾)C𝐾))
Theorem	sticksstones15 40124*	Sticks and stones with almost collapsed definitions for positive integers. (Contributed by metakunt, 7-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + 𝐾)C𝐾))
Theorem	sticksstones16 40125*	Sticks and stones with collapsed definitions for positive integers. (Contributed by metakunt, 20-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1)))
Theorem	sticksstones17 40126*	Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)}    &   ⊢ (𝜑 → 𝑍:(1...𝐾)–1-1-onto→𝑆)    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍‘𝑦))))    ⇒   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
Theorem	sticksstones18 40127*	Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)}    &   ⊢ (𝜑 → 𝑍:(1...𝐾)–1-1-onto→𝑆)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
Theorem	sticksstones19 40128*	Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)}    &   ⊢ (𝜑 → 𝑍:(1...𝐾)–1-1-onto→𝑆)    &   ⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))    &   ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍‘𝑦))))    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	sticksstones20 40129*	Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakung, 24-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}    &   ⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)}    &   ⊢ (𝜑 → (♯‘𝑆) = 𝐾)    ⇒   ⊢ (𝜑 → (♯‘𝐵) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1)))
Theorem	sticksstones21 40130*	Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakunt, 24-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝑆 ≠ ∅)    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 𝑁)}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
Theorem	sticksstones22 40131*	Non-exhaustive sticks and stones. (Contributed by metakunt, 26-Oct-2024.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝑆 ≠ ∅)    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}    ⇒   ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
20.25.7  Permutation results
Theorem	metakunt1 40132*	A is an endomapping. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    ⇒   ⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀))
Theorem	metakunt2 40133*	A is an endomapping. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1))))    ⇒   ⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀))
Theorem	metakunt3 40134*	Value of A. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝐴‘𝑋) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))))
Theorem	metakunt4 40135*	Value of A. (Contributed by metakunt, 23-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝐴‘𝑋) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))))
Theorem	metakunt5 40136*	C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 = 𝐼) → (𝐶‘(𝐴‘𝑋)) = 𝑋)
Theorem	metakunt6 40137*	C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐶‘(𝐴‘𝑋)) = 𝑋)
Theorem	metakunt7 40138*	C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ((𝐴‘𝑋) = (𝑋 − 1) ∧ ¬ (𝐴‘𝑋) = 𝑀 ∧ ¬ (𝐴‘𝑋) < 𝐼))
Theorem	metakunt8 40139*	C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐶‘(𝐴‘𝑋)) = 𝑋)
Theorem	metakunt9 40140*	C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝐶‘(𝐴‘𝑋)) = 𝑋)
Theorem	metakunt10 40141*	C is the right inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 = 𝑀) → (𝐴‘(𝐶‘𝑋)) = 𝑋)
Theorem	metakunt11 40142*	C is the right inverse for A. (Contributed by metakunt, 24-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐴‘(𝐶‘𝑋)) = 𝑋)
Theorem	metakunt12 40143*	C is the right inverse for A. (Contributed by metakunt, 25-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ ((𝜑 ∧ ¬ (𝑋 = 𝑀 ∨ 𝑋 < 𝐼)) → (𝐴‘(𝐶‘𝑋)) = 𝑋)
Theorem	metakunt13 40144*	C is the right inverse for A. (Contributed by metakunt, 25-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝐴‘(𝐶‘𝑋)) = 𝑋)
Theorem	metakunt14 40145*	A is a primitive permutation that moves the I-th element to the end and C is its inverse that moves the last element back to the I-th position. (Contributed by metakunt, 25-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    ⇒   ⊢ (𝜑 → (𝐴:(1...𝑀)–1-1-onto→(1...𝑀) ∧ ◡𝐴 = 𝐶))
Theorem	metakunt15 40146*	Construction of another permutation. (Contributed by metakunt, 25-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐹 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼)))    ⇒   ⊢ (𝜑 → 𝐹:(1...(𝐼 − 1))–1-1-onto→(((𝑀 − 𝐼) + 1)...(𝑀 − 1)))
Theorem	metakunt16 40147*	Construction of another permutation. (Contributed by metakunt, 25-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))    ⇒   ⊢ (𝜑 → 𝐹:(𝐼...(𝑀 − 1))–1-1-onto→(1...(𝑀 − 𝐼)))
Theorem	metakunt17 40148	The union of three disjoint bijections is a bijection. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐺:𝐴–1-1-onto→𝑋)    &   ⊢ (𝜑 → 𝐻:𝐵–1-1-onto→𝑌)    &   ⊢ (𝜑 → 𝐼:𝐶–1-1-onto→𝑍)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅)    &   ⊢ (𝜑 → (𝐵 ∩ 𝐶) = ∅)    &   ⊢ (𝜑 → (𝑋 ∩ 𝑌) = ∅)    &   ⊢ (𝜑 → (𝑋 ∩ 𝑍) = ∅)    &   ⊢ (𝜑 → (𝑌 ∩ 𝑍) = ∅)    &   ⊢ (𝜑 → 𝐹 = ((𝐺 ∪ 𝐻) ∪ 𝐼))    &   ⊢ (𝜑 → 𝐷 = ((𝐴 ∪ 𝐵) ∪ 𝐶))    &   ⊢ (𝜑 → 𝑊 = ((𝑋 ∪ 𝑌) ∪ 𝑍))    ⇒   ⊢ (𝜑 → 𝐹:𝐷–1-1-onto→𝑊)
Theorem	metakunt18 40149	Disjoint domains and codomains. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    ⇒   ⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅)))
Theorem	metakunt19 40150*	Domains on restrictions of functions. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))))    &   ⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼)))    &   ⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))    ⇒   ⊢ (𝜑 → ((𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) ∧ {⟨𝑀, 𝑀⟩} Fn {𝑀}))
Theorem	metakunt20 40151*	Show that B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))))    &   ⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼)))    &   ⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝑋 = 𝑀)    ⇒   ⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {⟨𝑀, 𝑀⟩})‘𝑋))
Theorem	metakunt21 40152*	Show that B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))))    &   ⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼)))    &   ⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    &   ⊢ (𝜑 → ¬ 𝑋 = 𝑀)    &   ⊢ (𝜑 → 𝑋 < 𝐼)    ⇒   ⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {⟨𝑀, 𝑀⟩})‘𝑋))
Theorem	metakunt22 40153*	Show that B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))))    &   ⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼)))    &   ⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    &   ⊢ (𝜑 → ¬ 𝑋 = 𝑀)    &   ⊢ (𝜑 → ¬ 𝑋 < 𝐼)    ⇒   ⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {⟨𝑀, 𝑀⟩})‘𝑋))
Theorem	metakunt23 40154*	B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))))    &   ⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼)))    &   ⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {⟨𝑀, 𝑀⟩})‘𝑋))
Theorem	metakunt24 40155	Technical condition such that metakunt17 40148 holds. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    ⇒   ⊢ (𝜑 → ((((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅ ∧ (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}) ∧ (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀})))
Theorem	metakunt25 40156*	B is a permutation. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))))    ⇒   ⊢ (𝜑 → 𝐵:(1...𝑀)–1-1-onto→(1...𝑀))
Theorem	metakunt26 40157*	Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))    &   ⊢ (𝜑 → 𝑋 = 𝐼)    ⇒   ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = 𝑋)
Theorem	metakunt27 40158*	Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))    &   ⊢ (𝜑 → ¬ 𝑋 = 𝐼)    &   ⊢ (𝜑 → 𝑋 < 𝐼)    ⇒   ⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 + (𝑀 − 𝐼)))
Theorem	metakunt28 40159*	Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))    &   ⊢ (𝜑 → ¬ 𝑋 = 𝐼)    &   ⊢ (𝜑 → ¬ 𝑋 < 𝐼)    ⇒   ⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 − 𝐼))
Theorem	metakunt29 40160*	Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))    &   ⊢ (𝜑 → ¬ 𝑋 = 𝐼)    &   ⊢ (𝜑 → 𝑋 < 𝐼)    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)    ⇒   ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
Theorem	metakunt30 40161*	Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))    &   ⊢ (𝜑 → ¬ 𝑋 = 𝐼)    &   ⊢ (𝜑 → ¬ 𝑋 < 𝐼)    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0)    ⇒   ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 − 𝐼) + 𝐻))
Theorem	metakunt31 40162*	Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ 𝐺 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)    &   ⊢ 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0)    &   ⊢ 𝑅 = if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻)))    ⇒   ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = 𝑅)
Theorem	metakunt32 40163*	Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))    &   ⊢ 𝐷 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑥, if(𝑥 < 𝐼, ((𝑥 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑥 + (𝑀 − 𝐼)), 1, 0)), ((𝑥 − 𝐼) + if(𝐼 ≤ (𝑥 − 𝐼), 1, 0)))))    &   ⊢ 𝐺 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)    &   ⊢ 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0)    &   ⊢ 𝑅 = if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻)))    ⇒   ⊢ (𝜑 → (𝐷‘𝑋) = 𝑅)
Theorem	metakunt33 40164*	Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))    &   ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   ⊢ 𝐷 = (𝑤 ∈ (1...𝑀) ↦ if(𝑤 = 𝐼, 𝑤, if(𝑤 < 𝐼, ((𝑤 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0)), ((𝑤 − 𝐼) + if(𝐼 ≤ (𝑤 − 𝐼), 1, 0)))))    ⇒   ⊢ (𝜑 → (𝐶 ∘ (𝐵 ∘ 𝐴)) = 𝐷)
Theorem	metakunt34 40165*	𝐷 is a permutation. (Contributed by metakunt, 18-Jul-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ≤ 𝑀)    &   ⊢ 𝐷 = (𝑤 ∈ (1...𝑀) ↦ if(𝑤 = 𝐼, 𝑤, if(𝑤 < 𝐼, ((𝑤 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0)), ((𝑤 − 𝐼) + if(𝐼 ≤ (𝑤 − 𝐼), 1, 0)))))    ⇒   ⊢ (𝜑 → 𝐷:(1...𝑀)–1-1-onto→(1...𝑀))
20.25.8  Unused lemmas scheduled for deletion
Theorem	andiff 40166	Adding biconditional when antecedents are conjuncted. (Contributed by metakunt, 16-Apr-2024.)
⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜓 → (𝜃 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
Theorem	fac2xp3 40167	Factorial of 2x+3, sublemma for sublemma for AKS. (Contributed by metakunt, 19-Apr-2024.)
⊢ (𝑥 ∈ ℕ0 → (!‘((2 · 𝑥) + 3)) = ((!‘((2 · 𝑥) + 1)) · (((2 · 𝑥) + 2) · ((2 · 𝑥) + 3))))
Theorem	prodsplit 40168*	Product split into two factors, original by Steven Nguyen. (Contributed by metakunt, 21-Apr-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 𝐾))) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...(𝑁 + 𝐾))𝐴 = (∏𝑘 ∈ (𝑀...𝑁)𝐴 · ∏𝑘 ∈ ((𝑁 + 1)...(𝑁 + 𝐾))𝐴))
Theorem	2xp3dxp2ge1d 40169	2x+3 is greater than or equal to x+2 for x >= -1, a deduction version (Contributed by metakunt, 21-Apr-2024.)
⊢ (𝜑 → 𝑋 ∈ (-1[,)+∞))    ⇒   ⊢ (𝜑 → 1 ≤ (((2 · 𝑋) + 3) / (𝑋 + 2)))
Theorem	factwoffsmonot 40170	A factorial with offset is monotonely increasing. (Contributed by metakunt, 20-Apr-2024.)
⊢ (((𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℕ0 ∧ 𝑋 ≤ 𝑌) ∧ 𝑁 ∈ ℕ0) → (!‘(𝑋 + 𝑁)) ≤ (!‘(𝑌 + 𝑁)))
20.26  Mathbox for Steven Nguyen
20.26.1  Miscellaneous theorems These theorems were added for illustration or pedagogical purposes without the intention of being used, but some may still be moved to main and used, of course.
Theorem	bicomdALT 40171	Alternate proof of bicomd 222 which is shorter after expanding all parent theorems (as of 8-Aug-2024, bicom 221 depends on bicom1 220 and sylib 217 depends on syl 17). Additionally, the labels bicom1 220 and syl 17 happen to contain fewer characters than bicom 221 and sylib 217. However, neither of these conditions count as a shortening according to conventions 28773. In the first case, the criteria could easily be broken by upstream changes, and in many cases the upstream dependency tree is nontrivial (see orass 919 and pm2.31 920). For the latter case, theorem labels are up to revision, so they are not counted in the size of a proof. (Contributed by SN, 21-May-2022.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ↔ 𝜓))
Theorem	elabgw 40172*	Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on 𝑥 and 𝐴. This is to elabg 3608 what sbievw2 2100 is to sbievw 2096. (Contributed by SN, 20-Apr-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒))
Theorem	elab2gw 40173*	Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on 𝑥 and 𝐴, which is not usually significant since 𝐵 is usually a constant. (Contributed by SN, 16-May-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ 𝐵 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜒))
Theorem	elrab2w 40174*	Membership in a restricted class abstraction. This is to elrab2 3628 what elab2gw 40173 is to elab2g 3612. (Contributed by SN, 2-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ 𝜑}    ⇒   ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜒))
Theorem	ruvALT 40175	Alternate proof of ruv 9370 with one fewer syntax step thanks to using elirrv 9364 instead of elirr 9365. However, it does not change the compressed proof size or the number of symbols in the generated display, so it is not considered a shortening according to conventions 28773. (Contributed by SN, 1-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V
Theorem	sn-wcdeq 40176	Alternative to wcdeq 3699 and df-cdeq 3700. This flattens the syntax representation ( wi ( weq vx vy ) wph ) to ( sn-wcdeq vx vy wph ), illustrating the comment of df-cdeq 3700. (Contributed by SN, 26-Sep-2024.) (New usage is discouraged.)
wff (𝑥 = 𝑦 → 𝜑)
Theorem	acos1half 40177	The arccosine of 1 / 2 is π / 3. (Contributed by SN, 31-Aug-2024.)
⊢ (arccos‘(1 / 2)) = (π / 3)
Theorem	isdomn5 40178*	The right conjunct in the right hand side of the equivalence of isdomn 20574 is logically equivalent to a less symmetric version where one of the variables is restricted to be nonzero. (Contributed by SN, 16-Sep-2024.)
⊢ (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → (𝑎 = 0 ∨ 𝑏 = 0 )) ↔ ∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → 𝑏 = 0 ))
Theorem	isdomn4 40179*	A ring is a domain iff it is nonzero and the cancellation law for multiplication holds. (Contributed by SN, 15-Sep-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐)))
20.26.2  Utility theorems
Theorem	ioin9i8 40180	Miscellaneous inference creating a biconditional from an implied converse implication. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜒 → ¬ 𝜃)    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
Theorem	jaodd 40181	Double deduction form of jaoi 854. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) → 𝜃)))
Theorem	syl3an12 40182	A double syllogism inference. (Contributed by SN, 15-Sep-2024.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
Theorem	sbtd 40183*	A true statement is true upon substitution (deduction). A similar proof is possible for icht 44915. (Contributed by SN, 4-May-2024.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → [𝑡 / 𝑥]𝜓)
Theorem	sbor2 40184	One direction of sbor 2305, using fewer axioms. Compare 19.33 1888. (Contributed by Steven Nguyen, 18-Aug-2023.)
⊢ (([𝑡 / 𝑥]𝜑 ∨ [𝑡 / 𝑥]𝜓) → [𝑡 / 𝑥](𝜑 ∨ 𝜓))
Theorem	19.9dev 40185*	19.9d 2197 in the case of an existential quantifier, avoiding the ax-10 2138 from nfex 2319 that would be used for the hypothesis of 19.9d 2197, at the cost of an additional DV condition on 𝑦, 𝜑. (Contributed by SN, 26-May-2024.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑦𝜓))
Theorem	rspcedvdw 40186*	Version of rspcedvd 3564 where the implicit substitution hypothesis does not have an antecedent, which also avoids a disjoint variable condition on 𝜑, 𝑥. (Contributed by SN, 20-Aug-2024.)
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	2rspcedvdw 40187*	Double application of rspcedvdw 40186. (Contributed by SN, 24-Aug-2024.)
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝜓)
Theorem	3rspcedvdw 40188*	Triple application of rspcedvdw 40186. (Contributed by SN, 20-Aug-2024.)
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∃𝑧 ∈ 𝑍 𝜓)
Theorem	3rspcedvd 40189*	Triple application of rspcedvd 3564. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ 𝑧 = 𝐶) → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 ∃𝑧 ∈ 𝐷 𝜓)
Theorem	eqimssd 40190	Equality implies inclusion, deduction version. (Contributed by SN, 6-Nov-2024.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	rabdif 40191*	Move difference in and out of a restricted class abstraction. (Contributed by Steven Nguyen, 6-Jun-2023.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ 𝐵) = {𝑥 ∈ (𝐴 ∖ 𝐵) ∣ 𝜑}
Theorem	sn-axrep5v 40192*	A condensed form of axrep5 5216. (Contributed by SN, 21-Sep-2023.)
⊢ (∀𝑤 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑))
Theorem	sn-axprlem3 40193*	axprlem3 5349 using only Tarski's FOL axiom schemes and ax-rep 5210. (Contributed by SN, 22-Sep-2023.)
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 if-(𝜑, 𝑧 = 𝑎, 𝑧 = 𝑏))
Theorem	sn-el 40194*	A version of el 5358 with an inner existential quantifier on 𝑥, which avoids ax-7 2012 and ax-8 2109. (Contributed by SN, 18-Sep-2023.)
⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦
Theorem	sn-dtru 40195*	dtru 5360 without ax-8 2109 or ax-12 2172. (Contributed by SN, 21-Sep-2023.)
⊢ ¬ ∀𝑥 𝑥 = 𝑦
Theorem	sn-iotalem 40196*	An unused lemma showing that many equivalences involving df-iota 6395 are potentially provable without ax-10 2138, ax-11 2155, ax-12 2172. (Contributed by SN, 6-Nov-2024.)
⊢ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧 ∣ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧}}
Theorem	sn-iotalemcor 40197*	Corollary of sn-iotalem 40196. Compare sb8iota 6407. (Contributed by SN, 6-Nov-2024.)
⊢ (℩𝑥𝜑) = (℩𝑦{𝑥 ∣ 𝜑} = {𝑦})
Theorem	abbi1sn 40198*	Originally part of uniabio 6410. Convert a theorem about df-iota 6395 to one about dfiota2 6396, without ax-10 2138, ax-11 2155, ax-12 2172. Although, eu6 2575 uses ax-10 2138 and ax-12 2172. (Contributed by SN, 23-Nov-2024.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → {𝑥 ∣ 𝜑} = {𝑦})
Theorem	iotavallem 40199*	Version of iotaval 6411 using df-iota 6395 instead of dfiota2 6396. (Contributed by SN, 6-Nov-2024.)
⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
Theorem	sn-iotauni 40200*	Version of iotauni 6412 using df-iota 6395 instead of dfiota2 6396. (Contributed by SN, 6-Nov-2024.)
⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∪ {𝑥 ∣ 𝜑})