![]() |
Metamath
Proof Explorer Theorem List (p. 426 of 437) | < 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-28351) |
![]() (28352-29876) |
![]() (29877-43667) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fmtno0prm 42501 | The 0 th Fermat number is a prime (first Fermat prime). (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘0) ∈ ℙ | ||
Theorem | fmtno1prm 42502 | The 1 st Fermat number is a prime (second Fermat prime). (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘1) ∈ ℙ | ||
Theorem | fmtno2prm 42503 | The 2 nd Fermat number is a prime (third Fermat prime). (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘2) ∈ ℙ | ||
Theorem | 257prm 42504 | 257 is a prime number (the fourth Fermat prime). (Contributed by AV, 15-Jun-2021.) |
⊢ ;;257 ∈ ℙ | ||
Theorem | fmtno3prm 42505 | The 3 rd Fermat number is a prime (fourth Fermat prime). (Contributed by AV, 15-Jun-2021.) |
⊢ (FermatNo‘3) ∈ ℙ | ||
Theorem | odz2prm2pw 42506 | 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 42507 | Lemma for fmtnoprmfac1 42508: 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 42508* | Divisor of Fermat number (special form of Euler's result, see fmtnofac1 42513): 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 42509 | Lemma for fmtnoprmfac2 42510. (Contributed by AV, 26-Jul-2021.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1) | ||
Theorem | fmtnoprmfac2 42510* | Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 42512): 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 42511* | Lemma for fmtnofac2 42512 (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 42512* | Divisor of Fermat number (Euler's Result refined by François Édouard Anatole Lucas), see fmtnofac1 42513: 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 42513* |
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 42512. (Contributed by AV, 30-Jul-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 1))) + 1)) | ||
Theorem | fmtno4sqrt 42514 | The floor of the square root of the fourth Fermat number is 256. (Contributed by AV, 28-Jul-2021.) |
⊢ (⌊‘(√‘(FermatNo‘4))) = ;;256 | ||
Theorem | fmtno4prmfac 42515 | 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 42516 | 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 42517 | 193 is not a (prime) factor of the fourth Fermat number. (Contributed by AV, 24-Jul-2021.) |
⊢ ¬ ;;193 ∥ (FermatNo‘4) | ||
Theorem | fmtno4prm 42518 | The 4-th Fermat number (65537) is a prime (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.) |
⊢ (FermatNo‘4) ∈ ℙ | ||
Theorem | 65537prm 42519 | 65537 is a prime number (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.) |
⊢ ;;;;65537 ∈ ℙ | ||
Theorem | fmtnofz04prm 42520 | The first five Fermat numbers are prime, see remark in [ApostolNT] p. 7. (Contributed by AV, 28-Jul-2021.) |
⊢ (𝑁 ∈ (0...4) → (FermatNo‘𝑁) ∈ ℙ) | ||
Theorem | fmtnole4prm 42521 | The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4) → (FermatNo‘𝑁) ∈ ℙ) | ||
Theorem | fmtno5faclem1 42522 | Lemma 1 for fmtno5fac 42525. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;6700417 · 4) = ;;;;;;;26801668 | ||
Theorem | fmtno5faclem2 42523 | Lemma 2 for fmtno5fac 42525. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;6700417 · 6) = ;;;;;;;40202502 | ||
Theorem | fmtno5faclem3 42524 | Lemma 3 for fmtno5fac 42525. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688 | ||
Theorem | fmtno5fac 42525 | 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 42526 | The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021.) |
⊢ (FermatNo‘5) ∉ ℙ | ||
Theorem | prmdvdsfmtnof1lem1 42527* | Lemma 1 for prmdvdsfmtnof1 42530. (Contributed by AV, 3-Aug-2021.) |
⊢ 𝐼 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹}, ℝ, < ) & ⊢ 𝐽 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺}, ℝ, < ) ⇒ ⊢ ((𝐹 ∈ (ℤ≥‘2) ∧ 𝐺 ∈ (ℤ≥‘2)) → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺))) | ||
Theorem | prmdvdsfmtnof1lem2 42528 | Lemma 2 for prmdvdsfmtnof1 42530. (Contributed by AV, 3-Aug-2021.) |
⊢ ((𝐹 ∈ ran FermatNo ∧ 𝐺 ∈ ran FermatNo) → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)) | ||
Theorem | prmdvdsfmtnof 42529* | 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 42530* | 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 42531 | The set of prime numbers is infinite. The proof of this variant of prminf 16027 is based on Goldbach's theorem goldbachth 42490 (via prmdvdsfmtnof1 42530 and prmdvdsfmtnof1lem2 42528), 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 42532* | The difference of two numbers to the same power is the difference of the two numbers multiplied with a finite sum. Generalization of subsq 13295. 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 42533* | 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 15008 is not based on geoser 15007, but on pwdif 42532 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 42534* | 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 42535* | 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 25408. 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 42549. This is an example of sgprmdvdsmersenne 42552, 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 42551, 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 42559. | ||
Theorem | m2prm 42536 | The second Mersenne number M2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021.) |
⊢ ((2↑2) − 1) ∈ ℙ | ||
Theorem | m3prm 42537 | The third Mersenne number M3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021.) |
⊢ ((2↑3) − 1) ∈ ℙ | ||
Theorem | 2exp5 42538 | Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑5) = ;32 | ||
Theorem | flsqrt 42539 | A condition equivalent to the floor of a square root. (Contributed by AV, 17-Aug-2021.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℕ0) → ((⌊‘(√‘𝐴)) = 𝐵 ↔ ((𝐵↑2) ≤ 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2)))) | ||
Theorem | flsqrt5 42540 | 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 42541 | 3 does not divide 4. (Contributed by AV, 18-Aug-2021.) |
⊢ ¬ 3 ∥ 4 | ||
Theorem | 139prmALT 42542 | 139 is a prime number. In contrast to 139prm 16233, the proof of this theorem uses 3dvds2dec 15465 for checking the divisibility by 3. Although the proof using 3dvds2dec 15465 is longer (regarding size: 1849 characters compared with 1809 for 139prm 16233), the number of essential steps is smaller (301 compared with 327 for 139prm 16233). (Contributed by Mario Carneiro, 19-Feb-2014.) (Revised by AV, 18-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ;;139 ∈ ℙ | ||
Theorem | 31prm 42543 | 31 is a prime number. In contrast to 37prm 16230, the proof of this theorem is not based on the "blanket" prmlem2 16229, but on isprm7 15828. 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 16230 (1810 characters compared with 1213 for 37prm 16230). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 16230). (Contributed by AV, 17-Aug-2021.) (Proof modification is discouraged.) |
⊢ ;31 ∈ ℙ | ||
Theorem | m5prm 42544 | The fifth Mersenne number M5 = 31 is a prime number. (Contributed by AV, 17-Aug-2021.) |
⊢ ((2↑5) − 1) ∈ ℙ | ||
Theorem | 2exp7 42545 | Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑7) = ;;128 | ||
Theorem | 127prm 42546 | 127 is a prime number. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 16-Sep-2021.) |
⊢ ;;127 ∈ ℙ | ||
Theorem | m7prm 42547 | The seventh Mersenne number M7 = 127 is a prime number. (Contributed by AV, 18-Aug-2021.) |
⊢ ((2↑7) − 1) ∈ ℙ | ||
Theorem | 2exp11 42548 | Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑;11) = ;;;2048 | ||
Theorem | m11nprm 42549 | The eleventh Mersenne number M11 = 2047 is not a prime number. (Contributed by AV, 18-Aug-2021.) |
⊢ ((2↑;11) − 1) = (;89 · ;23) | ||
Theorem | mod42tp1mod8 42550 | 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 42551 | 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 42552 | 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 42553 | Lemma 1 for lighneal 42559. (Contributed by AV, 11-Aug-2021.) |
⊢ ((𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) − 1) ≠ (𝑃↑𝑀)) | ||
Theorem | lighneallem2 42554 | Lemma 2 for lighneal 42559. (Contributed by AV, 13-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneallem3 42555 | Lemma 3 for lighneal 42559. (Contributed by AV, 11-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneallem4a 42556 | Lemma 1 for lighneallem4 42558. (Contributed by AV, 16-Aug-2021.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘3) ∧ 𝑆 = (((𝐴↑𝑀) + 1) / (𝐴 + 1))) → 2 ≤ 𝑆) | ||
Theorem | lighneallem4b 42557* | Lemma 2 for lighneallem4 42558. (Contributed by AV, 16-Aug-2021.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘2) ∧ ¬ 2 ∥ 𝑀) → Σ𝑘 ∈ (0...(𝑀 − 1))((-1↑𝑘) · (𝐴↑𝑘)) ∈ (ℤ≥‘2)) | ||
Theorem | lighneallem4 42558 | Lemma 3 for lighneal 42559. (Contributed by AV, 16-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ ¬ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneal 42559 | 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 25408 (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 42560 | 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 42561 | Lemma for proththd 42562. (Contributed by AV, 4-Jul-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1)) ⇒ ⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ)) | ||
Theorem | proththd 42562* | 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 16018), 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 42563 | 5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020.) |
⊢ (5 · (2↑3)) = ;40 | ||
Theorem | 3exp4mod41 42564 | 3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020.) |
⊢ ((3↑4) mod ;41) = (-1 mod ;41) | ||
Theorem | 41prothprmlem1 42565 | Lemma 1 for 41prothprm 42567. (Contributed by AV, 4-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ ((𝑃 − 1) / 2) = ;20 | ||
Theorem | 41prothprmlem2 42566 | Lemma 2 for 41prothprm 42567. (Contributed by AV, 5-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ ((3↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) | ||
Theorem | 41prothprm 42567 | 41 is a Proth prime. (Contributed by AV, 5-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ (𝑃 = ((5 · (2↑3)) + 1) ∧ 𝑃 ∈ ℙ) | ||
Theorem | quad1 42568* | 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 42569* | 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 42570* | 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 42571* | 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 42574 and df-odd 42575. Alternate definitions resp. charaterizations are provided in dfeven2 42597, dfeven3 42605, dfeven4 42586 and in dfodd2 42584, dfodd3 42598, dfodd4 42606, dfodd5 42607, dfodd6 42585. Each characterization can be useful (and used) in an appropriate context, e.g. dfodd6 42585 in opoeALTV 42629 and dfodd3 42598 in oddprmALTV 42633. 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 42628 and divgcdodd 15830). | ||
Syntax | ceven 42572 | Extend the definition of a class to include the set of even numbers. |
class Even | ||
Syntax | codd 42573 | Extend the definition of a class to include the set of odd numbers. |
class Odd | ||
Definition | df-even 42574 | Define the set of even numbers. (Contributed by AV, 14-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ} | ||
Definition | df-odd 42575 | Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ} | ||
Theorem | iseven 42576 | 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 42577 | 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 42578 | An even number is an integer. (Contributed by AV, 14-Jun-2020.) |
⊢ (𝑍 ∈ Even → 𝑍 ∈ ℤ) | ||
Theorem | oddz 42579 | An odd number is an integer. (Contributed by AV, 14-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ) | ||
Theorem | evendiv2z 42580 | The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 / 2) ∈ ℤ) | ||
Theorem | oddp1div2z 42581 | 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 42582 | 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 42583 | 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 42584 | Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 − 1) / 2) ∈ ℤ} | ||
Theorem | dfodd6 42585* | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = ((2 · 𝑖) + 1)} | ||
Theorem | dfeven4 42586* | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = (2 · 𝑖)} | ||
Theorem | evenm1odd 42587 | The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 − 1) ∈ Odd ) | ||
Theorem | evenp1odd 42588 | The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 + 1) ∈ Odd ) | ||
Theorem | oddp1eveni 42589 | The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Odd → (𝑍 + 1) ∈ Even ) | ||
Theorem | oddm1eveni 42590 | The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.) |
⊢ (𝑍 ∈ Odd → (𝑍 − 1) ∈ Even ) | ||
Theorem | evennodd 42591 | An even number is not an odd number. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → ¬ 𝑍 ∈ Odd ) | ||
Theorem | oddneven 42592 | An odd number is not an even number. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Odd → ¬ 𝑍 ∈ Even ) | ||
Theorem | enege 42593 | The negative of an even number is even. (Contributed by AV, 20-Jun-2020.) |
⊢ (𝐴 ∈ Even → -𝐴 ∈ Even ) | ||
Theorem | onego 42594 | The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.) |
⊢ (𝐴 ∈ Odd → -𝐴 ∈ Odd ) | ||
Theorem | m1expevenALTV 42595 | 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 42596 | Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020.) |
⊢ (𝑁 ∈ Odd → (-1↑𝑁) = -1) | ||
Theorem | dfeven2 42597 | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ 2 ∥ 𝑧} | ||
Theorem | dfodd3 42598 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} | ||
Theorem | iseven2 42599 | The predicate "is an even number". An even number is an integer which is divisible by 2. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ 2 ∥ 𝑍)) | ||
Theorem | isodd3 42600 | The predicate "is an odd number". An odd number is an integer which is not divisible by 2. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ¬ 2 ∥ 𝑍)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |