| Metamath
Proof Explorer Theorem List (p. 423 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | aks5lem7 42201* | Lemma for aks5. We clean up the hypotheses compared to aks5lem6 42193. (Contributed by metakunt, 9-Aug-2025.) |
| ⊢ (𝜑 → (♯‘(Base‘𝐾)) ∈ ℕ) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → 𝑅 ∥ ((♯‘(Base‘𝐾)) − 1)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))(𝑋(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))𝑋)(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿)) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁)) & ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))𝑋)(-g‘𝑆)(1r‘𝑆))}) & ⊢ 𝑋 = (var1‘(ℤ/nℤ‘𝑁)) ⇒ ⊢ (𝜑 → 𝑁 = (𝑃↑(𝑃 pCnt 𝑁))) | ||
| Theorem | aks5lem8 42202* | Lemma for aks5. Clean up the conclusion. (Contributed by metakunt, 9-Aug-2025.) |
| ⊢ (𝜑 → (♯‘(Base‘𝐾)) ∈ ℕ) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → 𝑅 ∥ ((♯‘(Base‘𝐾)) − 1)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))(𝑋(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))𝑋)(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿)) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁)) & ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))𝑋)(-g‘𝑆)(1r‘𝑆))}) & ⊢ 𝑋 = (var1‘(ℤ/nℤ‘𝑁)) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑛 ∈ ℕ 𝑁 = (𝑝↑𝑛)) | ||
| Axiom | ax-exfinfld 42203* | Existence axiom for finite fields, eventually we want to construct them. (Contributed by metakunt, 13-Jul-2025.) |
| ⊢ ∀𝑝 ∈ ℙ ∀𝑛 ∈ ℕ ∃𝑘 ∈ Field ((♯‘(Base‘𝑘)) = (𝑝↑𝑛) ∧ (chr‘𝑘) = 𝑝) | ||
| Theorem | exfinfldd 42204* | For any prime 𝑃 and any positive integer 𝑁 there exists a field 𝑘 such that 𝑘 contains 𝑃↑𝑁 elements. (Contributed by metakunt, 13-Jul-2025.) |
| ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ Field ((♯‘(Base‘𝑘)) = (𝑃↑𝑁) ∧ (chr‘𝑘) = 𝑃)) | ||
| Theorem | aks5 42205* | The AKS Primality test, given an integer 𝑁 greater than or equal to 3, find a coprime 𝑅 such that 𝑅 is big enough. Then, if a bunch of polynomial equalities in the residue ring hold then 𝑁 is a prime power. Currently depends on the axiom ax-exfinfld 42203, since we currently do not have the existence of finite fields in the database. (Contributed by metakunt, 16-Aug-2025.) |
| ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ 𝑋 = (var1‘(ℤ/nℤ‘𝑁)) & ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁)) & ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))𝑋)(-g‘𝑆)(1r‘𝑆))}) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))(𝑋(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))𝑋)(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)(𝑎 gcd 𝑁) = 1) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑛 ∈ ℕ 𝑁 = (𝑝↑𝑛)) | ||
| Theorem | metakunt1 42206* | A is an endomapping. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) ⇒ ⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀)) | ||
| Theorem | metakunt2 42207* | A is an endomapping. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)))) ⇒ ⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀)) | ||
| Theorem | metakunt3 42208* | Value of A. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)))) | ||
| Theorem | metakunt4 42209* | Value of A. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)))) | ||
| Theorem | metakunt5 42210* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 = 𝐼) → (𝐶‘(𝐴‘𝑋)) = 𝑋) | ||
| Theorem | metakunt6 42211* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐶‘(𝐴‘𝑋)) = 𝑋) | ||
| Theorem | metakunt7 42212* | 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 42213* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐶‘(𝐴‘𝑋)) = 𝑋) | ||
| Theorem | metakunt9 42214* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐶‘(𝐴‘𝑋)) = 𝑋) | ||
| Theorem | metakunt10 42215* | C is the right inverse for A. (Contributed by metakunt, 24-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 = 𝑀) → (𝐴‘(𝐶‘𝑋)) = 𝑋) | ||
| Theorem | metakunt11 42216* | C is the right inverse for A. (Contributed by metakunt, 24-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐴‘(𝐶‘𝑋)) = 𝑋) | ||
| Theorem | metakunt12 42217* | C is the right inverse for A. (Contributed by metakunt, 25-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ ¬ (𝑋 = 𝑀 ∨ 𝑋 < 𝐼)) → (𝐴‘(𝐶‘𝑋)) = 𝑋) | ||
| Theorem | metakunt13 42218* | C is the right inverse for A. (Contributed by metakunt, 25-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐴‘(𝐶‘𝑋)) = 𝑋) | ||
| Theorem | metakunt14 42219* | 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 42220* | Construction of another permutation. (Contributed by metakunt, 25-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐹 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ⇒ ⊢ (𝜑 → 𝐹:(1...(𝐼 − 1))–1-1-onto→(((𝑀 − 𝐼) + 1)...(𝑀 − 1))) | ||
| Theorem | metakunt16 42221* | Construction of another permutation. (Contributed by metakunt, 25-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐹 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) ⇒ ⊢ (𝜑 → 𝐹:(𝐼...(𝑀 − 1))–1-1-onto→(1...(𝑀 − 𝐼))) | ||
| Theorem | metakunt17 42222 | 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 42223 | Disjoint domains and codomains. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) ⇒ ⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) | ||
| Theorem | metakunt19 42224* | 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 42225* | 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 42226* | 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 42227* | 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 42228* | 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 42229 | Technical condition such that metakunt17 42222 holds. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) ⇒ ⊢ (𝜑 → ((((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅ ∧ (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}) ∧ (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}))) | ||
| Theorem | metakunt25 42230* | B is a permutation. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) ⇒ ⊢ (𝜑 → 𝐵:(1...𝑀)–1-1-onto→(1...𝑀)) | ||
| Theorem | metakunt26 42231* | 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 42232* | 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 42233* | 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 42234* | 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 42235* | 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 42236* | 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 42237* | 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 42238* | 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 42239* | 𝐷 is a permutation. (Contributed by metakunt, 18-Jul-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐷 = (𝑤 ∈ (1...𝑀) ↦ if(𝑤 = 𝐼, 𝑤, if(𝑤 < 𝐼, ((𝑤 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0)), ((𝑤 − 𝐼) + if(𝐼 ≤ (𝑤 − 𝐼), 1, 0))))) ⇒ ⊢ (𝜑 → 𝐷:(1...𝑀)–1-1-onto→(1...𝑀)) | ||
| Theorem | fac2xp3 42240 | 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 42241* | Product split into two factors, original by Steven Nguyen. (Contributed by metakunt, 21-Apr-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 𝐾))) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...(𝑁 + 𝐾))𝐴 = (∏𝑘 ∈ (𝑀...𝑁)𝐴 · ∏𝑘 ∈ ((𝑁 + 1)...(𝑁 + 𝐾))𝐴)) | ||
| Theorem | 2xp3dxp2ge1d 42242 | 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 42243 | A factorial with offset is monotonely increasing. (Contributed by metakunt, 20-Apr-2024.) |
| ⊢ (((𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℕ0 ∧ 𝑋 ≤ 𝑌) ∧ 𝑁 ∈ ℕ0) → (!‘(𝑋 + 𝑁)) ≤ (!‘(𝑌 + 𝑁))) | ||
| Theorem | jarrii 42244 | Inference associated with jarri 107. A consequence of ax-mp 5 and ax-1 6. (Contributed by SN, 14-Oct-2025.) |
| ⊢ 𝜓 & ⊢ ((𝜑 → 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
| Theorem | intnanrt 42245 | Introduction of conjunct inside of a contradiction. Would be used in elfvov1 7473. (Contributed by SN, 18-May-2025.) |
| ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓)) | ||
| Theorem | ioin9i8 42246 | Miscellaneous inference creating a biconditional from an implied converse implication. (Contributed by Steven Nguyen, 17-Jul-2022.) |
| ⊢ (𝜑 → (𝜓 ∨ 𝜒)) & ⊢ (𝜒 → ¬ 𝜃) & ⊢ (𝜓 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
| Theorem | jaodd 42247 | Double deduction form of jaoi 858. (Contributed by Steven Nguyen, 17-Jul-2022.) |
| ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) → 𝜃))) | ||
| Theorem | syl3an12 42248 | A double syllogism inference. (Contributed by SN, 15-Sep-2024.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) | ||
| Theorem | exbiii 42249 | Inference associated with exbii 1848. Weaker version of eximii 1837. (Contributed by SN, 14-Oct-2025.) |
| ⊢ ∃𝑥𝜑 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ∃𝑥𝜓 | ||
| Theorem | sbtd 42250* | A true statement is true upon substitution (deduction). A similar proof is possible for icht 47439. (Contributed by SN, 4-May-2024.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → [𝑡 / 𝑥]𝜓) | ||
| Theorem | sbor2 42251 | One direction of sbor 2307, using fewer axioms. Compare 19.33 1884. (Contributed by Steven Nguyen, 18-Aug-2023.) |
| ⊢ (([𝑡 / 𝑥]𝜑 ∨ [𝑡 / 𝑥]𝜓) → [𝑡 / 𝑥](𝜑 ∨ 𝜓)) | ||
| Theorem | sbalexi 42252* | Inference form of sbalex 2242, avoiding ax-10 2141 by using ax-gen 1795. (Contributed by SN, 12-Aug-2025.) |
| ⊢ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ⇒ ⊢ ∀𝑥(𝑥 = 𝑦 → 𝜑) | ||
| Theorem | 19.9dev 42253* | 19.9d 2203 in the case of an existential quantifier, avoiding the ax-10 2141 from nfex 2324 that would be used for the hypothesis of 19.9d 2203, at the cost of an additional DV condition on 𝑦, 𝜑. (Contributed by SN, 26-May-2024.) |
| ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑦𝜓)) | ||
| Theorem | 3rspcedvd 42254* | Triple application of rspcedvd 3624. (Contributed by Steven Nguyen, 27-Feb-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (𝜒 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝑧 = 𝐶) → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 ∃𝑧 ∈ 𝐷 𝜓) | ||
| Theorem | sn-axrep5v 42255* | A condensed form of axrep5 5287. (Contributed by SN, 21-Sep-2023.) |
| ⊢ (∀𝑤 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑)) | ||
| Theorem | sn-axprlem3 42256* | axprlem3 5425 using only Tarski's FOL axiom schemes and ax-rep 5279. (Contributed by SN, 22-Sep-2023.) |
| ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 if-(𝜑, 𝑧 = 𝑎, 𝑧 = 𝑏)) | ||
| Theorem | sn-exelALT 42257* | Alternate proof of exel 5438, avoiding ax-pr 5432 but requiring ax-5 1910, ax-9 2118, and ax-pow 5365. This is similar to how elALT2 5369 uses ax-pow 5365 instead of ax-pr 5432 compared to el 5442. (Contributed by SN, 18-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦 | ||
| Theorem | ss2ab1 42258 | Class abstractions in a subclass relationship, closed form. One direction of ss2ab 4062 using fewer axioms. (Contributed by SN, 22-Dec-2024.) |
| ⊢ (∀𝑥(𝜑 → 𝜓) → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}) | ||
| Theorem | ssabdv 42259* | Deduction of abstraction subclass from implication. (Contributed by SN, 22-Dec-2024.) |
| ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ {𝑥 ∣ 𝜓}) | ||
| Theorem | sn-iotalem 42260* | An unused lemma showing that many equivalences involving df-iota 6514 are potentially provable without ax-10 2141, ax-11 2157, ax-12 2177. (Contributed by SN, 6-Nov-2024.) |
| ⊢ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧 ∣ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧}} | ||
| Theorem | sn-iotalemcor 42261* | Corollary of sn-iotalem 42260. Compare sb8iota 6525. (Contributed by SN, 6-Nov-2024.) |
| ⊢ (℩𝑥𝜑) = (℩𝑦{𝑥 ∣ 𝜑} = {𝑦}) | ||
| Theorem | abbi1sn 42262* | Originally part of uniabio 6528. Convert a theorem about df-iota 6514 to one about dfiota2 6515, without ax-10 2141, ax-11 2157, ax-12 2177. Although, eu6 2574 uses ax-10 2141 and ax-12 2177. (Contributed by SN, 23-Nov-2024.) |
| ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → {𝑥 ∣ 𝜑} = {𝑦}) | ||
| Theorem | brif2 42263 | Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.) |
| ⊢ (𝐶𝑅if(𝜑, 𝐴, 𝐵) ↔ if-(𝜑, 𝐶𝑅𝐴, 𝐶𝑅𝐵)) | ||
| Theorem | brif12 42264 | Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.) |
| ⊢ (if(𝜑, 𝐴, 𝐵)𝑅if(𝜑, 𝐶, 𝐷) ↔ if-(𝜑, 𝐴𝑅𝐶, 𝐵𝑅𝐷)) | ||
| Theorem | pssexg 42265 | The proper subset of a set is also a set. (Contributed by Steven Nguyen, 17-Jul-2022.) |
| ⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) | ||
| Theorem | pssn0 42266 | A proper superset is nonempty. (Contributed by Steven Nguyen, 17-Jul-2022.) |
| ⊢ (𝐴 ⊊ 𝐵 → 𝐵 ≠ ∅) | ||
| Theorem | psspwb 42267 | Classes are proper subclasses if and only if their power classes are proper subclasses. (Contributed by Steven Nguyen, 17-Jul-2022.) |
| ⊢ (𝐴 ⊊ 𝐵 ↔ 𝒫 𝐴 ⊊ 𝒫 𝐵) | ||
| Theorem | xppss12 42268 | Proper subset theorem for Cartesian product. (Contributed by Steven Nguyen, 17-Jul-2022.) |
| ⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷) → (𝐴 × 𝐶) ⊊ (𝐵 × 𝐷)) | ||
| Theorem | elpwbi 42269 | Membership in a power set, biconditional. (Contributed by Steven Nguyen, 17-Jul-2022.) (Proof shortened by Steven Nguyen, 16-Sep-2022.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵) | ||
| Theorem | imaopab 42270* | The image of a class of ordered pairs. (Contributed by Steven Nguyen, 6-Jun-2023.) |
| ⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} | ||
| Theorem | fnsnbt 42271 | A function's domain is a singleton iff the function is a singleton. (Contributed by Steven Nguyen, 18-Aug-2023.) |
| ⊢ (𝐴 ∈ V → (𝐹 Fn {𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉})) | ||
| Theorem | fnimasnd 42272 | The image of a function by a singleton whose element is in the domain of the function. (Contributed by Steven Nguyen, 7-Jun-2023.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 “ {𝑆}) = {(𝐹‘𝑆)}) | ||
| Theorem | eqresfnbd 42273 | Property of being the restriction of a function. Note that this is closer to funssres 6610 than fnssres 6691. (Contributed by SN, 11-Mar-2025.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑅 = (𝐹 ↾ 𝐴) ↔ (𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹))) | ||
| Theorem | f1o2d2 42274* | Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by SN, 11-Mar-2025.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝐼 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝐽 ∈ 𝐵) & ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐷)) → ((𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ 𝑧 = 𝐶)) ⇒ ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷) | ||
| Theorem | fmpocos 42275* | Composition of two functions. Variation of fmpoco 8120 with more context in the substitution hypothesis for 𝑇. (Contributed by SN, 14-Mar-2025.) |
| ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) | ||
| Theorem | ovmpogad 42276* | Value of an operation given by a maps-to rule. Deduction form of ovmpoga 7587. (Contributed by SN, 14-Mar-2025.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
| Theorem | ofun 42277 | A function operation of unions of disjoint functions is a union of function operations. (Contributed by SN, 16-Jun-2024.) |
| ⊢ (𝜑 → 𝐴 Fn 𝑀) & ⊢ (𝜑 → 𝐵 Fn 𝑀) & ⊢ (𝜑 → 𝐶 Fn 𝑁) & ⊢ (𝜑 → 𝐷 Fn 𝑁) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ 𝑊) & ⊢ (𝜑 → (𝑀 ∩ 𝑁) = ∅) ⇒ ⊢ (𝜑 → ((𝐴 ∪ 𝐶) ∘f 𝑅(𝐵 ∪ 𝐷)) = ((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷))) | ||
| Theorem | dfqs2 42278* | Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.) |
| ⊢ (𝐴 / 𝑅) = ran (𝑥 ∈ 𝐴 ↦ [𝑥]𝑅) | ||
| Theorem | dfqs3 42279* | Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.) |
| ⊢ (𝐴 / 𝑅) = ∪ 𝑥 ∈ 𝐴 {[𝑥]𝑅} | ||
| Theorem | qseq12d 42280 | Equality theorem for quotient set, deduction form. (Contributed by Steven Nguyen, 30-Apr-2023.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐷)) | ||
| Theorem | qsalrel 42281* | The quotient set is equal to the singleton of 𝐴 when all elements are related and 𝐴 is nonempty. (Contributed by SN, 8-Jun-2023.) |
| ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∼ 𝑦) & ⊢ (𝜑 → ∼ Er 𝐴) & ⊢ (𝜑 → 𝑁 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐴 / ∼ ) = {𝐴}) | ||
| Theorem | elmapssresd 42282 | A restricted mapping is a mapping. EDITORIAL: Could be used to shorten elpm2r 8885 with some reordering involving mapsspm 8916. (Contributed by SN, 11-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m 𝐶)) & ⊢ (𝜑 → 𝐷 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑m 𝐷)) | ||
| Theorem | supinf 42283* | The supremum is the infimum of the upper bounds. (Contributed by SN, 29-Jun-2025.) |
| ⊢ (𝜑 → < Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐵 𝑦 < 𝑧))) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, < ) = inf({𝑥 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤}, 𝐴, < )) | ||
| Theorem | mapcod 42284 | Compose two mappings. (Contributed by SN, 11-Mar-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑m 𝐵)) & ⊢ (𝜑 → 𝐺 ∈ (𝐵 ↑m 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (𝐴 ↑m 𝐶)) | ||
| Theorem | fisdomnn 42285 | A finite set is dominated by the set of natural numbers. (Contributed by SN, 6-Jul-2025.) |
| ⊢ (𝐴 ∈ Fin → 𝐴 ≺ ℕ) | ||
| Theorem | ltex 42286 | The less-than relation is a set. (Contributed by SN, 5-Jun-2025.) |
| ⊢ < ∈ V | ||
| Theorem | leex 42287 | The less-than-or-equal-to relation is a set. (Contributed by SN, 5-Jun-2025.) |
| ⊢ ≤ ∈ V | ||
| Theorem | subex 42288 | The subtraction operation is a set. (Contributed by SN, 5-Jun-2025.) |
| ⊢ − ∈ V | ||
| Theorem | absex 42289 | The absolute value function is a set. (Contributed by SN, 5-Jun-2025.) |
| ⊢ abs ∈ V | ||
| Theorem | cjex 42290 | The conjugate function is a set. (Contributed by SN, 5-Jun-2025.) |
| ⊢ ∗ ∈ V | ||
| Theorem | fzosumm1 42291* | Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023.) |
| ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = (𝑁 − 1) → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝐴 = (Σ𝑘 ∈ (𝑀..^(𝑁 − 1))𝐴 + 𝐵)) | ||
| Theorem | ccatcan2d 42292 | Cancellation law for concatenation. (Contributed by SN, 6-Sep-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ Word 𝑉) & ⊢ (𝜑 → 𝐵 ∈ Word 𝑉) & ⊢ (𝜑 → 𝐶 ∈ Word 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 ++ 𝐶) = (𝐵 ++ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Towards the start of this section are several proofs regarding the different complex number axioms that could be used to prove some results. For example, ax-1rid 11225 is used in mulrid 11259 related theorems, so one could trade off the extra axioms in mulrid 11259 for the axioms needed to prove that something is a real number. Another example is avoiding complex number closure laws by using real number closure laws and then using ax-resscn 11212; in the other direction, real number closure laws can be avoided by using ax-resscn 11212 and then the complex number closure laws. (This only works if the result of (𝐴 + 𝐵) only needs to be a complex number). The natural numbers are especially amenable to axiom reductions, as the set ℕ is the recursive set {1, (1 + 1), ((1 + 1) + 1)}, etc., i.e. the set of numbers formed by only additions of 1. The digits 2 through 9 are defined so that they expand into additions of 1. This conveniently allows for adding natural numbers by rearranging parentheses, as shown below: (4 + 3) = 7 ((3 + 1) + (2 + 1)) = (6 + 1) ((((1 + 1) + 1) + 1) + ((1 + 1) + 1)) = ((((((1 + 1) + 1) + 1) + 1) + 1) + 1) This only requires ax-addass 11220, ax-1cn 11213, and ax-addcl 11215. (And in practice, the expression isn't fully expanded into ones.) Multiplication by 1 requires either mullidi 11266 or (ax-1rid 11225 and 1re 11261) as seen in 1t1e1 12428 and 1t1e1ALT 42296. Multiplying with greater natural numbers uses ax-distr 11222. Still, this takes fewer axioms than adding zero, which is often implicit in theorems such as (9 + 1) = ;10. Adding zero uses almost every complex number axiom, though notably not ax-mulcom 11219 (see readdrid 42439 and readdlid 42433). | ||
| Theorem | c0exALT 42293 | Alternate proof of c0ex 11255 using more set theory axioms but fewer complex number axioms (add ax-10 2141, ax-11 2157, ax-13 2377, ax-nul 5306, and remove ax-1cn 11213, ax-icn 11214, ax-addcl 11215, and ax-mulcl 11217). (Contributed by Steven Nguyen, 4-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 0 ∈ V | ||
| Theorem | 0cnALT3 42294 | Alternate proof of 0cn 11253 using ax-resscn 11212, ax-addrcl 11216, ax-rnegex 11226, ax-cnre 11228 instead of ax-icn 11214, ax-addcl 11215, ax-mulcl 11217, ax-i2m1 11223. Version of 0cnALT 11496 using ax-1cn 11213 instead of ax-icn 11214. (Contributed by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 0 ∈ ℂ | ||
| Theorem | elre0re 42295 | Specialized version of 0red 11264 without using ax-1cn 11213 and ax-cnre 11228. (Contributed by Steven Nguyen, 28-Jan-2023.) |
| ⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ) | ||
| Theorem | 1t1e1ALT 42296 | Alternate proof of 1t1e1 12428 using a different set of axioms (add ax-mulrcl 11218, ax-i2m1 11223, ax-1ne0 11224, ax-rrecex 11227 and remove ax-resscn 11212, ax-mulcom 11219, ax-mulass 11221, ax-distr 11222). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (1 · 1) = 1 | ||
| Theorem | lttrii 42297 | 'Less than' is transitive. (Contributed by SN, 26-Aug-2025.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 𝐴 < 𝐵 & ⊢ 𝐵 < 𝐶 ⇒ ⊢ 𝐴 < 𝐶 | ||
| Theorem | remulcan2d 42298 | mulcan2d 11897 for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | readdridaddlidd 42299 | 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 11435, 𝐴 is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐵 + 𝐴) = 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) = 𝐶) | ||
| Theorem | sn-1ne2 42300 | A proof of 1ne2 12474 without using ax-mulcom 11219, ax-mulass 11221, ax-pre-mulgt0 11232. Based on mul02lem2 11438. (Contributed by SN, 13-Dec-2023.) |
| ⊢ 1 ≠ 2 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |