![]() |
Metamath
Proof Explorer Theorem List (p. 423 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | metakunt16 42201* | Construction of another permutation. (Contributed by metakunt, 25-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐹 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) ⇒ ⊢ (𝜑 → 𝐹:(𝐼...(𝑀 − 1))–1-1-onto→(1...(𝑀 − 𝐼))) | ||
Theorem | metakunt17 42202 | 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 42203 | Disjoint domains and codomains. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) ⇒ ⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) | ||
Theorem | metakunt19 42204* | 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 42205* | 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 42206* | 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 42207* | 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 42208* | 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 42209 | Technical condition such that metakunt17 42202 holds. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) ⇒ ⊢ (𝜑 → ((((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅ ∧ (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}) ∧ (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}))) | ||
Theorem | metakunt25 42210* | B is a permutation. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ≤ 𝑀) & ⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) ⇒ ⊢ (𝜑 → 𝐵:(1...𝑀)–1-1-onto→(1...𝑀)) | ||
Theorem | metakunt26 42211* | 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 42212* | 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 42213* | 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 42214* | 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 42215* | 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 42216* | 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 42217* | 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 42218* | 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 42219* | 𝐷 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 42220 | 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 42221* | Product split into two factors, original by Steven Nguyen. (Contributed by metakunt, 21-Apr-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 𝐾))) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...(𝑁 + 𝐾))𝐴 = (∏𝑘 ∈ (𝑀...𝑁)𝐴 · ∏𝑘 ∈ ((𝑁 + 1)...(𝑁 + 𝐾))𝐴)) | ||
Theorem | 2xp3dxp2ge1d 42222 | 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 42223 | A factorial with offset is monotonely increasing. (Contributed by metakunt, 20-Apr-2024.) |
⊢ (((𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℕ0 ∧ 𝑋 ≤ 𝑌) ∧ 𝑁 ∈ ℕ0) → (!‘(𝑋 + 𝑁)) ≤ (!‘(𝑌 + 𝑁))) | ||
Theorem | intnanrt 42224 | Introduction of conjunct inside of a contradiction. Would be used in elfvov1 7472. (Contributed by SN, 18-May-2025.) |
⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓)) | ||
Theorem | ioin9i8 42225 | Miscellaneous inference creating a biconditional from an implied converse implication. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ (𝜑 → (𝜓 ∨ 𝜒)) & ⊢ (𝜒 → ¬ 𝜃) & ⊢ (𝜓 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | jaodd 42226 | Double deduction form of jaoi 857. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) → 𝜃))) | ||
Theorem | syl3an12 42227 | A double syllogism inference. (Contributed by SN, 15-Sep-2024.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) | ||
Theorem | sbtd 42228* | A true statement is true upon substitution (deduction). A similar proof is possible for icht 47376. (Contributed by SN, 4-May-2024.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → [𝑡 / 𝑥]𝜓) | ||
Theorem | sbor2 42229 | One direction of sbor 2305, using fewer axioms. Compare 19.33 1881. (Contributed by Steven Nguyen, 18-Aug-2023.) |
⊢ (([𝑡 / 𝑥]𝜑 ∨ [𝑡 / 𝑥]𝜓) → [𝑡 / 𝑥](𝜑 ∨ 𝜓)) | ||
Theorem | sbalexi 42230* | Inference form of sbalex 2239, avoiding ax-10 2138 by using ax-gen 1791. (Contributed by SN, 12-Aug-2025.) |
⊢ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ⇒ ⊢ ∀𝑥(𝑥 = 𝑦 → 𝜑) | ||
Theorem | 19.9dev 42231* | 19.9d 2200 in the case of an existential quantifier, avoiding the ax-10 2138 from nfex 2322 that would be used for the hypothesis of 19.9d 2200, at the cost of an additional DV condition on 𝑦, 𝜑. (Contributed by SN, 26-May-2024.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑦𝜓)) | ||
Theorem | 3rspcedvd 42232* | Triple application of rspcedvd 3623. (Contributed by Steven Nguyen, 27-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (𝜒 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝑧 = 𝐶) → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 ∃𝑧 ∈ 𝐷 𝜓) | ||
Theorem | sn-axrep5v 42233* | A condensed form of axrep5 5292. (Contributed by SN, 21-Sep-2023.) |
⊢ (∀𝑤 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑)) | ||
Theorem | sn-axprlem3 42234* | axprlem3 5430 using only Tarski's FOL axiom schemes and ax-rep 5284. (Contributed by SN, 22-Sep-2023.) |
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 if-(𝜑, 𝑧 = 𝑎, 𝑧 = 𝑏)) | ||
Theorem | sn-exelALT 42235* | Alternate proof of exel 5443, avoiding ax-pr 5437 but requiring ax-5 1907, ax-9 2115, and ax-pow 5370. This is similar to how elALT2 5374 uses ax-pow 5370 instead of ax-pr 5437 compared to el 5447. (Contributed by SN, 18-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦 | ||
Theorem | ss2ab1 42236 | Class abstractions in a subclass relationship, closed form. One direction of ss2ab 4071 using fewer axioms. (Contributed by SN, 22-Dec-2024.) |
⊢ (∀𝑥(𝜑 → 𝜓) → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}) | ||
Theorem | ssabdv 42237* | Deduction of abstraction subclass from implication. (Contributed by SN, 22-Dec-2024.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ {𝑥 ∣ 𝜓}) | ||
Theorem | sn-iotalem 42238* | An unused lemma showing that many equivalences involving df-iota 6515 are potentially provable without ax-10 2138, ax-11 2154, ax-12 2174. (Contributed by SN, 6-Nov-2024.) |
⊢ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧 ∣ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧}} | ||
Theorem | sn-iotalemcor 42239* | Corollary of sn-iotalem 42238. Compare sb8iota 6526. (Contributed by SN, 6-Nov-2024.) |
⊢ (℩𝑥𝜑) = (℩𝑦{𝑥 ∣ 𝜑} = {𝑦}) | ||
Theorem | abbi1sn 42240* | Originally part of uniabio 6529. Convert a theorem about df-iota 6515 to one about dfiota2 6516, without ax-10 2138, ax-11 2154, ax-12 2174. Although, eu6 2571 uses ax-10 2138 and ax-12 2174. (Contributed by SN, 23-Nov-2024.) |
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → {𝑥 ∣ 𝜑} = {𝑦}) | ||
Theorem | brif2 42241 | Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.) |
⊢ (𝐶𝑅if(𝜑, 𝐴, 𝐵) ↔ if-(𝜑, 𝐶𝑅𝐴, 𝐶𝑅𝐵)) | ||
Theorem | brif12 42242 | Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.) |
⊢ (if(𝜑, 𝐴, 𝐵)𝑅if(𝜑, 𝐶, 𝐷) ↔ if-(𝜑, 𝐴𝑅𝐶, 𝐵𝑅𝐷)) | ||
Theorem | pssexg 42243 | The proper subset of a set is also a set. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) | ||
Theorem | pssn0 42244 | A proper superset is nonempty. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ (𝐴 ⊊ 𝐵 → 𝐵 ≠ ∅) | ||
Theorem | psspwb 42245 | Classes are proper subclasses if and only if their power classes are proper subclasses. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ (𝐴 ⊊ 𝐵 ↔ 𝒫 𝐴 ⊊ 𝒫 𝐵) | ||
Theorem | xppss12 42246 | Proper subset theorem for Cartesian product. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷) → (𝐴 × 𝐶) ⊊ (𝐵 × 𝐷)) | ||
Theorem | elpwbi 42247 | Membership in a power set, biconditional. (Contributed by Steven Nguyen, 17-Jul-2022.) (Proof shortened by Steven Nguyen, 16-Sep-2022.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵) | ||
Theorem | imaopab 42248* | The image of a class of ordered pairs. (Contributed by Steven Nguyen, 6-Jun-2023.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} | ||
Theorem | fnsnbt 42249 | A function's domain is a singleton iff the function is a singleton. (Contributed by Steven Nguyen, 18-Aug-2023.) |
⊢ (𝐴 ∈ V → (𝐹 Fn {𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉})) | ||
Theorem | fnimasnd 42250 | 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 42251 | Property of being the restriction of a function. Note that this is closer to funssres 6611 than fnssres 6691. (Contributed by SN, 11-Mar-2025.) |
⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑅 = (𝐹 ↾ 𝐴) ↔ (𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹))) | ||
Theorem | f1o2d2 42252* | 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 42253* | Composition of two functions. Variation of fmpoco 8118 with more context in the substitution hypothesis for 𝑇. (Contributed by SN, 14-Mar-2025.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) | ||
Theorem | ovmpogad 42254* | Value of an operation given by a maps-to rule. Deduction form of ovmpoga 7586. (Contributed by SN, 14-Mar-2025.) |
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ofun 42255 | 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 42256* | Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ (𝐴 / 𝑅) = ran (𝑥 ∈ 𝐴 ↦ [𝑥]𝑅) | ||
Theorem | dfqs3 42257* | Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ (𝐴 / 𝑅) = ∪ 𝑥 ∈ 𝐴 {[𝑥]𝑅} | ||
Theorem | qseq12d 42258 | Equality theorem for quotient set, deduction form. (Contributed by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐷)) | ||
Theorem | qsalrel 42259* | 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 42260 | A restricted mapping is a mapping. EDITORIAL: Could be used to shorten elpm2r 8883 with some reordering involving mapsspm 8914. (Contributed by SN, 11-Mar-2025.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m 𝐶)) & ⊢ (𝜑 → 𝐷 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑m 𝐷)) | ||
Theorem | supinf 42261* | The supremum is the infimum of the upper bounds. (Contributed by SN, 29-Jun-2025.) |
⊢ (𝜑 → < Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐵 𝑦 < 𝑧))) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, < ) = inf({𝑥 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤}, 𝐴, < )) | ||
Theorem | mapcod 42262 | Compose two mappings. (Contributed by SN, 11-Mar-2025.) |
⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑m 𝐵)) & ⊢ (𝜑 → 𝐺 ∈ (𝐵 ↑m 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (𝐴 ↑m 𝐶)) | ||
Theorem | fisdomnn 42263 | A finite set is dominated by the set of natural numbers. (Contributed by SN, 6-Jul-2025.) |
⊢ (𝐴 ∈ Fin → 𝐴 ≺ ℕ) | ||
Theorem | ltex 42264 | The less-than relation is a set. (Contributed by SN, 5-Jun-2025.) |
⊢ < ∈ V | ||
Theorem | leex 42265 | The less-than-or-equal-to relation is a set. (Contributed by SN, 5-Jun-2025.) |
⊢ ≤ ∈ V | ||
Theorem | subex 42266 | The subtraction operation is a set. (Contributed by SN, 5-Jun-2025.) |
⊢ − ∈ V | ||
Theorem | absex 42267 | The absolute value function is a set. (Contributed by SN, 5-Jun-2025.) |
⊢ abs ∈ V | ||
Theorem | cjex 42268 | The conjugate function is a set. (Contributed by SN, 5-Jun-2025.) |
⊢ ∗ ∈ V | ||
Theorem | fzosumm1 42269* | Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023.) |
⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = (𝑁 − 1) → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝐴 = (Σ𝑘 ∈ (𝑀..^(𝑁 − 1))𝐴 + 𝐵)) | ||
Theorem | ccatcan2d 42270 | 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 11222 is used in mulrid 11256 related theorems, so one could trade off the extra axioms in mulrid 11256 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 11209; in the other direction, real number closure laws can be avoided by using ax-resscn 11209 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 11217, ax-1cn 11210, and ax-addcl 11212. (And in practice, the expression isn't fully expanded into ones.) Multiplication by 1 requires either mullidi 11263 or (ax-1rid 11222 and 1re 11258) as seen in 1t1e1 12425 and 1t1e1ALT 42274. Multiplying with greater natural numbers uses ax-distr 11219. 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 11216 (see readdrid 42415 and readdlid 42409). | ||
Theorem | c0exALT 42271 | Alternate proof of c0ex 11252 using more set theory axioms but fewer complex number axioms (add ax-10 2138, ax-11 2154, ax-13 2374, ax-nul 5311, and remove ax-1cn 11210, ax-icn 11211, ax-addcl 11212, and ax-mulcl 11214). (Contributed by Steven Nguyen, 4-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ V | ||
Theorem | 0cnALT3 42272 | Alternate proof of 0cn 11250 using ax-resscn 11209, ax-addrcl 11213, ax-rnegex 11223, ax-cnre 11225 instead of ax-icn 11211, ax-addcl 11212, ax-mulcl 11214, ax-i2m1 11220. Version of 0cnALT 11493 using ax-1cn 11210 instead of ax-icn 11211. (Contributed by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ ℂ | ||
Theorem | elre0re 42273 | Specialized version of 0red 11261 without using ax-1cn 11210 and ax-cnre 11225. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ) | ||
Theorem | 1t1e1ALT 42274 | Alternate proof of 1t1e1 12425 using a different set of axioms (add ax-mulrcl 11215, ax-i2m1 11220, ax-1ne0 11221, ax-rrecex 11224 and remove ax-resscn 11209, ax-mulcom 11216, ax-mulass 11218, ax-distr 11219). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (1 · 1) = 1 | ||
Theorem | lttrii 42275 | 'Less than' is transitive. (Contributed by SN, 26-Aug-2025.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 𝐴 < 𝐵 & ⊢ 𝐵 < 𝐶 ⇒ ⊢ 𝐴 < 𝐶 | ||
Theorem | remulcan2d 42276 | mulcan2d 11894 for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | readdridaddlidd 42277 | 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 11432, 𝐴 is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐵 + 𝐴) = 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) = 𝐶) | ||
Theorem | sn-1ne2 42278 | A proof of 1ne2 12471 without using ax-mulcom 11216, ax-mulass 11218, ax-pre-mulgt0 11229. Based on mul02lem2 11435. (Contributed by SN, 13-Dec-2023.) |
⊢ 1 ≠ 2 | ||
Theorem | nnn1suc 42279* | A positive integer that is not 1 is a successor of some other positive integer. (Contributed by Steven Nguyen, 19-Aug-2023.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ≠ 1) → ∃𝑥 ∈ ℕ (𝑥 + 1) = 𝐴) | ||
Theorem | nnadd1com 42280 | Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) = (1 + 𝐴)) | ||
Theorem | nnaddcom 42281 | Addition is commutative for natural numbers. Uses fewer axioms than addcom 11444. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | nnaddcomli 42282 | Version of addcomli 11450 for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ (𝐵 + 𝐴) = 𝐶 | ||
Theorem | nnadddir 42283 | Right-distributivity for natural numbers without ax-mulcom 11216. (Contributed by SN, 5-Feb-2024.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | nnmul1com 42284 | Multiplication with 1 is commutative for natural numbers, without ax-mulcom 11216. Since (𝐴 · 1) is 𝐴 by ax-1rid 11222, this is equivalent to remullid 42439 for natural numbers, but using fewer axioms (avoiding ax-resscn 11209, ax-addass 11217, ax-mulass 11218, ax-rnegex 11223, ax-pre-lttri 11226, ax-pre-lttrn 11227, ax-pre-ltadd 11228). (Contributed by SN, 5-Feb-2024.) |
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1)) | ||
Theorem | nnmulcom 42285 | Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | readdrcl2d 42286 | Reverse closure for addition: the second addend is real if the first addend is real and the sum is real. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ∈ ℝ) | ||
Theorem | mvrrsubd 42287 |
Move a subtraction in the RHS to a right-addition in the LHS. Converse
of mvlraddd 11670.
EDITORIAL: Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶)) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) = 𝐵) | ||
Theorem | laddrotrd 42288 |
Rotate the variables right in an equation with addition on the left,
converting it into a subtraction. Version of mvlladdd 11671 with a commuted
consequent, and of mvrladdd 11673 with a commuted hypothesis.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: ply1dg3rt0irred 33586. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐶 − 𝐴) = 𝐵) | ||
Theorem | raddswap12d 42289 |
Swap the first two variables in an equation with addition on the right,
converting it into a subtraction. Version of mvrraddd 11672 with a commuted
consequent, and of mvlraddd 11670 with a commuted hypothesis.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = (𝐴 − 𝐶)) | ||
Theorem | lsubrotld 42290 |
Rotate the variables left in an equation with subtraction on the left,
converting it into an addition.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐵 + 𝐶) = 𝐴) | ||
Theorem | rsubrotld 42291 |
Rotate the variables left in an equation with subtraction on the right,
converting it into an addition.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 4-Jul-2025.) |
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 + 𝐴)) | ||
Theorem | lsubswap23d 42292 |
Swap the second and third variables in an equation with subtraction on
the left, converting it into an addition.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 23-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = 𝐵) | ||
Theorem | addsubeq4com 42293 | Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵))) | ||
Theorem | sqsumi 42294 | A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵))) | ||
Theorem | negn0nposznnd 42295 | Lemma for dffltz 42620. (Contributed by Steven Nguyen, 27-Feb-2023.) |
⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → ¬ 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℕ) | ||
Theorem | sqmid3api 42296 | Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝑁 ∈ ℂ & ⊢ (𝐴 + 𝑁) = 𝐵 & ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁)) | ||
Theorem | decaddcom 42297 | Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵) | ||
Theorem | sqn5i 42298 | The square of a number ending in 5. This shortcut only works because 5 is half of 10. (Contributed by Steven Nguyen, 16-Sep-2022.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (;𝐴5 · ;𝐴5) = ;;(𝐴 · (𝐴 + 1))25 | ||
Theorem | sqn5ii 42299 | The square of a number ending in 5. This shortcut only works because 5 is half of 10. (Contributed by Steven Nguyen, 16-Sep-2022.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ (𝐴 + 1) = 𝐵 & ⊢ (𝐴 · 𝐵) = 𝐶 ⇒ ⊢ (;𝐴5 · ;𝐴5) = ;;𝐶25 | ||
Theorem | decpmulnc 42300 | Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11711. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐸 & ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹 & ⊢ (𝐵 · 𝐷) = 𝐺 ⇒ ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐸𝐹𝐺 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |