![]() |
Intuitionistic Logic Explorer Theorem List (p. 143 of 147) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description | ||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||
Theorem | lgsval3 14201 | The Legendre symbol at an odd prime (this is the traditional domain of the Legendre symbol). (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsvalmod 14202 |
The Legendre symbol is equivalent to ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsval4 14203* |
Restate lgsval 14187 for nonzero ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsfcl3 14204* |
Closure of the function ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsval4a 14205* |
Same as lgsval4 14203 for positive ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgscl1 14206 | The value of the Legendre symbol is either -1 or 0 or 1. (Contributed by AV, 13-Jul-2021.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsneg 14207 | The Legendre symbol is either even or odd under negation with respect to the second parameter according to the sign of the first. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsneg1 14208 | The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsmod 14209 |
The Legendre (Jacobi) symbol is preserved under reduction ![]() ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdilem 14210 | Lemma for lgsdi 14220 and lgsdir 14218: the sign part of the Legendre symbol is multiplicative. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdir2lem1 14211 | Lemma for lgsdir2 14216. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdir2lem2 14212 | Lemma for lgsdir2 14216. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdir2lem3 14213 | Lemma for lgsdir2 14216. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdir2lem4 14214 | Lemma for lgsdir2 14216. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdir2lem5 14215 | Lemma for lgsdir2 14216. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdir2 14216 |
The Legendre symbol is completely multiplicative at ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdirprm 14217 | 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.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdir 14218 |
The Legendre symbol is completely multiplicative in its left argument.
Generalization of theorem 9.9(a) in [ApostolNT] p. 188 (which assumes
that ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdilem2 14219* | Lemma for lgsdi 14220. (Contributed by Mario Carneiro, 4-Feb-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdi 14220 |
The Legendre symbol is completely multiplicative in its right
argument. Generalization of theorem 9.9(b) in [ApostolNT] p. 188
(which assumes that ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsne0 14221 |
The Legendre symbol is nonzero (and hence equal to ![]() ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsabs1 14222 |
The Legendre symbol is nonzero (and hence equal to ![]() ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgssq 14223 |
The Legendre symbol at a square is equal to ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgssq2 14224 |
The Legendre symbol at a square is equal to ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsprme0 14225 |
The Legendre symbol at any prime (even at 2) is ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 1lgs 14226 |
The Legendre symbol at ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgs1 14227 |
The Legendre symbol at ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsmodeq 14228 |
The Legendre (Jacobi) symbol is preserved under reduction ![]() ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsmulsqcoprm 14229 | 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.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdirnn0 14230 |
Variation on lgsdir 14218 valid for all ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | lgsdinn0 14231 |
Variation on lgsdi 14220 valid for all ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem1 14232* | Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem2 14233* | Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | mul2sq 14234 | 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.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem3 14235 | Lemma for 2sqlem5 14237. (Contributed by Mario Carneiro, 20-Jun-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem4 14236 | Lemma for 2sqlem5 14237. (Contributed by Mario Carneiro, 20-Jun-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem5 14237 | 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.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem6 14238* | 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.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem7 14239* | Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem8a 14240* | Lemma for 2sqlem8 14241. (Contributed by Mario Carneiro, 4-Jun-2016.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem8 14241* | Lemma for 2sq . (Contributed by Mario Carneiro, 20-Jun-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem9 14242* | Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 2sqlem10 14243* | 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.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
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 14244 |
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 14245 | Example for ax-io 709. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | ex-an 14246 | Example for ax-ia1 106. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 1kp2ke3k 14247 |
Example for df-dec 9379, 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 This proof heavily relies on the decimal constructor df-dec 9379 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.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | ex-fl 14248 | Example for df-fl 10263. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | ex-ceil 14249 | Example for df-ceil 10264. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | ex-exp 14250 | Example for df-exp 10513. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | ex-fac 14251 | Example for df-fac 10697. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | ex-bc 14252 | Example for df-bc 10719. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | ex-dvds 14253 | Example for df-dvds 11786: 3 divides into 6. (Contributed by David A. Wheeler, 19-May-2015.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | ex-gcd 14254 | Example for df-gcd 11934. (Contributed by AV, 5-Sep-2021.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | mathbox 14255 |
(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 14256 | 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 14257 | Double negation of a disjunction in terms of implication. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-nnim 14258 | The double negation of an implication implies the implication with the consequent doubly negated. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-nnan 14259 | The double negation of a conjunction implies the conjunction of the double negations. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-nnclavius 14260 | Clavius law with doubly negated consequent. (Contributed by BJ, 4-Dec-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-imnimnn 14261 | 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 14260 as its last step. (Contributed by BJ, 27-Oct-2024.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Some of the following theorems, like bj-sttru 14263 or bj-stfal 14265 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 14262 | A provable formula is stable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-sttru 14263 | The true truth value is stable. (Contributed by BJ, 5-Aug-2024.) | ||||||||||||||||||||||||||||||
![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-fast 14264 | A refutable formula is stable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-stfal 14265 | The false truth value is stable. (Contributed by BJ, 5-Aug-2024.) | ||||||||||||||||||||||||||||||
![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-nnst 14266 |
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 14513 for the version not using the definition of
stability.
(Contributed by BJ, 9-Oct-2019.) Prove it in ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-nnbist 14267 |
If a formula is not refutable, then it is stable if and only if it is
provable. By double-negation translation, if ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-stst 14268 | Stability of a proposition is stable if and only if that proposition is stable. STAB is idempotent. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-stim 14269 | A conjunction with a stable consequent is stable. See stabnot 833 for negation , bj-stan 14270 for conjunction , and bj-stal 14272 for universal quantification. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-stan 14270 | The conjunction of two stable formulas is stable. See bj-stim 14269 for implication, stabnot 833 for negation, and bj-stal 14272 for universal quantification. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-stand 14271 | The conjunction of two stable formulas is stable. Deduction form of bj-stan 14270. Its proof is shorter (when counting all steps, including syntactic steps), so one could prove it first and then bj-stan 14270 from it, the usual way. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-stal 14272 | The universal quantification of a stable formula is stable. See bj-stim 14269 for implication, stabnot 833 for negation, and bj-stan 14270 for conjunction. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-pm2.18st 14273 | Clavius law for stable formulas. See pm2.18dc 855. (Contributed by BJ, 4-Dec-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-con1st 14274 | Contraposition when the antecedent is a negated stable proposition. See con1dc 856. (Contributed by BJ, 11-Nov-2024.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-trdc 14275 | A provable formula is decidable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-dctru 14276 | The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.) | ||||||||||||||||||||||||||||||
![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-fadc 14277 | A refutable formula is decidable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-dcfal 14278 | The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.) | ||||||||||||||||||||||||||||||
![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-dcstab 14279 | A decidable formula is stable. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-nnbidc 14280 | If a formula is not refutable, then it is decidable if and only if it is provable. See also comment of bj-nnbist 14267. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-nndcALT 14281 | Alternate proof of nndc 851. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-dcdc 14282 | Decidability of a proposition is decidable if and only if that proposition is decidable. DECID is idempotent. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-stdc 14283 | 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.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-dcst 14284 | Stability of a proposition is decidable if and only if that proposition is stable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-ex 14285* | 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 14286 | Closed form of hbal 1477 (copied from set.mm). (Contributed by BJ, 2-May-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-nfalt 14287 | Closed form of nfal 1576 (copied from set.mm). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | spimd 14288 | Deduction form of spim 1738. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | 2spim 14289* | Double substitution, as in spim 1738. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | ch2var 14290* |
Implicit substitution of ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | ch2varv 14291* | Version of ch2var 14290 with nonfreeness hypotheses replaced with disjoint variable conditions. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-exlimmp 14292 | Lemma for bj-vtoclgf 14299. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-exlimmpi 14293 | Lemma for bj-vtoclgf 14299. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-sbimedh 14294 | A strengthening of sbiedh 1787 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-sbimeh 14295 | A strengthening of sbieh 1790 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-sbime 14296 | A strengthening of sbie 1791 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-el2oss1o 14297 | Shorter proof of el2oss1o 6439 using more axioms. (Contributed by BJ, 21-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Various utility theorems using FOL and extensionality. | ||||||||||||||||||||||||||||||||
Theorem | bj-vtoclgft 14298 | Weakening two hypotheses of vtoclgf 2795. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | bj-vtoclgf 14299 | Weakening two hypotheses of vtoclgf 2795. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||||||||||||||||||||||||||||||||
Theorem | elabgf0 14300 | Lemma for elabgf 2879. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||||||||
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |