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-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sigarperm 44801* | 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 44802* | 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 44803* | Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
โข ๐บ = (๐ฅ โ โ, ๐ฆ โ โ โฆ (โโ((โโ๐ฅ) ยท ๐ฆ))) & โข (๐ โ (๐ด โ โ โง ๐ต โ โ)) โ โข (๐ โ (๐ด๐บ๐ต) โ โ) | ||
Theorem | sigariz 44804* | 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 44805* | 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 44806* | 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 44807* | Subtracting (double) area of ๐ด๐ท๐ถ from ๐ด๐ต๐ถ yields the (double) area of ๐ท๐ต๐ถ. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
โข ๐บ = (๐ฅ โ โ, ๐ฆ โ โ โฆ (โโ((โโ๐ฅ) ยท ๐ฆ))) & โข (๐ โ (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) & โข (๐ โ (๐ท โ โ โง ((๐ด โ ๐ท)๐บ(๐ต โ ๐ท)) = 0)) โ โข (๐ โ (((๐ต โ ๐ถ)๐บ(๐ด โ ๐ถ)) โ ((๐ท โ ๐ถ)๐บ(๐ด โ ๐ถ))) = ((๐ต โ ๐ถ)๐บ(๐ท โ ๐ถ))) | ||
Theorem | cevathlem1 44808 | 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 44809* | 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 44810* |
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 44809 three times and then using cevathlem1 44808 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 44805. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
โข ๐บ = (๐ฅ โ โ, ๐ฆ โ โ โฆ (โโ((โโ๐ฅ) ยท ๐ฆ))) & โข (๐ โ (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) & โข (๐ โ (๐น โ โ โง ๐ท โ โ โง ๐ธ โ โ)) & โข (๐ โ ๐ โ โ) & โข (๐ โ (((๐ด โ ๐)๐บ(๐ท โ ๐)) = 0 โง ((๐ต โ ๐)๐บ(๐ธ โ ๐)) = 0 โง ((๐ถ โ ๐)๐บ(๐น โ ๐)) = 0)) & โข (๐ โ (((๐ด โ ๐น)๐บ(๐ต โ ๐น)) = 0 โง ((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) = 0 โง ((๐ถ โ ๐ธ)๐บ(๐ด โ ๐ธ)) = 0)) & โข (๐ โ (((๐ด โ ๐)๐บ(๐ต โ ๐)) โ 0 โง ((๐ต โ ๐)๐บ(๐ถ โ ๐)) โ 0 โง ((๐ถ โ ๐)๐บ(๐ด โ ๐)) โ 0)) โ โข (๐ โ (((๐ด โ ๐น) ยท (๐ถ โ ๐ธ)) ยท (๐ต โ ๐ท)) = (((๐น โ ๐ต) ยท (๐ธ โ ๐ด)) ยท (๐ท โ ๐ถ))) | ||
Theorem | simpcntrab 44811 | 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 44812 | 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 44813 | 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 44814 | The square root of a negative number is not a real number. (Contributed by Ender Ting, 5-Jan-2025.) |
โข ((๐ด โ โ โง ๐ด < 0) โ ยฌ (โโ๐ด) โ โ) | ||
Theorem | natlocalincr 44815* | 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 44816* | 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 44817 | Extend class notation to include the set of strictly increasing sequences. |
class UpWord๐ | ||
Definition | df-upword 44818* | 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 44819 | Empty set is an increasing sequence for every range. (Contributed by Ender Ting, 19-Nov-2024.) |
โข โ โ UpWord๐ | ||
Theorem | upwordisword 44820 | Any increasing sequence is a sequence. (Contributed by Ender Ting, 19-Nov-2024.) |
โข (๐ด โ UpWord๐ โ ๐ด โ Word ๐) | ||
Theorem | singoutnword 44821 | Singleton with character out of range ๐ is not a word for that range. (Contributed by Ender Ting, 21-Nov-2024.) |
โข ๐ด โ V โ โข (ยฌ ๐ด โ ๐ โ ยฌ โจโ๐ดโโฉ โ Word ๐) | ||
Theorem | singoutnupword 44822 | 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 44823 | Singleton is an increasing sequence for any compatible range. (Contributed by Ender Ting, 21-Nov-2024.) |
โข ๐ด โ ๐ โ โข โจโ๐ดโโฉ โ UpWord๐ | ||
Theorem | upwordsseti 44824 | Strictly increasing sequences with a set given for range form a set. (Contributed by Ender Ting, 21-Nov-2024.) |
โข ๐ โ V โ โข UpWord๐ โ V | ||
Theorem | tworepnotupword 44825 | Concatenation of identical singletons is never an increasing sequence. (Contributed by Ender Ting, 22-Nov-2024.) |
โข ๐ด โ V โ โข ยฌ (โจโ๐ดโโฉ ++ โจโ๐ดโโฉ) โ UpWord๐ | ||
Theorem | upwrdfi 44826* | 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 44827 | 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 44828 | Recover ax-3 8 from hirstL-ax3 44827. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ((ยฌ ๐ โ ยฌ ๐) โ (๐ โ ๐)) | ||
Theorem | aibandbiaiffaiffb 44829 | 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 44830 | 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 44831 | 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 44832 | Given a is equivalent to โค, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
โข (๐ โ โค) โ โข ๐ | ||
Theorem | aisfina 44833 | Given a is equivalent to โฅ, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
โข (๐ โ โฅ) โ โข ยฌ ๐ | ||
Theorem | bothtbothsame 44834 | 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 44835 | 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 44836 | 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 44837 | 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 44838 | 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 44839 | 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 44840 | 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 44841 | Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.) |
โข (๐ โ ๐) & โข ยฌ ๐ โ โข ยฌ ๐ | ||
Theorem | aibnbaif 44842 | Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.) |
โข (๐ โ ๐) & โข ยฌ ๐ โ โข (๐ โ โฅ) | ||
Theorem | aiffbtbat 44843 | 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 44844 | 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 44845 | 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 44846 | Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.) |
โข (๐ โ ๐) โ โข ยฌ (๐ โป ๐) | ||
Theorem | atbiffatnnb 44847 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.) |
โข ((๐ โ ๐) โ (๐ โ ยฌ ยฌ ๐)) | ||
Theorem | bisaiaisb 44848 | Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
โข ((๐ โ ๐) โ (๐ โ ๐)) | ||
Theorem | atbiffatnnbalt 44849 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
โข ((๐ โ ๐) โ (๐ โ ยฌ ยฌ ๐)) | ||
Theorem | abnotbtaxb 44850 | Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
โข ๐ & โข ยฌ ๐ โ โข (๐ โป ๐) | ||
Theorem | abnotataxb 44851 | Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
โข ยฌ ๐ & โข ๐ โ โข (๐ โป ๐) | ||
Theorem | conimpf 44852 | 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 44853 | 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 44854 | 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 44855 | 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 44856 | 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 44857 | 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 44858 | Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
โข ๐ โ โข ยฌ (๐ โ (๐ โง ยฌ ๐)) | ||
Theorem | ainaiaandna 44859 | Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
โข ๐ โ โข (๐ โ ยฌ (๐ โ (๐ โง ยฌ ๐))) | ||
Theorem | abcdta 44860 | Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
โข (((๐ โง ๐) โง ๐) โง ๐) โ โข ๐ | ||
Theorem | abcdtb 44861 | Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
โข (((๐ โง ๐) โง ๐) โง ๐) โ โข ๐ | ||
Theorem | abcdtc 44862 | Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
โข (((๐ โง ๐) โง ๐) โง ๐) โ โข ๐ | ||
Theorem | abcdtd 44863 | Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
โข (((๐ โง ๐) โง ๐) โง ๐) โ โข ๐ | ||
Theorem | abciffcbatnabciffncba 44864 | 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 44865 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
โข (((๐ โง ๐) โง ๐) โ ((๐ โง ๐) โง ๐)) โ โข (ยฌ ((๐ โง ๐) โง ๐) โ ยฌ ((๐ โง ๐) โง ๐)) | ||
Theorem | nabctnabc 44866 | not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.) |
โข ยฌ (๐ โ (๐ โง ๐)) โ โข (ยฌ ๐ โ (๐ โง ๐)) | ||
Theorem | jabtaib 44867 | For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.) |
โข (๐ โง ๐) โ โข (๐ โ ๐) | ||
Theorem | onenotinotbothi 44868 | 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 44869 | 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 44870 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
โข (๐ โง ยฌ ๐) & โข ๐ โ โข (๐ โ ((๐ โง ยฌ ๐) โจ (๐ โง ๐))) | ||
Theorem | cliftet 44871 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
โข (๐ โง ๐) & โข ๐ โ โข (๐ โ ((๐ โง ๐) โจ (๐ โง ยฌ ๐))) | ||
Theorem | clifteta 44872 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
โข ((๐ โง ยฌ ๐) โจ (๐ โง ๐)) & โข ๐ โ โข (๐ โ ((๐ โง ยฌ ๐) โจ (๐ โง ๐))) | ||
Theorem | cliftetb 44873 | show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.) |
โข ((๐ โง ๐) โจ (๐ โง ยฌ ๐)) & โข ๐ โ โข (๐ โ ((๐ โง ๐) โจ (๐ โง ยฌ ๐))) | ||
Theorem | confun 44874 | Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.) |
โข ๐ & โข (๐ โ ๐) & โข (๐ โ ๐) & โข (๐ โ (๐ โ ๐)) โ โข (๐ โ (๐ โ ๐)) | ||
Theorem | confun2 44875 | Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
โข (๐ โ ๐) & โข (๐ โ ยฌ (๐ โ (๐ โง ยฌ ๐))) & โข ((๐ โ ๐) โ ((๐ โ ๐) โ ๐)) โ โข (๐ โ (ยฌ (๐ โ (๐ โง ยฌ ๐)) โ (๐ โ ๐))) | ||
Theorem | confun3 44876 | Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.) |
โข (๐ โ (๐ โ ๐)) & โข (๐ โ ยฌ (๐ โ (๐ โง ยฌ ๐))) & โข (๐ โ ๐) & โข (๐ โ ยฌ (๐ โ (๐ โง ยฌ ๐))) & โข ((๐ โ ๐) โ ((๐ โ ๐) โ ๐)) โ โข (๐ โ (ยฌ (๐ โ (๐ โง ยฌ ๐)) โ (๐ โ ๐))) | ||
Theorem | confun4 44877 | An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.) |
โข ๐ & โข ((๐ โ ๐) โ ๐) & โข (๐ โ (๐ โ ๐)) & โข ((๐ โ ๐) โ ((๐ โ ๐) โ ๐)) & โข (๐ โ (๐ โ ๐)) & โข (๐ โ ยฌ (๐ โ (๐ โง ยฌ ๐))) & โข ๐ & โข (๐ โ ๐) โ โข (๐ โ (๐ โ ๐)) | ||
Theorem | confun5 44878 | 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 44879 | Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
โข (๐ โ ((((๐ โง ๐) โ ๐) โ (๐ โง ยฌ (๐ โง ยฌ ๐))) โง (๐ โง ยฌ (๐ โง ยฌ ๐)))) & โข ๐ & โข ๐ โ โข ๐ | ||
Theorem | pldofph 44880 | Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
โข (๐ โ ((๐ โ ๐) โง (๐ โ ๐) โง ((๐ โ ๐) โ (๐ โ ๐)))) & โข ๐ & โข ๐ & โข ๐ & โข ๐ โ โข ๐ | ||
Theorem | plvcofph 44881 | Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
โข (๐ โ ((((๐ โง ๐) โ ๐) โ (๐ โง ยฌ (๐ โง ยฌ ๐))) โง (๐ โง ยฌ (๐ โง ยฌ ๐)))) & โข (๐ โ ((๐ โ ๐) โง (๐ โ ๐) โง ((๐ โ ๐) โ (๐ โ ๐)))) & โข (๐ โ (๐ โง ๐)) & โข ๐ & โข ๐ & โข ๐ โ โข ๐ | ||
Theorem | plvcofphax 44882 | Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.) |
โข (๐ โ ((((๐ โง ๐) โ ๐) โ (๐ โง ยฌ (๐ โง ยฌ ๐))) โง (๐ โง ยฌ (๐ โง ยฌ ๐)))) & โข (๐ โ ((๐ โ ๐) โง (๐ โ ๐) โง ((๐ โ ๐) โ (๐ โ ๐)))) & โข (๐ โ (๐ โง ๐)) & โข ๐ & โข ๐ & โข ๐ & โข (๐ โ ยฌ (๐ โง ยฌ ๐)) โ โข ๐ | ||
Theorem | plvofpos 44883 | rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
โข (๐ โ (ยฌ ๐ โง ยฌ ๐)) & โข (๐ โ (ยฌ ๐ โง ๐)) & โข (๐ โ (๐ โง ยฌ ๐)) & โข (๐ โ (๐ โง ๐)) & โข (๐ โ (((((ยฌ ((๐ โ ๐) โง (๐ โ ๐)) โง ยฌ ((๐ โ ๐) โง (๐ โ ๐))) โง ยฌ ((๐ โ ๐) โง (๐ โ ๐))) โง ยฌ ((๐ โ ๐) โง (๐ โ ๐))) โง ยฌ ((๐ โ ๐) โง (๐ โ ๐))) โง ยฌ ((๐ โ ๐) โง (๐ โ ๐)))) & โข (๐ โ (((๐ โ ๐) โจ (๐ โ ๐)) โจ ((๐ โ ๐) โจ (๐ โ ๐)))) & โข (๐ โ (๐ โง ๐)) & โข ๐ & โข ๐ โ โข ๐ | ||
Theorem | mdandyv0 44884 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โฅ) & โข (๐ โ โฅ) & โข (๐ โ โฅ) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv1 44885 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โฅ) & โข (๐ โ โฅ) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv2 44886 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โฅ) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv3 44887 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โฅ) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv4 44888 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โฅ) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv5 44889 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โฅ) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv6 44890 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โฅ) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv7 44891 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โฅ) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv8 44892 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โฅ) & โข (๐ โ โฅ) & โข (๐ โ โค) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv9 44893 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โฅ) & โข (๐ โ โค) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv10 44894 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โค) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv11 44895 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โค) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv12 44896 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โค) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv13 44897 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โค) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv14 44898 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โค) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyv15 44899 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
โข (๐ โ โฅ) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โค) & โข (๐ โ โค) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) | ||
Theorem | mdandyvr0 44900 | Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
โข (๐ โ ๐) & โข (๐ โ ๐) & โข (๐ โ ๐) & โข (๐ โ ๐) & โข (๐ โ ๐) & โข (๐ โ ๐) โ โข ((((๐ โ ๐) โง (๐ โ ๐)) โง (๐ โ ๐)) โง (๐ โ ๐)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |