HomeTheorem List (p. 422 of 489)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 422 of 489) | < 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: | Metamath Proof Explorer
(1-30950) |
Hilbert Space Explorer
(30951-32473) |
Users' Mathboxes
(32474-48899) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 2np3bcnp1 42101 | Part of induction step for 2ap1caineq 42102. (Contributed by metakunt, 8-Jun-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (((2 · (𝑁 + 1)) + 1)C(𝑁 + 1)) = ((((2 · 𝑁) + 1)C𝑁) · (2 · (((2 · 𝑁) + 3) / (𝑁 + 2))))) | ||
| Theorem | 2ap1caineq 42102 | Inequality for Theorem 6.6 for AKS. (Contributed by metakunt, 8-Jun-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 2 ≤ 𝑁) ⇒ ⊢ (𝜑 → (2↑(𝑁 + 1)) < (((2 · 𝑁) + 1)C𝑁)) | ||
| Theorem | sticksstones1 42103* | 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 42104* | 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 42105* | 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 42106* | Equinumerosity lemma for sticks and stones. (Contributed by metakunt, 28-Sep-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾} & ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ⇒ ⊢ (𝜑 → 𝐴 ≈ 𝐵) | ||
| Theorem | sticksstones5 42107* | 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 42108* | 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 42109* | 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 42110* | 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 42111* | 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 42112* | 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 42113* | 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 42114* | 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 42115* | 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 42116* | 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 42117* | 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 42118* | 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 42119* | Sticks and stones with collapsed definitions for positive integers. (Contributed by metakunt, 20-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1))) | ||
| Theorem | sticksstones17 42120* | 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 42121* | 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 42122* | 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 42123* | 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 42124* | Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakunt, 24-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 𝑁)} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) | ||
| Theorem | sticksstones22 42125* | Non-exhaustive sticks and stones. (Contributed by metakunt, 26-Oct-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆))) | ||
| Theorem | sticksstones23 42126* | Non-exhaustive sticks and stones. (Contributed by metakunt, 7-May-2025.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ 𝐴 = {𝑓 ∈ (ℕ0 ↑m 𝑆) ∣ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁} ⇒ ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆))) | ||
| Theorem | aks6d1c6lem1 42127* | Lemma for claim 6, deduce exact degree of the polynomial. (Contributed by metakunt, 7-May-2025.) |
| ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐴 < 𝑃) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐻 = (ℎ ∈ (ℕ0 ↑m (0...𝐴)) ↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) & ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) & ⊢ 𝑆 = {𝑠 ∈ (ℕ0 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} & ⊢ (𝜑 → 𝑈 ∈ (ℕ0 ↑m (0...𝐴))) ⇒ ⊢ (𝜑 → ((deg1‘𝐾)‘(𝐺‘𝑈)) = Σ𝑡 ∈ (0...𝐴)(𝑈‘𝑡)) | ||
| Theorem | aks6d1c6lem2 42128* | Every primitive root is root of G(u)-G(v). (Contributed by metakunt, 8-May-2025.) |
| ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐴 < 𝑃) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐻 = (ℎ ∈ (ℕ0 ↑m (0...𝐴)) ↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) & ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) & ⊢ 𝑆 = {𝑠 ∈ (ℕ0 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑉 ∈ 𝑆) & ⊢ (𝜑 → ((𝐻 ↾ 𝑆)‘𝑈) = ((𝐻 ↾ 𝑆)‘𝑉)) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ 𝐽 = (𝑗 ∈ (ℕ0 × ℕ0) ↦ ((𝐸‘𝑗)(.g‘(mulGrp‘𝐾))𝑀)) & ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ≤ (♯‘(𝐽 “ (ℕ0 × ℕ0)))) ⇒ ⊢ (𝜑 → 𝐷 ≤ (♯‘(◡((eval1‘𝐾)‘((𝐺‘𝑈)(-g‘(Poly1‘𝐾))(𝐺‘𝑉))) “ {(0g‘𝐾)}))) | ||
| Theorem | aks6d1c6lem3 42129* | Claim 6 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf TODO, eliminate hypothesis. (Contributed by metakunt, 8-May-2025.) |
| ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → 𝐴 < 𝑃) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐻 = (ℎ ∈ (ℕ0 ↑m (0...𝐴)) ↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) & ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) & ⊢ 𝑆 = {𝑠 ∈ (ℕ0 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} & ⊢ 𝐽 = (𝑗 ∈ (ℕ0 × ℕ0) ↦ ((𝐸‘𝑗)(.g‘(mulGrp‘𝐾))𝑀)) & ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ≤ (♯‘(𝐽 “ (ℕ0 × ℕ0)))) ⇒ ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ0 ↑m (0...𝐴))))) | ||
| Theorem | aks6d1c6lem4 42130* | Claim 6 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf Add hypothesis on coprimality, lift function to the integers so that group operations may be applied. Inline definition. (Contributed by metakunt, 14-May-2025.) |
| ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐻 = (ℎ ∈ (ℕ0 ↑m (0...𝐴)) ↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) & ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) & ⊢ 𝑆 = {𝑠 ∈ (ℕ0 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} & ⊢ 𝐽 = (𝑗 ∈ ℤ ↦ (𝑗(.g‘((mulGrp‘𝐾) ↾s 𝑈))𝑀)) & ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ≤ (♯‘(𝐽 “ (𝐸 “ (ℕ0 × ℕ0))))) & ⊢ 𝑈 = {𝑚 ∈ (Base‘(mulGrp‘𝐾)) ∣ ∃𝑛 ∈ (Base‘(mulGrp‘𝐾))(𝑛(+g‘(mulGrp‘𝐾))𝑚) = (0g‘(mulGrp‘𝐾))} ⇒ ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ0 ↑m (0...𝐴))))) | ||
| Theorem | aks6d1c6isolem1 42131* | Lemma to construct the map out of the quotient for AKS. (Contributed by metakunt, 14-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥(.g‘(𝑅 ↾s 𝑈))𝑀)) & ⊢ (𝜑 → 𝑀 ∈ (𝑅 PrimRoots 𝐾)) ⇒ ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ↾s ran 𝐹) ∈ Grp) | ||
| Theorem | aks6d1c6isolem2 42132* | Lemma to construct the group homomorphism for the AKS Theorem. (Contributed by metakunt, 14-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥(.g‘(𝑅 ↾s 𝑈))𝑀)) & ⊢ (𝜑 → 𝑀 ∈ (𝑅 PrimRoots 𝐾)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (ℤring GrpHom ((𝑅 ↾s 𝑈) ↾s ran 𝐹))) | ||
| Theorem | aks6d1c6isolem3 42133* | The preimage of a map sending a primitive root to its powers of zero is equal to the set of integers that divide 𝑅. (Contributed by metakunt, 15-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥(.g‘(𝑅 ↾s 𝑈))𝑀)) & ⊢ (𝜑 → 𝑀 ∈ (𝑅 PrimRoots 𝐾)) & ⊢ 𝑆 = (RSpan‘ℤring) ⇒ ⊢ (𝜑 → (𝑆‘{𝐾}) = (◡𝐹 “ {(0g‘(𝑅 ↾s 𝑈))})) | ||
| Theorem | aks6d1c6lem5 42134* | Eliminate the size hypothesis. Claim 6. (Contributed by metakunt, 15-May-2025.) |
| ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐻 = (ℎ ∈ (ℕ0 ↑m (0...𝐴)) ↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) & ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) & ⊢ 𝑆 = {𝑠 ∈ (ℕ0 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} & ⊢ 𝐽 = (𝑗 ∈ ℤ ↦ (𝑗(.g‘((mulGrp‘𝐾) ↾s 𝑈))𝑀)) & ⊢ 𝑈 = {𝑚 ∈ (Base‘(mulGrp‘𝐾)) ∣ ∃𝑛 ∈ (Base‘(mulGrp‘𝐾))(𝑛(+g‘(mulGrp‘𝐾))𝑚) = (0g‘(mulGrp‘𝐾))} & ⊢ 𝑋 = (𝑏 ∈ (Base‘(ℤring /s (ℤring ~QG (◡𝐽 “ {(0g‘(((mulGrp‘𝐾) ↾s 𝑈) ↾s ran 𝐽))})))) ↦ ∪ (𝐽 “ 𝑏)) ⇒ ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ0 ↑m (0...𝐴))))) | ||
| Theorem | bcled 42135 | Inequality for binomial coefficients. (Contributed by metakunt, 12-May-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴C𝐶) ≤ (𝐵C𝐶)) | ||
| Theorem | bcle2d 42136 | Inequality for binomial coefficients. (Contributed by metakunt, 12-May-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) & ⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐷 ≤ 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶)C(𝐴 + 𝐷)) ≤ ((𝐵 + 𝐶)C(𝐵 + 𝐷))) | ||
| Theorem | aks6d1c7lem1 42137* | The last set of inequalities of Claim 7 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf. (Contributed by metakunt, 12-May-2025.) |
| ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) ⇒ ⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) < ((𝐷 + 𝐴)C(𝐷 − 1))) | ||
| Theorem | aks6d1c7lem2 42138* | Contradiction to Claim 2 and Claim 7. We assumed in Claim 2 that there are two different prime numbers 𝑃 and 𝑄. (Contributed by metakunt, 16-May-2025.) |
| ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) & ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅)) & ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐻 = (ℎ ∈ (ℕ0 ↑m (0...𝐴)) ↦ (((eval1‘𝐾)‘(𝐺‘ℎ))‘𝑀)) & ⊢ 𝐵 = (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) & ⊢ 𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵))) & ⊢ (𝜑 → (𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁)) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ 𝐺 = (𝑔 ∈ (ℕ0 ↑m (0...𝐴)) ↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ 𝑆 = {𝑠 ∈ (ℕ0 ↑m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⇒ ⊢ (𝜑 → 𝑃 = 𝑄) | ||
| Theorem | aks6d1c7lem3 42139* | Remove lots of hypotheses now that we have the AKS contradiction. (Contributed by metakunt, 16-May-2025.) |
| ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) & ⊢ (𝜑 → (𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁)) ⇒ ⊢ (𝜑 → 𝑃 = 𝑄) | ||
| Theorem | aks6d1c7lem4 42140* | In the AKS algorithm there exists a unique prime number 𝑝 that divides 𝑁. (Contributed by metakunt, 16-May-2025.) |
| ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) ⇒ ⊢ (𝜑 → ∃!𝑝 ∈ ℙ 𝑝 ∥ 𝑁) | ||
| Theorem | aks6d1c7 42141* | 𝑁 is a prime power if the hypotheses of the AKS algorithm hold. Claim 7 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf. (Contributed by metakunt, 16-May-2025.) |
| ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) ⇒ ⊢ (𝜑 → 𝑁 = (𝑃↑(𝑃 pCnt 𝑁))) | ||
| Theorem | rhmqusspan 42142* | Ring homomorphism out of a quotient given an ideal spanned by a singleton. (Contributed by metakunt, 7-Jun-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) & ⊢ (𝜑 → 𝐺 ∈ CRing) & ⊢ 𝑁 = ((RSpan‘𝐺)‘{𝑋}) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐺)) & ⊢ (𝜑 → (𝐹‘𝑋) = 0 ) ⇒ ⊢ (𝜑 → (𝐽 ∈ (𝑄 RingHom 𝐻) ∧ ∀𝑔 ∈ (Base‘𝐺)(𝐽‘[𝑔](𝐺 ~QG 𝑁)) = (𝐹‘𝑔))) | ||
| Theorem | aks5lem1 42143* | Section 5 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf. Construction of a ring homomorphism out of Zn X to K. (Contributed by metakunt, 7-Jun-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁)) & ⊢ 𝐹 = (𝑝 ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁))) ↦ (𝐺 ∘ 𝑝)) & ⊢ 𝐺 = (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞)) & ⊢ 𝐻 = (𝑟 ∈ (Base‘(Poly1‘𝐾)) ↦ (((eval1‘𝐾)‘𝑟)‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾)) ⇒ ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ ((Poly1‘(ℤ/nℤ‘𝑁)) RingHom 𝐾)) | ||
| Theorem | aks5lem2 42144* | Lemma for section 5 https://www3.nd.edu/%7eandyp/notes/AKS.pdf. Construct the quotient for the AKS reduction. (Contributed by metakunt, 7-Jun-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁)) & ⊢ 𝐹 = (𝑝 ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁))) ↦ (𝐺 ∘ 𝑝)) & ⊢ 𝐺 = (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞)) & ⊢ 𝐻 = (𝑟 ∈ (Base‘(Poly1‘𝐾)) ↦ (((eval1‘𝐾)‘𝑟)‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐼 = (𝑠 ∈ (Base‘𝐴) ↦ ∪ ((𝐻 ∘ 𝐹) “ 𝑠)) & ⊢ 𝐴 = ((Poly1‘(ℤ/nℤ‘𝑁)) /s ((Poly1‘(ℤ/nℤ‘𝑁)) ~QG 𝐿)) & ⊢ 𝐿 = ((RSpan‘(Poly1‘(ℤ/nℤ‘𝑁)))‘{((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))}) & ⊢ (𝜑 → 𝑅 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐼 ∈ (𝐴 RingHom 𝐾) ∧ ∀𝑔 ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝐼‘[𝑔]((Poly1‘(ℤ/nℤ‘𝑁)) ~QG 𝐿)) = ((𝐻 ∘ 𝐹)‘𝑔))) | ||
| Theorem | ply1asclzrhval 42145 | Transfer results from algebraic scalars and ZR ring homomorphisms. (Contributed by metakunt, 17-Jun-2025.) |
| ⊢ 𝑊 = (Poly1‘𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐵 = (ℤRHom‘𝑊) & ⊢ 𝐶 = (ℤRHom‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴‘(𝐶‘𝑋)) = (𝐵‘𝑋)) | ||
| Theorem | aks5lem3a 42146* | Lemma for AKS section 5. (Contributed by metakunt, 17-Jun-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁)) & ⊢ 𝐵 = (𝑆 /s (𝑆 ~QG 𝐿)) & ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(-g‘𝑆)(1r‘𝑆))}) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁)) & ⊢ 𝐹 = (𝑝 ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁))) ↦ (𝐺 ∘ 𝑝)) & ⊢ 𝐺 = (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞)) & ⊢ 𝐻 = (𝑟 ∈ (Base‘(Poly1‘𝐾)) ↦ (((eval1‘𝐾)‘𝑟)‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ 𝐼 = (𝑠 ∈ (Base‘𝐵) ↦ ∪ ((𝐻 ∘ 𝐹) “ 𝑠)) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → [(𝑁(.g‘(mulGrp‘𝑆))((var1‘(ℤ/nℤ‘𝑁))(+g‘𝑆)((algSc‘𝑆)‘((ℤRHom‘(ℤ/nℤ‘𝑁))‘𝐴))))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(+g‘𝑆)((algSc‘𝑆)‘((ℤRHom‘(ℤ/nℤ‘𝑁))‘𝐴)))](𝑆 ~QG 𝐿)) ⇒ ⊢ (𝜑 → (𝑁(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝐴))))‘𝑀)) = (((eval1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑁(.g‘(mulGrp‘𝐾))𝑀))) | ||
| Theorem | aks5lem4a 42147* | Lemma for AKS section 5, reduce hypotheses. (Contributed by metakunt, 17-Jun-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁)) & ⊢ 𝐵 = (𝑆 /s (𝑆 ~QG 𝐿)) & ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(-g‘𝑆)(1r‘𝑆))}) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → [(𝑁(.g‘(mulGrp‘𝑆))((var1‘(ℤ/nℤ‘𝑁))(+g‘𝑆)((algSc‘𝑆)‘((ℤRHom‘(ℤ/nℤ‘𝑁))‘𝐴))))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(+g‘𝑆)((algSc‘𝑆)‘((ℤRHom‘(ℤ/nℤ‘𝑁))‘𝐴)))](𝑆 ~QG 𝐿)) ⇒ ⊢ (𝜑 → (𝑁(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝐴))))‘𝑀)) = (((eval1‘𝐾)‘((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑁(.g‘(mulGrp‘𝐾))𝑀))) | ||
| Theorem | aks5lem5a 42148* | Lemma for AKS, section 5, connect to Theorem 6.1. (Contributed by metakunt, 17-Jun-2025.) |
| ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁)) & ⊢ 𝐵 = (𝑆 /s (𝑆 ~QG 𝐿)) & ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(-g‘𝑆)(1r‘𝑆))}) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))((var1‘(ℤ/nℤ‘𝑁))(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿)) ⇒ ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) | ||
| Theorem | aks5lem6 42149* | Connect results of section 5 and Theorem 6.1 AKS. (Contributed by metakunt, 25-Jun-2025.) |
| ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} & ⊢ 𝑃 = (chr‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Field) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑅 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) & ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) & ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁)) & ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) & ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) & ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁)) & ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))(var1‘(ℤ/nℤ‘𝑁)))(-g‘𝑆)(1r‘𝑆))}) & ⊢ 𝑋 = (var1‘(ℤ/nℤ‘𝑁)) & ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))(𝑋(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))𝑋)(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿)) ⇒ ⊢ (𝜑 → 𝑁 = (𝑃↑(𝑃 pCnt 𝑁))) | ||
| Theorem | indstrd 42150* | Strong induction, deduction version. (Contributed by Steven Nguyen, 13-Jul-2025.) |
| ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ ∧ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜒)) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝜃) | ||
| Theorem | grpods 42151* | Relate sums of elements of orders and roots of unity. (Contributed by metakunt, 14-Jul-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ {𝑚 ∈ (1...𝑁) ∣ 𝑚 ∥ 𝑁} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ (𝑁 ↑ 𝑥) = (0g‘𝐺)})) | ||
| Theorem | unitscyglem1 42152* | Lemma for unitscyg. (Contributed by metakunt, 13-Jul-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) = ((od‘𝐺)‘𝐴)) | ||
| Theorem | unitscyglem2 42153* | Lemma for unitscyg. (Contributed by metakunt, 13-Jul-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ((od‘𝐺)‘𝐴) = 𝐷) & ⊢ (𝜑 → ∀𝑐 ∈ ℕ (𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ⇒ ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)) | ||
| Theorem | unitscyglem3 42154* | Lemma for unitscyg. (Contributed by metakunt, 14-Jul-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛) ⇒ ⊢ (𝜑 → ∀𝑑 ∈ ℕ ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))) | ||
| Theorem | unitscyglem4 42155* | Lemma for unitscyg (Contributed by metakunt, 14-Jul-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵)) ⇒ ⊢ (𝜑 → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷)) | ||
| Theorem | unitscyglem5 42156 | Lemma for unitscyg (Contributed by metakunt, 9-Aug-2025.) |
| ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → (Base‘𝑅) ∈ Fin) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∥ (♯‘(Base‘𝐺))) ⇒ ⊢ (𝜑 → ((mulGrp‘𝑅) PrimRoots 𝐷) ≠ ∅) | ||
| Theorem | aks5lem7 42157* | Lemma for aks5. We clean up the hypotheses compared to aks5lem6 42149. (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 42158* | 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 42159* | Existence axiom for finite fields, eventually we want to construct them. (Contributed by metakunt, 13-Jul-2025.) |
| ⊢ ∀𝑝 ∈ ℙ ∀𝑛 ∈ ℕ ∃𝑘 ∈ Field ((♯‘(Base‘𝑘)) = (𝑝↑𝑛) ∧ (chr‘𝑘) = 𝑝) | ||
| Theorem | exfinfldd 42160* | 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 42161* | 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 42159, 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 42162* | A is an endomapping. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) ⇒ ⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀)) | ||
| Theorem | metakunt2 42163* | A is an endomapping. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)))) ⇒ ⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀)) | ||
| Theorem | metakunt3 42164* | Value of A. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)))) | ||
| Theorem | metakunt4 42165* | Value of A. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐴‘𝑋) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)))) | ||
| Theorem | metakunt5 42166* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 = 𝐼) → (𝐶‘(𝐴‘𝑋)) = 𝑋) | ||
| Theorem | metakunt6 42167* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐶‘(𝐴‘𝑋)) = 𝑋) | ||
| Theorem | metakunt7 42168* | 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 42169* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐶‘(𝐴‘𝑋)) = 𝑋) | ||
| Theorem | metakunt9 42170* | C is the left inverse for A. (Contributed by metakunt, 24-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐶‘(𝐴‘𝑋)) = 𝑋) | ||
| Theorem | metakunt10 42171* | C is the right inverse for A. (Contributed by metakunt, 24-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 = 𝑀) → (𝐴‘(𝐶‘𝑋)) = 𝑋) | ||
| Theorem | metakunt11 42172* | C is the right inverse for A. (Contributed by metakunt, 24-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 < 𝐼) → (𝐴‘(𝐶‘𝑋)) = 𝑋) | ||
| Theorem | metakunt12 42173* | C is the right inverse for A. (Contributed by metakunt, 25-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ ((𝜑 ∧ ¬ (𝑋 = 𝑀 ∨ 𝑋 < 𝐼)) → (𝐴‘(𝐶‘𝑋)) = 𝑋) | ||
| Theorem | metakunt13 42174* | C is the right inverse for A. (Contributed by metakunt, 25-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) & ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝐴‘(𝐶‘𝑋)) = 𝑋) | ||
| Theorem | metakunt14 42175* | 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 42176* | Construction of another permutation. (Contributed by metakunt, 25-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐹 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ⇒ ⊢ (𝜑 → 𝐹:(1...(𝐼 − 1))–1-1-onto→(((𝑀 − 𝐼) + 1)...(𝑀 − 1))) | ||
| Theorem | metakunt16 42177* | Construction of another permutation. (Contributed by metakunt, 25-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐹 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) ⇒ ⊢ (𝜑 → 𝐹:(𝐼...(𝑀 − 1))–1-1-onto→(1...(𝑀 − 𝐼))) | ||
| Theorem | metakunt17 42178 | 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 42179 | Disjoint domains and codomains. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) ⇒ ⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) | ||
| Theorem | metakunt19 42180* | 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 42181* | 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 42182* | 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 42183* | 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 42184* | 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 42185 | Technical condition such that metakunt17 42178 holds. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) ⇒ ⊢ (𝜑 → ((((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅ ∧ (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}) ∧ (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}))) | ||
| Theorem | metakunt25 42186* | B is a permutation. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) ⇒ ⊢ (𝜑 → 𝐵:(1...𝑀)–1-1-onto→(1...𝑀)) | ||
| Theorem | metakunt26 42187* | 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 42188* | 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 42189* | 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 42190* | 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 42191* | 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 42192* | 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 42193* | 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 42194* | 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 42195* | 𝐷 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 42196 | 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 42197* | Product split into two factors, original by Steven Nguyen. (Contributed by metakunt, 21-Apr-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 𝐾))) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...(𝑁 + 𝐾))𝐴 = (∏𝑘 ∈ (𝑀...𝑁)𝐴 · ∏𝑘 ∈ ((𝑁 + 1)...(𝑁 + 𝐾))𝐴)) | ||
| Theorem | 2xp3dxp2ge1d 42198 | 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 42199 | A factorial with offset is monotonely increasing. (Contributed by metakunt, 20-Apr-2024.) |
| ⊢ (((𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℕ0 ∧ 𝑋 ≤ 𝑌) ∧ 𝑁 ∈ ℕ0) → (!‘(𝑋 + 𝑁)) ≤ (!‘(𝑌 + 𝑁))) | ||
| Theorem | intnanrt 42200 | Introduction of conjunct inside of a contradiction. Would be used in elfvov1 7490. (Contributed by SN, 18-May-2025.) |
| ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |