Home | Metamath
Proof Explorer Theorem List (p. 391 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fnimasnd 39001 | 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 | dfqs2 39002* | Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ (𝐴 / 𝑅) = ran (𝑥 ∈ 𝐴 ↦ [𝑥]𝑅) | ||
Theorem | dfqs3 39003* | Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ (𝐴 / 𝑅) = ∪ 𝑥 ∈ 𝐴 {[𝑥]𝑅} | ||
Theorem | qseq12d 39004 | Equality theorem for quotient set, deduction form. (Contributed by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐷)) | ||
Theorem | qsalrel 39005* | The quotient set is equal to the singleton of 𝐴 when all elements are related and 𝐴 is a nonempty set. (Contributed by Steven Nguyen, 8-Jun-2023.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∼ 𝑦) & ⊢ (𝜑 → ∼ Er 𝐴) & ⊢ (𝜑 → 𝑁 ∈ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 / ∼ ) = {𝐴}) | ||
Theorem | fzosumm1 39006* | Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023.) |
⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = (𝑁 − 1) → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝐴 = (Σ𝑘 ∈ (𝑀..^(𝑁 − 1))𝐴 + 𝐵)) | ||
Theorem | ccatcan2d 39007 | Cancellation law for concatenation. (Contributed by SN, 6-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ Word 𝑉) & ⊢ (𝜑 → 𝐵 ∈ Word 𝑉) & ⊢ (𝜑 → 𝐶 ∈ Word 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 ++ 𝐶) = (𝐵 ++ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | nelsubginvcld 39008 | The inverse of a non-subgroup-member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023.) |
⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑆)) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝜑 → (𝑁‘𝑋) ∈ (𝐵 ∖ 𝑆)) | ||
Theorem | nelsubgcld 39009 | A non-subgroup-member plus a subgroup member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023.) |
⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑆)) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐵 ∖ 𝑆)) | ||
Theorem | nelsubgsubcld 39010 | A non-subgroup-member minus a subgroup member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023.) |
⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑆)) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝐵 ∖ 𝑆)) | ||
Theorem | rnasclg 39011 | The set of injected scalars is also interpretable as the span of the identity. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 1 = (1r‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) → ran 𝐴 = (𝑁‘{ 1 })) | ||
Theorem | selvval2lem1 39012 | 𝑇 is an associative algebra. For simplicity, 𝐼 stands for (𝐼 ∖ 𝐽) and we have 𝐽 ∈ 𝑊 instead of 𝐽 ⊆ 𝐼. (Contributed by SN, 15-Dec-2023.) |
⊢ 𝑈 = (𝐼 mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑇 ∈ AssAlg) | ||
Theorem | selvval2lem2 39013 | 𝐷 is a ring homomorphism. (Contributed by SN, 15-Dec-2023.) |
⊢ 𝑈 = (𝐼 mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝐷 ∈ (𝑅 RingHom 𝑇)) | ||
Theorem | selvval2lem3 39014 | The third argument passed to evalSub is in the domain. (Contributed by SN, 15-Dec-2023.) |
⊢ 𝑈 = (𝐼 mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → ran 𝐷 ∈ (SubRing‘𝑇)) | ||
Theorem | selvval2lemn 39015 | A lemma to illustrate the purpose of selvval2lem3 39014 and the value of 𝑄. Will be renamed in the future when this section is moved to main. (Contributed by SN, 5-Nov-2023.) |
⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ 𝑄 = ((𝐼 evalSub 𝑇)‘ran 𝐷) & ⊢ 𝑊 = (𝐼 mPoly 𝑆) & ⊢ 𝑆 = (𝑇 ↾s ran 𝐷) & ⊢ 𝑋 = (𝑇 ↑s (𝐵 ↑m 𝐼)) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) ⇒ ⊢ (𝜑 → 𝑄 ∈ (𝑊 RingHom 𝑋)) | ||
Theorem | selvval2lem4 39016 | The fourth argument passed to evalSub is in the domain (a polynomial in (𝐼 mPoly (𝐽 mPoly ((𝐼 ∖ 𝐽) mPoly 𝑅)))). (Contributed by SN, 5-Nov-2023.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ 𝑆 = (𝑇 ↾s ran 𝐷) & ⊢ 𝑊 = (𝐼 mPoly 𝑆) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷 ∘ 𝐹) ∈ 𝑋) | ||
Theorem | selvval2lem5 39017* | The fifth argument passed to evalSub is in the domain (a function 𝐼⟶𝐸). (Contributed by SN, 22-Feb-2024.) |
⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐸 = (Base‘𝑇) & ⊢ 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐸 ↑m 𝐼)) | ||
Theorem | selvcl 39018 | Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐸 = (Base‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∈ 𝐸) | ||
Theorem | frlmfielbas 39019 | The vectors of a finite free module are the functions from 𝐼 to 𝑁. (Contributed by SN, 31-Aug-2023.) |
⊢ 𝐹 = (𝑅 freeLMod 𝐼) & ⊢ 𝑁 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin) → (𝑋 ∈ 𝐵 ↔ 𝑋:𝐼⟶𝑁)) | ||
Theorem | frlmfzwrd 39020 | A vector of a module with indices from 0 to 𝑁 is a word over the scalars of the module. (Contributed by SN, 31-Aug-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (Base‘𝐾) ⇒ ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝑆) | ||
Theorem | frlmfzowrd 39021 | A vector of a module with indices from 0 to 𝑁 − 1 is a word over the scalars of the module. (Contributed by SN, 31-Aug-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0..^𝑁)) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (Base‘𝐾) ⇒ ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝑆) | ||
Theorem | frlmfzolen 39022 | The dimension of a vector of a module with indices from 0 to 𝑁 − 1. (Contributed by SN, 1-Sep-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0..^𝑁)) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (Base‘𝐾) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (♯‘𝑋) = 𝑁) | ||
Theorem | frlmfzowrdb 39023 | The vectors of a module with indices 0 to 𝑁 − 1 are the length- 𝑁 words over the scalars of the module. (Contributed by SN, 1-Sep-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0..^𝑁)) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (Base‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑋 ∈ 𝐵 ↔ (𝑋 ∈ Word 𝑆 ∧ (♯‘𝑋) = 𝑁))) | ||
Theorem | frlmfzoccat 39024 | The concatenation of two vectors of dimension 𝑁 and 𝑀 forms a vector of dimension 𝑁 + 𝑀. (Contributed by SN, 31-Aug-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0..^𝐿)) & ⊢ 𝑋 = (𝐾 freeLMod (0..^𝑀)) & ⊢ 𝑌 = (𝐾 freeLMod (0..^𝑁)) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐶 = (Base‘𝑋) & ⊢ 𝐷 = (Base‘𝑌) & ⊢ (𝜑 → 𝐾 ∈ Ring) & ⊢ (𝜑 → (𝑀 + 𝑁) = 𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑈 ∈ 𝐶) & ⊢ (𝜑 → 𝑉 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑈 ++ 𝑉) ∈ 𝐵) | ||
Theorem | frlmvscadiccat 39025 | Scalar multiplication distributes over concatenation. (Contributed by SN, 6-Sep-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0..^𝐿)) & ⊢ 𝑋 = (𝐾 freeLMod (0..^𝑀)) & ⊢ 𝑌 = (𝐾 freeLMod (0..^𝑁)) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐶 = (Base‘𝑋) & ⊢ 𝐷 = (Base‘𝑌) & ⊢ (𝜑 → 𝐾 ∈ Ring) & ⊢ (𝜑 → (𝑀 + 𝑁) = 𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑈 ∈ 𝐶) & ⊢ (𝜑 → 𝑉 ∈ 𝐷) & ⊢ 𝑂 = ( ·𝑠 ‘𝑊) & ⊢ ∙ = ( ·𝑠 ‘𝑋) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝑂(𝑈 ++ 𝑉)) = ((𝐴 ∙ 𝑈) ++ (𝐴 · 𝑉))) | ||
Theorem | lvecgrp 39026 | A left vector is a group. (Contributed by Steven Nguyen, 28-May-2023.) |
⊢ (𝑊 ∈ LVec → 𝑊 ∈ Grp) | ||
Theorem | lvecring 39027 | The scalar component of a left vector is a ring. (Contributed by Steven Nguyen, 28-May-2023.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → 𝐹 ∈ Ring) | ||
Theorem | lmhmlvec 39028 | The property for modules to be vector spaces is invariant under module isomorphism. (Contributed by Steven Nguyen, 15-Aug-2023.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑆 ∈ LVec ↔ 𝑇 ∈ LVec)) | ||
Theorem | frlmsnic 39029* | Given a free module with a singleton as the index set, that is, a free module of one-dimensional vectors, the function that maps each vector to its coordinate is a module isomorphism from that module to its ring of scalars seen as a module. (Contributed by Steven Nguyen, 18-Aug-2023.) |
⊢ 𝑊 = (𝐾 freeLMod {𝐼}) & ⊢ 𝐹 = (𝑥 ∈ (Base‘𝑊) ↦ (𝑥‘𝐼)) ⇒ ⊢ ((𝐾 ∈ Ring ∧ 𝐼 ∈ V) → 𝐹 ∈ (𝑊 LMIso (ringLMod‘𝐾))) | ||
Theorem | uvccl 39030 | A unit vector is a vector. (Contributed by Steven Nguyen, 16-Jul-2023.) |
⊢ 𝑈 = (𝑅 unitVec 𝐼) & ⊢ 𝑌 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ∈ 𝐵) | ||
Theorem | uvcn0 39031 | A unit vector is nonzero. (Contributed by Steven Nguyen, 16-Jul-2023.) |
⊢ 𝑈 = (𝑅 unitVec 𝐼) & ⊢ 𝑌 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 0 = (0g‘𝑌) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ≠ 0 ) | ||
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 10596 is used in mulid1 10628 related theorems, so one could trade off the extra axioms in mulid1 10628 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 10583; in the other direction, real number closure laws can be avoided by using ax-resscn 10583 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 makes adding natural numbers conveniently only require the rearrangement of parentheses, as shown with the following: (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 10591, ax-1cn 10584, and ax-addcl 10586. (And in practice, the expression isn't completely expanded into ones.) Multiplication by 1 requires either mulid2i 10635 or (ax-1rid 10596 and 1re 10630) as seen in 1t1e1 11788 and 1t1e1ALT 39035. Multiplying with greater natural numbers uses ax-distr 10593. Still, this takes fewer axioms than adding zero. When zero is involved in the decimal constructor, there's an implicit addition operation which causes such theorems (e.g. (9 + 1) = ;10) to use almost every complex number axiom. | ||
Theorem | c0exALT 39032 | Alternate proof of c0ex 10624 using more set theory axioms but fewer complex number axioms (add ax-10 2136, ax-11 2151, ax-13 2383, ax-nul 5202, and remove ax-1cn 10584, ax-icn 10585, ax-addcl 10586, and ax-mulcl 10588). (Contributed by Steven Nguyen, 4-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ V | ||
Theorem | 0cnALT3 39033 | Alternate proof of 0cn 10622 using ax-resscn 10583, ax-addrcl 10587, ax-rnegex 10597, ax-cnre 10599 instead of ax-icn 10585, ax-addcl 10586, ax-mulcl 10588, ax-i2m1 10594. Version of 0cnALT 10863 using ax-1cn 10584 instead of ax-icn 10585. (Contributed by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ ℂ | ||
Theorem | elre0re 39034 | Specialized version of 0red 10633 without using ax-1cn 10584 and ax-cnre 10599. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ) | ||
Theorem | 1t1e1ALT 39035 | Alternate proof of 1t1e1 11788 using a different set of axioms (add ax-mulrcl 10589, ax-i2m1 10594, ax-1ne0 10595, ax-rrecex 10598 and remove ax-resscn 10583, ax-mulcom 10590, ax-mulass 10592, ax-distr 10593). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (1 · 1) = 1 | ||
Theorem | remulcan2d 39036 | mulcan2d 11263 for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | readdid1addid2d 39037 | 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 10803, 𝐴 is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐵 + 𝐴) = 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) = 𝐶) | ||
Theorem | sn-1ne2 39038 | A proof of 1ne2 11834 without using ax-mulcom 10590, ax-mulass 10592, ax-pre-mulgt0 10603. Based on mul02lem2 10806. (Contributed by SN, 13-Dec-2023.) |
⊢ 1 ≠ 2 | ||
Theorem | nnn1suc 39039* | 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 39040 | Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) = (1 + 𝐴)) | ||
Theorem | nnaddcom 39041 | Addition is commutative for natural numbers. Uses fewer axioms than addcom 10815. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | nnaddcomli 39042 | Version of addcomli 10821 for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ (𝐵 + 𝐴) = 𝐶 | ||
Theorem | nnadddir 39043 | Right-distributivity for natural numbers without ax-mulcom 10590. (Contributed by SN, 5-Feb-2024.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | nnmul1com 39044 | Multiplication with 1 is commutative for natural numbers, without ax-mulcom 10590. Since (𝐴 · 1) is 𝐴 by ax-1rid 10596, this is equivalent to remulid2 39129 for natural numbers, but using fewer axioms (avoiding ax-resscn 10583, ax-addass 10591, ax-mulass 10592, ax-rnegex 10597, ax-pre-lttri 10600, ax-pre-lttrn 10601, ax-pre-ltadd 10602). (Contributed by SN, 5-Feb-2024.) |
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1)) | ||
Theorem | nnmulcom 39045 | Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | addsubeq4com 39046 | Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵))) | ||
Theorem | sqsumi 39047 | A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵))) | ||
Theorem | negn0nposznnd 39048 | Lemma for dffltz 39151. (Contributed by Steven Nguyen, 27-Feb-2023.) |
⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → ¬ 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℕ) | ||
Theorem | sqmid3api 39049 | Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝑁 ∈ ℂ & ⊢ (𝐴 + 𝑁) = 𝐵 & ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁)) | ||
Theorem | decaddcom 39050 | Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵) | ||
Theorem | sqn5i 39051 | 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 39052 | 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 39053 | Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11080. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐸 & ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹 & ⊢ (𝐵 · 𝐷) = 𝐺 ⇒ ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐸𝐹𝐺 | ||
Theorem | decpmul 39054 | Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐸 & ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹 & ⊢ (𝐵 · 𝐷) = ;𝐺𝐻 & ⊢ (;𝐸𝐺 + 𝐹) = 𝐼 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 ⇒ ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;𝐼𝐻 | ||
Theorem | sqdeccom12 39055 | The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) | ||
Theorem | sq3deccom12 39056 | Variant of sqdeccom12 39055 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐴 + 𝐶) = 𝐷 ⇒ ⊢ ((;;𝐴𝐵𝐶 · ;;𝐴𝐵𝐶) − (;𝐷𝐵 · ;𝐷𝐵)) = (;99 · ((;𝐴𝐵 · ;𝐴𝐵) − (𝐶 · 𝐶))) | ||
Theorem | 235t711 39057 |
Calculate a product by long multiplication as a base comparison with other
multiplication algorithms.
Conveniently, 711 has two ones which greatly simplifies calculations like 235 · 1. There isn't a higher level mulcomli 10639 saving the lower level uses of mulcomli 10639 within 235 · 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12196 are added then this proof would benefit more than ex-decpmul 39058. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 11761 or 8t7e56 12207. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) |
⊢ (;;235 · ;;711) = ;;;;;167085 | ||
Theorem | ex-decpmul 39058 | Example usage of decpmul 39054. This proof is significantly longer than 235t711 39057. There is more unnecessary carrying compared to 235t711 39057. Although saving 5 visual steps, using mulcomli 10639 early on increases the compressed proof length. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (;;235 · ;;711) = ;;;;;167085 | ||
Theorem | oexpreposd 39059 | Lemma for dffltz 39151. (Contributed by Steven Nguyen, 4-Mar-2023.) |
⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → ¬ (𝑀 / 2) ∈ ℕ) ⇒ ⊢ (𝜑 → (0 < 𝑁 ↔ 0 < (𝑁↑𝑀))) | ||
Theorem | cxpgt0d 39060 | Exponentiation with a positive mantissa is positive. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℝ) ⇒ ⊢ (𝜑 → 0 < (𝐴↑𝑐𝑁)) | ||
Theorem | dvdsexpim 39061 | dvdssqim 15894 generalized to nonnegative exponents. (Contributed by Steven Nguyen, 2-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ 𝐵 → (𝐴↑𝑁) ∥ (𝐵↑𝑁))) | ||
Theorem | nn0rppwr 39062 | If 𝐴 and 𝐵 are relatively prime, then so are 𝐴↑𝑁 and 𝐵↑𝑁. rppwr 15898 extended to nonnegative integers. (Contributed by Steven Nguyen, 4-Apr-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑁) gcd (𝐵↑𝑁)) = 1)) | ||
Theorem | expgcd 39063 | Exponentiation distributes over GCD. sqgcd 15899 extended to nonnegative exponents. (Contributed by Steven Nguyen, 4-Apr-2023.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) | ||
Theorem | nn0expgcd 39064 | Exponentiation distributes over GCD. nn0gcdsq 16082 extended to nonnegative exponents. expgcd 39063 extended to nonnegative bases. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) | ||
Theorem | zexpgcd 39065 | Exponentiation distributes over GCD. zgcdsq 16083 extended to nonnegative exponents. nn0expgcd 39064 extended to integer bases by symmetry. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) | ||
Theorem | numdenexp 39066 | numdensq 16084 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → ((numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁) ∧ (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁))) | ||
Theorem | numexp 39067 | numsq 16085 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁)) | ||
Theorem | denexp 39068 | densq 16086 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁)) | ||
Theorem | exp11d 39069 | sq11d 13611 for positive real bases and nonzero exponents. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ≠ 0) & ⊢ (𝜑 → (𝐴↑𝑁) = (𝐵↑𝑁)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | ltexp1d 39070 | ltmul1d 12462 for exponentiation of positive reals. (Contributed by Steven Nguyen, 22-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑𝑁) < (𝐵↑𝑁))) | ||
Theorem | ltexp1dd 39071 | Raising both sides of 'less than' to the same positive integer preserves ordering. (Contributed by Steven Nguyen, 24-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) < (𝐵↑𝑁)) | ||
Theorem | zrtelqelz 39072 | zsqrtelqelz 16088 generalized to positive integer roots. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑐(1 / 𝑁)) ∈ ℚ) → (𝐴↑𝑐(1 / 𝑁)) ∈ ℤ) | ||
Theorem | zrtdvds 39073 | A positive integer root divides its integer. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑐(1 / 𝑁)) ∈ ℕ) → (𝐴↑𝑐(1 / 𝑁)) ∥ 𝐴) | ||
Theorem | rtprmirr 39074 | The root of a prime number is irrational. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑃↑𝑐(1 / 𝑁)) ∈ (ℝ ∖ ℚ)) | ||
Syntax | cresub 39075 | Real number subtraction. |
class −ℝ | ||
Definition | df-resub 39076* | Define subtraction between real numbers. This operator saves a few axioms over df-sub 10861 in certain situations. Theorem resubval 39077 shows its value, resubadd 39089 relates it to addition, and rersubcl 39088 proves its closure. Based on df-sub 10861. (Contributed by Steven Nguyen, 7-Jan-2022.) |
⊢ −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥)) | ||
Theorem | resubval 39077* | Value of real subtraction, which is the (unique) real 𝑥 such that 𝐵 + 𝑥 = 𝐴. (Contributed by Steven Nguyen, 7-Jan-2022.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴)) | ||
Theorem | renegeulemv 39078* | Lemma for renegeu 39080 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴) | ||
Theorem | renegeulem 39079* | Lemma for renegeu 39080 and similar. Remove a change in bound variables from renegeulemv 39078. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) | ||
Theorem | renegeu 39080* | Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Theorem | rernegcl 39081 | Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → (0 −ℝ 𝐴) ∈ ℝ) | ||
Theorem | renegadd 39082 | Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 −ℝ 𝐴) = 𝐵 ↔ (𝐴 + 𝐵) = 0)) | ||
Theorem | renegid 39083 | Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → (𝐴 + (0 −ℝ 𝐴)) = 0) | ||
Theorem | reneg0addid2 39084 | Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 0) + 𝐴) = 𝐴) | ||
Theorem | resubeulem1 39085 | Lemma for resubeu 39087. A value which when added to zero, results in negative zero. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → (0 + (0 −ℝ (0 + 0))) = (0 −ℝ 0)) | ||
Theorem | resubeulem2 39086 | Lemma for resubeu 39087. A value which when added to 𝐴, results in 𝐵. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + ((0 −ℝ 𝐴) + ((0 −ℝ (0 + 0)) + 𝐵))) = 𝐵) | ||
Theorem | resubeu 39087* | Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 𝐵) | ||
Theorem | rersubcl 39088 | Closure for real subtraction. Based on subcl 10874. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) ∈ ℝ) | ||
Theorem | resubadd 39089 | Relation between real subtraction and addition. Based on subadd 10878. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | resubaddd 39090 | Relationship between subtraction and addition. Based on subaddd 11004. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | resubf 39091 | Real subtraction is an operation on the real numbers. Based on subf 10877. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ −ℝ :(ℝ × ℝ)⟶ℝ | ||
Theorem | repncan2 39092 | Addition and subtraction of equals. Compare pncan2 10882. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐴) = 𝐵) | ||
Theorem | repncan3 39093 | Addition and subtraction of equals. Based on pncan3 10883. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (𝐵 −ℝ 𝐴)) = 𝐵) | ||
Theorem | readdsub 39094 | Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐶) = ((𝐴 −ℝ 𝐶) + 𝐵)) | ||
Theorem | reladdrsub 39095 | Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11040 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 −ℝ 𝐴)) | ||
Theorem | reltsub1 39096 | Subtraction from both sides of 'less than'. Compare ltsub1 11125. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 −ℝ 𝐶) < (𝐵 −ℝ 𝐶))) | ||
Theorem | reltsubadd2 39097 | 'Less than' relationship between addition and subtraction. Compare ltsubadd2 11100. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))) | ||
Theorem | resubcan2 39098 | Cancellation law for real subtraction. Compare subcan2 10900. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) = (𝐵 −ℝ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | resubsub4 39099 | Law for double subtraction. Compare subsub4 10908. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) −ℝ 𝐶) = (𝐴 −ℝ (𝐵 + 𝐶))) | ||
Theorem | rennncan2 39100 | Cancellation law for real subtraction. Compare nnncan2 10912. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) −ℝ (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |