![]() |
Metamath
Proof Explorer Theorem List (p. 466 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fmtnoodd 46501 | Each Fermat number is odd. (Contributed by AV, 26-Jul-2021.) |
β’ (π β β0 β Β¬ 2 β₯ (FermatNoβπ)) | ||
Theorem | fmtnorn 46502* | A Fermat number is a function value of the enumeration of the Fermat numbers. (Contributed by AV, 3-Aug-2021.) |
β’ (πΉ β ran FermatNo β βπ β β0 (FermatNoβπ) = πΉ) | ||
Theorem | fmtnof1 46503 | The enumeration of the Fermat numbers is a one-one function into the positive integers. (Contributed by AV, 3-Aug-2021.) |
β’ FermatNo:β0β1-1ββ | ||
Theorem | fmtnoinf 46504 | The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021.) |
β’ ran FermatNo β Fin | ||
Theorem | fmtnorec1 46505 | The first recurrence relation for Fermat numbers, see Wikipedia "Fermat number", https://en.wikipedia.org/wiki/Fermat_number#Basic_properties, 22-Jul-2021. (Contributed by AV, 22-Jul-2021.) |
β’ (π β β0 β (FermatNoβ(π + 1)) = ((((FermatNoβπ) β 1)β2) + 1)) | ||
Theorem | sqrtpwpw2p 46506 | The floor of the square root of 2 to the power of 2 to the power of a positive integer plus a bounded nonnegative integer. (Contributed by AV, 28-Jul-2021.) |
β’ ((π β β β§ π β β0 β§ π < ((2β((2β(π β 1)) + 1)) + 1)) β (ββ(ββ((2β(2βπ)) + π))) = (2β(2β(π β 1)))) | ||
Theorem | fmtnosqrt 46507 | The floor of the square root of a Fermat number. (Contributed by AV, 28-Jul-2021.) |
β’ (π β β β (ββ(ββ(FermatNoβπ))) = (2β(2β(π β 1)))) | ||
Theorem | fmtno0 46508 | The 0 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
β’ (FermatNoβ0) = 3 | ||
Theorem | fmtno1 46509 | The 1 st Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
β’ (FermatNoβ1) = 5 | ||
Theorem | fmtnorec2lem 46510* | Lemma for fmtnorec2 46511 (induction step). (Contributed by AV, 29-Jul-2021.) |
β’ (π¦ β β0 β ((FermatNoβ(π¦ + 1)) = (βπ β (0...π¦)(FermatNoβπ) + 2) β (FermatNoβ((π¦ + 1) + 1)) = (βπ β (0...(π¦ + 1))(FermatNoβπ) + 2))) | ||
Theorem | fmtnorec2 46511* | The second recurrence relation for Fermat numbers, see ProofWiki "Product of Sequence of Fermat Numbers plus 2", 29-Jul-2021, https://proofwiki.org/wiki/Product_of_Sequence_of_Fermat_Numbers_plus_2 or Wikipedia "Fermat number", 29-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 29-Jul-2021.) |
β’ (π β β0 β (FermatNoβ(π + 1)) = (βπ β (0...π)(FermatNoβπ) + 2)) | ||
Theorem | fmtnodvds 46512 | Any Fermat number divides a greater Fermat number minus 2. Corollary of fmtnorec2 46511, see ProofWiki "Product of Sequence of Fermat Numbers plus 2/Corollary", 31-Jul-2021. (Contributed by AV, 1-Aug-2021.) |
β’ ((π β β0 β§ π β β) β (FermatNoβπ) β₯ ((FermatNoβ(π + π)) β 2)) | ||
Theorem | goldbachthlem1 46513 | Lemma 1 for goldbachth 46515. (Contributed by AV, 1-Aug-2021.) |
β’ ((π β β0 β§ π β β0 β§ π < π) β (FermatNoβπ) β₯ ((FermatNoβπ) β 2)) | ||
Theorem | goldbachthlem2 46514 | Lemma 2 for goldbachth 46515. (Contributed by AV, 1-Aug-2021.) |
β’ ((π β β0 β§ π β β0 β§ π < π) β ((FermatNoβπ) gcd (FermatNoβπ)) = 1) | ||
Theorem | goldbachth 46515 | Goldbach's theorem: Two different Fermat numbers are coprime. See ProofWiki "Goldbach's theorem", 31-Jul-2021, https://proofwiki.org/wiki/Goldbach%27s_Theorem or Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 1-Aug-2021.) |
β’ ((π β β0 β§ π β β0 β§ π β π) β ((FermatNoβπ) gcd (FermatNoβπ)) = 1) | ||
Theorem | fmtnorec3 46516* | The third recurrence relation for Fermat numbers, see Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 2-Aug-2021.) |
β’ (π β (β€β₯β2) β (FermatNoβπ) = ((FermatNoβ(π β 1)) + ((2β(2β(π β 1))) Β· βπ β (0...(π β 2))(FermatNoβπ)))) | ||
Theorem | fmtnorec4 46517 | The fourth recurrence relation for Fermat numbers, see Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 31-Jul-2021.) |
β’ (π β (β€β₯β2) β (FermatNoβπ) = (((FermatNoβ(π β 1))β2) β (2 Β· (((FermatNoβ(π β 2)) β 1)β2)))) | ||
Theorem | fmtno2 46518 | The 2 nd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
β’ (FermatNoβ2) = ;17 | ||
Theorem | fmtno3 46519 | The 3 rd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
β’ (FermatNoβ3) = ;;257 | ||
Theorem | fmtno4 46520 | The 4 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
β’ (FermatNoβ4) = ;;;;65537 | ||
Theorem | fmtno5lem1 46521 | Lemma 1 for fmtno5 46525. (Contributed by AV, 22-Jul-2021.) |
β’ (;;;;65536 Β· 6) = ;;;;;393216 | ||
Theorem | fmtno5lem2 46522 | Lemma 2 for fmtno5 46525. (Contributed by AV, 22-Jul-2021.) |
β’ (;;;;65536 Β· 5) = ;;;;;327680 | ||
Theorem | fmtno5lem3 46523 | Lemma 3 for fmtno5 46525. (Contributed by AV, 22-Jul-2021.) |
β’ (;;;;65536 Β· 3) = ;;;;;196608 | ||
Theorem | fmtno5lem4 46524 | Lemma 4 for fmtno5 46525. (Contributed by AV, 30-Jul-2021.) |
β’ (;;;;65536β2) = ;;;;;;;;;4294967296 | ||
Theorem | fmtno5 46525 | The 5 th Fermat number. (Contributed by AV, 30-Jul-2021.) |
β’ (FermatNoβ5) = ;;;;;;;;;4294967297 | ||
Theorem | fmtno0prm 46526 | The 0 th Fermat number is a prime (first Fermat prime). (Contributed by AV, 13-Jun-2021.) |
β’ (FermatNoβ0) β β | ||
Theorem | fmtno1prm 46527 | The 1 st Fermat number is a prime (second Fermat prime). (Contributed by AV, 13-Jun-2021.) |
β’ (FermatNoβ1) β β | ||
Theorem | fmtno2prm 46528 | The 2 nd Fermat number is a prime (third Fermat prime). (Contributed by AV, 13-Jun-2021.) |
β’ (FermatNoβ2) β β | ||
Theorem | 257prm 46529 | 257 is a prime number (the fourth Fermat prime). (Contributed by AV, 15-Jun-2021.) |
β’ ;;257 β β | ||
Theorem | fmtno3prm 46530 | The 3 rd Fermat number is a prime (fourth Fermat prime). (Contributed by AV, 15-Jun-2021.) |
β’ (FermatNoβ3) β β | ||
Theorem | odz2prm2pw 46531 | Any power of two is coprime to any prime not being two. (Contributed by AV, 25-Jul-2021.) |
β’ (((π β β β§ π β (β β {2})) β§ (((2β(2βπ)) mod π) β 1 β§ ((2β(2β(π + 1))) mod π) = 1)) β ((odβ€βπ)β2) = (2β(π + 1))) | ||
Theorem | fmtnoprmfac1lem 46532 | Lemma for fmtnoprmfac1 46533: The order of 2 modulo a prime that divides the n-th Fermat number is 2^(n+1). (Contributed by AV, 25-Jul-2021.) (Proof shortened by AV, 18-Mar-2022.) |
β’ ((π β β β§ π β (β β {2}) β§ π β₯ (FermatNoβπ)) β ((odβ€βπ)β2) = (2β(π + 1))) | ||
Theorem | fmtnoprmfac1 46533* | Divisor of Fermat number (special form of Euler's result, see fmtnofac1 46538): Let Fn be a Fermat number. Let p be a prime divisor of Fn. Then p is in the form: k*2^(n+1)+1 where k is a positive integer. (Contributed by AV, 25-Jul-2021.) |
β’ ((π β β β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β π = ((π Β· (2β(π + 1))) + 1)) | ||
Theorem | fmtnoprmfac2lem1 46534 | Lemma for fmtnoprmfac2 46535. (Contributed by AV, 26-Jul-2021.) |
β’ ((π β (β€β₯β2) β§ π β (β β {2}) β§ π β₯ (FermatNoβπ)) β ((2β((π β 1) / 2)) mod π) = 1) | ||
Theorem | fmtnoprmfac2 46535* | Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 46537): Let Fn be a Fermat number. Let p be a prime divisor of Fn. Then p is in the form: k*2^(n+2)+1 where k is a positive integer. (Contributed by AV, 26-Jul-2021.) |
β’ ((π β (β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β π = ((π Β· (2β(π + 2))) + 1)) | ||
Theorem | fmtnofac2lem 46536* | Lemma for fmtnofac2 46537 (Induction step). (Contributed by AV, 30-Jul-2021.) |
β’ ((π¦ β (β€β₯β2) β§ π§ β (β€β₯β2)) β ((((π β (β€β₯β2) β§ π¦ β₯ (FermatNoβπ)) β βπ β β0 π¦ = ((π Β· (2β(π + 2))) + 1)) β§ ((π β (β€β₯β2) β§ π§ β₯ (FermatNoβπ)) β βπ β β0 π§ = ((π Β· (2β(π + 2))) + 1))) β ((π β (β€β₯β2) β§ (π¦ Β· π§) β₯ (FermatNoβπ)) β βπ β β0 (π¦ Β· π§) = ((π Β· (2β(π + 2))) + 1)))) | ||
Theorem | fmtnofac2 46537* | Divisor of Fermat number (Euler's Result refined by FranΓ§ois Γdouard Anatole Lucas), see fmtnofac1 46538: Let Fn be a Fermat number. Let m be divisor of Fn. Then m is in the form: k*2^(n+2)+1 where k is a nonnegative integer. (Contributed by AV, 30-Jul-2021.) |
β’ ((π β (β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β0 π = ((π Β· (2β(π + 2))) + 1)) | ||
Theorem | fmtnofac1 46538* |
Divisor of Fermat number (Euler's Result), see ProofWiki "Divisor of
Fermat Number/Euler's Result", 24-Jul-2021,
https://proofwiki.org/wiki/Divisor_of_Fermat_Number/Euler's_Result):
"Let Fn be a Fermat number. Let
m be divisor of Fn. Then m is in the
form: k*2^(n+1)+1 where k is a positive integer." Here, however, k
must
be a nonnegative integer, because k must be 0 to represent 1 (which is a
divisor of Fn ).
Historical Note: In 1747, Leonhard Paul Euler proved that a divisor of a Fermat number Fn is always in the form kx2^(n+1)+1. This was later refined to k*2^(n+2)+1 by FranΓ§ois Γdouard Anatole Lucas, see fmtnofac2 46537. (Contributed by AV, 30-Jul-2021.) |
β’ ((π β β β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β0 π = ((π Β· (2β(π + 1))) + 1)) | ||
Theorem | fmtno4sqrt 46539 | The floor of the square root of the fourth Fermat number is 256. (Contributed by AV, 28-Jul-2021.) |
β’ (ββ(ββ(FermatNoβ4))) = ;;256 | ||
Theorem | fmtno4prmfac 46540 | If P was a (prime) factor of the fourth Fermat number less than the square root of the fourth Fermat number, it would be either 65 or 129 or 193. (Contributed by AV, 28-Jul-2021.) |
β’ ((π β β β§ π β₯ (FermatNoβ4) β§ π β€ (ββ(ββ(FermatNoβ4)))) β (π = ;65 β¨ π = ;;129 β¨ π = ;;193)) | ||
Theorem | fmtno4prmfac193 46541 | If P was a (prime) factor of the fourth Fermat number, it would be 193. (Contributed by AV, 28-Jul-2021.) |
β’ ((π β β β§ π β₯ (FermatNoβ4) β§ π β€ (ββ(ββ(FermatNoβ4)))) β π = ;;193) | ||
Theorem | fmtno4nprmfac193 46542 | 193 is not a (prime) factor of the fourth Fermat number. (Contributed by AV, 24-Jul-2021.) |
β’ Β¬ ;;193 β₯ (FermatNoβ4) | ||
Theorem | fmtno4prm 46543 | The 4-th Fermat number (65537) is a prime (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.) |
β’ (FermatNoβ4) β β | ||
Theorem | 65537prm 46544 | 65537 is a prime number (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.) |
β’ ;;;;65537 β β | ||
Theorem | fmtnofz04prm 46545 | The first five Fermat numbers are prime, see remark in [ApostolNT] p. 7. (Contributed by AV, 28-Jul-2021.) |
β’ (π β (0...4) β (FermatNoβπ) β β) | ||
Theorem | fmtnole4prm 46546 | The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021.) |
β’ ((π β β0 β§ π β€ 4) β (FermatNoβπ) β β) | ||
Theorem | fmtno5faclem1 46547 | Lemma 1 for fmtno5fac 46550. (Contributed by AV, 22-Jul-2021.) |
β’ (;;;;;;6700417 Β· 4) = ;;;;;;;26801668 | ||
Theorem | fmtno5faclem2 46548 | Lemma 2 for fmtno5fac 46550. (Contributed by AV, 22-Jul-2021.) |
β’ (;;;;;;6700417 Β· 6) = ;;;;;;;40202502 | ||
Theorem | fmtno5faclem3 46549 | Lemma 3 for fmtno5fac 46550. (Contributed by AV, 22-Jul-2021.) |
β’ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688 | ||
Theorem | fmtno5fac 46550 | The factorisation of the 5 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 22-Jul-2021.) |
β’ (FermatNoβ5) = (;;;;;;6700417 Β· ;;641) | ||
Theorem | fmtno5nprm 46551 | The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021.) |
β’ (FermatNoβ5) β β | ||
Theorem | prmdvdsfmtnof1lem1 46552* | Lemma 1 for prmdvdsfmtnof1 46555. (Contributed by AV, 3-Aug-2021.) |
β’ πΌ = inf({π β β β£ π β₯ πΉ}, β, < ) & β’ π½ = inf({π β β β£ π β₯ πΊ}, β, < ) β β’ ((πΉ β (β€β₯β2) β§ πΊ β (β€β₯β2)) β (πΌ = π½ β (πΌ β β β§ πΌ β₯ πΉ β§ πΌ β₯ πΊ))) | ||
Theorem | prmdvdsfmtnof1lem2 46553 | Lemma 2 for prmdvdsfmtnof1 46555. (Contributed by AV, 3-Aug-2021.) |
β’ ((πΉ β ran FermatNo β§ πΊ β ran FermatNo) β ((πΌ β β β§ πΌ β₯ πΉ β§ πΌ β₯ πΊ) β πΉ = πΊ)) | ||
Theorem | prmdvdsfmtnof 46554* | The mapping of a Fermat number to its smallest prime factor is a function. (Contributed by AV, 4-Aug-2021.) (Proof shortened by II, 16-Feb-2023.) |
β’ πΉ = (π β ran FermatNo β¦ inf({π β β β£ π β₯ π}, β, < )) β β’ πΉ:ran FermatNoβΆβ | ||
Theorem | prmdvdsfmtnof1 46555* | The mapping of a Fermat number to its smallest prime factor is a one-to-one function. (Contributed by AV, 4-Aug-2021.) |
β’ πΉ = (π β ran FermatNo β¦ inf({π β β β£ π β₯ π}, β, < )) β β’ πΉ:ran FermatNoβ1-1ββ | ||
Theorem | prminf2 46556 | The set of prime numbers is infinite. The proof of this variant of prminf 16853 is based on Goldbach's theorem goldbachth 46515 (via prmdvdsfmtnof1 46555 and prmdvdsfmtnof1lem2 46553), see Wikipedia "Fermat number", 4-Aug-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties 46553. (Contributed by AV, 4-Aug-2021.) |
β’ β β Fin | ||
Theorem | 2pwp1prm 46557* | For ((2βπ) + 1) to be prime, π must be a power of 2, see Wikipedia "Fermat number", section "Other theorms about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number, 5-Aug-2021. (Contributed by AV, 7-Aug-2021.) |
β’ ((πΎ β β β§ ((2βπΎ) + 1) β β) β βπ β β0 πΎ = (2βπ)) | ||
Theorem | 2pwp1prmfmtno 46558* | Every prime number of the form ((2βπ) + 1) must be a Fermat number. (Contributed by AV, 7-Aug-2021.) |
β’ ((πΎ β β β§ π = ((2βπΎ) + 1) β§ π β β) β βπ β β0 π = (FermatNoβπ)) | ||
"In mathematics, a Mersenne prime is a prime number that is one less than a power of two. That is, it is a prime number of the form Mn = 2^n-1 for some integer n. They are named after Marin Mersenne ... If n is a composite number then so is 2^n-1. Therefore, an equivalent definition of the Mersenne primes is that they are the prime numbers of the form Mp = 2^p-1 for some prime p.", see Wikipedia "Mersenne prime", 16-Aug-2021, https://en.wikipedia.org/wiki/Mersenne_prime. See also definition in [ApostolNT] p. 4. This means that if Mn = 2^n-1 is prime, than n must be prime, too, see mersenne 26963. The reverse direction is not generally valid: If p is prime, then Mp = 2^p-1 needs not be prime, e.g. M11 = 2047 = 23 x 89, see m11nprm 46569. This is an example of sgprmdvdsmersenne 46572, stating that if p with p = 3 modulo 4 (here 11) and q=2p+1 (here 23) are prime, then q divides Mp. "In number theory, a prime number p is a Sophie Germain prime if 2p+1 is also prime. The number 2p+1 associated with a Sophie Germain prime is called a safe prime.", see Wikipedia "Safe and Sophie Germain primes", 21-Aug-2021, https://en.wikipedia.org/wiki/Safe_and_Sophie_Germain_primes 46572. Hence, 11 is a Sophie Germain prime and 2x11+1=23 is its associated safe prime. By sfprmdvdsmersenne 46571, it is shown that if a safe prime q is congruent to 7 modulo 8, then it is a divisor of the Mersenne number with its matching Sophie Germain prime as exponent. The main result of this section, however, is the formal proof of a theorem of S. Ligh and L. Neal in "A note on Mersenne numbers", see lighneal 46579. | ||
Theorem | m2prm 46559 | The second Mersenne number M2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021.) |
β’ ((2β2) β 1) β β | ||
Theorem | m3prm 46560 | The third Mersenne number M3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021.) |
β’ ((2β3) β 1) β β | ||
Theorem | flsqrt 46561 | A condition equivalent to the floor of a square root. (Contributed by AV, 17-Aug-2021.) |
β’ (((π΄ β β β§ 0 β€ π΄) β§ π΅ β β0) β ((ββ(ββπ΄)) = π΅ β ((π΅β2) β€ π΄ β§ π΄ < ((π΅ + 1)β2)))) | ||
Theorem | flsqrt5 46562 | The floor of the square root of a nonnegative number is 5 iff the number is between 25 and 35. (Contributed by AV, 17-Aug-2021.) |
β’ ((π β β β§ 0 β€ π) β ((;25 β€ π β§ π < ;36) β (ββ(ββπ)) = 5)) | ||
Theorem | 3ndvds4 46563 | 3 does not divide 4. (Contributed by AV, 18-Aug-2021.) |
β’ Β¬ 3 β₯ 4 | ||
Theorem | 139prmALT 46564 | 139 is a prime number. In contrast to 139prm 17062, the proof of this theorem uses 3dvds2dec 16281 for checking the divisibility by 3. Although the proof using 3dvds2dec 16281 is longer (regarding size: 1849 characters compared with 1809 for 139prm 17062), the number of essential steps is smaller (301 compared with 327 for 139prm 17062). (Contributed by Mario Carneiro, 19-Feb-2014.) (Revised by AV, 18-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ ;;139 β β | ||
Theorem | 31prm 46565 | 31 is a prime number. In contrast to 37prm 17059, the proof of this theorem is not based on the "blanket" prmlem2 17058, but on isprm7 16650. Although the checks for non-divisibility by the primes 7 to 23 are not needed, the proof is much longer (regarding size) than the proof of 37prm 17059 (1810 characters compared with 1213 for 37prm 17059). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 17059). (Contributed by AV, 17-Aug-2021.) (Proof modification is discouraged.) |
β’ ;31 β β | ||
Theorem | m5prm 46566 | The fifth Mersenne number M5 = 31 is a prime number. (Contributed by AV, 17-Aug-2021.) |
β’ ((2β5) β 1) β β | ||
Theorem | 127prm 46567 | 127 is a prime number. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 16-Sep-2021.) |
β’ ;;127 β β | ||
Theorem | m7prm 46568 | The seventh Mersenne number M7 = 127 is a prime number. (Contributed by AV, 18-Aug-2021.) |
β’ ((2β7) β 1) β β | ||
Theorem | m11nprm 46569 | The eleventh Mersenne number M11 = 2047 is not a prime number. (Contributed by AV, 18-Aug-2021.) |
β’ ((2β;11) β 1) = (;89 Β· ;23) | ||
Theorem | mod42tp1mod8 46570 | If a number is 3 modulo 4, twice the number plus 1 is 7 modulo 8. (Contributed by AV, 19-Aug-2021.) |
β’ ((π β β€ β§ (π mod 4) = 3) β (((2 Β· π) + 1) mod 8) = 7) | ||
Theorem | sfprmdvdsmersenne 46571 | If π is a safe prime (i.e. π = ((2 Β· π) + 1) for a prime π) with πβ‘7 (mod 8), then π divides the π-th Mersenne number MP. (Contributed by AV, 20-Aug-2021.) |
β’ ((π β β β§ (π β β β§ (π mod 8) = 7 β§ π = ((2 Β· π) + 1))) β π β₯ ((2βπ) β 1)) | ||
Theorem | sgprmdvdsmersenne 46572 | If π is a Sophie Germain prime (i.e. π = ((2 Β· π) + 1) is also prime) with πβ‘3 (mod 4), then π divides the π-th Mersenne number MP. (Contributed by AV, 20-Aug-2021.) |
β’ (((π β β β§ (π mod 4) = 3) β§ (π = ((2 Β· π) + 1) β§ π β β)) β π β₯ ((2βπ) β 1)) | ||
Theorem | lighneallem1 46573 | Lemma 1 for lighneal 46579. (Contributed by AV, 11-Aug-2021.) |
β’ ((π = 2 β§ π β β β§ π β β) β ((2βπ) β 1) β (πβπ)) | ||
Theorem | lighneallem2 46574 | Lemma 2 for lighneal 46579. (Contributed by AV, 13-Aug-2021.) |
β’ (((π β (β β {2}) β§ π β β β§ π β β) β§ 2 β₯ π β§ ((2βπ) β 1) = (πβπ)) β π = 1) | ||
Theorem | lighneallem3 46575 | Lemma 3 for lighneal 46579. (Contributed by AV, 11-Aug-2021.) |
β’ (((π β (β β {2}) β§ π β β β§ π β β) β§ (Β¬ 2 β₯ π β§ 2 β₯ π) β§ ((2βπ) β 1) = (πβπ)) β π = 1) | ||
Theorem | lighneallem4a 46576 | Lemma 1 for lighneallem4 46578. (Contributed by AV, 16-Aug-2021.) |
β’ ((π΄ β (β€β₯β2) β§ π β (β€β₯β3) β§ π = (((π΄βπ) + 1) / (π΄ + 1))) β 2 β€ π) | ||
Theorem | lighneallem4b 46577* | Lemma 2 for lighneallem4 46578. (Contributed by AV, 16-Aug-2021.) |
β’ ((π΄ β (β€β₯β2) β§ π β (β€β₯β2) β§ Β¬ 2 β₯ π) β Ξ£π β (0...(π β 1))((-1βπ) Β· (π΄βπ)) β (β€β₯β2)) | ||
Theorem | lighneallem4 46578 | Lemma 3 for lighneal 46579. (Contributed by AV, 16-Aug-2021.) |
β’ (((π β (β β {2}) β§ π β β β§ π β β) β§ (Β¬ 2 β₯ π β§ Β¬ 2 β₯ π) β§ ((2βπ) β 1) = (πβπ)) β π = 1) | ||
Theorem | lighneal 46579 | If a power of a prime π (i.e. πβπ) is of the form 2βπ β 1, then π must be prime and π must be 1. Generalization of mersenne 26963 (where π = 1 is a prerequisite). Theorem of S. Ligh and L. Neal (1974) "A note on Mersenne mumbers", Mathematics Magazine, 47:4, 231-233. (Contributed by AV, 16-Aug-2021.) |
β’ (((π β β β§ π β β β§ π β β) β§ ((2βπ) β 1) = (πβπ)) β (π = 1 β§ π β β)) | ||
Theorem | modexp2m1d 46580 | The square of an integer which is -1 modulo a number greater than 1 is 1 modulo the same modulus. (Contributed by AV, 5-Jul-2020.) |
β’ (π β π΄ β β€) & β’ (π β πΈ β β+) & β’ (π β 1 < πΈ) & β’ (π β (π΄ mod πΈ) = (-1 mod πΈ)) β β’ (π β ((π΄β2) mod πΈ) = 1) | ||
Theorem | proththdlem 46581 | Lemma for proththd 46582. (Contributed by AV, 4-Jul-2020.) |
β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β π = ((πΎ Β· (2βπ)) + 1)) β β’ (π β (π β β β§ 1 < π β§ ((π β 1) / 2) β β)) | ||
Theorem | proththd 46582* | Proth's theorem (1878). If P is a Proth number, i.e. a number of the form k2^n+1 with k less than 2^n, and if there exists an integer x for which x^((P-1)/2) is -1 modulo P, then P is prime. Such a prime is called a Proth prime. Like Pocklington's theorem (see pockthg 16844), Proth's theorem allows for a convenient method for verifying large primes. (Contributed by AV, 5-Jul-2020.) |
β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β π = ((πΎ Β· (2βπ)) + 1)) & β’ (π β πΎ < (2βπ)) & β’ (π β βπ₯ β β€ ((π₯β((π β 1) / 2)) mod π) = (-1 mod π)) β β’ (π β π β β) | ||
Theorem | 5tcu2e40 46583 | 5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020.) |
β’ (5 Β· (2β3)) = ;40 | ||
Theorem | 3exp4mod41 46584 | 3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020.) |
β’ ((3β4) mod ;41) = (-1 mod ;41) | ||
Theorem | 41prothprmlem1 46585 | Lemma 1 for 41prothprm 46587. (Contributed by AV, 4-Jul-2020.) |
β’ π = ;41 β β’ ((π β 1) / 2) = ;20 | ||
Theorem | 41prothprmlem2 46586 | Lemma 2 for 41prothprm 46587. (Contributed by AV, 5-Jul-2020.) |
β’ π = ;41 β β’ ((3β((π β 1) / 2)) mod π) = (-1 mod π) | ||
Theorem | 41prothprm 46587 | 41 is a Proth prime. (Contributed by AV, 5-Jul-2020.) |
β’ π = ;41 β β’ (π = ((5 Β· (2β3)) + 1) β§ π β β) | ||
Theorem | quad1 46588* | A condition for a quadratic equation with complex coefficients to have (exactly) one complex solution. (Contributed by AV, 23-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· = ((π΅β2) β (4 Β· (π΄ Β· πΆ)))) β β’ (π β (β!π₯ β β ((π΄ Β· (π₯β2)) + ((π΅ Β· π₯) + πΆ)) = 0 β π· = 0)) | ||
Theorem | requad01 46589* | A condition for a quadratic equation with real coefficients to have (at least) one real solution. (Contributed by AV, 23-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· = ((π΅β2) β (4 Β· (π΄ Β· πΆ)))) β β’ (π β (βπ₯ β β ((π΄ Β· (π₯β2)) + ((π΅ Β· π₯) + πΆ)) = 0 β 0 β€ π·)) | ||
Theorem | requad1 46590* | A condition for a quadratic equation with real coefficients to have (exactly) one real solution. (Contributed by AV, 26-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· = ((π΅β2) β (4 Β· (π΄ Β· πΆ)))) β β’ (π β (β!π₯ β β ((π΄ Β· (π₯β2)) + ((π΅ Β· π₯) + πΆ)) = 0 β π· = 0)) | ||
Theorem | requad2 46591* | A condition for a quadratic equation with real coefficients to have (exactly) two different real solutions. (Contributed by AV, 28-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· = ((π΅β2) β (4 Β· (π΄ Β· πΆ)))) β β’ (π β (β!π β π« β((β―βπ) = 2 β§ βπ₯ β π ((π΄ Β· (π₯β2)) + ((π΅ Β· π₯) + πΆ)) = 0) β 0 < π·)) | ||
Even and odd numbers can be characterized in many different ways. In the following, the definition of even and odd numbers is based on the fact that dividing an even number (resp. an odd number increased by 1) by 2 is an integer, see df-even 46594 and df-odd 46595. Alternate definitions resp. characterizations are provided in dfeven2 46617, dfeven3 46626, dfeven4 46606 and in dfodd2 46604, dfodd3 46618, dfodd4 46627, dfodd5 46628, dfodd6 46605. Each characterization can be useful (and used) in an appropriate context, e.g. dfodd6 46605 in opoeALTV 46651 and dfodd3 46618 in oddprmALTV 46655. Having a fixed definition for even and odd numbers, and alternate characterizations as theorems, advanced theorems about even and/or odd numbers can be expressed more explicitly, and the appropriate characterization can be chosen for their proof, which may become clearer and sometimes also shorter (see, for example, divgcdoddALTV 46650 and divgcdodd 16652). | ||
Syntax | ceven 46592 | Extend the definition of a class to include the set of even numbers. |
class Even | ||
Syntax | codd 46593 | Extend the definition of a class to include the set of odd numbers. |
class Odd | ||
Definition | df-even 46594 | Define the set of even numbers. (Contributed by AV, 14-Jun-2020.) |
β’ Even = {π§ β β€ β£ (π§ / 2) β β€} | ||
Definition | df-odd 46595 | Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.) |
β’ Odd = {π§ β β€ β£ ((π§ + 1) / 2) β β€} | ||
Theorem | iseven 46596 | The predicate "is an even number". An even number is an integer which is divisible by 2, i.e. the result of dividing the even integer by 2 is still an integer. (Contributed by AV, 14-Jun-2020.) |
β’ (π β Even β (π β β€ β§ (π / 2) β β€)) | ||
Theorem | isodd 46597 | The predicate "is an odd number". An odd number is an integer which is not divisible by 2, i.e. the result of dividing the odd integer increased by 1 and then divided by 2 is still an integer. (Contributed by AV, 14-Jun-2020.) |
β’ (π β Odd β (π β β€ β§ ((π + 1) / 2) β β€)) | ||
Theorem | evenz 46598 | An even number is an integer. (Contributed by AV, 14-Jun-2020.) |
β’ (π β Even β π β β€) | ||
Theorem | oddz 46599 | An odd number is an integer. (Contributed by AV, 14-Jun-2020.) |
β’ (π β Odd β π β β€) | ||
Theorem | evendiv2z 46600 | The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.) |
β’ (π β Even β (π / 2) β β€) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |