![]() |
Metamath
Proof Explorer Theorem List (p. 409 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hlhilsca 40801 | The scalar of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ π = (πΈ sSet β¨(*πβndx), πΊβ©) β β’ (π β π = (Scalarβπ)) | ||
Theorem | hlhilbase 40802 | The base set of the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (BaseβπΏ) β β’ (π β π = (Baseβπ)) | ||
Theorem | hlhilplus 40803 | The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ + = (+gβπΏ) β β’ (π β + = (+gβπ)) | ||
Theorem | hlhilslem 40804 | Lemma for hlhilsbase 40806 etc. (Contributed by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΉ = Slot (πΉβndx) & β’ (πΉβndx) β (*πβndx) & β’ πΆ = (πΉβπΈ) β β’ (π β πΆ = (πΉβπ )) | ||
Theorem | hlhilslemOLD 40805 | Obsolete version of hlhilslem 40804 as of 6-Nov-2024. Lemma for hlhilsbase 40806. (Contributed by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΉ = Slot π & β’ π β β & β’ π < 4 & β’ πΆ = (πΉβπΈ) β β’ (π β πΆ = (πΉβπ )) | ||
Theorem | hlhilsbase 40806 | The scalar base set of 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 β§ π β π»)) & β’ πΆ = (BaseβπΈ) β β’ (π β πΆ = (Baseβπ )) | ||
Theorem | hlhilsbaseOLD 40807 | Obsolete version of hlhilsbase 40806 as of 6-Nov-2024. The scalar base set of 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 β§ π β π»)) & β’ πΆ = (BaseβπΈ) β β’ (π β πΆ = (Baseβπ )) | ||
Theorem | hlhilsplus 40808 | Scalar addition 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 β§ π β π»)) & β’ + = (+gβπΈ) β β’ (π β + = (+gβπ )) | ||
Theorem | hlhilsplusOLD 40809 | Obsolete version of hlhilsplus 40808 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 40810 | 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 40811 | Obsolete version of hlhilsmul 40810 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 40812 | 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 40813 | 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 40814 | 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 40815 | 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 40816 | 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 40817 | 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 40818* | 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 40819 | 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 40820 | 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 40821 | 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 40822 | 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 40823 | Lemma for hlhilsrng 40824. (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 40824 | 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 40825 | 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 40826 | 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 40827 | 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 40828 | The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 40802 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 40829* | Lemma for hlhil 24959. (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 40830* | Lemma for hlhil 24959. (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 40831 |
Construction of a Hilbert space (df-hil 21258) π from a Hilbert
lattice (df-hlat 38216) πΎ, where π is a fixed but arbitrary
hyperplane (co-atom) in πΎ.
The Hilbert space π is identical to the vector space ((DVecHβπΎ)βπ) (see dvhlvec 39975) 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 39975. π 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 21258. 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 40832 | Weak base ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β0) & β’ (π β 0 β€ π΄) & β’ (π β π΄ β€ π΅) β β’ (π β (π΄βπ) β€ (π΅βπ)) | ||
Theorem | relogbcld 40833 | 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 40834 | 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 40835 | 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 40836 | The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.) |
β’ (π β π΅ β β€) & β’ (π β 2 β€ π΅) & β’ (π β π β β) & β’ (π β 0 < π) & β’ (π β π β β) & β’ (π β 0 < π) & β’ (π β π β€ π) β β’ (π β (π΅ logb π) β€ (π΅ logb π)) | ||
Theorem | uzindd 40837* | 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 40838 | Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π½ β (π...π)) & β’ (π β πΎ β (π...π)) & β’ (π β π = (π + π)) & β’ (π β π = (π + π)) β β’ (π β (π½ + πΎ) β (π...π )) | ||
Theorem | zltlem1d 40839 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π < π β π β€ (π β 1))) | ||
Theorem | zltp1led 40840 | Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π < π β (π + 1) β€ π)) | ||
Theorem | fzne2d 40841 | Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.) |
β’ (π β πΎ β (π...π)) & β’ (π β πΎ β π) β β’ (π β πΎ < π) | ||
Theorem | eqfnfv2d2 40842* | Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.) |
β’ (π β πΉ Fn π΄) & β’ (π β πΊ Fn π΅) & β’ (π β π΄ = π΅) & β’ ((π β§ π₯ β π΄) β (πΉβπ₯) = (πΊβπ₯)) β β’ (π β πΉ = πΊ) | ||
Theorem | fzsplitnd 40843 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
β’ (π β πΎ β (π...π)) β β’ (π β (π...π) = ((π...(πΎ β 1)) βͺ (πΎ...π))) | ||
Theorem | fzsplitnr 40844 | Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β β€) & β’ (π β π β€ πΎ) & β’ (π β πΎ β€ π) β β’ (π β (π...π) = ((π...(πΎ β 1)) βͺ (πΎ...π))) | ||
Theorem | addassnni 40845 | Associative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ)) | ||
Theorem | addcomnni 40846 | Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ + π΅) = (π΅ + π΄) | ||
Theorem | mulassnni 40847 | Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ)) | ||
Theorem | mulcomnni 40848 | Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β· π΅) = (π΅ Β· π΄) | ||
Theorem | gcdcomnni 40849 | Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd π) = (π gcd π) | ||
Theorem | gcdnegnni 40850 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd -π) = (π gcd π) | ||
Theorem | neggcdnni 40851 | Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (-π gcd π) = (π gcd π) | ||
Theorem | bccl2d 40852 | Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β πΎ β β0) & β’ (π β πΎ β€ π) β β’ (π β (πCπΎ) β β) | ||
Theorem | recbothd 40853 | Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β π΅ β 0) & β’ (π β πΆ β β) & β’ (π β πΆ β 0) & β’ (π β π· β β) & β’ (π β π· β 0) β β’ (π β ((π΄ / π΅) = (πΆ / π·) β (π΅ / π΄) = (π· / πΆ))) | ||
Theorem | gcdmultiplei 40854 | The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd (π Β· π)) = π | ||
Theorem | gcdaddmzz2nni 40855 | 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 40856 | 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 40857 | Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β β β’ (π gcd π) β β | ||
Theorem | muldvds1d 40858 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β (πΎ Β· π) β₯ π) β β’ (π β πΎ β₯ π) | ||
Theorem | muldvds2d 40859 | If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β (πΎ Β· π) β₯ π) β β’ (π β π β₯ π) | ||
Theorem | nndivdvdsd 40860 | A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds 16205. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) β β’ (π β (π β₯ π β (π / π) β β)) | ||
Theorem | nnproddivdvdsd 40861 | 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 40862 | 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 40863 | The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;12 gcd 5) = 1 | ||
Theorem | 60gcd6e6 40864 | The gcd of 60 and 6 is 6. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 gcd 6) = 6 | ||
Theorem | 60gcd7e1 40865 | The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 gcd 7) = 1 | ||
Theorem | 420gcd8e4 40866 | The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;;420 gcd 8) = 4 | ||
Theorem | lcmeprodgcdi 40867 | Calculate the least common multiple of two natural numbers. (Contributed by metakunt, 25-Apr-2024.) |
β’ π β β & β’ π β β & β’ πΊ β β & β’ π» β β & β’ (π gcd π) = πΊ & β’ (πΊ Β· π») = π΄ & β’ (π Β· π) = π΄ β β’ (π lcm π) = π» | ||
Theorem | 12lcm5e60 40868 | The lcm of 12 and 5 is 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;12 lcm 5) = ;60 | ||
Theorem | 60lcm6e60 40869 | The lcm of 60 and 6 is 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 lcm 6) = ;60 | ||
Theorem | 60lcm7e420 40870 | The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;60 lcm 7) = ;;420 | ||
Theorem | 420lcm8e840 40871 | The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024.) |
β’ (;;420 lcm 8) = ;;840 | ||
Theorem | lcmfunnnd 40872 | 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 40873 | Least common multiple of natural numbers up to 1 equals 1. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...1)) = 1 | ||
Theorem | lcm2un 40874 | Least common multiple of natural numbers up to 2 equals 2. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...2)) = 2 | ||
Theorem | lcm3un 40875 | Least common multiple of natural numbers up to 3 equals 6. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...3)) = 6 | ||
Theorem | lcm4un 40876 | Least common multiple of natural numbers up to 4 equals 12. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...4)) = ;12 | ||
Theorem | lcm5un 40877 | Least common multiple of natural numbers up to 5 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...5)) = ;60 | ||
Theorem | lcm6un 40878 | Least common multiple of natural numbers up to 6 equals 60. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...6)) = ;60 | ||
Theorem | lcm7un 40879 | Least common multiple of natural numbers up to 7 equals 420. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...7)) = ;;420 | ||
Theorem | lcm8un 40880 | Least common multiple of natural numbers up to 8 equals 840. (Contributed by metakunt, 25-Apr-2024.) |
β’ (lcmβ(1...8)) = ;;840 | ||
Theorem | 3factsumint1 40881* | 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 40882* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
β’ ((π β§ π₯ β π΄) β πΉ β β) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β π» β β) β β’ (π β Ξ£π β π΅ β«π΄(πΉ Β· (πΊ Β· π»)) dπ₯ = Ξ£π β π΅ β«π΄(πΊ Β· (πΉ Β· π»)) dπ₯) | ||
Theorem | 3factsumint3 40883* | 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 40884* | Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.) |
β’ (π β π΅ β Fin) & β’ ((π β§ π₯ β π΄) β πΉ β β) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β π» β β) β β’ (π β β«π΄Ξ£π β π΅ (πΉ Β· (πΊ Β· π»)) dπ₯ = β«π΄(πΉ Β· Ξ£π β π΅ (πΊ Β· π»)) dπ₯) | ||
Theorem | 3factsumint 40885* | Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024.) |
β’ π΄ = (πΏ[,]π) & β’ (π β π΅ β Fin) & β’ (π β πΏ β β) & β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ πΉ) β (π΄βcnββ)) & β’ ((π β§ π β π΅) β πΊ β β) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ π») β (π΄βcnββ)) β β’ (π β β«π΄(πΉ Β· Ξ£π β π΅ (πΊ Β· π»)) dπ₯ = Ξ£π β π΅ (πΊ Β· β«π΄(πΉ Β· π») dπ₯)) | ||
Theorem | resopunitintvd 40886 | Restrict continuous function on open unit interval. (Contributed by metakunt, 12-May-2024.) |
β’ (π β (π₯ β β β¦ π΄) β (ββcnββ)) β β’ (π β (π₯ β (0(,)1) β¦ π΄) β ((0(,)1)βcnββ)) | ||
Theorem | resclunitintvd 40887 | Restrict continuous function on closed unit interval. (Contributed by metakunt, 12-May-2024.) |
β’ (π β (π₯ β β β¦ π΄) β (ββcnββ)) β β’ (π β (π₯ β (0[,]1) β¦ π΄) β ((0[,]1)βcnββ)) | ||
Theorem | resdvopclptsd 40888* | Restrict derivative on unit interval. (Contributed by metakunt, 12-May-2024.) |
β’ (π β (β D (π₯ β β β¦ π΄)) = (π₯ β β β¦ π΅)) & β’ ((π β§ π₯ β β) β π΄ β β) & β’ ((π β§ π₯ β β) β π΅ β β) β β’ (π β (β D (π₯ β (0[,]1) β¦ π΄)) = (π₯ β (0(,)1) β¦ π΅)) | ||
Theorem | lcmineqlem1 40889* | 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 40890* | 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 40891* | 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 40892 | 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 40894. (Contributed by metakunt, 10-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β πΎ β (0...(π β π))) β β’ (π β ((lcmβ(1...π)) / (π + πΎ)) β β€) | ||
Theorem | lcmineqlem5 40893 | Technical lemma for reciprocal multiplication in deduction form. (Contributed by metakunt, 10-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β πΆ β 0) β β’ (π β (π΄ Β· (π΅ Β· (1 / πΆ))) = (π΅ Β· (π΄ / πΆ))) | ||
Theorem | lcmineqlem6 40894* | 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 40895 | Derivative of 1-x for chain rule application. (Contributed by metakunt, 12-May-2024.) |
β’ (β D (π₯ β β β¦ (1 β π₯))) = (π₯ β β β¦ -1) | ||
Theorem | lcmineqlem8 40896* | Derivative of (1-x)^(N-M). (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π < π) β β’ (π β (β D (π₯ β β β¦ ((1 β π₯)β(π β π)))) = (π₯ β β β¦ (-(π β π) Β· ((1 β π₯)β((π β π) β 1))))) | ||
Theorem | lcmineqlem9 40897* | (1-x)^(N-M) is continuous. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) β β’ (π β (π₯ β β β¦ ((1 β π₯)β(π β π))) β (ββcnββ)) | ||
Theorem | lcmineqlem10 40898* | Induction step of lcmineqlem13 40901 (deduction form). (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π < π) β β’ (π β β«(0[,]1)((π₯β((π + 1) β 1)) Β· ((1 β π₯)β(π β (π + 1)))) dπ₯ = ((π / (π β π)) Β· β«(0[,]1)((π₯β(π β 1)) Β· ((1 β π₯)β(π β π))) dπ₯)) | ||
Theorem | lcmineqlem11 40899 | Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π < π) β β’ (π β (1 / ((π + 1) Β· (πC(π + 1)))) = ((π / (π β π)) Β· (1 / (π Β· (πCπ))))) | ||
Theorem | lcmineqlem12 40900* | Base case for induction. (Contributed by metakunt, 12-May-2024.) |
β’ (π β π β β) β β’ (π β β«(0[,]1)((π‘β(1 β 1)) Β· ((1 β π‘)β(π β 1))) dπ‘ = (1 / (1 Β· (πC1)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |