HomeTheorem List (p. 428 of 506)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 428 of 506) | < 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-31236) |
Hilbert Space Explorer
(31237-32759) |
Users' Mathboxes
(32760-50572) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hlhilphllem 42701* | Lemma for hlhil 25581. (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 42702* | Lemma for hlhil 25581. (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 42703 |
Construction of a Hilbert space (df-hil 21833) 𝑈 from a Hilbert
lattice (df-hlat 40093) 𝐾, where 𝑊 is a fixed but arbitrary
hyperplane (co-atom) in 𝐾.
The Hilbert space 𝑈 is identical to the vector space ((DVecH‘𝐾)‘𝑊) (see dvhlvec 41851) 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 41851. 𝑊 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 21833. 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 42704 | Extend class notation with the class of all commutative semirings. |
| class CSRing | ||
| Definition | df-csring 42705 | Define the class of all commutative semirings. (Contributed by metakunt, 4-Apr-2025.) |
| ⊢ CSRing = {𝑓 ∈ SRing ∣ (mulGrp‘𝑓) ∈ CMnd} | ||
| Theorem | iscsrg 42706 | A commutative semiring is a semiring whose multiplication is a commutative monoid. (Contributed by metakunt, 4-Apr-2025.) |
| ⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ CSRing ↔ (𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd)) | ||
| Theorem | rhmzrhval 42707 | Evaluation of integers across a ring homomorphism. (Contributed by metakunt, 4-Jun-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝑋 ∈ ℤ) & ⊢ 𝑀 = (ℤRHom‘𝑅) & ⊢ 𝑁 = (ℤRHom‘𝑆) ⇒ ⊢ (𝜑 → (𝐹‘(𝑀‘𝑋)) = (𝑁‘𝑋)) | ||
| Theorem | zndvdchrrhm 42708* | 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 | relogbcld 42709 | 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 42710 | 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 42711 | 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 42712 | The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.) |
| ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 2 ≤ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝑌) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌)) | ||
| Theorem | uzindd 42713* | 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 42714 | Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑂 ∈ ℤ) & ⊢ (𝜑 → 𝑃 ∈ ℤ) & ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐾 ∈ (𝑂...𝑃)) & ⊢ (𝜑 → 𝑄 = (𝑀 + 𝑂)) & ⊢ (𝜑 → 𝑅 = (𝑁 + 𝑃)) ⇒ ⊢ (𝜑 → (𝐽 + 𝐾) ∈ (𝑄...𝑅)) | ||
| Theorem | fzne2d 42715 | Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐾 ≠ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 < 𝑁) | ||
| Theorem | eqfnfv2d2 42716* | Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
| Theorem | fzsplitnd 42717 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁))) | ||
| Theorem | fzsplitnr 42718 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝐾) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁))) | ||
| Theorem | addassnni 42719 | Associative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐶 ∈ ℕ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) | ||
| Theorem | addcomnni 42720 | Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) | ||
| Theorem | mulassnni 42721 | Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐶 ∈ ℕ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) | ||
| Theorem | mulcomnni 42722 | Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) | ||
| Theorem | gcdcomnni 42723 | Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀) | ||
| Theorem | gcdnegnni 42724 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁) | ||
| Theorem | neggcdnni 42725 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁) | ||
| Theorem | bccl2d 42726 | Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ) | ||
| Theorem | recbothd 42727 | Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐵 / 𝐴) = (𝐷 / 𝐶))) | ||
| Theorem | gcdmultiplei 42728 | The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd (𝑀 · 𝑁)) = 𝑀 | ||
| Theorem | gcdaddmzz2nni 42729 | 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 42730 | 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 42731 | Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd 𝑁) ∈ ℕ | ||
| Theorem | muldvds1d 42732 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∥ 𝑁) | ||
| Theorem | muldvds2d 42733 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝑀 ∥ 𝑁) | ||
| Theorem | nndivdvdsd 42734 | A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds 16318. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℕ)) | ||
| Theorem | nnproddivdvdsd 42735 | 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 42736 | 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 42737 | An image of a function under a finite set is dominated by the set. (Contributed by SN, 10-May-2025.) |
| ⊢ ((𝐴 ∈ Fin ∧ Fun 𝐹) → (𝐹 “ 𝐴) ≼ 𝐴) | ||
| Theorem | 12gcd5e1 42738 | The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;12 gcd 5) = 1 | ||
| Theorem | 60gcd6e6 42739 | The gcd of 60 and 6 is 6. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;60 gcd 6) = 6 | ||
| Theorem | 60gcd7e1 42740 | The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;60 gcd 7) = 1 | ||
| Theorem | 420gcd8e4 42741 | The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;;420 gcd 8) = 4 | ||
| Theorem | lcmeprodgcdi 42742 | Calculate the least common multiple of two natural numbers. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐺 ∈ ℕ & ⊢ 𝐻 ∈ ℕ & ⊢ (𝑀 gcd 𝑁) = 𝐺 & ⊢ (𝐺 · 𝐻) = 𝐴 & ⊢ (𝑀 · 𝑁) = 𝐴 ⇒ ⊢ (𝑀 lcm 𝑁) = 𝐻 | ||
| Theorem | 12lcm5e60 42743 | The lcm of 12 and 5 is 60. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;12 lcm 5) = ;60 | ||
| Theorem | 60lcm6e60 42744 | The lcm of 60 and 6 is 60. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;60 lcm 6) = ;60 | ||
| Theorem | 60lcm7e420 42745 | The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;60 lcm 7) = ;;420 | ||
| Theorem | 420lcm8e840 42746 | The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;;420 lcm 8) = ;;840 | ||
| Theorem | lcmfunnnd 42747 | 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 42748 | Least common multiple of natural numbers up to 1 equals 1. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...1)) = 1 | ||
| Theorem | lcm2un 42749 | Least common multiple of natural numbers up to 2 equals 2. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...2)) = 2 | ||
| Theorem | lcm3un 42750 | Least common multiple of natural numbers up to 3 equals 6. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...3)) = 6 | ||
| Theorem | lcm4un 42751 | Least common multiple of natural numbers up to 4 equals 12. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...4)) = ;12 | ||
| Theorem | lcm5un 42752 | Least common multiple of natural numbers up to 5 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...5)) = ;60 | ||
| Theorem | lcm6un 42753 | Least common multiple of natural numbers up to 6 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...6)) = ;60 | ||
| Theorem | lcm7un 42754 | Least common multiple of natural numbers up to 7 equals 420. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...7)) = ;;420 | ||
| Theorem | lcm8un 42755 | Least common multiple of natural numbers up to 8 equals 840. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...8)) = ;;840 | ||
| Theorem | 3factsumint1 42756* | 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 42757* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 ∫𝐴(𝐹 · (𝐺 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 ∫𝐴(𝐺 · (𝐹 · 𝐻)) d𝑥) | ||
| Theorem | 3factsumint3 42758* | 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 42759* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
| ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ) ⇒ ⊢ (𝜑 → ∫𝐴Σ𝑘 ∈ 𝐵 (𝐹 · (𝐺 · 𝐻)) d𝑥 = ∫𝐴(𝐹 · Σ𝑘 ∈ 𝐵 (𝐺 · 𝐻)) d𝑥) | ||
| Theorem | 3factsumint 42760* | Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024.) |
| ⊢ 𝐴 = (𝐿[,]𝑈) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐿 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐴–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐻) ∈ (𝐴–cn→ℂ)) ⇒ ⊢ (𝜑 → ∫𝐴(𝐹 · Σ𝑘 ∈ 𝐵 (𝐺 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 (𝐺 · ∫𝐴(𝐹 · 𝐻) d𝑥)) | ||
| Theorem | resopunitintvd 42761 | Restrict continuous function on open unit interval. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐴) ∈ (ℂ–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ 𝐴) ∈ ((0(,)1)–cn→ℂ)) | ||
| Theorem | resclunitintvd 42762 | Restrict continuous function on closed unit interval. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐴) ∈ (ℂ–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝐴) ∈ ((0[,]1)–cn→ℂ)) | ||
| Theorem | resdvopclptsd 42763* | Restrict derivative on unit interval. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]1) ↦ 𝐴)) = (𝑥 ∈ (0(,)1) ↦ 𝐵)) | ||
| Theorem | lcmineqlem1 42764* | 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 42765* | 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 42766* | 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 42767 | 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 42769. (Contributed by metakunt, 10-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) & ⊢ (𝜑 → 𝐾 ∈ (0...(𝑁 − 𝑀))) ⇒ ⊢ (𝜑 → ((lcm‘(1...𝑁)) / (𝑀 + 𝐾)) ∈ ℤ) | ||
| Theorem | lcmineqlem5 42768 | Technical lemma for reciprocal multiplication in deduction form. (Contributed by metakunt, 10-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · (1 / 𝐶))) = (𝐵 · (𝐴 / 𝐶))) | ||
| Theorem | lcmineqlem6 42769* | 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 42770 | Derivative of 1-x for chain rule application. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (1 − 𝑥))) = (𝑥 ∈ ℂ ↦ -1) | ||
| Theorem | lcmineqlem8 42771* | Derivative of (1-x)^(N-M). (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀)))) = (𝑥 ∈ ℂ ↦ (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) | ||
| Theorem | lcmineqlem9 42772* | (1-x)^(N-M) is continuous. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀))) ∈ (ℂ–cn→ℂ)) | ||
| Theorem | lcmineqlem10 42773* | Induction step of lcmineqlem13 42776 (deduction form). (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥 = ((𝑀 / (𝑁 − 𝑀)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) | ||
| Theorem | lcmineqlem11 42774 | Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → (1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = ((𝑀 / (𝑁 − 𝑀)) · (1 / (𝑀 · (𝑁C𝑀))))) | ||
| Theorem | lcmineqlem12 42775* | Base case for induction. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ∫(0[,]1)((𝑡↑(1 − 1)) · ((1 − 𝑡)↑(𝑁 − 1))) d𝑡 = (1 / (1 · (𝑁C1)))) | ||
| Theorem | lcmineqlem13 42776* | Induction proof for lcm integral. (Contributed by metakunt, 12-May-2024.) |
| ⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐹 = (1 / (𝑀 · (𝑁C𝑀)))) | ||
| Theorem | lcmineqlem14 42777 | Technical lemma for inequality estimate. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝐸 ∈ ℕ) & ⊢ (𝜑 → (𝐴 · 𝐶) ∥ 𝐷) & ⊢ (𝜑 → (𝐵 · 𝐶) ∥ 𝐸) & ⊢ (𝜑 → 𝐷 ∥ 𝐸) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) ∥ 𝐸) | ||
| Theorem | lcmineqlem15 42778* | 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 42779 | Technical divisibility lemma. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑀 · (𝑁C𝑀)) ∥ (lcm‘(1...𝑁))) | ||
| Theorem | lcmineqlem17 42780 | Inequality of 2^{2n}. (Contributed by metakunt, 29-Apr-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁))) | ||
| Theorem | lcmineqlem18 42781 | 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 42782 | Dividing implies inequality for lcm inequality lemma. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∥ (lcm‘(1...((2 · 𝑁) + 1)))) | ||
| Theorem | lcmineqlem20 42783 | Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ≤ (lcm‘(1...((2 · 𝑁) + 1)))) | ||
| Theorem | lcmineqlem21 42784 | 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 42785 | 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 42786 | Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 9 ≤ 𝑁) ⇒ ⊢ (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁))) | ||
| Theorem | lcmineqlem 42787 | 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 42788 | 3 to the power of 7 equals 2187. (Contributed by metakunt, 21-Aug-2024.) |
| ⊢ (3↑7) = ;;;2187 | ||
| Theorem | 3lexlogpow5ineq1 42789 | First inequality in inequality chain, proposed by Mario Carneiro (Contributed by metakunt, 22-May-2024.) |
| ⊢ 9 < ((;11 / 7)↑5) | ||
| Theorem | 3lexlogpow5ineq2 42790 | Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.) |
| ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 3 ≤ 𝑋) ⇒ ⊢ (𝜑 → ((;11 / 7)↑5) ≤ ((2 logb 𝑋)↑5)) | ||
| Theorem | 3lexlogpow5ineq4 42791 | Sharper logarithm inequality chain. (Contributed by metakunt, 21-Aug-2024.) |
| ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 3 ≤ 𝑋) ⇒ ⊢ (𝜑 → 9 < ((2 logb 𝑋)↑5)) | ||
| Theorem | 3lexlogpow5ineq3 42792 | Combined inequality chain for a specific power of the binary logarithm, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.) |
| ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 3 ≤ 𝑋) ⇒ ⊢ (𝜑 → 7 < ((2 logb 𝑋)↑5)) | ||
| Theorem | 3lexlogpow2ineq1 42793 | Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.) |
| ⊢ ((3 / 2) < (2 logb 3) ∧ (2 logb 3) < (5 / 3)) | ||
| Theorem | 3lexlogpow2ineq2 42794 | Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.) |
| ⊢ (2 < ((2 logb 3)↑2) ∧ ((2 logb 3)↑2) < 3) | ||
| Theorem | 3lexlogpow5ineq5 42795 | Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.) |
| ⊢ ((2 logb 3)↑5) ≤ ;15 | ||
| Theorem | intlewftc 42796* | Inequality inference by invoking fundamental theorem of calculus. (Contributed by metakunt, 22-Jul-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐷 = (ℝ D 𝐹)) & ⊢ (𝜑 → 𝐸 = (ℝ D 𝐺)) & ⊢ (𝜑 → 𝐷 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐷 ∈ 𝐿1) & ⊢ (𝜑 → 𝐸 ∈ 𝐿1) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)) & ⊢ (𝜑 → 𝐸 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑃 ≤ 𝑄) & ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐺‘𝐴)) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐺‘𝐵)) | ||
| Theorem | aks4d1lem1 42797 | Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℕ ∧ 9 < 𝐵)) | ||
| Theorem | aks4d1p1p1 42798* | Exponential law for finite products, special case. (Contributed by metakunt, 22-Jul-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ (1...𝑁)(𝐴↑𝑐𝑘) = (𝐴↑𝑐Σ𝑘 ∈ (1...𝑁)𝑘)) | ||
| Theorem | dvrelog2 42799* | The derivative of the logarithm, ftc2 26182 version. (Contributed by metakunt, 11-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥)) & ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥)) ⇒ ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) | ||
| Theorem | dvrelog3 42800* | The derivative of the logarithm on an open interval. (Contributed by metakunt, 11-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (log‘𝑥)) & ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥)) ⇒ ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |