Home | Metamath
Proof Explorer Theorem List (p. 437 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fmtno3prm 43601 | The 3 rd Fermat number is a prime (fourth Fermat prime). (Contributed by AV, 15-Jun-2021.) |
⊢ (FermatNo‘3) ∈ ℙ | ||
Theorem | odz2prm2pw 43602 | 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 43603 | Lemma for fmtnoprmfac1 43604: 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 43604* | Divisor of Fermat number (special form of Euler's result, see fmtnofac1 43609): 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 43605 | Lemma for fmtnoprmfac2 43606. (Contributed by AV, 26-Jul-2021.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1) | ||
Theorem | fmtnoprmfac2 43606* | Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 43608): 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 43607* | Lemma for fmtnofac2 43608 (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 43608* | Divisor of Fermat number (Euler's Result refined by François Édouard Anatole Lucas), see fmtnofac1 43609: 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 43609* |
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 43608. (Contributed by AV, 30-Jul-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 1))) + 1)) | ||
Theorem | fmtno4sqrt 43610 | The floor of the square root of the fourth Fermat number is 256. (Contributed by AV, 28-Jul-2021.) |
⊢ (⌊‘(√‘(FermatNo‘4))) = ;;256 | ||
Theorem | fmtno4prmfac 43611 | 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 43612 | 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 43613 | 193 is not a (prime) factor of the fourth Fermat number. (Contributed by AV, 24-Jul-2021.) |
⊢ ¬ ;;193 ∥ (FermatNo‘4) | ||
Theorem | fmtno4prm 43614 | The 4-th Fermat number (65537) is a prime (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.) |
⊢ (FermatNo‘4) ∈ ℙ | ||
Theorem | 65537prm 43615 | 65537 is a prime number (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.) |
⊢ ;;;;65537 ∈ ℙ | ||
Theorem | fmtnofz04prm 43616 | The first five Fermat numbers are prime, see remark in [ApostolNT] p. 7. (Contributed by AV, 28-Jul-2021.) |
⊢ (𝑁 ∈ (0...4) → (FermatNo‘𝑁) ∈ ℙ) | ||
Theorem | fmtnole4prm 43617 | The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4) → (FermatNo‘𝑁) ∈ ℙ) | ||
Theorem | fmtno5faclem1 43618 | Lemma 1 for fmtno5fac 43621. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;6700417 · 4) = ;;;;;;;26801668 | ||
Theorem | fmtno5faclem2 43619 | Lemma 2 for fmtno5fac 43621. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;6700417 · 6) = ;;;;;;;40202502 | ||
Theorem | fmtno5faclem3 43620 | Lemma 3 for fmtno5fac 43621. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688 | ||
Theorem | fmtno5fac 43621 | 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 43622 | The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021.) |
⊢ (FermatNo‘5) ∉ ℙ | ||
Theorem | prmdvdsfmtnof1lem1 43623* | Lemma 1 for prmdvdsfmtnof1 43626. (Contributed by AV, 3-Aug-2021.) |
⊢ 𝐼 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹}, ℝ, < ) & ⊢ 𝐽 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺}, ℝ, < ) ⇒ ⊢ ((𝐹 ∈ (ℤ≥‘2) ∧ 𝐺 ∈ (ℤ≥‘2)) → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺))) | ||
Theorem | prmdvdsfmtnof1lem2 43624 | Lemma 2 for prmdvdsfmtnof1 43626. (Contributed by AV, 3-Aug-2021.) |
⊢ ((𝐹 ∈ ran FermatNo ∧ 𝐺 ∈ ran FermatNo) → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)) | ||
Theorem | prmdvdsfmtnof 43625* | 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 43626* | 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 43627 | The set of prime numbers is infinite. The proof of this variant of prminf 16239 is based on Goldbach's theorem goldbachth 43586 (via prmdvdsfmtnof1 43626 and prmdvdsfmtnof1lem2 43624), see Wikipedia "Fermat number", 4-Aug-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties 43624. (Contributed by AV, 4-Aug-2021.) |
⊢ ℙ ∉ Fin | ||
Theorem | 2pwp1prm 43628* | 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 43629* | 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 25730. 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 43643. This is an example of sgprmdvdsmersenne 43646, 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 43646. Hence, 11 is a Sophie Germain prime and 2x11+1=23 is its associated safe prime. By sfprmdvdsmersenne 43645, 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 43653. | ||
Theorem | m2prm 43630 | The second Mersenne number M2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021.) |
⊢ ((2↑2) − 1) ∈ ℙ | ||
Theorem | m3prm 43631 | The third Mersenne number M3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021.) |
⊢ ((2↑3) − 1) ∈ ℙ | ||
Theorem | 2exp5 43632 | Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑5) = ;32 | ||
Theorem | flsqrt 43633 | A condition equivalent to the floor of a square root. (Contributed by AV, 17-Aug-2021.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℕ0) → ((⌊‘(√‘𝐴)) = 𝐵 ↔ ((𝐵↑2) ≤ 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2)))) | ||
Theorem | flsqrt5 43634 | 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 43635 | 3 does not divide 4. (Contributed by AV, 18-Aug-2021.) |
⊢ ¬ 3 ∥ 4 | ||
Theorem | 139prmALT 43636 | 139 is a prime number. In contrast to 139prm 16445, the proof of this theorem uses 3dvds2dec 15670 for checking the divisibility by 3. Although the proof using 3dvds2dec 15670 is longer (regarding size: 1849 characters compared with 1809 for 139prm 16445), the number of essential steps is smaller (301 compared with 327 for 139prm 16445). (Contributed by Mario Carneiro, 19-Feb-2014.) (Revised by AV, 18-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ;;139 ∈ ℙ | ||
Theorem | 31prm 43637 | 31 is a prime number. In contrast to 37prm 16442, the proof of this theorem is not based on the "blanket" prmlem2 16441, but on isprm7 16040. 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 16442 (1810 characters compared with 1213 for 37prm 16442). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 16442). (Contributed by AV, 17-Aug-2021.) (Proof modification is discouraged.) |
⊢ ;31 ∈ ℙ | ||
Theorem | m5prm 43638 | The fifth Mersenne number M5 = 31 is a prime number. (Contributed by AV, 17-Aug-2021.) |
⊢ ((2↑5) − 1) ∈ ℙ | ||
Theorem | 2exp7 43639 | Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑7) = ;;128 | ||
Theorem | 127prm 43640 | 127 is a prime number. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 16-Sep-2021.) |
⊢ ;;127 ∈ ℙ | ||
Theorem | m7prm 43641 | The seventh Mersenne number M7 = 127 is a prime number. (Contributed by AV, 18-Aug-2021.) |
⊢ ((2↑7) − 1) ∈ ℙ | ||
Theorem | 2exp11 43642 | Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑;11) = ;;;2048 | ||
Theorem | m11nprm 43643 | The eleventh Mersenne number M11 = 2047 is not a prime number. (Contributed by AV, 18-Aug-2021.) |
⊢ ((2↑;11) − 1) = (;89 · ;23) | ||
Theorem | mod42tp1mod8 43644 | 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 43645 | 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 43646 | 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 43647 | Lemma 1 for lighneal 43653. (Contributed by AV, 11-Aug-2021.) |
⊢ ((𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) − 1) ≠ (𝑃↑𝑀)) | ||
Theorem | lighneallem2 43648 | Lemma 2 for lighneal 43653. (Contributed by AV, 13-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneallem3 43649 | Lemma 3 for lighneal 43653. (Contributed by AV, 11-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneallem4a 43650 | Lemma 1 for lighneallem4 43652. (Contributed by AV, 16-Aug-2021.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘3) ∧ 𝑆 = (((𝐴↑𝑀) + 1) / (𝐴 + 1))) → 2 ≤ 𝑆) | ||
Theorem | lighneallem4b 43651* | Lemma 2 for lighneallem4 43652. (Contributed by AV, 16-Aug-2021.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘2) ∧ ¬ 2 ∥ 𝑀) → Σ𝑘 ∈ (0...(𝑀 − 1))((-1↑𝑘) · (𝐴↑𝑘)) ∈ (ℤ≥‘2)) | ||
Theorem | lighneallem4 43652 | Lemma 3 for lighneal 43653. (Contributed by AV, 16-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ ¬ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneal 43653 | 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 25730 (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 43654 | 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 43655 | Lemma for proththd 43656. (Contributed by AV, 4-Jul-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1)) ⇒ ⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ)) | ||
Theorem | proththd 43656* | 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 16230), 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 43657 | 5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020.) |
⊢ (5 · (2↑3)) = ;40 | ||
Theorem | 3exp4mod41 43658 | 3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020.) |
⊢ ((3↑4) mod ;41) = (-1 mod ;41) | ||
Theorem | 41prothprmlem1 43659 | Lemma 1 for 41prothprm 43661. (Contributed by AV, 4-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ ((𝑃 − 1) / 2) = ;20 | ||
Theorem | 41prothprmlem2 43660 | Lemma 2 for 41prothprm 43661. (Contributed by AV, 5-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ ((3↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) | ||
Theorem | 41prothprm 43661 | 41 is a Proth prime. (Contributed by AV, 5-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ (𝑃 = ((5 · (2↑3)) + 1) ∧ 𝑃 ∈ ℙ) | ||
Theorem | quad1 43662* | 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 43663* | 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 43664* | 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 43665* | 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 43668 and df-odd 43669. Alternate definitions resp. characterizations are provided in dfeven2 43691, dfeven3 43700, dfeven4 43680 and in dfodd2 43678, dfodd3 43692, dfodd4 43701, dfodd5 43702, dfodd6 43679. Each characterization can be useful (and used) in an appropriate context, e.g. dfodd6 43679 in opoeALTV 43725 and dfodd3 43692 in oddprmALTV 43729. 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 43724 and divgcdodd 16042). | ||
Syntax | ceven 43666 | Extend the definition of a class to include the set of even numbers. |
class Even | ||
Syntax | codd 43667 | Extend the definition of a class to include the set of odd numbers. |
class Odd | ||
Definition | df-even 43668 | Define the set of even numbers. (Contributed by AV, 14-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ} | ||
Definition | df-odd 43669 | Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ} | ||
Theorem | iseven 43670 | 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 43671 | 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 43672 | An even number is an integer. (Contributed by AV, 14-Jun-2020.) |
⊢ (𝑍 ∈ Even → 𝑍 ∈ ℤ) | ||
Theorem | oddz 43673 | An odd number is an integer. (Contributed by AV, 14-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ) | ||
Theorem | evendiv2z 43674 | The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 / 2) ∈ ℤ) | ||
Theorem | oddp1div2z 43675 | 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 43676 | 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 43677 | 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 43678 | Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 − 1) / 2) ∈ ℤ} | ||
Theorem | dfodd6 43679* | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = ((2 · 𝑖) + 1)} | ||
Theorem | dfeven4 43680* | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = (2 · 𝑖)} | ||
Theorem | evenm1odd 43681 | The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 − 1) ∈ Odd ) | ||
Theorem | evenp1odd 43682 | The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 + 1) ∈ Odd ) | ||
Theorem | oddp1eveni 43683 | The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Odd → (𝑍 + 1) ∈ Even ) | ||
Theorem | oddm1eveni 43684 | The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.) |
⊢ (𝑍 ∈ Odd → (𝑍 − 1) ∈ Even ) | ||
Theorem | evennodd 43685 | An even number is not an odd number. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → ¬ 𝑍 ∈ Odd ) | ||
Theorem | oddneven 43686 | An odd number is not an even number. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Odd → ¬ 𝑍 ∈ Even ) | ||
Theorem | enege 43687 | The negative of an even number is even. (Contributed by AV, 20-Jun-2020.) |
⊢ (𝐴 ∈ Even → -𝐴 ∈ Even ) | ||
Theorem | onego 43688 | The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.) |
⊢ (𝐴 ∈ Odd → -𝐴 ∈ Odd ) | ||
Theorem | m1expevenALTV 43689 | 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 43690 | Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020.) |
⊢ (𝑁 ∈ Odd → (-1↑𝑁) = -1) | ||
Theorem | dfeven2 43691 | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ 2 ∥ 𝑧} | ||
Theorem | dfodd3 43692 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} | ||
Theorem | iseven2 43693 | 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 43694 | 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 ∥ 𝑍)) | ||
Theorem | 2dvdseven 43695 | 2 divides an even number. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Even → 2 ∥ 𝑍) | ||
Theorem | m2even 43696 | A multiple of 2 is an even number. (Contributed by AV, 5-Jun-2023.) |
⊢ (𝑍 ∈ ℤ → (2 · 𝑍) ∈ Even ) | ||
Theorem | 2ndvdsodd 43697 | 2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd → ¬ 2 ∥ 𝑍) | ||
Theorem | 2dvdsoddp1 43698 | 2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 + 1)) | ||
Theorem | 2dvdsoddm1 43699 | 2 divides an odd number decreased by 1. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 − 1)) | ||
Theorem | dfeven3 43700 | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 0} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |