Home | Metamath
Proof Explorer Theorem List (p. 392 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fac2xp3 39101 | 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 | facp2 39102 | The factorial of a successor's successor. (Contributed by metakunt, 19-Apr-2024.) |
⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 2)) = ((!‘𝑁) · ((𝑁 + 1) · (𝑁 + 2)))) | ||
Theorem | prodsplit 39103* | Product split into two factors, original by Steven Nguyen. (Contributed by metakunt, 21-Apr-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 𝐾))) → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...(𝑁 + 𝐾))𝐴 = (∏𝑘 ∈ (𝑀...𝑁)𝐴 · ∏𝑘 ∈ ((𝑁 + 1)...(𝑁 + 𝐾))𝐴)) | ||
Theorem | 2xp3dxp2ge1d 39104 | 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 39105 | A factorial with offset is monotonely increasing (Contributed by metakunt, 20-Apr-2024.) |
⊢ (((𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℕ0 ∧ 𝑋 ≤ 𝑌) ∧ 𝑁 ∈ ℕ0) → (!‘(𝑋 + 𝑁)) ≤ (!‘(𝑌 + 𝑁))) | ||
Theorem | ioin9i8 39106 | Miscellaneous inference creating a biconditional from an implied converse implication. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ (𝜑 → (𝜓 ∨ 𝜒)) & ⊢ (𝜒 → ¬ 𝜃) & ⊢ (𝜓 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | jaodd 39107 | Double deduction form of jaoi 853. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) → 𝜃))) | ||
Theorem | nsb 39108 | Generalization rule for negated wff. (Contributed by Steven Nguyen, 3-May-2023.) |
⊢ ¬ 𝜑 ⇒ ⊢ ¬ [𝑥 / 𝑦]𝜑 | ||
Theorem | sbn1 39109 | One direction of sbn 2287, using fewer axioms. Compare 19.2 1981. (Contributed by Steven Nguyen, 18-Aug-2023.) |
⊢ ([𝑡 / 𝑥] ¬ 𝜑 → ¬ [𝑡 / 𝑥]𝜑) | ||
Theorem | sbor2 39110 | One direction of sbor 2316, using fewer axioms. Compare 19.33 1885. (Contributed by Steven Nguyen, 18-Aug-2023.) |
⊢ (([𝑡 / 𝑥]𝜑 ∨ [𝑡 / 𝑥]𝜓) → [𝑡 / 𝑥](𝜑 ∨ 𝜓)) | ||
Theorem | sn-elabg 39111* | Membership in a class abstraction, using implicit substitution and an intermediate setvar 𝑦 to avoid ax-10 2145, ax-11 2161, ax-12 2177. It also avoids a disjoint variable condition on 𝑥 and 𝐴. Compare sbievw2 2107. (Contributed by SN, 20-Apr-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒)) | ||
Theorem | 3rspcedvd 39112* | Triple application of rspcedvd 3628. (Contributed by Steven Nguyen, 27-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (𝜒 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝑧 = 𝐶) → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 ∃𝑧 ∈ 𝐷 𝜓) | ||
Theorem | rabeqcda 39113* | When 𝜓 is always true in a context, a restricted class abstraction is equal to the restricting class. Deduction form of rabeqc 3680. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = 𝐴) | ||
Theorem | rabdif 39114* | Move difference in and out of a restricted class abstraction. (Contributed by Steven Nguyen, 6-Jun-2023.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ 𝐵) = {𝑥 ∈ (𝐴 ∖ 𝐵) ∣ 𝜑} | ||
Theorem | sn-axrep5v 39115* | A condensed form of axrep5 5198. (Contributed by SN, 21-Sep-2023.) |
⊢ (∀𝑤 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑)) | ||
Theorem | sn-axprlem3 39116* | axprlem3 5328 using only Tarski's FOL axiom schemes and ax-rep 5192. (Contributed by SN, 22-Sep-2023.) |
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 if-(𝜑, 𝑧 = 𝑎, 𝑧 = 𝑏)) | ||
Theorem | sn-el 39117* | A version of el 5272 with an inner existential quantifier on 𝑥, which avoids ax-7 2015 and ax-8 2116. (Contributed by SN, 18-Sep-2023.) |
⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦 | ||
Theorem | sn-dtru 39118* | dtru 5273 without ax-8 2116 or ax-12 2177. (Contributed by SN, 21-Sep-2023.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | pssexg 39119 | The proper subset of a set is also a set. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) | ||
Theorem | pssn0 39120 | A proper superset is nonempty. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ (𝐴 ⊊ 𝐵 → 𝐵 ≠ ∅) | ||
Theorem | psspwb 39121 | Classes are proper subclasses if and only if their power classes are proper subclasses. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ (𝐴 ⊊ 𝐵 ↔ 𝒫 𝐴 ⊊ 𝒫 𝐵) | ||
Theorem | xppss12 39122 | Proper subset theorem for Cartesian product. (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷) → (𝐴 × 𝐶) ⊊ (𝐵 × 𝐷)) | ||
Theorem | elpwbi 39123 | Membership in a power set, biconditional. (Contributed by Steven Nguyen, 17-Jul-2022.) (Proof shortened by Steven Nguyen, 16-Sep-2022.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵) | ||
Theorem | opelxpii 39124 | Ordered pair membership in a Cartesian product (implication). (Contributed by Steven Nguyen, 17-Jul-2022.) |
⊢ 𝐴 ∈ 𝐶 & ⊢ 𝐵 ∈ 𝐷 ⇒ ⊢ 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) | ||
Theorem | iunsn 39125* | Indexed union of a singleton. Compare dfiun2 4960 and rnmpt 5829. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ ∪ 𝑥 ∈ 𝐴 {𝐵} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} | ||
Theorem | imaopab 39126* | The image of a class of ordered pairs. (Contributed by Steven Nguyen, 6-Jun-2023.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} | ||
Theorem | fnsnbt 39127 | A function's domain is a singleton iff the function is a singleton. (Contributed by Steven Nguyen, 18-Aug-2023.) |
⊢ (𝐴 ∈ V → (𝐹 Fn {𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉})) | ||
Theorem | fnimasnd 39128 | 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 39129* | Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ (𝐴 / 𝑅) = ran (𝑥 ∈ 𝐴 ↦ [𝑥]𝑅) | ||
Theorem | dfqs3 39130* | Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ (𝐴 / 𝑅) = ∪ 𝑥 ∈ 𝐴 {[𝑥]𝑅} | ||
Theorem | qseq12d 39131 | Equality theorem for quotient set, deduction form. (Contributed by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐷)) | ||
Theorem | qsalrel 39132* | 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 | fzosumm1 39133* | Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023.) |
⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = (𝑁 − 1) → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝐴 = (Σ𝑘 ∈ (𝑀..^(𝑁 − 1))𝐴 + 𝐵)) | ||
Theorem | ccatcan2d 39134 | Cancellation law for concatenation. (Contributed by SN, 6-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ Word 𝑉) & ⊢ (𝜑 → 𝐵 ∈ Word 𝑉) & ⊢ (𝜑 → 𝐶 ∈ Word 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 ++ 𝐶) = (𝐵 ++ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | nelsubginvcld 39135 | 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 39136 | 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 39137 | 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 39138 | 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 39139 | 𝑇 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 39140 | 𝐷 is a ring homomorphism. (Contributed by SN, 15-Dec-2023.) |
⊢ 𝑈 = (𝐼 mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝐷 ∈ (𝑅 RingHom 𝑇)) | ||
Theorem | selvval2lem3 39141 | 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 39142 | A lemma to illustrate the purpose of selvval2lem3 39141 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 39143 | 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 39144* | 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 39145 | Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐸 = (Base‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∈ 𝐸) | ||
Theorem | frlmfielbas 39146 | The vectors of a finite free module are the functions from 𝐼 to 𝑁. (Contributed by SN, 31-Aug-2023.) |
⊢ 𝐹 = (𝑅 freeLMod 𝐼) & ⊢ 𝑁 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin) → (𝑋 ∈ 𝐵 ↔ 𝑋:𝐼⟶𝑁)) | ||
Theorem | frlmfzwrd 39147 | 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 39148 | 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 39149 | 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 39150 | 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 39151 | 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 39152 | 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 39153 | A left vector is a group. (Contributed by Steven Nguyen, 28-May-2023.) |
⊢ (𝑊 ∈ LVec → 𝑊 ∈ Grp) | ||
Theorem | lvecring 39154 | The scalar component of a left vector is a ring. (Contributed by Steven Nguyen, 28-May-2023.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → 𝐹 ∈ Ring) | ||
Theorem | lmhmlvec 39155 | 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 39156* | 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 39157 | A unit vector is a vector. (Contributed by Steven Nguyen, 16-Jul-2023.) |
⊢ 𝑈 = (𝑅 unitVec 𝐼) & ⊢ 𝑌 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ∈ 𝐵) | ||
Theorem | uvcn0 39158 | 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 10609 is used in mulid1 10641 related theorems, so one could trade off the extra axioms in mulid1 10641 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 10596; in the other direction, real number closure laws can be avoided by using ax-resscn 10596 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 10604, ax-1cn 10597, and ax-addcl 10599. (And in practice, the expression isn't completely expanded into ones.) Multiplication by 1 requires either mulid2i 10648 or (ax-1rid 10609 and 1re 10643) as seen in 1t1e1 11802 and 1t1e1ALT 39162. Multiplying with greater natural numbers uses ax-distr 10606. 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 39159 | Alternate proof of c0ex 10637 using more set theory axioms but fewer complex number axioms (add ax-10 2145, ax-11 2161, ax-13 2390, ax-nul 5212, and remove ax-1cn 10597, ax-icn 10598, ax-addcl 10599, and ax-mulcl 10601). (Contributed by Steven Nguyen, 4-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ V | ||
Theorem | 0cnALT3 39160 | Alternate proof of 0cn 10635 using ax-resscn 10596, ax-addrcl 10600, ax-rnegex 10610, ax-cnre 10612 instead of ax-icn 10598, ax-addcl 10599, ax-mulcl 10601, ax-i2m1 10607. Version of 0cnALT 10876 using ax-1cn 10597 instead of ax-icn 10598. (Contributed by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ ℂ | ||
Theorem | elre0re 39161 | Specialized version of 0red 10646 without using ax-1cn 10597 and ax-cnre 10612. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ) | ||
Theorem | 1t1e1ALT 39162 | Alternate proof of 1t1e1 11802 using a different set of axioms (add ax-mulrcl 10602, ax-i2m1 10607, ax-1ne0 10608, ax-rrecex 10611 and remove ax-resscn 10596, ax-mulcom 10603, ax-mulass 10605, ax-distr 10606). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (1 · 1) = 1 | ||
Theorem | remulcan2d 39163 | mulcan2d 11276 for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | readdid1addid2d 39164 | 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 10816, 𝐴 is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐵 + 𝐴) = 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) = 𝐶) | ||
Theorem | sn-1ne2 39165 | A proof of 1ne2 11848 without using ax-mulcom 10603, ax-mulass 10605, ax-pre-mulgt0 10616. Based on mul02lem2 10819. (Contributed by SN, 13-Dec-2023.) |
⊢ 1 ≠ 2 | ||
Theorem | nnn1suc 39166* | 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 39167 | Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) = (1 + 𝐴)) | ||
Theorem | nnaddcom 39168 | Addition is commutative for natural numbers. Uses fewer axioms than addcom 10828. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | nnaddcomli 39169 | Version of addcomli 10834 for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ (𝐵 + 𝐴) = 𝐶 | ||
Theorem | nnadddir 39170 | Right-distributivity for natural numbers without ax-mulcom 10603. (Contributed by SN, 5-Feb-2024.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | nnmul1com 39171 | Multiplication with 1 is commutative for natural numbers, without ax-mulcom 10603. Since (𝐴 · 1) is 𝐴 by ax-1rid 10609, this is equivalent to remulid2 39256 for natural numbers, but using fewer axioms (avoiding ax-resscn 10596, ax-addass 10604, ax-mulass 10605, ax-rnegex 10610, ax-pre-lttri 10613, ax-pre-lttrn 10614, ax-pre-ltadd 10615). (Contributed by SN, 5-Feb-2024.) |
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1)) | ||
Theorem | nnmulcom 39172 | Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | addsubeq4com 39173 | Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵))) | ||
Theorem | sqsumi 39174 | A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵))) | ||
Theorem | negn0nposznnd 39175 | Lemma for dffltz 39278. (Contributed by Steven Nguyen, 27-Feb-2023.) |
⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → ¬ 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℕ) | ||
Theorem | sqmid3api 39176 | Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝑁 ∈ ℂ & ⊢ (𝐴 + 𝑁) = 𝐵 & ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁)) | ||
Theorem | decaddcom 39177 | Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵) | ||
Theorem | sqn5i 39178 | 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 39179 | 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 39180 | Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11093. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐸 & ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹 & ⊢ (𝐵 · 𝐷) = 𝐺 ⇒ ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐸𝐹𝐺 | ||
Theorem | decpmul 39181 | Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐸 & ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹 & ⊢ (𝐵 · 𝐷) = ;𝐺𝐻 & ⊢ (;𝐸𝐺 + 𝐹) = 𝐼 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 ⇒ ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;𝐼𝐻 | ||
Theorem | sqdeccom12 39182 | The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) | ||
Theorem | sq3deccom12 39183 | Variant of sqdeccom12 39182 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐴 + 𝐶) = 𝐷 ⇒ ⊢ ((;;𝐴𝐵𝐶 · ;;𝐴𝐵𝐶) − (;𝐷𝐵 · ;𝐷𝐵)) = (;99 · ((;𝐴𝐵 · ;𝐴𝐵) − (𝐶 · 𝐶))) | ||
Theorem | 235t711 39184 |
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 10652 saving the lower level uses of mulcomli 10652 within 235 · 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12210 are added then this proof would benefit more than ex-decpmul 39185. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 11775 or 8t7e56 12221. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) |
⊢ (;;235 · ;;711) = ;;;;;167085 | ||
Theorem | ex-decpmul 39185 | Example usage of decpmul 39181. This proof is significantly longer than 235t711 39184. There is more unnecessary carrying compared to 235t711 39184. Although saving 5 visual steps, using mulcomli 10652 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 39186 | Lemma for dffltz 39278. (Contributed by Steven Nguyen, 4-Mar-2023.) |
⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → ¬ (𝑀 / 2) ∈ ℕ) ⇒ ⊢ (𝜑 → (0 < 𝑁 ↔ 0 < (𝑁↑𝑀))) | ||
Theorem | cxpgt0d 39187 | Exponentiation with a positive mantissa is positive. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℝ) ⇒ ⊢ (𝜑 → 0 < (𝐴↑𝑐𝑁)) | ||
Theorem | dvdsexpim 39188 | dvdssqim 15906 generalized to nonnegative exponents. (Contributed by Steven Nguyen, 2-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ 𝐵 → (𝐴↑𝑁) ∥ (𝐵↑𝑁))) | ||
Theorem | nn0rppwr 39189 | If 𝐴 and 𝐵 are relatively prime, then so are 𝐴↑𝑁 and 𝐵↑𝑁. rppwr 15910 extended to nonnegative integers. (Contributed by Steven Nguyen, 4-Apr-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑁) gcd (𝐵↑𝑁)) = 1)) | ||
Theorem | expgcd 39190 | Exponentiation distributes over GCD. sqgcd 15911 extended to nonnegative exponents. (Contributed by Steven Nguyen, 4-Apr-2023.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) | ||
Theorem | nn0expgcd 39191 | Exponentiation distributes over GCD. nn0gcdsq 16094 extended to nonnegative exponents. expgcd 39190 extended to nonnegative bases. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) | ||
Theorem | zexpgcd 39192 | Exponentiation distributes over GCD. zgcdsq 16095 extended to nonnegative exponents. nn0expgcd 39191 extended to integer bases by symmetry. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) | ||
Theorem | numdenexp 39193 | numdensq 16096 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → ((numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁) ∧ (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁))) | ||
Theorem | numexp 39194 | numsq 16097 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁)) | ||
Theorem | denexp 39195 | densq 16098 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁)) | ||
Theorem | exp11d 39196 | sq11d 13624 for positive real bases and nonzero exponents. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ≠ 0) & ⊢ (𝜑 → (𝐴↑𝑁) = (𝐵↑𝑁)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | ltexp1d 39197 | ltmul1d 12475 for exponentiation of positive reals. (Contributed by Steven Nguyen, 22-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑𝑁) < (𝐵↑𝑁))) | ||
Theorem | ltexp1dd 39198 | Raising both sides of 'less than' to the same positive integer preserves ordering. (Contributed by Steven Nguyen, 24-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) < (𝐵↑𝑁)) | ||
Theorem | zrtelqelz 39199 | zsqrtelqelz 16100 generalized to positive integer roots. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑐(1 / 𝑁)) ∈ ℚ) → (𝐴↑𝑐(1 / 𝑁)) ∈ ℤ) | ||
Theorem | zrtdvds 39200 | A positive integer root divides its integer. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑐(1 / 𝑁)) ∈ ℕ) → (𝐴↑𝑐(1 / 𝑁)) ∥ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |