Home | Metamath
Proof Explorer Theorem List (p. 404 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hlhilip 40301* | Inner product operation for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (BaseβπΏ) & β’ π = ((HDMapβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ , = (π₯ β π, π¦ β π β¦ ((πβπ¦)βπ₯)) β β’ (π β , = (Β·πβπ)) | ||
Theorem | hlhilipval 40302 | Value of inner product operation for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (BaseβπΏ) & β’ π = ((HDMapβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ , = (Β·πβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π , π) = ((πβπ)βπ)) | ||
Theorem | hlhilnvl 40303 | 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 40304 | 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 40305 | 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 40306 | Lemma for hlhilsrng 40307. (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 40307 | 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 40308 | 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 40309 | 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 40310 | 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 40311 | The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 40285 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 40312* | Lemma for hlhil 24729. (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 40313* | Lemma for hlhil 24729. (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 40314 |
Construction of a Hilbert space (df-hil 21033) π from a Hilbert
lattice (df-hlat 37699) πΎ, where π is a fixed but arbitrary
hyperplane (co-atom) in πΎ.
The Hilbert space π is identical to the vector space ((DVecHβπΎ)βπ) (see dvhlvec 39458) 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 39458. π 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 21033. 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 40315 | Weak base ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β0) & β’ (π β 0 β€ π΄) & β’ (π β π΄ β€ π΅) β β’ (π β (π΄βπ) β€ (π΅βπ)) | ||
Theorem | relogbcld 40316 | 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 40317 | 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 40318 | 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 40319 | The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.) |
β’ (π β π΅ β β€) & β’ (π β 2 β€ π΅) & β’ (π β π β β) & β’ (π β 0 < π) & β’ (π β π β β) & β’ (π β 0 < π) & β’ (π β π β€ π) β β’ (π β (π΅ logb π) β€ (π΅ logb π)) | ||
Theorem | uzindd 40320* | 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 40321 | Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π½ β (π...π)) & β’ (π β πΎ β (π...π)) & β’ (π β π = (π + π)) & β’ (π β π = (π + π)) β β’ (π β (π½ + πΎ) β (π...π )) | ||
Theorem | zltlem1d 40322 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π < π β π β€ (π β 1))) | ||
Theorem | zltp1led 40323 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π < π β (π + 1) β€ π)) | ||
Theorem | fzne2d 40324 | Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.) |
β’ (π β πΎ β (π...π)) & β’ (π β πΎ β π) β β’ (π β πΎ < π) | ||
Theorem | eqfnfv2d2 40325* | Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.) |
β’ (π β πΉ Fn π΄) & β’ (π β πΊ Fn π΅) & β’ (π β π΄ = π΅) & β’ ((π β§ π₯ β π΄) β (πΉβπ₯) = (πΊβπ₯)) β β’ (π β πΉ = πΊ) | ||
Theorem | fzsplitnd 40326 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
β’ (π β πΎ β (π...π)) β β’ (π β (π...π) = ((π...(πΎ β 1)) βͺ (πΎ...π))) | ||
Theorem | fzsplitnr 40327 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β β€) & β’ (π β π β€ πΎ) & β’ (π β πΎ β€ π) β β’ (π β (π...π) = ((π...(πΎ β 1)) βͺ (πΎ...π))) | ||
Theorem | addassnni 40328 | Associative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ)) | ||
Theorem | addcomnni 40329 | Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ + π΅) = (π΅ + π΄) | ||
Theorem | mulassnni 40330 | Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ)) | ||
Theorem | mulcomnni 40331 | Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β· π΅) = (π΅ Β· π΄) | ||
Theorem | gcdcomnni 40332 | Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd π) = (π gcd π) | ||
Theorem | gcdnegnni 40333 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd -π) = (π gcd π) | ||
Theorem | neggcdnni 40334 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (-π gcd π) = (π gcd π) | ||
Theorem | bccl2d 40335 | Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β πΎ β β0) & β’ (π β πΎ β€ π) β β’ (π β (πCπΎ) β β) | ||
Theorem | recbothd 40336 | Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β π΅ β 0) & β’ (π β πΆ β β) & β’ (π β πΆ β 0) & β’ (π β π· β β) & β’ (π β π· β 0) β β’ (π β ((π΄ / π΅) = (πΆ / π·) β (π΅ / π΄) = (π· / πΆ))) | ||
Theorem | gcdmultiplei 40337 | The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd (π Β· π)) = π | ||
Theorem | gcdaddmzz2nni 40338 | 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 40339 | 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 40340 | Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd π) β β | ||
Theorem | muldvds1d 40341 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β (πΎ Β· π) β₯ π) β β’ (π β πΎ β₯ π) | ||
Theorem | muldvds2d 40342 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β (πΎ Β· π) β₯ π) β β’ (π β π β₯ π) | ||
Theorem | nndivdvdsd 40343 | A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds 16080. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) β β’ (π β (π β₯ π β (π / π) β β)) | ||
Theorem | nnproddivdvdsd 40344 | 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 40345 | 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 40346 | The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;12 gcd 5) = 1 | ||
Theorem | 60gcd6e6 40347 | The gcd of 60 and 6 is 6. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 gcd 6) = 6 | ||
Theorem | 60gcd7e1 40348 | The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 gcd 7) = 1 | ||
Theorem | 420gcd8e4 40349 | The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;;420 gcd 8) = 4 | ||
Theorem | lcmeprodgcdi 40350 | Calculate the least common multiple of two natural numbers. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β & β’ πΊ β β & β’ π» β β & β’ (π gcd π) = πΊ & β’ (πΊ Β· π») = π΄ & β’ (π Β· π) = π΄ β β’ (π lcm π) = π» | ||
Theorem | 12lcm5e60 40351 | The lcm of 12 and 5 is 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;12 lcm 5) = ;60 | ||
Theorem | 60lcm6e60 40352 | The lcm of 60 and 6 is 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 lcm 6) = ;60 | ||
Theorem | 60lcm7e420 40353 | The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 lcm 7) = ;;420 | ||
Theorem | 420lcm8e840 40354 | The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;;420 lcm 8) = ;;840 | ||
Theorem | lcmfunnnd 40355 | 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 40356 | Least common multiple of natural numbers up to 1 equals 1. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...1)) = 1 | ||
Theorem | lcm2un 40357 | Least common multiple of natural numbers up to 2 equals 2. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...2)) = 2 | ||
Theorem | lcm3un 40358 | Least common multiple of natural numbers up to 3 equals 6. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...3)) = 6 | ||
Theorem | lcm4un 40359 | Least common multiple of natural numbers up to 4 equals 12. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...4)) = ;12 | ||
Theorem | lcm5un 40360 | Least common multiple of natural numbers up to 5 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...5)) = ;60 | ||
Theorem | lcm6un 40361 | Least common multiple of natural numbers up to 6 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...6)) = ;60 | ||
Theorem | lcm7un 40362 | Least common multiple of natural numbers up to 7 equals 420. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...7)) = ;;420 | ||
Theorem | lcm8un 40363 | Least common multiple of natural numbers up to 8 equals 840. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...8)) = ;;840 | ||
Theorem | 3factsumint1 40364* | 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 40365* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
β’ ((π β§ π₯ β π΄) β πΉ β β) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β π» β β) β β’ (π β Ξ£π β π΅ β«π΄(πΉ Β· (πΊ Β· π»)) dπ₯ = Ξ£π β π΅ β«π΄(πΊ Β· (πΉ Β· π»)) dπ₯) | ||
Theorem | 3factsumint3 40366* | 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 40367* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
β’ (π β π΅ β Fin) & β’ ((π β§ π₯ β π΄) β πΉ β β) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β π» β β) β β’ (π β β«π΄Ξ£π β π΅ (πΉ Β· (πΊ Β· π»)) dπ₯ = β«π΄(πΉ Β· Ξ£π β π΅ (πΊ Β· π»)) dπ₯) | ||
Theorem | 3factsumint 40368* | Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024.) |
β’ π΄ = (πΏ[,]π) & β’ (π β π΅ β Fin) & β’ (π β πΏ β β) & β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ πΉ) β (π΄βcnββ)) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ π») β (π΄βcnββ)) β β’ (π β β«π΄(πΉ Β· Ξ£π β π΅ (πΊ Β· π»)) dπ₯ = Ξ£π β π΅ (πΊ Β· β«π΄(πΉ Β· π») dπ₯)) | ||
Theorem | resopunitintvd 40369 | Restrict continuous function on open unit interval. (Contributed by metakunt, 12-May-2024.) |
β’ (π β (π₯ β β β¦ π΄) β (ββcnββ)) β β’ (π β (π₯ β (0(,)1) β¦ π΄) β ((0(,)1)βcnββ)) | ||
Theorem | resclunitintvd 40370 | Restrict continuous function on closed unit interval. (Contributed by metakunt, 12-May-2024.) |
β’ (π β (π₯ β β β¦ π΄) β (ββcnββ)) β β’ (π β (π₯ β (0[,]1) β¦ π΄) β ((0[,]1)βcnββ)) | ||
Theorem | resdvopclptsd 40371* | Restrict derivative on unit interval. (Contributed by metakunt, 12-May-2024.) |
β’ (π β (β D (π₯ β β β¦ π΄)) = (π₯ β β β¦ π΅)) & β’ ((π β§ π₯ β β) β π΄ β β) & β’ ((π β§ π₯ β β) β π΅ β β) β β’ (π β (β D (π₯ β (0[,]1) β¦ π΄)) = (π₯ β (0(,)1) β¦ π΅)) | ||
Theorem | lcmineqlem1 40372* | 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 40373* | 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 40374* | 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 40375 | 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 40377. (Contributed by metakunt, 10-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β πΎ β (0...(π β π))) β β’ (π β ((lcmβ(1...π)) / (π + πΎ)) β β€) | ||
Theorem | lcmineqlem5 40376 | Technical lemma for reciprocal multiplication in deduction form. (Contributed by metakunt, 10-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β πΆ β 0) β β’ (π β (π΄ Β· (π΅ Β· (1 / πΆ))) = (π΅ Β· (π΄ / πΆ))) | ||
Theorem | lcmineqlem6 40377* | 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 40378 | Derivative of 1-x for chain rule application. (Contributed by metakunt, 12-May-2024.) |
β’ (β D (π₯ β β β¦ (1 β π₯))) = (π₯ β β β¦ -1) | ||
Theorem | lcmineqlem8 40379* | Derivative of (1-x)^(N-M). (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π < π) β β’ (π β (β D (π₯ β β β¦ ((1 β π₯)β(π β π)))) = (π₯ β β β¦ (-(π β π) Β· ((1 β π₯)β((π β π) β 1))))) | ||
Theorem | lcmineqlem9 40380* | (1-x)^(N-M) is continuous. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) β β’ (π β (π₯ β β β¦ ((1 β π₯)β(π β π))) β (ββcnββ)) | ||
Theorem | lcmineqlem10 40381* | Induction step of lcmineqlem13 40384 (deduction form). (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π < π) β β’ (π β β«(0[,]1)((π₯β((π + 1) β 1)) Β· ((1 β π₯)β(π β (π + 1)))) dπ₯ = ((π / (π β π)) Β· β«(0[,]1)((π₯β(π β 1)) Β· ((1 β π₯)β(π β π))) dπ₯)) | ||
Theorem | lcmineqlem11 40382 | Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π < π) β β’ (π β (1 / ((π + 1) Β· (πC(π + 1)))) = ((π / (π β π)) Β· (1 / (π Β· (πCπ))))) | ||
Theorem | lcmineqlem12 40383* | Base case for induction. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) β β’ (π β β«(0[,]1)((π‘β(1 β 1)) Β· ((1 β π‘)β(π β 1))) dπ‘ = (1 / (1 Β· (πC1)))) | ||
Theorem | lcmineqlem13 40384* | Induction proof for lcm integral. (Contributed by metakunt, 12-May-2024.) |
β’ πΉ = β«(0[,]1)((π₯β(π β 1)) Β· ((1 β π₯)β(π β π))) dπ₯ & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) β β’ (π β πΉ = (1 / (π Β· (πCπ)))) | ||
Theorem | lcmineqlem14 40385 | Technical lemma for inequality estimate. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΈ β β) & β’ (π β (π΄ Β· πΆ) β₯ π·) & β’ (π β (π΅ Β· πΆ) β₯ πΈ) & β’ (π β π· β₯ πΈ) & β’ (π β (π΄ gcd π΅) = 1) β β’ (π β ((π΄ Β· π΅) Β· πΆ) β₯ πΈ) | ||
Theorem | lcmineqlem15 40386* | 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 40387 | Technical divisibility lemma. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) β β’ (π β (π Β· (πCπ)) β₯ (lcmβ(1...π))) | ||
Theorem | lcmineqlem17 40388 | Inequality of 2^{2n}. (Contributed by metakunt, 29-Apr-2024.) |
β’ (π β π β β0) β β’ (π β (2β(2 Β· π)) β€ (((2 Β· π) + 1) Β· ((2 Β· π)Cπ))) | ||
Theorem | lcmineqlem18 40389 | 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 40390 | Dividing implies inequality for lcm inequality lemma. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) β β’ (π β ((π Β· ((2 Β· π) + 1)) Β· ((2 Β· π)Cπ)) β₯ (lcmβ(1...((2 Β· π) + 1)))) | ||
Theorem | lcmineqlem20 40391 | Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) β β’ (π β (π Β· (2β(2 Β· π))) β€ (lcmβ(1...((2 Β· π) + 1)))) | ||
Theorem | lcmineqlem21 40392 | 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 40393 | 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 40394 | Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β 9 β€ π) β β’ (π β (2βπ) β€ (lcmβ(1...π))) | ||
Theorem | lcmineqlem 40395 | 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 40396 | 3 to the power of 7 equals 2187. (Contributed by metakunt, 21-Aug-2024.) |
β’ (3β7) = ;;;2187 | ||
Theorem | 3lexlogpow5ineq1 40397 | First inequality in inequality chain, proposed by Mario Carneiro (Contributed by metakunt, 22-May-2024.) |
β’ 9 < ((;11 / 7)β5) | ||
Theorem | 3lexlogpow5ineq2 40398 | Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.) |
β’ (π β π β β) & β’ (π β 3 β€ π) β β’ (π β ((;11 / 7)β5) β€ ((2 logb π)β5)) | ||
Theorem | 3lexlogpow5ineq4 40399 | Sharper logarithm inequality chain. (Contributed by metakunt, 21-Aug-2024.) |
β’ (π β π β β) & β’ (π β 3 β€ π) β β’ (π β 9 < ((2 logb π)β5)) | ||
Theorem | 3lexlogpow5ineq3 40400 | 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)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |