![]() |
Metamath
Proof Explorer Theorem List (p. 417 of 485) | < 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-30843) |
![]() (30844-32366) |
![]() (32367-48490) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hlhilnvl 41601 | The involution operation of the star division ring for the final constructed Hilbert space. (Contributed by NM, 20-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ ∗ = ((HGMap‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ∗ = (*𝑟‘𝑅)) | ||
Theorem | hlhillvec 41602 | The final constructed Hilbert space is a vector space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑈 ∈ LVec) | ||
Theorem | hlhildrng 41603 | The star division ring for the final constructed Hilbert space is a division ring. (Contributed by NM, 20-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝑅 = (Scalar‘𝑈) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
Theorem | hlhilsrnglem 41604 | Lemma for hlhilsrng 41605. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (Scalar‘𝐿) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑆) & ⊢ · = (.r‘𝑆) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) ⇒ ⊢ (𝜑 → 𝑅 ∈ *-Ring) | ||
Theorem | hlhilsrng 41605 | The star division ring for the final constructed Hilbert space is a division ring. (Contributed by NM, 21-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝑅 = (Scalar‘𝑈) ⇒ ⊢ (𝜑 → 𝑅 ∈ *-Ring) | ||
Theorem | hlhil0 41606 | The zero vector for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 0 = (0g‘𝐿) ⇒ ⊢ (𝜑 → 0 = (0g‘𝑈)) | ||
Theorem | hlhillsm 41607 | The vector sum operation for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ ⊕ = (LSSum‘𝐿) ⇒ ⊢ (𝜑 → ⊕ = (LSSum‘𝑈)) | ||
Theorem | hlhilocv 41608 | The orthocomplement for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝑉 = (Base‘𝐿) & ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑂 = (ocv‘𝑈) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑂‘𝑋) = (𝑁‘𝑋)) | ||
Theorem | hlhillcs 41609 | The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 41583 is applied over and over to conclusion rather than applied once to antecedent - would compressed proof be shorter if applied once to antecedent? (Contributed by NM, 23-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐶 = ran 𝐼) | ||
Theorem | hlhilphllem 41610* | Lemma for hlhil 25454. (Contributed by NM, 23-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐿) & ⊢ + = (+g‘𝐿) & ⊢ · = ( ·𝑠 ‘𝐿) & ⊢ 𝑅 = (Scalar‘𝐿) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 0 = (0g‘𝐿) & ⊢ , = (·𝑖‘𝑈) & ⊢ 𝐽 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ 𝐸 = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑉 ↦ ((𝐽‘𝑦)‘𝑥)) ⇒ ⊢ (𝜑 → 𝑈 ∈ PreHil) | ||
Theorem | hlhilhillem 41611* | Lemma for hlhil 25454. (Contributed by NM, 23-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐿) & ⊢ + = (+g‘𝐿) & ⊢ · = ( ·𝑠 ‘𝐿) & ⊢ 𝑅 = (Scalar‘𝐿) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⨣ = (+g‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑄 = (0g‘𝑅) & ⊢ 0 = (0g‘𝐿) & ⊢ , = (·𝑖‘𝑈) & ⊢ 𝐽 = ((HDMap‘𝐾)‘𝑊) & ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) & ⊢ 𝐸 = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑉 ↦ ((𝐽‘𝑦)‘𝑥)) & ⊢ 𝑂 = (ocv‘𝑈) & ⊢ 𝐶 = (ClSubSp‘𝑈) ⇒ ⊢ (𝜑 → 𝑈 ∈ Hil) | ||
Theorem | hlathil 41612 |
Construction of a Hilbert space (df-hil 21694) 𝑈 from a Hilbert
lattice (df-hlat 38997) 𝐾, where 𝑊 is a fixed but arbitrary
hyperplane (co-atom) in 𝐾.
The Hilbert space 𝑈 is identical to the vector space ((DVecH‘𝐾)‘𝑊) (see dvhlvec 40756) except that it is extended with involution and inner product components. The construction of these two components is provided by Theorem 3.6 in [Holland95] p. 13, whose proof we follow loosely. An example of involution is the complex conjugate when the division ring is the field of complex numbers. The nature of the division ring we constructed is indeterminate, however, until we specialize the initial Hilbert lattice with additional conditions found by Maria Solèr in 1995 and refined by René Mayet in 1998 that result in a division ring isomorphic to ℂ. See additional discussion at https://us.metamath.org/qlegif/mmql.html#what 40756. 𝑊 corresponds to the w in the proof of Theorem 13.4 of [Crawley] p. 111. Such a 𝑊 always exists since HL has lattice rank of at least 4 by df-hil 21694. It can be eliminated if we just want to show the existence of a Hilbert space, as is done in the literature. (Contributed by NM, 23-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑈 ∈ Hil) | ||
Syntax | ccsrg 41613 | Extend class notation with the class of all commutative semirings. |
class CSRing | ||
Definition | df-csring 41614 | Define the class of all commutative semirings. (Contributed by metakunt, 4-Apr-2025.) |
⊢ CSRing = {𝑓 ∈ SRing ∣ (mulGrp‘𝑓) ∈ CMnd} | ||
Theorem | iscsrg 41615 | A commutative semiring is a semiring whose multiplication is a commutative monoid. (Contributed by metakunt, 4-Apr-2025.) |
⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ CSRing ↔ (𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd)) | ||
Theorem | rhmzrhval 41616 | Evaluation of integers across a ring homomorphism. (Contributed by metakunt, 4-Jun-2025.) |
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ ℤ) & ⊢ 𝑀 = (ℤRHom‘𝑅) & ⊢ 𝑁 = (ℤRHom‘𝑆) ⇒ ⊢ (𝜑 → (𝐹‘(𝑀‘𝑋)) = (𝑁‘𝑋)) | ||
Theorem | zndvdchrrhm 41617* | Construction of a ring homomorphism from ℤ/nℤ to 𝑅 when the characteristic of 𝑅 divides 𝑁. (Contributed by metakunt, 4-Jun-2025.) |
⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (chr‘𝑅) ∈ ℤ) & ⊢ (𝜑 → (chr‘𝑅) ∥ 𝑁) & ⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = (𝑥 ∈ (Base‘𝑍) ↦ ∪ ((ℤRHom‘𝑅) “ 𝑥)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑍 RingHom 𝑅)) | ||
Theorem | leexp1ad 41618 | Weak base ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐵↑𝑁)) | ||
Theorem | relogbcld 41619 | Closure of the general logarithm with a positive real base on positive reals, a deduction version. (Contributed by metakunt, 22-May-2024.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝑋) & ⊢ (𝜑 → 𝐵 ≠ 1) ⇒ ⊢ (𝜑 → (𝐵 logb 𝑋) ∈ ℝ) | ||
Theorem | relogbexpd 41620 | Identity law for general logarithm: the logarithm of a power to the base is the exponent, a deduction version. (Contributed by metakunt, 22-May-2024.) |
⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ≠ 1) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐵 logb (𝐵↑𝑀)) = 𝑀) | ||
Theorem | relogbzexpd 41621 | Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power, a deduction version. (Contributed by metakunt, 22-May-2024.) |
⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ≠ 1) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐵 logb (𝐶↑𝑁)) = (𝑁 · (𝐵 logb 𝐶))) | ||
Theorem | logblebd 41622 | The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.) |
⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 2 ≤ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝑌) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌)) | ||
Theorem | uzindd 41623* | Induction on the upper integers that start at 𝑀. The first four hypotheses give us the substitution instances we need; the following two are the basis and the induction step, a deduction version. (Contributed by metakunt, 8-Jun-2024.) |
⊢ (𝑗 = 𝑀 → (𝜓 ↔ 𝜒)) & ⊢ (𝑗 = 𝑘 → (𝜓 ↔ 𝜃)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜓 ↔ 𝜏)) & ⊢ (𝑗 = 𝑁 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝜃 ∧ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘)) → 𝜏) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | fzadd2d 41624 | Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑂 ∈ ℤ) & ⊢ (𝜑 → 𝑃 ∈ ℤ) & ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐾 ∈ (𝑂...𝑃)) & ⊢ (𝜑 → 𝑄 = (𝑀 + 𝑂)) & ⊢ (𝜑 → 𝑅 = (𝑁 + 𝑃)) ⇒ ⊢ (𝜑 → (𝐽 + 𝐾) ∈ (𝑄...𝑅)) | ||
Theorem | zltlem1d 41625 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) | ||
Theorem | zltp1led 41626 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) | ||
Theorem | fzne2d 41627 | Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐾 ≠ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 < 𝑁) | ||
Theorem | eqfnfv2d2 41628* | Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | fzsplitnd 41629 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁))) | ||
Theorem | fzsplitnr 41630 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝐾) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁))) | ||
Theorem | addassnni 41631 | Associative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐶 ∈ ℕ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) | ||
Theorem | addcomnni 41632 | Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) | ||
Theorem | mulassnni 41633 | Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐶 ∈ ℕ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) | ||
Theorem | mulcomnni 41634 | Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) | ||
Theorem | gcdcomnni 41635 | Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀) | ||
Theorem | gcdnegnni 41636 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁) | ||
Theorem | neggcdnni 41637 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁) | ||
Theorem | bccl2d 41638 | Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ) | ||
Theorem | recbothd 41639 | Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐵 / 𝐴) = (𝐷 / 𝐶))) | ||
Theorem | gcdmultiplei 41640 | The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd (𝑀 · 𝑁)) = 𝑀 | ||
Theorem | gcdaddmzz2nni 41641 | Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + (𝐾 · 𝑀))) | ||
Theorem | gcdaddmzz2nncomi 41642 | Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) | ||
Theorem | gcdnncli 41643 | Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd 𝑁) ∈ ℕ | ||
Theorem | muldvds1d 41644 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∥ 𝑁) | ||
Theorem | muldvds2d 41645 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝑀 ∥ 𝑁) | ||
Theorem | nndivdvdsd 41646 | A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds 16260. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℕ)) | ||
Theorem | nnproddivdvdsd 41647 | A product of natural numbers divides a natural number if and only if a factor divides the quotient, a deduction version. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝐾 · 𝑀) ∥ 𝑁 ↔ 𝐾 ∥ (𝑁 / 𝑀))) | ||
Theorem | coprmdvds2d 41648 | If an integer is divisible by two coprime integers, then it is divisible by their product, a deduction version. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝐾 gcd 𝑀) = 1) & ⊢ (𝜑 → 𝐾 ∥ 𝑁) & ⊢ (𝜑 → 𝑀 ∥ 𝑁) ⇒ ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁) | ||
Theorem | imadomfi 41649 | An image of a function under a finite set is dominated by the set. (Contributed by SN, 10-May-2025.) |
⊢ ((𝐴 ∈ Fin ∧ Fun 𝐹) → (𝐹 “ 𝐴) ≼ 𝐴) | ||
Theorem | 12gcd5e1 41650 | The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;12 gcd 5) = 1 | ||
Theorem | 60gcd6e6 41651 | The gcd of 60 and 6 is 6. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;60 gcd 6) = 6 | ||
Theorem | 60gcd7e1 41652 | The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;60 gcd 7) = 1 | ||
Theorem | 420gcd8e4 41653 | The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;;420 gcd 8) = 4 | ||
Theorem | lcmeprodgcdi 41654 | Calculate the least common multiple of two natural numbers. (Contributed by metakunt, 25-Apr-2024.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐺 ∈ ℕ & ⊢ 𝐻 ∈ ℕ & ⊢ (𝑀 gcd 𝑁) = 𝐺 & ⊢ (𝐺 · 𝐻) = 𝐴 & ⊢ (𝑀 · 𝑁) = 𝐴 ⇒ ⊢ (𝑀 lcm 𝑁) = 𝐻 | ||
Theorem | 12lcm5e60 41655 | The lcm of 12 and 5 is 60. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;12 lcm 5) = ;60 | ||
Theorem | 60lcm6e60 41656 | The lcm of 60 and 6 is 60. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;60 lcm 6) = ;60 | ||
Theorem | 60lcm7e420 41657 | The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;60 lcm 7) = ;;420 | ||
Theorem | 420lcm8e840 41658 | The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (;;420 lcm 8) = ;;840 | ||
Theorem | lcmfunnnd 41659 | Useful equation to calculate the least common multiple of 1 to n. (Contributed by metakunt, 29-Apr-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (lcm‘(1...𝑁)) = ((lcm‘(1...(𝑁 − 1))) lcm 𝑁)) | ||
Theorem | lcm1un 41660 | Least common multiple of natural numbers up to 1 equals 1. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (lcm‘(1...1)) = 1 | ||
Theorem | lcm2un 41661 | Least common multiple of natural numbers up to 2 equals 2. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (lcm‘(1...2)) = 2 | ||
Theorem | lcm3un 41662 | Least common multiple of natural numbers up to 3 equals 6. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (lcm‘(1...3)) = 6 | ||
Theorem | lcm4un 41663 | Least common multiple of natural numbers up to 4 equals 12. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (lcm‘(1...4)) = ;12 | ||
Theorem | lcm5un 41664 | Least common multiple of natural numbers up to 5 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (lcm‘(1...5)) = ;60 | ||
Theorem | lcm6un 41665 | Least common multiple of natural numbers up to 6 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (lcm‘(1...6)) = ;60 | ||
Theorem | lcm7un 41666 | Least common multiple of natural numbers up to 7 equals 420. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (lcm‘(1...7)) = ;;420 | ||
Theorem | lcm8un 41667 | Least common multiple of natural numbers up to 8 equals 840. (Contributed by metakunt, 25-Apr-2024.) |
⊢ (lcm‘(1...8)) = ;;840 | ||
Theorem | 3factsumint1 41668* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
⊢ 𝐴 = (𝐿[,]𝑈) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐿 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐴–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐻) ∈ (𝐴–cn→ℂ)) ⇒ ⊢ (𝜑 → ∫𝐴Σ𝑘 ∈ 𝐵 (𝐹 · (𝐺 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 ∫𝐴(𝐹 · (𝐺 · 𝐻)) d𝑥) | ||
Theorem | 3factsumint2 41669* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 ∫𝐴(𝐹 · (𝐺 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 ∫𝐴(𝐺 · (𝐹 · 𝐻)) d𝑥) | ||
Theorem | 3factsumint3 41670* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
⊢ 𝐴 = (𝐿[,]𝑈) & ⊢ (𝜑 → 𝐿 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐴–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐻) ∈ (𝐴–cn→ℂ)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 ∫𝐴(𝐺 · (𝐹 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 (𝐺 · ∫𝐴(𝐹 · 𝐻) d𝑥)) | ||
Theorem | 3factsumint4 41671* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ) ⇒ ⊢ (𝜑 → ∫𝐴Σ𝑘 ∈ 𝐵 (𝐹 · (𝐺 · 𝐻)) d𝑥 = ∫𝐴(𝐹 · Σ𝑘 ∈ 𝐵 (𝐺 · 𝐻)) d𝑥) | ||
Theorem | 3factsumint 41672* | Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024.) |
⊢ 𝐴 = (𝐿[,]𝑈) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐿 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐴–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐻) ∈ (𝐴–cn→ℂ)) ⇒ ⊢ (𝜑 → ∫𝐴(𝐹 · Σ𝑘 ∈ 𝐵 (𝐺 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 (𝐺 · ∫𝐴(𝐹 · 𝐻) d𝑥)) | ||
Theorem | resopunitintvd 41673 | Restrict continuous function on open unit interval. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐴) ∈ (ℂ–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ 𝐴) ∈ ((0(,)1)–cn→ℂ)) | ||
Theorem | resclunitintvd 41674 | Restrict continuous function on closed unit interval. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐴) ∈ (ℂ–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝐴) ∈ ((0[,]1)–cn→ℂ)) | ||
Theorem | resdvopclptsd 41675* | Restrict derivative on unit interval. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]1) ↦ 𝐴)) = (𝑥 ∈ (0(,)1) ↦ 𝐵)) | ||
Theorem | lcmineqlem1 41676* | Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 29-Apr-2024.) |
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · Σ𝑘 ∈ (0...(𝑁 − 𝑀))(((-1↑𝑘) · ((𝑁 − 𝑀)C𝑘)) · (𝑥↑𝑘))) d𝑥) | ||
Theorem | lcmineqlem2 41677* | Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 29-Apr-2024.) |
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐹 = Σ𝑘 ∈ (0...(𝑁 − 𝑀))(((-1↑𝑘) · ((𝑁 − 𝑀)C𝑘)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · (𝑥↑𝑘)) d𝑥)) | ||
Theorem | lcmineqlem3 41678* | Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 30-Apr-2024.) |
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐹 = Σ𝑘 ∈ (0...(𝑁 − 𝑀))(((-1↑𝑘) · ((𝑁 − 𝑀)C𝑘)) · (1 / (𝑀 + 𝑘)))) | ||
Theorem | lcmineqlem4 41679 | Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. F is found in lcmineqlem6 41681. (Contributed by metakunt, 10-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) & ⊢ (𝜑 → 𝐾 ∈ (0...(𝑁 − 𝑀))) ⇒ ⊢ (𝜑 → ((lcm‘(1...𝑁)) / (𝑀 + 𝐾)) ∈ ℤ) | ||
Theorem | lcmineqlem5 41680 | Technical lemma for reciprocal multiplication in deduction form. (Contributed by metakunt, 10-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · (1 / 𝐶))) = (𝐵 · (𝐴 / 𝐶))) | ||
Theorem | lcmineqlem6 41681* | Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 10-May-2024.) |
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((lcm‘(1...𝑁)) · 𝐹) ∈ ℤ) | ||
Theorem | lcmineqlem7 41682 | Derivative of 1-x for chain rule application. (Contributed by metakunt, 12-May-2024.) |
⊢ (ℂ D (𝑥 ∈ ℂ ↦ (1 − 𝑥))) = (𝑥 ∈ ℂ ↦ -1) | ||
Theorem | lcmineqlem8 41683* | Derivative of (1-x)^(N-M). (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀)))) = (𝑥 ∈ ℂ ↦ (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) | ||
Theorem | lcmineqlem9 41684* | (1-x)^(N-M) is continuous. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀))) ∈ (ℂ–cn→ℂ)) | ||
Theorem | lcmineqlem10 41685* | Induction step of lcmineqlem13 41688 (deduction form). (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥 = ((𝑀 / (𝑁 − 𝑀)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) | ||
Theorem | lcmineqlem11 41686 | Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → (1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = ((𝑀 / (𝑁 − 𝑀)) · (1 / (𝑀 · (𝑁C𝑀))))) | ||
Theorem | lcmineqlem12 41687* | Base case for induction. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ∫(0[,]1)((𝑡↑(1 − 1)) · ((1 − 𝑡)↑(𝑁 − 1))) d𝑡 = (1 / (1 · (𝑁C1)))) | ||
Theorem | lcmineqlem13 41688* | Induction proof for lcm integral. (Contributed by metakunt, 12-May-2024.) |
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐹 = (1 / (𝑀 · (𝑁C𝑀)))) | ||
Theorem | lcmineqlem14 41689 | Technical lemma for inequality estimate. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝐸 ∈ ℕ) & ⊢ (𝜑 → (𝐴 · 𝐶) ∥ 𝐷) & ⊢ (𝜑 → (𝐵 · 𝐶) ∥ 𝐸) & ⊢ (𝜑 → 𝐷 ∥ 𝐸) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) ∥ 𝐸) | ||
Theorem | lcmineqlem15 41690* | F times the least common multiple of 1 to n is a natural number. (Contributed by metakunt, 10-May-2024.) |
⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((lcm‘(1...𝑁)) · 𝐹) ∈ ℕ) | ||
Theorem | lcmineqlem16 41691 | Technical divisibility lemma. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑀 · (𝑁C𝑀)) ∥ (lcm‘(1...𝑁))) | ||
Theorem | lcmineqlem17 41692 | Inequality of 2^{2n}. (Contributed by metakunt, 29-Apr-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁))) | ||
Theorem | lcmineqlem18 41693 | Technical lemma to shift factors in binomial coefficient. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑁 + 1) · (((2 · 𝑁) + 1)C(𝑁 + 1))) = (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁))) | ||
Theorem | lcmineqlem19 41694 | Dividing implies inequality for lcm inequality lemma. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∥ (lcm‘(1...((2 · 𝑁) + 1)))) | ||
Theorem | lcmineqlem20 41695 | Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ≤ (lcm‘(1...((2 · 𝑁) + 1)))) | ||
Theorem | lcmineqlem21 41696 | The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 4 ≤ 𝑁) ⇒ ⊢ (𝜑 → (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 1)))) | ||
Theorem | lcmineqlem22 41697 | The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 4 ≤ 𝑁) ⇒ ⊢ (𝜑 → ((2↑((2 · 𝑁) + 1)) ≤ (lcm‘(1...((2 · 𝑁) + 1))) ∧ (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 2))))) | ||
Theorem | lcmineqlem23 41698 | Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 9 ≤ 𝑁) ⇒ ⊢ (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁))) | ||
Theorem | lcmineqlem 41699 | The least common multiple inequality lemma, a central result for future use. Theorem 3.1 from https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 16-May-2024.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 7 ≤ 𝑁) ⇒ ⊢ (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁))) | ||
Theorem | 3exp7 41700 | 3 to the power of 7 equals 2187. (Contributed by metakunt, 21-Aug-2024.) |
⊢ (3↑7) = ;;;2187 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |