Home | Metamath
Proof Explorer Theorem List (p. 401 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fmtno3 40001 | The 3 rd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘3) = ;;257 | ||
Theorem | fmtno4 40002 | The 4 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘4) = ;;;;65537 | ||
Theorem | fmtno5lem1 40003 | Lemma 1 for fmtno5 40007. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;65536 · 6) = ;;;;;393216 | ||
Theorem | fmtno5lem2 40004 | Lemma 2 for fmtno5 40007. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;65536 · 5) = ;;;;;327680 | ||
Theorem | fmtno5lem3 40005 | Lemma 3 for fmtno5 40007. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;65536 · 3) = ;;;;;196608 | ||
Theorem | fmtno5lem4 40006 | Lemma 4 for fmtno5 40007. (Contributed by AV, 30-Jul-2021.) |
⊢ (;;;;65536↑2) = ;;;;;;;;;4294967296 | ||
Theorem | fmtno5 40007 | The 5 th Fermat number. (Contributed by AV, 30-Jul-2021.) |
⊢ (FermatNo‘5) = ;;;;;;;;;4294967297 | ||
Theorem | fmtno0prm 40008 | The 0 th Fermat number is a prime (first Fermat prime). (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘0) ∈ ℙ | ||
Theorem | fmtno1prm 40009 | The 1 st Fermat number is a prime (second Fermat prime). (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘1) ∈ ℙ | ||
Theorem | fmtno2prm 40010 | The 2 nd Fermat number is a prime (third Fermat prime). (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘2) ∈ ℙ | ||
Theorem | 257prm 40011 | 257 is a prime number (the fourth Fermat prime). (Contributed by AV, 15-Jun-2021.) |
⊢ ;;257 ∈ ℙ | ||
Theorem | fmtno3prm 40012 | The 3 rd Fermat number is a prime (fourth Fermat prime). (Contributed by AV, 15-Jun-2021.) |
⊢ (FermatNo‘3) ∈ ℙ | ||
Theorem | odz2prm2pw 40013 | 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 40014 | Lemma for fmtnoprmfac1 40015: The order of 2 modulo a prime that divides the n-th Fermat number is 2^(n+1). (Contributed by AV, 25-Jul-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) | ||
Theorem | fmtnoprmfac1 40015* | Divisor of Fermat number (special form of Euler's result, see fmtnofac1 40020): 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 40016 | Lemma for fmtnoprmfac2 40017. (Contributed by AV, 26-Jul-2021.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1) | ||
Theorem | fmtnoprmfac2 40017* | Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 40019): 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 40018* | Lemma for fmtnofac2 40019 (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 40019* | Divisor of Fermat number (Euler's Result refined by François Édouard Anatole Lucas), see fmtnofac1 40020: 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 40020* |
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 40019. (Contributed by AV, 30-Jul-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 1))) + 1)) | ||
Theorem | fmtno4sqrt 40021 | The floor of the square root of the fourth Fermat number is 256. (Contributed by AV, 28-Jul-2021.) |
⊢ (⌊‘(√‘(FermatNo‘4))) = ;;256 | ||
Theorem | fmtno4prmfac 40022 | 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 40023 | 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 40024 | 193 is not a (prime) factor of the fourth Fermat number. (Contributed by AV, 24-Jul-2021.) |
⊢ ¬ ;;193 ∥ (FermatNo‘4) | ||
Theorem | fmtno4prm 40025 | The 4-th Fermat number (65537) is a prime (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.) |
⊢ (FermatNo‘4) ∈ ℙ | ||
Theorem | 65537prm 40026 | 65537 is a prime number (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.) |
⊢ ;;;;65537 ∈ ℙ | ||
Theorem | fmtnofz04prm 40027 | The first five Fermat numbers are prime, see remark in [ApostolNT] p. 7. (Contributed by AV, 28-Jul-2021.) |
⊢ (𝑁 ∈ (0...4) → (FermatNo‘𝑁) ∈ ℙ) | ||
Theorem | fmtnole4prm 40028 | The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4) → (FermatNo‘𝑁) ∈ ℙ) | ||
Theorem | fmtno5faclem1 40029 | Lemma 1 for fmtno5fac 40032. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;6700417 · 4) = ;;;;;;;26801668 | ||
Theorem | fmtno5faclem2 40030 | Lemma 2 for fmtno5fac 40032. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;6700417 · 6) = ;;;;;;;40202502 | ||
Theorem | fmtno5faclem3 40031 | Lemma 3 for fmtno5fac 40032. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688 | ||
Theorem | fmtno5fac 40032 | 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 40033 | The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021.) |
⊢ (FermatNo‘5) ∉ ℙ | ||
Theorem | prmdvdsfmtnof1lem1 40034* | Lemma 1 for prmdvdsfmtnof1 40037. (Contributed by AV, 3-Aug-2021.) |
⊢ 𝐼 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹}, ℝ, < ) & ⊢ 𝐽 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺}, ℝ, < ) ⇒ ⊢ ((𝐹 ∈ (ℤ≥‘2) ∧ 𝐺 ∈ (ℤ≥‘2)) → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺))) | ||
Theorem | prmdvdsfmtnof1lem2 40035 | Lemma 2 for prmdvdsfmtnof1 40037. (Contributed by AV, 3-Aug-2021.) |
⊢ ((𝐹 ∈ ran FermatNo ∧ 𝐺 ∈ ran FermatNo) → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)) | ||
Theorem | prmdvdsfmtnof 40036* | The mapping of a Fermat number to its smallest prime factor is a function. (Contributed by AV, 4-Aug-2021.) |
⊢ 𝐹 = (𝑓 ∈ ran FermatNo ↦ inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓}, ℝ, < )) ⇒ ⊢ 𝐹:ran FermatNo⟶ℙ | ||
Theorem | prmdvdsfmtnof1 40037* | 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 40038 | The set of prime numbers is infinite. The proof of this variant of prminf 15457 is based on Goldbach's theorem goldbachth 39997 (via prmdvdsfmtnof1 40037 and prmdvdsfmtnof1lem2 40035), see Wikipedia "Fermat number", 4-Aug-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 4-Aug-2021.) |
⊢ ℙ ∉ Fin | ||
Theorem | pwdif 40039* | The difference of two numbers to the same power is the difference of the two numbers multiplied with a finite sum. Generalization of subsq 12834. See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number, 5-Aug-2021. (Contributed by AV, 6-Aug-2021.) (Revised by AV, 19-Aug-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) − (𝐵↑𝑁)) = ((𝐴 − 𝐵) · Σ𝑘 ∈ (0..^𝑁)((𝐴↑𝑘) · (𝐵↑((𝑁 − 𝑘) − 1))))) | ||
Theorem | pwm1geoserALT 40040* | The n-th power of a number decreased by 1 expressed by the finite geometric series 1 + 𝐴↑1 + 𝐴↑2 +... + 𝐴↑(𝑁 − 1). This alternate proof of pwm1geoser 14439 is not based on geoser 14438, but on pwdif 40039 and therefore shorter than the original proof. (Contributed by AV, 19-Aug-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘))) | ||
Theorem | 2pwp1prm 40041* | For every prime number of the form ((2↑𝑘) + 1) 𝑘 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 40042* | 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 24752. 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 40056. This is an example of sgprmdvdsmersenne 40059, 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. Hence, 11 is a Sophie Germain prime and 2x11+1=23 is its associated safe prime. By sfprmdvdsmersenne 40058, 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 40066. | ||
Theorem | m2prm 40043 | The second Mersenne number M2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021.) |
⊢ ((2↑2) − 1) ∈ ℙ | ||
Theorem | m3prm 40044 | The third Mersenne number M3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021.) |
⊢ ((2↑3) − 1) ∈ ℙ | ||
Theorem | 2exp5 40045 | Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑5) = ;32 | ||
Theorem | flsqrt 40046 | A condition equivalent to the floor of a square root. (Contributed by AV, 17-Aug-2021.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℕ0) → ((⌊‘(√‘𝐴)) = 𝐵 ↔ ((𝐵↑2) ≤ 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2)))) | ||
Theorem | flsqrt5 40047 | 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 40048 | 3 does not divide 4. (Contributed by AV, 18-Aug-2021.) |
⊢ ¬ 3 ∥ 4 | ||
Theorem | 139prmALT 40049 | 139 is a prime number. In contrast to 139prm 15669, the proof of this theorem uses 3dvds2dec 14894 for checking the divisibility by 3. Although the proof using 3dvds2dec 14894 is longer (regarding size: 1849 characters compared with 1809 for 139prm 15669), the number of essential steps is smaller (301 compared with 327 for 139prm 15669). (Contributed by Mario Carneiro, 19-Feb-2014.) (Revised by AV, 18-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ;;139 ∈ ℙ | ||
Theorem | 31prm 40050 | 31 is a prime number. In contrast to 37prm 15666, the proof of this theorem is not based on the "blanket" prmlem2 15665, but on isprm7 15258. 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 15666 (1810 characters compared with 1213 for 37prm 15666). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 15666). (Contributed by AV, 17-Aug-2021.) (Proof modification is discouraged.) |
⊢ ;31 ∈ ℙ | ||
Theorem | m5prm 40051 | The fifth Mersenne number M5 = 31 is a prime number. (Contributed by AV, 17-Aug-2021.) |
⊢ ((2↑5) − 1) ∈ ℙ | ||
Theorem | 2exp7 40052 | Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑7) = ;;128 | ||
Theorem | 127prm 40053 | 127 is a prime number. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 16-Sep-2021.) |
⊢ ;;127 ∈ ℙ | ||
Theorem | m7prm 40054 | The seventh Mersenne number M7 = 127 is a prime number. (Contributed by AV, 18-Aug-2021.) |
⊢ ((2↑7) − 1) ∈ ℙ | ||
Theorem | 2exp11 40055 | Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑;11) = ;;;2048 | ||
Theorem | m11nprm 40056 | The eleventh Mersenne number M11 = 2047 is not a prime number. (Contributed by AV, 18-Aug-2021.) |
⊢ ((2↑;11) − 1) = (;89 · ;23) | ||
Theorem | mod42tp1mod8 40057 | 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 40058 | 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 40059 | 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 40060 | Lemma 1 for lighneal 40066. (Contributed by AV, 11-Aug-2021.) |
⊢ ((𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) − 1) ≠ (𝑃↑𝑀)) | ||
Theorem | lighneallem2 40061 | Lemma 2 for lighneal 40066. (Contributed by AV, 13-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneallem3 40062 | Lemma 3 for lighneal 40066. (Contributed by AV, 11-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneallem4a 40063 | Lemma 1 for lighneallem4 40065. (Contributed by AV, 16-Aug-2021.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘3) ∧ 𝑆 = (((𝐴↑𝑀) + 1) / (𝐴 + 1))) → 2 ≤ 𝑆) | ||
Theorem | lighneallem4b 40064* | Lemma 2 for lighneallem4 40065. (Contributed by AV, 16-Aug-2021.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘2) ∧ ¬ 2 ∥ 𝑀) → Σ𝑘 ∈ (0...(𝑀 − 1))((-1↑𝑘) · (𝐴↑𝑘)) ∈ (ℤ≥‘2)) | ||
Theorem | lighneallem4 40065 | Lemma 3 for lighneal 40066. (Contributed by AV, 16-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ ¬ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneal 40066 | 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 24752 (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 40067 | 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 40068 | Lemma for proththd 40069. (Contributed by AV, 4-Jul-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1)) ⇒ ⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ)) | ||
Theorem | proththd 40069* | 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 15448), 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 40070 | 5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020.) |
⊢ (5 · (2↑3)) = ;40 | ||
Theorem | 3exp4mod41 40071 | 3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020.) |
⊢ ((3↑4) mod ;41) = (-1 mod ;41) | ||
Theorem | 41prothprmlem1 40072 | Lemma 1 for 41prothprm 40074. (Contributed by AV, 4-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ ((𝑃 − 1) / 2) = ;20 | ||
Theorem | 41prothprmlem2 40073 | Lemma 2 for 41prothprm 40074. (Contributed by AV, 5-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ ((3↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) | ||
Theorem | 41prothprm 40074 | 41 is a Proth prime. (Contributed by AV, 5-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ (𝑃 = ((5 · (2↑3)) + 1) ∧ 𝑃 ∈ ℙ) | ||
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 40077 and df-odd 40078. Alternate definitions resp. charaterizations are provided in dfeven2 40100, dfeven3 40108, dfeven4 40089 and in dfodd2 40087, dfodd3 40101, dfodd4 40109, dfodd5 40110, dfodd6 40088. Each characterization can be useful (and used) in an appropriate context, e.g. dfodd6 40088 in opoeALTV 40132 and dfodd3 40101 in oddprmALTV 40136. 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 40131 and divgcdodd 15260). | ||
Syntax | ceven 40075 | Extend the definition of a class to include the set of even numbers. |
class Even | ||
Syntax | codd 40076 | Extend the definition of a class to include the set of odd numbers. |
class Odd | ||
Definition | df-even 40077 | Define the set of even numbers. (Contributed by AV, 14-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ} | ||
Definition | df-odd 40078 | Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ} | ||
Theorem | iseven 40079 | 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 40080 | 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 40081 | An even number is an integer. (Contributed by AV, 14-Jun-2020.) |
⊢ (𝑍 ∈ Even → 𝑍 ∈ ℤ) | ||
Theorem | oddz 40082 | An odd number is an integer. (Contributed by AV, 14-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ) | ||
Theorem | evendiv2z 40083 | The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 / 2) ∈ ℤ) | ||
Theorem | oddp1div2z 40084 | The result of dividing an odd number increased by 1 and then divided by 2 is an integer. (Contributed by AV, 15-Jun-2020.) |
⊢ (𝑍 ∈ Odd → ((𝑍 + 1) / 2) ∈ ℤ) | ||
Theorem | oddm1div2z 40085 | The result of dividing an odd number decreased by 1 and then divided by 2 is an integer. (Contributed by AV, 15-Jun-2020.) |
⊢ (𝑍 ∈ Odd → ((𝑍 − 1) / 2) ∈ ℤ) | ||
Theorem | isodd2 40086 | 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 number decreased by 1 and then divided by 2 is still an integer. (Contributed by AV, 15-Jun-2020.) |
⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ((𝑍 − 1) / 2) ∈ ℤ)) | ||
Theorem | dfodd2 40087 | Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 − 1) / 2) ∈ ℤ} | ||
Theorem | dfodd6 40088* | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = ((2 · 𝑖) + 1)} | ||
Theorem | dfeven4 40089* | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = (2 · 𝑖)} | ||
Theorem | evenm1odd 40090 | The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 − 1) ∈ Odd ) | ||
Theorem | evenp1odd 40091 | The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 + 1) ∈ Odd ) | ||
Theorem | oddp1eveni 40092 | The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Odd → (𝑍 + 1) ∈ Even ) | ||
Theorem | oddm1eveni 40093 | The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.) |
⊢ (𝑍 ∈ Odd → (𝑍 − 1) ∈ Even ) | ||
Theorem | evennodd 40094 | An even number is not an odd number. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → ¬ 𝑍 ∈ Odd ) | ||
Theorem | oddneven 40095 | An odd number is not an even number. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Odd → ¬ 𝑍 ∈ Even ) | ||
Theorem | enege 40096 | The negative of an even number is even. (Contributed by AV, 20-Jun-2020.) |
⊢ (𝐴 ∈ Even → -𝐴 ∈ Even ) | ||
Theorem | onego 40097 | The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.) |
⊢ (𝐴 ∈ Odd → -𝐴 ∈ Odd ) | ||
Theorem | m1expevenALTV 40098 | Exponentiation of -1 by an even power. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 6-Jul-2020.) |
⊢ (𝑁 ∈ Even → (-1↑𝑁) = 1) | ||
Theorem | m1expoddALTV 40099 | Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020.) |
⊢ (𝑁 ∈ Odd → (-1↑𝑁) = -1) | ||
Theorem | dfeven2 40100 | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ 2 ∥ 𝑧} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |