HomeTheorem List (p. 400 of 464)
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. 400 of 464) | < 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-29181) |
Hilbert Space Explorer
(29182-30704) |
Users' Mathboxes
(30705-46395) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hlhillsm 39901 | 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 39902 | 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 39903 | The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 39877 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 39904* | Lemma for hlhil 24512. (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 39905* | Lemma for hlhil 24512. (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 39906 |
Construction of a Hilbert space (df-hil 20821) 𝑈 from a Hilbert
lattice (df-hlat 37292) 𝐾, where 𝑊 is a fixed but arbitrary
hyperplane (co-atom) in 𝐾.
The Hilbert space 𝑈 is identical to the vector space ((DVecH‘𝐾)‘𝑊) (see dvhlvec 39050) 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 39050. 𝑊 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 20821. 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) | ||
| Theorem | leexp1ad 39907 | Weak base ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐵↑𝑁)) | ||
| Theorem | relogbcld 39908 | 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 39909 | 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 39910 | 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 39911 | The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.) |
| ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 2 ≤ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝑌) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌)) | ||
| Theorem | fzindd 39912* | Induction on the integers from M to N inclusive, a deduction version. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝑥 = 𝑀 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁) ∧ 𝜃) → 𝜏) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ ℤ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)) → 𝜂) | ||
| Theorem | uzindd 39913* | 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 39914 | Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑂 ∈ ℤ) & ⊢ (𝜑 → 𝑃 ∈ ℤ) & ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐾 ∈ (𝑂...𝑃)) & ⊢ (𝜑 → 𝑄 = (𝑀 + 𝑂)) & ⊢ (𝜑 → 𝑅 = (𝑁 + 𝑃)) ⇒ ⊢ (𝜑 → (𝐽 + 𝐾) ∈ (𝑄...𝑅)) | ||
| Theorem | zltlem1d 39915 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) | ||
| Theorem | zltp1led 39916 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) | ||
| Theorem | fzne2d 39917 | Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐾 ≠ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 < 𝑁) | ||
| Theorem | eqfnfv2d2 39918* | Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
| Theorem | fzsplitnd 39919 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁))) | ||
| Theorem | fzsplitnr 39920 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝐾) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁))) | ||
| Theorem | addassnni 39921 | Associative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐶 ∈ ℕ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) | ||
| Theorem | addcomnni 39922 | Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) | ||
| Theorem | mulassnni 39923 | Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐶 ∈ ℕ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) | ||
| Theorem | mulcomnni 39924 | Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) | ||
| Theorem | gcdcomnni 39925 | Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀) | ||
| Theorem | gcdnegnni 39926 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁) | ||
| Theorem | neggcdnni 39927 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁) | ||
| Theorem | bccl2d 39928 | Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ) | ||
| Theorem | recbothd 39929 | Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐵 / 𝐴) = (𝐷 / 𝐶))) | ||
| Theorem | gcdmultiplei 39930 | The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd (𝑀 · 𝑁)) = 𝑀 | ||
| Theorem | gcdaddmzz2nni 39931 | 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 39932 | 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 39933 | Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑀 gcd 𝑁) ∈ ℕ | ||
| Theorem | muldvds1d 39934 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∥ 𝑁) | ||
| Theorem | muldvds2d 39935 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝐾 · 𝑀) ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝑀 ∥ 𝑁) | ||
| Theorem | nndivdvdsd 39936 | A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds 15900. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℕ)) | ||
| Theorem | nnproddivdvdsd 39937 | 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 39938 | 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 | 12gcd5e1 39939 | The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;12 gcd 5) = 1 | ||
| Theorem | 60gcd6e6 39940 | The gcd of 60 and 6 is 6. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;60 gcd 6) = 6 | ||
| Theorem | 60gcd7e1 39941 | The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;60 gcd 7) = 1 | ||
| Theorem | 420gcd8e4 39942 | The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;;420 gcd 8) = 4 | ||
| Theorem | lcmeprodgcdi 39943 | Calculate the least common multiple of two natural numbers. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐺 ∈ ℕ & ⊢ 𝐻 ∈ ℕ & ⊢ (𝑀 gcd 𝑁) = 𝐺 & ⊢ (𝐺 · 𝐻) = 𝐴 & ⊢ (𝑀 · 𝑁) = 𝐴 ⇒ ⊢ (𝑀 lcm 𝑁) = 𝐻 | ||
| Theorem | 12lcm5e60 39944 | The lcm of 12 and 5 is 60. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;12 lcm 5) = ;60 | ||
| Theorem | 60lcm6e60 39945 | The lcm of 60 and 6 is 60. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;60 lcm 6) = ;60 | ||
| Theorem | 60lcm7e420 39946 | The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;60 lcm 7) = ;;420 | ||
| Theorem | 420lcm8e840 39947 | The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (;;420 lcm 8) = ;;840 | ||
| Theorem | lcmfunnnd 39948 | 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 39949 | Least common multiple of natural numbers up to 1 equals 1. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...1)) = 1 | ||
| Theorem | lcm2un 39950 | Least common multiple of natural numbers up to 2 equals 2. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...2)) = 2 | ||
| Theorem | lcm3un 39951 | Least common multiple of natural numbers up to 3 equals 6. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...3)) = 6 | ||
| Theorem | lcm4un 39952 | Least common multiple of natural numbers up to 4 equals 12. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...4)) = ;12 | ||
| Theorem | lcm5un 39953 | Least common multiple of natural numbers up to 5 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...5)) = ;60 | ||
| Theorem | lcm6un 39954 | Least common multiple of natural numbers up to 6 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...6)) = ;60 | ||
| Theorem | lcm7un 39955 | Least common multiple of natural numbers up to 7 equals 420. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...7)) = ;;420 | ||
| Theorem | lcm8un 39956 | Least common multiple of natural numbers up to 8 equals 840. (Contributed by metakunt, 25-Apr-2024.) |
| ⊢ (lcm‘(1...8)) = ;;840 | ||
| Theorem | 3factsumint1 39957* | 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 39958* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 ∫𝐴(𝐹 · (𝐺 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 ∫𝐴(𝐺 · (𝐹 · 𝐻)) d𝑥) | ||
| Theorem | 3factsumint3 39959* | 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 39960* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
| ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐻 ∈ ℂ) ⇒ ⊢ (𝜑 → ∫𝐴Σ𝑘 ∈ 𝐵 (𝐹 · (𝐺 · 𝐻)) d𝑥 = ∫𝐴(𝐹 · Σ𝑘 ∈ 𝐵 (𝐺 · 𝐻)) d𝑥) | ||
| Theorem | 3factsumint 39961* | Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024.) |
| ⊢ 𝐴 = (𝐿[,]𝑈) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐿 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐴–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐻) ∈ (𝐴–cn→ℂ)) ⇒ ⊢ (𝜑 → ∫𝐴(𝐹 · Σ𝑘 ∈ 𝐵 (𝐺 · 𝐻)) d𝑥 = Σ𝑘 ∈ 𝐵 (𝐺 · ∫𝐴(𝐹 · 𝐻) d𝑥)) | ||
| Theorem | resopunitintvd 39962 | Restrict continuous function on open unit interval. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐴) ∈ (ℂ–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (0(,)1) ↦ 𝐴) ∈ ((0(,)1)–cn→ℂ)) | ||
| Theorem | resclunitintvd 39963 | Restrict continuous function on closed unit interval. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐴) ∈ (ℂ–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝐴) ∈ ((0[,]1)–cn→ℂ)) | ||
| Theorem | resdvopclptsd 39964* | Restrict derivative on unit interval. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℝ D (𝑥 ∈ (0[,]1) ↦ 𝐴)) = (𝑥 ∈ (0(,)1) ↦ 𝐵)) | ||
| Theorem | lcmineqlem1 39965* | 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 39966* | 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 39967* | 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 39968 | 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 39970. (Contributed by metakunt, 10-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) & ⊢ (𝜑 → 𝐾 ∈ (0...(𝑁 − 𝑀))) ⇒ ⊢ (𝜑 → ((lcm‘(1...𝑁)) / (𝑀 + 𝐾)) ∈ ℤ) | ||
| Theorem | lcmineqlem5 39969 | Technical lemma for reciprocal multiplication in deduction form. (Contributed by metakunt, 10-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · (1 / 𝐶))) = (𝐵 · (𝐴 / 𝐶))) | ||
| Theorem | lcmineqlem6 39970* | 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 39971 | Derivative of 1-x for chain rule application. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (1 − 𝑥))) = (𝑥 ∈ ℂ ↦ -1) | ||
| Theorem | lcmineqlem8 39972* | Derivative of (1-x)^(N-M). (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀)))) = (𝑥 ∈ ℂ ↦ (-(𝑁 − 𝑀) · ((1 − 𝑥)↑((𝑁 − 𝑀) − 1))))) | ||
| Theorem | lcmineqlem9 39973* | (1-x)^(N-M) is continuous. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁 − 𝑀))) ∈ (ℂ–cn→ℂ)) | ||
| Theorem | lcmineqlem10 39974* | Induction step of lcmineqlem13 39977 (deduction form). (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥 = ((𝑀 / (𝑁 − 𝑀)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥)) | ||
| Theorem | lcmineqlem11 39975 | Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → (1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = ((𝑀 / (𝑁 − 𝑀)) · (1 / (𝑀 · (𝑁C𝑀))))) | ||
| Theorem | lcmineqlem12 39976* | Base case for induction. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ∫(0[,]1)((𝑡↑(1 − 1)) · ((1 − 𝑡)↑(𝑁 − 1))) d𝑡 = (1 / (1 · (𝑁C1)))) | ||
| Theorem | lcmineqlem13 39977* | Induction proof for lcm integral. (Contributed by metakunt, 12-May-2024.) |
| ⊢ 𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁 − 𝑀))) d𝑥 & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐹 = (1 / (𝑀 · (𝑁C𝑀)))) | ||
| Theorem | lcmineqlem14 39978 | Technical lemma for inequality estimate. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝐸 ∈ ℕ) & ⊢ (𝜑 → (𝐴 · 𝐶) ∥ 𝐷) & ⊢ (𝜑 → (𝐵 · 𝐶) ∥ 𝐸) & ⊢ (𝜑 → 𝐷 ∥ 𝐸) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) ∥ 𝐸) | ||
| Theorem | lcmineqlem15 39979* | 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 39980 | Technical divisibility lemma. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → (𝑀 · (𝑁C𝑀)) ∥ (lcm‘(1...𝑁))) | ||
| Theorem | lcmineqlem17 39981 | Inequality of 2^{2n}. (Contributed by metakunt, 29-Apr-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁))) | ||
| Theorem | lcmineqlem18 39982 | 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 39983 | Dividing implies inequality for lcm inequality lemma. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∥ (lcm‘(1...((2 · 𝑁) + 1)))) | ||
| Theorem | lcmineqlem20 39984 | Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ≤ (lcm‘(1...((2 · 𝑁) + 1)))) | ||
| Theorem | lcmineqlem21 39985 | 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 39986 | 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 39987 | Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 9 ≤ 𝑁) ⇒ ⊢ (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁))) | ||
| Theorem | lcmineqlem 39988 | 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 39989 | 3 to the power of 7 equals 2187. (Contributed by metakunt, 21-Aug-2024.) |
| ⊢ (3↑7) = ;;;2187 | ||
| Theorem | 3lexlogpow5ineq1 39990 | First inequality in inequality chain, proposed by Mario Carneiro (Contributed by metakunt, 22-May-2024.) |
| ⊢ 9 < ((;11 / 7)↑5) | ||
| Theorem | 3lexlogpow5ineq2 39991 | Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.) |
| ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 3 ≤ 𝑋) ⇒ ⊢ (𝜑 → ((;11 / 7)↑5) ≤ ((2 logb 𝑋)↑5)) | ||
| Theorem | 3lexlogpow5ineq4 39992 | Sharper logarithm inequality chain. (Contributed by metakunt, 21-Aug-2024.) |
| ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 3 ≤ 𝑋) ⇒ ⊢ (𝜑 → 9 < ((2 logb 𝑋)↑5)) | ||
| Theorem | 3lexlogpow5ineq3 39993 | 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 39994 | 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 39995 | 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 39996 | Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024.) |
| ⊢ ((2 logb 3)↑5) ≤ ;15 | ||
| Theorem | intlewftc 39997* | Inequality inference by invoking fundamental theorem of calculus. (Contributed by metakunt, 22-Jul-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐷 = (ℝ D 𝐹)) & ⊢ (𝜑 → 𝐸 = (ℝ D 𝐺)) & ⊢ (𝜑 → 𝐷 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℝ)) & ⊢ (𝜑 → 𝐷 ∈ 𝐿1) & ⊢ (𝜑 → 𝐸 ∈ 𝐿1) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)) & ⊢ (𝜑 → 𝐸 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑃 ≤ 𝑄) & ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐺‘𝐴)) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐺‘𝐵)) | ||
| Theorem | aks4d1lem1 39998 | Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024.) |
| ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3)) & ⊢ 𝐵 = (⌈‘((2 logb 𝑁)↑5)) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℕ ∧ 9 < 𝐵)) | ||
| Theorem | aks4d1p1p1 39999* | Exponential law for finite products, special case. (Contributed by metakunt, 22-Jul-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ (1...𝑁)(𝐴↑𝑐𝑘) = (𝐴↑𝑐Σ𝑘 ∈ (1...𝑁)𝑘)) | ||
| Theorem | dvrelog2 40000* | The derivative of the logarithm, ftc2 25113 version. (Contributed by metakunt, 11-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (log‘𝑥)) & ⊢ 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑥)) ⇒ ⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |