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