Home | Metamath
Proof Explorer Theorem List (p. 449 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-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | smfdivdmmbl 44801 | If a functions and a sigma-measurable function have domains in the sigma-algebra, the domain of the division of the two functions is in the sigma-algebra. This is the third statement of Proposition 121H of [Fremlin1] p. 39 . Note: While the theorem in the book assumes both functions are sigma-measurable, this assumption is unnecessary for the part concerning their division, for the function at the numerator (it is needed only for the function at the denominator). (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
β’ β²π₯π & β’ β²π₯π΅ & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ ((π β§ π₯ β π΅) β π· β π) & β’ (π β (π₯ β π΅ β¦ π·) β (SMblFnβπ)) & β’ πΈ = {π₯ β π΅ β£ π· β 0} β β’ (π β (π΄ β© πΈ) β π) | ||
Theorem | smfpimne 44802* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of reals that are different from a value in the extended reals is in the subspace of sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
β’ β²π₯π & β’ β²π₯πΉ & β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ (π β π΄ β β*) β β’ (π β {π₯ β π· β£ (πΉβπ₯) β π΄} β (π βΎt π·)) | ||
Theorem | smfpimne2 44803* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of reals that are different from a value is in the subspace sigma-algebra induced by its domain. Notice that π΄ is not assumed to be an extended real. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
β’ β²π₯π & β’ β²π₯πΉ & β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ β β’ (π β {π₯ β π· β£ (πΉβπ₯) β π΄} β (π βΎt π·)) | ||
Theorem | smfdivdmmbl2 44804 | If a functions and a sigma-measurable function have domains in the sigma-algebra, the domain of the division of the two functions is in the sigma-algebra. This is the third statement of Proposition 121H of [Fremlin1] p. 39 . Note: While the theorem in the book assumes both functions are sigma-measurable, this assumption is unnecessary for the part concerning their division, for the function at the numerator. It is required only for the function at the denominator. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
β’ β²π₯π & β’ β²π₯πΉ & β’ β²π₯πΊ & β’ (π β π β SAlg) & β’ (π β πΉ:π΄βΆπ) & β’ (π β πΊ β (SMblFnβπ)) & β’ (π β π΄ β π) & β’ (π β dom πΊ β π) & β’ π· = {π₯ β dom πΊ β£ (πΊβπ₯) β 0} & β’ π» = (π₯ β (dom πΉ β© π·) β¦ ((πΉβπ₯) / (πΊβπ₯))) β β’ (π β dom π» β π) | ||
Theorem | fsupdm 44805* | The domain of the sup function is defined in Proposition 121F (b) of [Fremlin1], p. 38. Note that this definition of the sup function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fourth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
β’ β²ππ & β’ β²π₯π & β’ β²ππ & β’ β²π₯πΉ & β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ*) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} & β’ π» = (π β π β¦ (π β β β¦ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < π})) β β’ (π β π· = βͺ π β β β© π β π ((π»βπ)βπ)) | ||
Theorem | fsupdm2 44806* | The domain of the sup function is defined in Proposition 121F (b) of [Fremlin1], p. 38. Note that this definition of the sup function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fourth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
β’ β²ππ & β’ β²π₯π & β’ β²ππ & β’ β²π₯πΉ & β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ*) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} & β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) & β’ π» = (π β π β¦ (π β β β¦ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < π})) β β’ (π β dom πΊ = βͺ π β β β© π β π ((π»βπ)βπ)) | ||
Theorem | smfsupdmmbllem 44807* | If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their supremum function has the domain in the sigma-algebra. This is the fourth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
β’ β²ππ & β’ β²π₯π & β’ β²ππ & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ ((π β§ π β π) β dom (πΉβπ) β π) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} & β’ π» = (π β π β¦ (π β β β¦ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < π})) & β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) β β’ (π β dom πΊ β π) | ||
Theorem | smfsupdmmbl 44808* | If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their supremum function has the domain in the sigma-algebra. This is the fourth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
β’ β²ππ & β’ β²π₯π & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ ((π β§ π β π) β dom (πΉβπ) β π) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} & β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) β β’ (π β dom πΊ β π) | ||
Theorem | sigarval 44809* | Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) = (ββ((ββπ΄) Β· π΅))) | ||
Theorem | sigarim 44810* | Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) β β) | ||
Theorem | sigarac 44811* | Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) = -(π΅πΊπ΄)) | ||
Theorem | sigaraf 44812* | Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + πΆ)πΊπ΅) = ((π΄πΊπ΅) + (πΆπΊπ΅))) | ||
Theorem | sigarmf 44813* | Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β πΆ)πΊπ΅) = ((π΄πΊπ΅) β (πΆπΊπ΅))) | ||
Theorem | sigaras 44814* | Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ + πΆ)) = ((π΄πΊπ΅) + (π΄πΊπΆ))) | ||
Theorem | sigarms 44815* | Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ β πΆ)) = ((π΄πΊπ΅) β (π΄πΊπΆ))) | ||
Theorem | sigarls 44816* | Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ Β· πΆ)) = ((π΄πΊπ΅) Β· πΆ)) | ||
Theorem | sigarid 44817* | Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ (π΄ β β β (π΄πΊπ΄) = 0) | ||
Theorem | sigarexp 44818* | Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β πΆ)πΊ(π΅ β πΆ)) = (((π΄πΊπ΅) β (π΄πΊπΆ)) β (πΆπΊπ΅))) | ||
Theorem | sigarperm 44819* | Signed area (π΄ β πΆ)πΊ(π΅ β πΆ) acts as a double area of a triangle π΄π΅πΆ. Here we prove that cyclically permuting the vertices doesn't change the area. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β πΆ)πΊ(π΅ β πΆ)) = ((π΅ β π΄)πΊ(πΆ β π΄))) | ||
Theorem | sigardiv 44820* | If signed area between vectors π΅ β π΄ and πΆ β π΄ is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β Β¬ πΆ = π΄) & β’ (π β ((π΅ β π΄)πΊ(πΆ β π΄)) = 0) β β’ (π β ((π΅ β π΄) / (πΆ β π΄)) β β) | ||
Theorem | sigarimcd 44821* | Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β)) β β’ (π β (π΄πΊπ΅) β β) | ||
Theorem | sigariz 44822* | If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β)) & β’ (π β (π΄πΊπ΅) = 0) β β’ (π β (π΅πΊπ΄) = 0) | ||
Theorem | sigarcol 44823* | Given three points π΄, π΅ and πΆ such that Β¬ π΄ = π΅, the point πΆ lies on the line going through π΄ and π΅ iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β Β¬ π΄ = π΅) β β’ (π β (((π΄ β πΆ)πΊ(π΅ β πΆ)) = 0 β βπ‘ β β πΆ = (π΅ + (π‘ Β· (π΄ β π΅))))) | ||
Theorem | sharhght 44824* | Let π΄π΅πΆ be a triangle, and let π· lie on the line π΄π΅. Then (doubled) areas of triangles π΄π·πΆ and πΆπ·π΅ relate as lengths of corresponding bases π΄π· and π·π΅. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (π· β β β§ ((π΄ β π·)πΊ(π΅ β π·)) = 0)) β β’ (π β (((πΆ β π΄)πΊ(π· β π΄)) Β· (π΅ β π·)) = (((πΆ β π΅)πΊ(π· β π΅)) Β· (π΄ β π·))) | ||
Theorem | sigaradd 44825* | Subtracting (double) area of π΄π·πΆ from π΄π΅πΆ yields the (double) area of π·π΅πΆ. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (π· β β β§ ((π΄ β π·)πΊ(π΅ β π·)) = 0)) β β’ (π β (((π΅ β πΆ)πΊ(π΄ β πΆ)) β ((π· β πΆ)πΊ(π΄ β πΆ))) = ((π΅ β πΆ)πΊ(π· β πΆ))) | ||
Theorem | cevathlem1 44826 | Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (π· β β β§ πΈ β β β§ πΉ β β)) & β’ (π β (πΊ β β β§ π» β β β§ πΎ β β)) & β’ (π β (π΄ β 0 β§ πΈ β 0 β§ πΆ β 0)) & β’ (π β ((π΄ Β· π΅) = (πΆ Β· π·) β§ (πΈ Β· πΉ) = (π΄ Β· πΊ) β§ (πΆ Β· π») = (πΈ Β· πΎ))) β β’ (π β ((π΅ Β· πΉ) Β· π») = ((π· Β· πΊ) Β· πΎ)) | ||
Theorem | cevathlem2 44827* | Ceva's theorem second lemma. Relate (doubled) areas of triangles πΆπ΄π and π΄π΅π with of segments π΅π· and π·πΆ. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (πΉ β β β§ π· β β β§ πΈ β β)) & β’ (π β π β β) & β’ (π β (((π΄ β π)πΊ(π· β π)) = 0 β§ ((π΅ β π)πΊ(πΈ β π)) = 0 β§ ((πΆ β π)πΊ(πΉ β π)) = 0)) & β’ (π β (((π΄ β πΉ)πΊ(π΅ β πΉ)) = 0 β§ ((π΅ β π·)πΊ(πΆ β π·)) = 0 β§ ((πΆ β πΈ)πΊ(π΄ β πΈ)) = 0)) & β’ (π β (((π΄ β π)πΊ(π΅ β π)) β 0 β§ ((π΅ β π)πΊ(πΆ β π)) β 0 β§ ((πΆ β π)πΊ(π΄ β π)) β 0)) β β’ (π β (((πΆ β π)πΊ(π΄ β π)) Β· (π΅ β π·)) = (((π΄ β π)πΊ(π΅ β π)) Β· (π· β πΆ))) | ||
Theorem | cevath 44828* |
Ceva's theorem. Let π΄π΅πΆ be a triangle and let points πΉ,
π· and πΈ lie on sides π΄π΅, π΅πΆ, πΆπ΄
correspondingly. Suppose that cevians π΄π·, π΅πΈ and πΆπΉ
intersect at one point π. Then triangle's sides are
partitioned
into segments and their lengths satisfy a certain identity. Here we
obtain a bit stronger version by using complex numbers themselves
instead of their absolute values.
The proof goes by applying cevathlem2 44827 three times and then using cevathlem1 44826 to multiply obtained identities and prove the theorem. In the theorem statement we are using function πΊ as a collinearity indicator. For justification of that use, see sigarcol 44823. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (πΉ β β β§ π· β β β§ πΈ β β)) & β’ (π β π β β) & β’ (π β (((π΄ β π)πΊ(π· β π)) = 0 β§ ((π΅ β π)πΊ(πΈ β π)) = 0 β§ ((πΆ β π)πΊ(πΉ β π)) = 0)) & β’ (π β (((π΄ β πΉ)πΊ(π΅ β πΉ)) = 0 β§ ((π΅ β π·)πΊ(πΆ β π·)) = 0 β§ ((πΆ β πΈ)πΊ(π΄ β πΈ)) = 0)) & β’ (π β (((π΄ β π)πΊ(π΅ β π)) β 0 β§ ((π΅ β π)πΊ(πΆ β π)) β 0 β§ ((πΆ β π)πΊ(π΄ β π)) β 0)) β β’ (π β (((π΄ β πΉ) Β· (πΆ β πΈ)) Β· (π΅ β π·)) = (((πΉ β π΅) Β· (πΈ β π΄)) Β· (π· β πΆ))) | ||
Theorem | simpcntrab 44829 | The center of a simple group is trivial or the group is abelian. (Contributed by SS, 3-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (CntrβπΊ) & β’ (π β πΊ β SimpGrp) β β’ (π β (π = { 0 } β¨ πΊ β Abel)) | ||
Theorem | et-ltneverrefl 44830 | Less-than class is never reflexive. (Contributed by Ender Ting, 22-Nov-2024.) Prefer to specify theorem domain and then apply ltnri 11198. (New usage is discouraged.) |
β’ Β¬ π΄ < π΄ | ||
Theorem | et-equeucl 44831 | Alternative proof that equality is left-Euclidean, using ax7 2020 directly instead of utility theorems; done for practice. (Contributed by Ender Ting, 21-Dec-2024.) |
β’ (π₯ = π§ β (π¦ = π§ β π₯ = π¦)) | ||
Theorem | et-sqrtnegnre 44832 | The square root of a negative number is not a real number. (Contributed by Ender Ting, 5-Jan-2025.) |
β’ ((π΄ β β β§ π΄ < 0) β Β¬ (ββπ΄) β β) | ||
Theorem | natlocalincr 44833* | Global monotonicity on half-open range implies local monotonicity. Inference form. (Contributed by Ender Ting, 22-Nov-2024.) |
β’ βπ β (0..^π)βπ‘ β (1..^(π + 1))(π < π‘ β (π΅βπ) < (π΅βπ‘)) β β’ βπ β (0..^π)(π΅βπ) < (π΅β(π + 1)) | ||
Theorem | natglobalincr 44834* | Local monotonicity on half-open integer range implies global monotonicity. Inference form. (Contributed by Ender Ting, 23-Nov-2024.) |
β’ βπ β (0..^π)(π΅βπ) < (π΅β(π + 1)) & β’ π β β€ β β’ βπ β (0..^π)βπ‘ β ((π + 1)...π)(π΅βπ) < (π΅βπ‘) | ||
Syntax | cupword 44835 | Extend class notation to include the set of strictly increasing sequences. |
class UpWordπ | ||
Definition | df-upword 44836* | Strictly increasing sequence is a sequence, adjacent elements of which increase. (Contributed by Ender Ting, 19-Nov-2024.) |
β’ UpWordπ = {π€ β£ (π€ β Word π β§ βπ β (0..^((β―βπ€) β 1))(π€βπ) < (π€β(π + 1)))} | ||
Theorem | upwordnul 44837 | Empty set is an increasing sequence for every range. (Contributed by Ender Ting, 19-Nov-2024.) |
β’ β β UpWordπ | ||
Theorem | upwordisword 44838 | Any increasing sequence is a sequence. (Contributed by Ender Ting, 19-Nov-2024.) |
β’ (π΄ β UpWordπ β π΄ β Word π) | ||
Theorem | singoutnword 44839 | Singleton with character out of range π is not a word for that range. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π΄ β V β β’ (Β¬ π΄ β π β Β¬ β¨βπ΄ββ© β Word π) | ||
Theorem | singoutnupword 44840 | Singleton with character out of range π is not an increasing sequence for that range. (Contributed by Ender Ting, 22-Nov-2024.) |
β’ π΄ β V β β’ (Β¬ π΄ β π β Β¬ β¨βπ΄ββ© β UpWordπ) | ||
Theorem | upwordsing 44841 | Singleton is an increasing sequence for any compatible range. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π΄ β π β β’ β¨βπ΄ββ© β UpWordπ | ||
Theorem | upwordsseti 44842 | Strictly increasing sequences with a set given for range form a set. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π β V β β’ UpWordπ β V | ||
Theorem | tworepnotupword 44843 | Concatenation of identical singletons is never an increasing sequence. (Contributed by Ender Ting, 22-Nov-2024.) |
β’ π΄ β V β β’ Β¬ (β¨βπ΄ββ© ++ β¨βπ΄ββ©) β UpWordπ | ||
Theorem | upwrdfi 44844* | There is a finite number of strictly increasing sequences of a given length over finite alphabet. Trivially holds for invalid lengths where there're zero matching sequences. (Contributed by Ender Ting, 5-Jan-2024.) |
β’ (π β Fin β {π β UpWordπ β£ (β―βπ) = π} β Fin) | ||
Theorem | hirstL-ax3 44845 | The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015.) (Proof modification is discouraged.) |
β’ ((Β¬ π β Β¬ π) β ((Β¬ π β π) β π)) | ||
Theorem | ax3h 44846 | Recover ax-3 8 from hirstL-ax3 44845. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((Β¬ π β Β¬ π) β (π β π)) | ||
Theorem | aibandbiaiffaiffb 44847 | A closed form showing (a implies b and b implies a) same-as (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.) |
β’ (((π β π) β§ (π β π)) β (π β π)) | ||
Theorem | aibandbiaiaiffb 44848 | A closed form showing (a implies b and b implies a) implies (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.) |
β’ (((π β π) β§ (π β π)) β (π β π)) | ||
Theorem | notatnand 44849 | Do not use. Use intnanr instead. Given not a, there exists a proof for not (a and b). (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ Β¬ π β β’ Β¬ (π β§ π) | ||
Theorem | aistia 44850 | Given a is equivalent to β€, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
β’ (π β β€) β β’ π | ||
Theorem | aisfina 44851 | Given a is equivalent to β₯, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
β’ (π β β₯) β β’ Β¬ π | ||
Theorem | bothtbothsame 44852 | Given both a, b are equivalent to β€, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ (π β β€) & β’ (π β β€) β β’ (π β π) | ||
Theorem | bothfbothsame 44853 | Given both a, b are equivalent to β₯, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ (π β β₯) & β’ (π β β₯) β β’ (π β π) | ||
Theorem | aiffbbtat 44854 | Given a is equivalent to b, b is equivalent to β€ there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
β’ (π β π) & β’ (π β β€) β β’ (π β β€) | ||
Theorem | aisbbisfaisf 44855 | Given a is equivalent to b, b is equivalent to β₯ there exists a proof for a is equivalent to F. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
β’ (π β π) & β’ (π β β₯) β β’ (π β β₯) | ||
Theorem | axorbtnotaiffb 44856 | Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1511 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
β’ (π β» π) β β’ Β¬ (π β π) | ||
Theorem | aiffnbandciffatnotciffb 44857 | Given a is equivalent to (not b), c is equivalent to a, there exists a proof for ( not ( c iff b ) ). (Contributed by Jarvin Udandy, 7-Sep-2016.) |
β’ (π β Β¬ π) & β’ (π β π) β β’ Β¬ (π β π) | ||
Theorem | axorbciffatcxorb 44858 | Given a is equivalent to (not b), c is equivalent to a. there exists a proof for ( c xor b ). (Contributed by Jarvin Udandy, 7-Sep-2016.) |
β’ (π β» π) & β’ (π β π) β β’ (π β» π) | ||
Theorem | aibnbna 44859 | Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.) |
β’ (π β π) & β’ Β¬ π β β’ Β¬ π | ||
Theorem | aibnbaif 44860 | Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.) |
β’ (π β π) & β’ Β¬ π β β’ (π β β₯) | ||
Theorem | aiffbtbat 44861 | Given a is equivalent to b, T. is equivalent to b. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
β’ (π β π) & β’ (β€ β π) β β’ (π β β€) | ||
Theorem | astbstanbst 44862 | Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for a and b is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
β’ (π β β€) & β’ (π β β€) β β’ ((π β§ π) β β€) | ||
Theorem | aistbistaandb 44863 | Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for (a and b). (Contributed by Jarvin Udandy, 9-Sep-2016.) |
β’ (π β β€) & β’ (π β β€) β β’ (π β§ π) | ||
Theorem | aisbnaxb 44864 | Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.) |
β’ (π β π) β β’ Β¬ (π β» π) | ||
Theorem | atbiffatnnb 44865 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.) |
β’ ((π β π) β (π β Β¬ Β¬ π)) | ||
Theorem | bisaiaisb 44866 | Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ ((π β π) β (π β π)) | ||
Theorem | atbiffatnnbalt 44867 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
β’ ((π β π) β (π β Β¬ Β¬ π)) | ||
Theorem | abnotbtaxb 44868 | Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ π & β’ Β¬ π β β’ (π β» π) | ||
Theorem | abnotataxb 44869 | Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ Β¬ π & β’ π β β’ (π β» π) | ||
Theorem | conimpf 44870 | Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 28-Aug-2016.) |
β’ π & β’ Β¬ π & β’ (π β π) β β’ (π β β₯) | ||
Theorem | conimpfalt 44871 | Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 29-Aug-2016.) |
β’ π & β’ Β¬ π & β’ (π β π) β β’ (π β β₯) | ||
Theorem | aistbisfiaxb 44872 | Given a is equivalent to T., Given b is equivalent to F. there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ (π β β€) & β’ (π β β₯) β β’ (π β» π) | ||
Theorem | aisfbistiaxb 44873 | Given a is equivalent to F., Given b is equivalent to T., there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ (π β β₯) & β’ (π β β€) β β’ (π β» π) | ||
Theorem | aifftbifffaibif 44874 | Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a implies b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
β’ (π β β€) & β’ (π β β₯) β β’ ((π β π) β β₯) | ||
Theorem | aifftbifffaibifff 44875 | Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a iff b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
β’ (π β β€) & β’ (π β β₯) β β’ ((π β π) β β₯) | ||
Theorem | atnaiana 44876 | Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
β’ π β β’ Β¬ (π β (π β§ Β¬ π)) | ||
Theorem | ainaiaandna 44877 | Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
β’ π β β’ (π β Β¬ (π β (π β§ Β¬ π))) | ||
Theorem | abcdta 44878 | Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
β’ (((π β§ π) β§ π) β§ π) β β’ π | ||
Theorem | abcdtb 44879 | Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
β’ (((π β§ π) β§ π) β§ π) β β’ π | ||
Theorem | abcdtc 44880 | Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
β’ (((π β§ π) β§ π) β§ π) β β’ π | ||
Theorem | abcdtd 44881 | Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
β’ (((π β§ π) β§ π) β§ π) β β’ π | ||
Theorem | abciffcbatnabciffncba 44882 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. Closed form. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
β’ (Β¬ ((π β§ π) β§ π) β Β¬ ((π β§ π) β§ π)) | ||
Theorem | abciffcbatnabciffncbai 44883 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
β’ (((π β§ π) β§ π) β ((π β§ π) β§ π)) β β’ (Β¬ ((π β§ π) β§ π) β Β¬ ((π β§ π) β§ π)) | ||
Theorem | nabctnabc 44884 | not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.) |
β’ Β¬ (π β (π β§ π)) β β’ (Β¬ π β (π β§ π)) | ||
Theorem | jabtaib 44885 | For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.) |
β’ (π β§ π) β β’ (π β π) | ||
Theorem | onenotinotbothi 44886 | From one negated implication it is not the case its nonnegated form and a random others are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
β’ Β¬ (π β π) β β’ Β¬ ((π β π) β§ (π β π)) | ||
Theorem | twonotinotbothi 44887 | From these two negated implications it is not the case their nonnegated forms are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
β’ Β¬ (π β π) & β’ Β¬ (π β π) β β’ Β¬ ((π β π) β§ (π β π)) | ||
Theorem | clifte 44888 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
β’ (π β§ Β¬ π) & β’ π β β’ (π β ((π β§ Β¬ π) β¨ (π β§ π))) | ||
Theorem | cliftet 44889 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
β’ (π β§ π) & β’ π β β’ (π β ((π β§ π) β¨ (π β§ Β¬ π))) | ||
Theorem | clifteta 44890 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
β’ ((π β§ Β¬ π) β¨ (π β§ π)) & β’ π β β’ (π β ((π β§ Β¬ π) β¨ (π β§ π))) | ||
Theorem | cliftetb 44891 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
β’ ((π β§ π) β¨ (π β§ Β¬ π)) & β’ π β β’ (π β ((π β§ π) β¨ (π β§ Β¬ π))) | ||
Theorem | confun 44892 | Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.) |
β’ π & β’ (π β π) & β’ (π β π) & β’ (π β (π β π)) β β’ (π β (π β π)) | ||
Theorem | confun2 44893 | Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
β’ (π β π) & β’ (π β Β¬ (π β (π β§ Β¬ π))) & β’ ((π β π) β ((π β π) β π)) β β’ (π β (Β¬ (π β (π β§ Β¬ π)) β (π β π))) | ||
Theorem | confun3 44894 | Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.) |
β’ (π β (π β π)) & β’ (π β Β¬ (π β (π β§ Β¬ π))) & β’ (π β π) & β’ (π β Β¬ (π β (π β§ Β¬ π))) & β’ ((π β π) β ((π β π) β π)) β β’ (π β (Β¬ (π β (π β§ Β¬ π)) β (π β π))) | ||
Theorem | confun4 44895 | An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
β’ π & β’ ((π β π) β π) & β’ (π β (π β π)) & β’ ((π β π) β ((π β π) β π)) & β’ (π β (π β π)) & β’ (π β Β¬ (π β (π β§ Β¬ π))) & β’ π & β’ (π β π) β β’ (π β (π β π)) | ||
Theorem | confun5 44896 | An attempt at derivative. Resisted simplest path to a proof. Interesting that ch, th, ta, et were all provable. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
β’ π & β’ ((π β π) β π) & β’ (π β (π β π)) & β’ ((π β π) β ((π β π) β π)) & β’ (π β (π β π)) & β’ (π β Β¬ (π β (π β§ Β¬ π))) & β’ π & β’ (π β π) β β’ (π β (π β π)) | ||
Theorem | plcofph 44897 | Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
β’ (π β ((((π β§ π) β π) β (π β§ Β¬ (π β§ Β¬ π))) β§ (π β§ Β¬ (π β§ Β¬ π)))) & β’ π & β’ π β β’ π | ||
Theorem | pldofph 44898 | Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
β’ (π β ((π β π) β§ (π β π) β§ ((π β π) β (π β π)))) & β’ π & β’ π & β’ π & β’ π β β’ π | ||
Theorem | plvcofph 44899 | Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
β’ (π β ((((π β§ π) β π) β (π β§ Β¬ (π β§ Β¬ π))) β§ (π β§ Β¬ (π β§ Β¬ π)))) & β’ (π β ((π β π) β§ (π β π) β§ ((π β π) β (π β π)))) & β’ (π β (π β§ π)) & β’ π & β’ π & β’ π β β’ π | ||
Theorem | plvcofphax 44900 | Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
β’ (π β ((((π β§ π) β π) β (π β§ Β¬ (π β§ Β¬ π))) β§ (π β§ Β¬ (π β§ Β¬ π)))) & β’ (π β ((π β π) β§ (π β π) β§ ((π β π) β (π β π)))) & β’ (π β (π β§ π)) & β’ π & β’ π & β’ π & β’ (π β Β¬ (π β§ Β¬ π)) β β’ π |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |