![]() |
Intuitionistic Logic Explorer Theorem List (p. 145 of 149) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description | ||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||
Theorem | lgsdir2lem3 14401 | Lemma for lgsdir2 14404. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ โค โง ยฌ 2 โฅ ๐ด) โ (๐ด mod 8) โ ({1, 7} โช {3, 5})) | ||||||||||||||||||||||||||||||||
Theorem | lgsdir2lem4 14402 | Lemma for lgsdir2 14404. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) โ {1, 7}) โ (((๐ด ยท ๐ต) mod 8) โ {1, 7} โ (๐ต mod 8) โ {1, 7})) | ||||||||||||||||||||||||||||||||
Theorem | lgsdir2lem5 14403 | Lemma for lgsdir2 14404. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
โข (((๐ด โ โค โง ๐ต โ โค) โง ((๐ด mod 8) โ {3, 5} โง (๐ต mod 8) โ {3, 5})) โ ((๐ด ยท ๐ต) mod 8) โ {1, 7}) | ||||||||||||||||||||||||||||||||
Theorem | lgsdir2 14404 | The Legendre symbol is completely multiplicative at 2. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ โค โง ๐ต โ โค) โ ((๐ด ยท ๐ต) /L 2) = ((๐ด /L 2) ยท (๐ต /L 2))) | ||||||||||||||||||||||||||||||||
Theorem | lgsdirprm 14405 | The Legendre symbol is completely multiplicative at the primes. See theorem 9.3 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 18-Mar-2022.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) | ||||||||||||||||||||||||||||||||
Theorem | lgsdir 14406 | The Legendre symbol is completely multiplicative in its left argument. Generalization of theorem 9.9(a) in [ApostolNT] p. 188 (which assumes that ๐ด and ๐ต are odd positive integers). (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) | ||||||||||||||||||||||||||||||||
Theorem | lgsdilem2 14407* | Lemma for lgsdi 14408. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ 0) & โข (๐ โ ๐ โ 0) & โข ๐น = (๐ โ โ โฆ if(๐ โ โ, ((๐ด /L ๐)โ(๐ pCnt ๐)), 1)) โ โข (๐ โ (seq1( ยท , ๐น)โ(absโ๐)) = (seq1( ยท , ๐น)โ(absโ(๐ ยท ๐)))) | ||||||||||||||||||||||||||||||||
Theorem | lgsdi 14408 | The Legendre symbol is completely multiplicative in its right argument. Generalization of theorem 9.9(b) in [ApostolNT] p. 188 (which assumes that ๐ and ๐ are odd positive integers). (Contributed by Mario Carneiro, 5-Feb-2015.) | ||||||||||||||||||||||||||||||
โข (((๐ด โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ โ 0 โง ๐ โ 0)) โ (๐ด /L (๐ ยท ๐)) = ((๐ด /L ๐) ยท (๐ด /L ๐))) | ||||||||||||||||||||||||||||||||
Theorem | lgsne0 14409 | The Legendre symbol is nonzero (and hence equal to 1 or -1) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ โค โง ๐ โ โค) โ ((๐ด /L ๐) โ 0 โ (๐ด gcd ๐) = 1)) | ||||||||||||||||||||||||||||||||
Theorem | lgsabs1 14410 | The Legendre symbol is nonzero (and hence equal to 1 or -1) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ โค โง ๐ โ โค) โ ((absโ(๐ด /L ๐)) = 1 โ (๐ด gcd ๐) = 1)) | ||||||||||||||||||||||||||||||||
Theorem | lgssq 14411 | The Legendre symbol at a square is equal to 1. Together with lgsmod 14397 this implies that the Legendre symbol takes value 1 at every quadratic residue. (Contributed by Mario Carneiro, 5-Feb-2015.) (Revised by AV, 20-Jul-2021.) | ||||||||||||||||||||||||||||||
โข (((๐ด โ โค โง ๐ด โ 0) โง ๐ โ โค โง (๐ด gcd ๐) = 1) โ ((๐ดโ2) /L ๐) = 1) | ||||||||||||||||||||||||||||||||
Theorem | lgssq2 14412 | The Legendre symbol at a square is equal to 1. (Contributed by Mario Carneiro, 5-Feb-2015.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ โค โง ๐ โ โ โง (๐ด gcd ๐) = 1) โ (๐ด /L (๐โ2)) = 1) | ||||||||||||||||||||||||||||||||
Theorem | lgsprme0 14413 | The Legendre symbol at any prime (even at 2) is 0 iff the prime does not divide the first argument. See definition in [ApostolNT] p. 179. (Contributed by AV, 20-Jul-2021.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ โค โง ๐ โ โ) โ ((๐ด /L ๐) = 0 โ (๐ด mod ๐) = 0)) | ||||||||||||||||||||||||||||||||
Theorem | 1lgs 14414 | The Legendre symbol at 1. See example 1 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 28-Apr-2016.) | ||||||||||||||||||||||||||||||
โข (๐ โ โค โ (1 /L ๐) = 1) | ||||||||||||||||||||||||||||||||
Theorem | lgs1 14415 | The Legendre symbol at 1. See definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 28-Apr-2016.) | ||||||||||||||||||||||||||||||
โข (๐ด โ โค โ (๐ด /L 1) = 1) | ||||||||||||||||||||||||||||||||
Theorem | lgsmodeq 14416 | The Legendre (Jacobi) symbol is preserved under reduction mod ๐ when ๐ is odd. Theorem 9.9(c) in [ApostolNT] p. 188. (Contributed by AV, 20-Jul-2021.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ โค โง ๐ต โ โค โง (๐ โ โ โง ยฌ 2 โฅ ๐)) โ ((๐ด mod ๐) = (๐ต mod ๐) โ (๐ด /L ๐) = (๐ต /L ๐))) | ||||||||||||||||||||||||||||||||
Theorem | lgsmulsqcoprm 14417 | The Legendre (Jacobi) symbol is preserved under multiplication with a square of an integer coprime to the second argument. Theorem 9.9(d) in [ApostolNT] p. 188. (Contributed by AV, 20-Jul-2021.) | ||||||||||||||||||||||||||||||
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0) โง (๐ โ โค โง (๐ด gcd ๐) = 1)) โ (((๐ดโ2) ยท ๐ต) /L ๐) = (๐ต /L ๐)) | ||||||||||||||||||||||||||||||||
Theorem | lgsdirnn0 14418 | Variation on lgsdir 14406 valid for all ๐ด, ๐ต but only for positive ๐. (The exact location of the failure of this law is for ๐ด = 0, ๐ต < 0, ๐ = -1 in which case (0 /L -1) = 1 but (๐ต /L -1) = -1.) (Contributed by Mario Carneiro, 28-Apr-2016.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ0) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) | ||||||||||||||||||||||||||||||||
Theorem | lgsdinn0 14419 | Variation on lgsdi 14408 valid for all ๐, ๐ but only for positive ๐ด. (The exact location of the failure of this law is for ๐ด = -1, ๐ = 0, and some ๐ in which case (-1 /L 0) = 1 but (-1 /L ๐) = -1 when -1 is not a quadratic residue mod ๐.) (Contributed by Mario Carneiro, 28-Apr-2016.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ โ0 โง ๐ โ โค โง ๐ โ โค) โ (๐ด /L (๐ ยท ๐)) = ((๐ด /L ๐) ยท (๐ด /L ๐))) | ||||||||||||||||||||||||||||||||
Theorem | lgseisenlem1 14420* | Lemma for Eisenstein's lemma. If ๐ (๐ข) = (๐ ยท ๐ข) mod ๐ and ๐(๐ข) = (-1โ๐ (๐ข)) ยท ๐ (๐ข), then for any even 1 โค ๐ข โค ๐ โ 1, ๐(๐ข) is also an even integer 1 โค ๐(๐ข) โค ๐ โ 1. To simplify these statements, we divide all the even numbers by 2, so that it becomes the statement that ๐(๐ฅ / 2) = (-1โ๐ (๐ฅ / 2)) ยท ๐ (๐ฅ / 2) / 2 is an integer between 1 and (๐ โ 1) / 2. (Contributed by Mario Carneiro, 17-Jun-2015.) | ||||||||||||||||||||||||||||||
โข (๐ โ ๐ โ (โ โ {2})) & โข (๐ โ ๐ โ (โ โ {2})) & โข (๐ โ ๐ โ ๐) & โข ๐ = ((๐ ยท (2 ยท ๐ฅ)) mod ๐) & โข ๐ = (๐ฅ โ (1...((๐ โ 1) / 2)) โฆ ((((-1โ๐ ) ยท ๐ ) mod ๐) / 2)) โ โข (๐ โ ๐:(1...((๐ โ 1) / 2))โถ(1...((๐ โ 1) / 2))) | ||||||||||||||||||||||||||||||||
Theorem | lgseisenlem2 14421* | Lemma for Eisenstein's lemma. The function ๐ is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 17-Jun-2015.) | ||||||||||||||||||||||||||||||
โข (๐ โ ๐ โ (โ โ {2})) & โข (๐ โ ๐ โ (โ โ {2})) & โข (๐ โ ๐ โ ๐) & โข ๐ = ((๐ ยท (2 ยท ๐ฅ)) mod ๐) & โข ๐ = (๐ฅ โ (1...((๐ โ 1) / 2)) โฆ ((((-1โ๐ ) ยท ๐ ) mod ๐) / 2)) & โข ๐ = ((๐ ยท (2 ยท ๐ฆ)) mod ๐) โ โข (๐ โ ๐:(1...((๐ โ 1) / 2))โ1-1-ontoโ(1...((๐ โ 1) / 2))) | ||||||||||||||||||||||||||||||||
Theorem | m1lgs 14422 | The first supplement to the law of quadratic reciprocity. Negative one is a square mod an odd prime ๐ iff ๐โก1 (mod 4). See first case of theorem 9.4 in [ApostolNT] p. 181. (Contributed by Mario Carneiro, 19-Jun-2015.) | ||||||||||||||||||||||||||||||
โข (๐ โ (โ โ {2}) โ ((-1 /L ๐) = 1 โ (๐ mod 4) = 1)) | ||||||||||||||||||||||||||||||||
Theorem | 2lgsoddprmlem1 14423 | Lemma 1 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ = ((8 ยท ๐ด) + ๐ต)) โ (((๐โ2) โ 1) / 8) = (((8 ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + (((๐ตโ2) โ 1) / 8))) | ||||||||||||||||||||||||||||||||
Theorem | 2lgsoddprmlem2 14424 | Lemma 2 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021.) | ||||||||||||||||||||||||||||||
โข ((๐ โ โค โง ยฌ 2 โฅ ๐ โง ๐ = (๐ mod 8)) โ (2 โฅ (((๐โ2) โ 1) / 8) โ 2 โฅ (((๐ โ2) โ 1) / 8))) | ||||||||||||||||||||||||||||||||
Theorem | 2lgsoddprmlem3a 14425 | Lemma 1 for 2lgsoddprmlem3 14429. (Contributed by AV, 20-Jul-2021.) | ||||||||||||||||||||||||||||||
โข (((1โ2) โ 1) / 8) = 0 | ||||||||||||||||||||||||||||||||
Theorem | 2lgsoddprmlem3b 14426 | Lemma 2 for 2lgsoddprmlem3 14429. (Contributed by AV, 20-Jul-2021.) | ||||||||||||||||||||||||||||||
โข (((3โ2) โ 1) / 8) = 1 | ||||||||||||||||||||||||||||||||
Theorem | 2lgsoddprmlem3c 14427 | Lemma 3 for 2lgsoddprmlem3 14429. (Contributed by AV, 20-Jul-2021.) | ||||||||||||||||||||||||||||||
โข (((5โ2) โ 1) / 8) = 3 | ||||||||||||||||||||||||||||||||
Theorem | 2lgsoddprmlem3d 14428 | Lemma 4 for 2lgsoddprmlem3 14429. (Contributed by AV, 20-Jul-2021.) | ||||||||||||||||||||||||||||||
โข (((7โ2) โ 1) / 8) = (2 ยท 3) | ||||||||||||||||||||||||||||||||
Theorem | 2lgsoddprmlem3 14429 | Lemma 3 for 2lgsoddprm . (Contributed by AV, 20-Jul-2021.) | ||||||||||||||||||||||||||||||
โข ((๐ โ โค โง ยฌ 2 โฅ ๐ โง ๐ = (๐ mod 8)) โ (2 โฅ (((๐ โ2) โ 1) / 8) โ ๐ โ {1, 7})) | ||||||||||||||||||||||||||||||||
Theorem | 2lgsoddprmlem4 14430 | Lemma 4 for 2lgsoddprm . (Contributed by AV, 20-Jul-2021.) | ||||||||||||||||||||||||||||||
โข ((๐ โ โค โง ยฌ 2 โฅ ๐) โ (2 โฅ (((๐โ2) โ 1) / 8) โ (๐ mod 8) โ {1, 7})) | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem1 14431* | Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) | ||||||||||||||||||||||||||||||
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) โ โข (๐ด โ ๐ โ โ๐ฅ โ โค[i] ๐ด = ((absโ๐ฅ)โ2)) | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem2 14432* | Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) | ||||||||||||||||||||||||||||||
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) โ โข (๐ด โ ๐ โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ด = ((๐ฅโ2) + (๐ฆโ2))) | ||||||||||||||||||||||||||||||||
Theorem | mul2sq 14433 | Fibonacci's identity (actually due to Diophantus). The product of two sums of two squares is also a sum of two squares. We can take advantage of Gaussian integers here to trivialize the proof. (Contributed by Mario Carneiro, 19-Jun-2015.) | ||||||||||||||||||||||||||||||
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) โ โข ((๐ด โ ๐ โง ๐ต โ ๐) โ (๐ด ยท ๐ต) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem3 14434 | Lemma for 2sqlem5 14436. (Contributed by Mario Carneiro, 20-Jun-2015.) | ||||||||||||||||||||||||||||||
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โค) & โข (๐ โ ๐ถ โ โค) & โข (๐ โ ๐ท โ โค) & โข (๐ โ (๐ ยท ๐) = ((๐ดโ2) + (๐ตโ2))) & โข (๐ โ ๐ = ((๐ถโ2) + (๐ทโ2))) & โข (๐ โ ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) โ โข (๐ โ ๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem4 14435 | Lemma for 2sqlem5 14436. (Contributed by Mario Carneiro, 20-Jun-2015.) | ||||||||||||||||||||||||||||||
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โค) & โข (๐ โ ๐ถ โ โค) & โข (๐ โ ๐ท โ โค) & โข (๐ โ (๐ ยท ๐) = ((๐ดโ2) + (๐ตโ2))) & โข (๐ โ ๐ = ((๐ถโ2) + (๐ทโ2))) โ โข (๐ โ ๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem5 14436 | Lemma for 2sq . If a number that is a sum of two squares is divisible by a prime that is a sum of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.) | ||||||||||||||||||||||||||||||
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐ ยท ๐) โ ๐) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ ๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem6 14437* | Lemma for 2sq . If a number that is a sum of two squares is divisible by a number whose prime divisors are all sums of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.) | ||||||||||||||||||||||||||||||
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ โ๐ โ โ (๐ โฅ ๐ต โ ๐ โ ๐)) & โข (๐ โ (๐ด ยท ๐ต) โ ๐) โ โข (๐ โ ๐ด โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem7 14438* | Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) | ||||||||||||||||||||||||||||||
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข ๐ = {๐ง โฃ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ๐ง = ((๐ฅโ2) + (๐ฆโ2)))} โ โข ๐ โ (๐ โฉ โ) | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem8a 14439* | Lemma for 2sqlem8 14440. (Contributed by Mario Carneiro, 4-Jun-2016.) | ||||||||||||||||||||||||||||||
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข ๐ = {๐ง โฃ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ๐ง = ((๐ฅโ2) + (๐ฆโ2)))} & โข (๐ โ โ๐ โ (1...(๐ โ 1))โ๐ โ ๐ (๐ โฅ ๐ โ ๐ โ ๐)) & โข (๐ โ ๐ โฅ ๐) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (โคโฅโ2)) & โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โค) & โข (๐ โ (๐ด gcd ๐ต) = 1) & โข (๐ โ ๐ = ((๐ดโ2) + (๐ตโ2))) & โข ๐ถ = (((๐ด + (๐ / 2)) mod ๐) โ (๐ / 2)) & โข ๐ท = (((๐ต + (๐ / 2)) mod ๐) โ (๐ / 2)) โ โข (๐ โ (๐ถ gcd ๐ท) โ โ) | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem8 14440* | Lemma for 2sq . (Contributed by Mario Carneiro, 20-Jun-2015.) | ||||||||||||||||||||||||||||||
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข ๐ = {๐ง โฃ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ๐ง = ((๐ฅโ2) + (๐ฆโ2)))} & โข (๐ โ โ๐ โ (1...(๐ โ 1))โ๐ โ ๐ (๐ โฅ ๐ โ ๐ โ ๐)) & โข (๐ โ ๐ โฅ ๐) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (โคโฅโ2)) & โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โค) & โข (๐ โ (๐ด gcd ๐ต) = 1) & โข (๐ โ ๐ = ((๐ดโ2) + (๐ตโ2))) & โข ๐ถ = (((๐ด + (๐ / 2)) mod ๐) โ (๐ / 2)) & โข ๐ท = (((๐ต + (๐ / 2)) mod ๐) โ (๐ / 2)) & โข ๐ธ = (๐ถ / (๐ถ gcd ๐ท)) & โข ๐น = (๐ท / (๐ถ gcd ๐ท)) โ โข (๐ โ ๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem9 14441* | Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) | ||||||||||||||||||||||||||||||
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข ๐ = {๐ง โฃ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ๐ง = ((๐ฅโ2) + (๐ฆโ2)))} & โข (๐ โ โ๐ โ (1...(๐ โ 1))โ๐ โ ๐ (๐ โฅ ๐ โ ๐ โ ๐)) & โข (๐ โ ๐ โฅ ๐) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ ๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem10 14442* | Lemma for 2sq . Every factor of a "proper" sum of two squares (where the summands are coprime) is a sum of two squares. (Contributed by Mario Carneiro, 19-Jun-2015.) | ||||||||||||||||||||||||||||||
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) & โข ๐ = {๐ง โฃ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ๐ง = ((๐ฅโ2) + (๐ฆโ2)))} โ โข ((๐ด โ ๐ โง ๐ต โ โ โง ๐ต โฅ ๐ด) โ ๐ต โ ๐) | ||||||||||||||||||||||||||||||||
This section describes the conventions we use. These conventions often refer to existing mathematical practices, which are discussed in more detail in other references. The following sources lay out how mathematics is developed without the law of the excluded middle. Of course, there are a greater number of sources which assume excluded middle and most of what is in them applies here too (especially in a treatment such as ours which is built on first-order logic and set theory, rather than, say, type theory). Studying how a topic is treated in the Metamath Proof Explorer and the references therein is often a good place to start (and is easy to compare with the Intuitionistic Logic Explorer). The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following:
| ||||||||||||||||||||||||||||||||
Theorem | conventions 14443 |
Unless there is a reason to diverge, we follow the conventions of the
Metamath Proof Explorer (MPE, set.mm). This list of conventions is
intended to be read in conjunction with the corresponding conventions in
the Metamath Proof Explorer, and only the differences are described
below.
Label naming conventions Here are a few of the label naming conventions:
The following table shows some commonly-used abbreviations in labels which are not found in the Metamath Proof Explorer, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME. For the "g" abbreviation, this is related to the set.mm usage, in which "is a set" conditions are converted from hypotheses to antecedents, but is also used where "is a set" conditions are added relative to similar set.mm theorems.
(Contributed by Jim Kingdon, 24-Feb-2020.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ๐ โ โข ๐ | ||||||||||||||||||||||||||||||||
Theorem | ex-or 14444 | Example for ax-io 709. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||||||||
โข (2 = 3 โจ 4 = 4) | ||||||||||||||||||||||||||||||||
Theorem | ex-an 14445 | Example for ax-ia1 106. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||||||||
โข (2 = 2 โง 3 = 3) | ||||||||||||||||||||||||||||||||
Theorem | 1kp2ke3k 14446 |
Example for df-dec 9384, 1000 + 2000 = 3000.
This proof disproves (by counterexample) the assertion of Hao Wang, who stated, "There is a theorem in the primitive notation of set theory that corresponds to the arithmetic theorem 1000 + 2000 = 3000. The formula would be forbiddingly long... even if (one) knows the definitions and is asked to simplify the long formula according to them, chances are he will make errors and arrive at some incorrect result." (Hao Wang, "Theory and practice in mathematics" , In Thomas Tymoczko, editor, New Directions in the Philosophy of Mathematics, pp 129-152, Birkauser Boston, Inc., Boston, 1986. (QA8.6.N48). The quote itself is on page 140.) This is noted in Metamath: A Computer Language for Pure Mathematics by Norman Megill (2007) section 1.1.3. Megill then states, "A number of writers have conveyed the impression that the kind of absolute rigor provided by Metamath is an impossible dream, suggesting that a complete, formal verification of a typical theorem would take millions of steps in untold volumes of books... These writers assume, however, that in order to achieve the kind of complete formal verification they desire one must break down a proof into individual primitive steps that make direct reference to the axioms. This is not necessary. There is no reason not to make use of previously proved theorems rather than proving them over and over... A hierarchy of theorems and definitions permits an exponential growth in the formula sizes and primitive proof steps to be described with only a linear growth in the number of symbols used. Of course, this is how ordinary informal mathematics is normally done anyway, but with Metamath it can be done with absolute rigor and precision." The proof here starts with (2 + 1) = 3, commutes it, and repeatedly multiplies both sides by ten. This is certainly longer than traditional mathematical proofs, e.g., there are a number of steps explicitly shown here to show that we're allowed to do operations such as multiplication. However, while longer, the proof is clearly a manageable size - even though every step is rigorously derived all the way back to the primitive notions of set theory and logic. And while there's a risk of making errors, the many independent verifiers make it much less likely that an incorrect result will be accepted. This proof heavily relies on the decimal constructor df-dec 9384 developed by Mario Carneiro in 2015. The underlying Metamath language has an intentionally very small set of primitives; it doesn't even have a built-in construct for numbers. Instead, the digits are defined using these primitives, and the decimal constructor is used to make it easy to express larger numbers as combinations of digits. (Contributed by David A. Wheeler, 29-Jun-2016.) (Shortened by Mario Carneiro using the arithmetic algorithm in mmj2, 30-Jun-2016.) | ||||||||||||||||||||||||||||||
โข (;;;1000 + ;;;2000) = ;;;3000 | ||||||||||||||||||||||||||||||||
Theorem | ex-fl 14447 | Example for df-fl 10269. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||
โข ((โโ(3 / 2)) = 1 โง (โโ-(3 / 2)) = -2) | ||||||||||||||||||||||||||||||||
Theorem | ex-ceil 14448 | Example for df-ceil 10270. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||
โข ((โโ(3 / 2)) = 2 โง (โโ-(3 / 2)) = -1) | ||||||||||||||||||||||||||||||||
Theorem | ex-exp 14449 | Example for df-exp 10519. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||
โข ((5โ2) = ;25 โง (-3โ-2) = (1 / 9)) | ||||||||||||||||||||||||||||||||
Theorem | ex-fac 14450 | Example for df-fac 10705. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||
โข (!โ5) = ;;120 | ||||||||||||||||||||||||||||||||
Theorem | ex-bc 14451 | Example for df-bc 10727. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||
โข (5C3) = ;10 | ||||||||||||||||||||||||||||||||
Theorem | ex-dvds 14452 | Example for df-dvds 11794: 3 divides into 6. (Contributed by David A. Wheeler, 19-May-2015.) | ||||||||||||||||||||||||||||||
โข 3 โฅ 6 | ||||||||||||||||||||||||||||||||
Theorem | ex-gcd 14453 | Example for df-gcd 11943. (Contributed by AV, 5-Sep-2021.) | ||||||||||||||||||||||||||||||
โข (-6 gcd 9) = 3 | ||||||||||||||||||||||||||||||||
Theorem | mathbox 14454 |
(This theorem is a dummy placeholder for these guidelines. The label
of this theorem, "mathbox", is hard-coded into the Metamath
program to
identify the start of the mathbox section for web page generation.)
A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of iset.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of iset.mm. Guidelines: Mathboxes in iset.mm follow the same practices as in set.mm, so refer to the mathbox guidelines there for more details. (Contributed by NM, 20-Feb-2007.) (Revised by the Metamath team, 9-Sep-2023.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ๐ โ โข ๐ | ||||||||||||||||||||||||||||||||
Theorem | bj-nnsn 14455 | As far as implying a negated formula is concerned, a formula is equivalent to its double negation. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข ((๐ โ ยฌ ๐) โ (ยฌ ยฌ ๐ โ ยฌ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-nnor 14456 | Double negation of a disjunction in terms of implication. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||||||||
โข (ยฌ ยฌ (๐ โจ ๐) โ (ยฌ ๐ โ ยฌ ยฌ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-nnim 14457 | The double negation of an implication implies the implication with the consequent doubly negated. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข (ยฌ ยฌ (๐ โ ๐) โ (๐ โ ยฌ ยฌ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-nnan 14458 | The double negation of a conjunction implies the conjunction of the double negations. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข (ยฌ ยฌ (๐ โง ๐) โ (ยฌ ยฌ ๐ โง ยฌ ยฌ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-nnclavius 14459 | Clavius law with doubly negated consequent. (Contributed by BJ, 4-Dec-2023.) | ||||||||||||||||||||||||||||||
โข ((ยฌ ๐ โ ๐) โ ยฌ ยฌ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-imnimnn 14460 | If a formula is implied by both a formula and its negation, then it is not refutable. There is another proof using the inference associated with bj-nnclavius 14459 as its last step. (Contributed by BJ, 27-Oct-2024.) | ||||||||||||||||||||||||||||||
โข (๐ โ ๐) & โข (ยฌ ๐ โ ๐) โ โข ยฌ ยฌ ๐ | ||||||||||||||||||||||||||||||||
Some of the following theorems, like bj-sttru 14462 or bj-stfal 14464 could be deduced from their analogues for decidability, but stability is not provable from decidability in minimal calculus, so direct proofs have their interest. | ||||||||||||||||||||||||||||||||
Theorem | bj-trst 14461 | A provable formula is stable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข (๐ โ STAB ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-sttru 14462 | The true truth value is stable. (Contributed by BJ, 5-Aug-2024.) | ||||||||||||||||||||||||||||||
โข STAB โค | ||||||||||||||||||||||||||||||||
Theorem | bj-fast 14463 | A refutable formula is stable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข (ยฌ ๐ โ STAB ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-stfal 14464 | The false truth value is stable. (Contributed by BJ, 5-Aug-2024.) | ||||||||||||||||||||||||||||||
โข STAB โฅ | ||||||||||||||||||||||||||||||||
Theorem | bj-nnst 14465 | Double negation of stability of a formula. Intuitionistic logic refutes unstability (but does not prove stability) of any formula. This theorem can also be proved in classical refutability calculus (see https://us.metamath.org/mpeuni/bj-peircestab.html) but not in minimal calculus (see https://us.metamath.org/mpeuni/bj-stabpeirce.html). See nnnotnotr 14712 for the version not using the definition of stability. (Contributed by BJ, 9-Oct-2019.) Prove it in ( โ , ยฌ ) -intuitionistic calculus with definitions (uses of ax-ia1 106, ax-ia2 107, ax-ia3 108 are via sylibr 134, necessary for definition unpackaging), and in ( โ , โ , ยฌ )-intuitionistic calculus, following a discussion with Jim Kingdon. (Revised by BJ, 27-Oct-2024.) | ||||||||||||||||||||||||||||||
โข ยฌ ยฌ STAB ๐ | ||||||||||||||||||||||||||||||||
Theorem | bj-nnbist 14466 | If a formula is not refutable, then it is stable if and only if it is provable. By double-negation translation, if ๐ is a classical tautology, then ยฌ ยฌ ๐ is an intuitionistic tautology. Therefore, if ๐ is a classical tautology, then ๐ is intuitionistically equivalent to its stability (and to its decidability, see bj-nnbidc 14479). (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข (ยฌ ยฌ ๐ โ (STAB ๐ โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-stst 14467 | Stability of a proposition is stable if and only if that proposition is stable. STAB is idempotent. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||||||||
โข (STAB STAB ๐ โ STAB ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-stim 14468 | A conjunction with a stable consequent is stable. See stabnot 833 for negation , bj-stan 14469 for conjunction , and bj-stal 14471 for universal quantification. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข (STAB ๐ โ STAB (๐ โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-stan 14469 | The conjunction of two stable formulas is stable. See bj-stim 14468 for implication, stabnot 833 for negation, and bj-stal 14471 for universal quantification. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข ((STAB ๐ โง STAB ๐) โ STAB (๐ โง ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-stand 14470 | The conjunction of two stable formulas is stable. Deduction form of bj-stan 14469. Its proof is shorter (when counting all steps, including syntactic steps), so one could prove it first and then bj-stan 14469 from it, the usual way. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ โ STAB ๐) & โข (๐ โ STAB ๐) โ โข (๐ โ STAB (๐ โง ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-stal 14471 | The universal quantification of a stable formula is stable. See bj-stim 14468 for implication, stabnot 833 for negation, and bj-stan 14469 for conjunction. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข (โ๐ฅSTAB ๐ โ STAB โ๐ฅ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-pm2.18st 14472 | Clavius law for stable formulas. See pm2.18dc 855. (Contributed by BJ, 4-Dec-2023.) | ||||||||||||||||||||||||||||||
โข (STAB ๐ โ ((ยฌ ๐ โ ๐) โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-con1st 14473 | Contraposition when the antecedent is a negated stable proposition. See con1dc 856. (Contributed by BJ, 11-Nov-2024.) | ||||||||||||||||||||||||||||||
โข (STAB ๐ โ ((ยฌ ๐ โ ๐) โ (ยฌ ๐ โ ๐))) | ||||||||||||||||||||||||||||||||
Theorem | bj-trdc 14474 | A provable formula is decidable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข (๐ โ DECID ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-dctru 14475 | The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.) | ||||||||||||||||||||||||||||||
โข DECID โค | ||||||||||||||||||||||||||||||||
Theorem | bj-fadc 14476 | A refutable formula is decidable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข (ยฌ ๐ โ DECID ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-dcfal 14477 | The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.) | ||||||||||||||||||||||||||||||
โข DECID โฅ | ||||||||||||||||||||||||||||||||
Theorem | bj-dcstab 14478 | A decidable formula is stable. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
โข (DECID ๐ โ STAB ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-nnbidc 14479 | If a formula is not refutable, then it is decidable if and only if it is provable. See also comment of bj-nnbist 14466. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข (ยฌ ยฌ ๐ โ (DECID ๐ โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-nndcALT 14480 | Alternate proof of nndc 851. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||||||||
โข ยฌ ยฌ DECID ๐ | ||||||||||||||||||||||||||||||||
Theorem | bj-dcdc 14481 | Decidability of a proposition is decidable if and only if that proposition is decidable. DECID is idempotent. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||||||||
โข (DECID DECID ๐ โ DECID ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-stdc 14482 | Decidability of a proposition is stable if and only if that proposition is decidable. In particular, the assumption that every formula is stable implies that every formula is decidable, hence classical logic. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||||||||
โข (STAB DECID ๐ โ DECID ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-dcst 14483 | Stability of a proposition is decidable if and only if that proposition is stable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
โข (DECID STAB ๐ โ STAB ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-ex 14484* | Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1598 and 19.9ht 1641 or 19.23ht 1497). (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
โข (โ๐ฅ๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-hbalt 14485 | Closed form of hbal 1477 (copied from set.mm). (Contributed by BJ, 2-May-2019.) | ||||||||||||||||||||||||||||||
โข (โ๐ฆ(๐ โ โ๐ฅ๐) โ (โ๐ฆ๐ โ โ๐ฅโ๐ฆ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-nfalt 14486 | Closed form of nfal 1576 (copied from set.mm). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
โข (โ๐ฅโฒ๐ฆ๐ โ โฒ๐ฆโ๐ฅ๐) | ||||||||||||||||||||||||||||||||
Theorem | spimd 14487 | Deduction form of spim 1738. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||||||||
โข (๐ โ โฒ๐ฅ๐) & โข (๐ โ โ๐ฅ(๐ฅ = ๐ฆ โ (๐ โ ๐))) โ โข (๐ โ (โ๐ฅ๐ โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | 2spim 14488* | Double substitution, as in spim 1738. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||||||||
โข โฒ๐ฅ๐ & โข โฒ๐ง๐ & โข ((๐ฅ = ๐ฆ โง ๐ง = ๐ก) โ (๐ โ ๐)) โ โข (โ๐งโ๐ฅ๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | ch2var 14489* | Implicit substitution of ๐ฆ for ๐ฅ and ๐ก for ๐ง into a theorem. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||||||||
โข โฒ๐ฅ๐ & โข โฒ๐ง๐ & โข ((๐ฅ = ๐ฆ โง ๐ง = ๐ก) โ (๐ โ ๐)) & โข ๐ โ โข ๐ | ||||||||||||||||||||||||||||||||
Theorem | ch2varv 14490* | Version of ch2var 14489 with nonfreeness hypotheses replaced with disjoint variable conditions. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||||||||
โข ((๐ฅ = ๐ฆ โง ๐ง = ๐ก) โ (๐ โ ๐)) & โข ๐ โ โข ๐ | ||||||||||||||||||||||||||||||||
Theorem | bj-exlimmp 14491 | Lemma for bj-vtoclgf 14498. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
โข โฒ๐ฅ๐ & โข (๐ โ ๐) โ โข (โ๐ฅ(๐ โ (๐ โ ๐)) โ (โ๐ฅ๐ โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-exlimmpi 14492 | Lemma for bj-vtoclgf 14498. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
โข โฒ๐ฅ๐ & โข (๐ โ ๐) & โข (๐ โ (๐ โ ๐)) โ โข (โ๐ฅ๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-sbimedh 14493 | A strengthening of sbiedh 1787 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||||||||||||||||||||
โข (๐ โ โ๐ฅ๐) & โข (๐ โ (๐ โ โ๐ฅ๐)) & โข (๐ โ (๐ฅ = ๐ฆ โ (๐ โ ๐))) โ โข (๐ โ ([๐ฆ / ๐ฅ]๐ โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-sbimeh 14494 | A strengthening of sbieh 1790 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||||||||||||||||||||
โข (๐ โ โ๐ฅ๐) & โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) โ โข ([๐ฆ / ๐ฅ]๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-sbime 14495 | A strengthening of sbie 1791 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||||||||||||||||||||
โข โฒ๐ฅ๐ & โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) โ โข ([๐ฆ / ๐ฅ]๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bj-el2oss1o 14496 | Shorter proof of el2oss1o 6443 using more axioms. (Contributed by BJ, 21-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ด โ 2o โ ๐ด โ 1o) | ||||||||||||||||||||||||||||||||
Various utility theorems using FOL and extensionality. | ||||||||||||||||||||||||||||||||
Theorem | bj-vtoclgft 14497 | Weakening two hypotheses of vtoclgf 2795. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||||||||
โข โฒ๐ฅ๐ด & โข โฒ๐ฅ๐ & โข (๐ฅ = ๐ด โ ๐) โ โข (โ๐ฅ(๐ฅ = ๐ด โ (๐ โ ๐)) โ (๐ด โ ๐ โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | bj-vtoclgf 14498 | Weakening two hypotheses of vtoclgf 2795. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||||||||
โข โฒ๐ฅ๐ด & โข โฒ๐ฅ๐ & โข (๐ฅ = ๐ด โ ๐) & โข (๐ฅ = ๐ด โ (๐ โ ๐)) โ โข (๐ด โ ๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | elabgf0 14499 | Lemma for elabgf 2879. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||||||||
โข (๐ฅ = ๐ด โ (๐ด โ {๐ฅ โฃ ๐} โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | elabgft1 14500 | One implication of elabgf 2879, in closed form. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||||||||
โข โฒ๐ฅ๐ด & โข โฒ๐ฅ๐ โ โข (โ๐ฅ(๐ฅ = ๐ด โ (๐ โ ๐)) โ (๐ด โ {๐ฅ โฃ ๐} โ ๐)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |