P. 484 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48301-48400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fmtno4prmfac 48301	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 48302	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 48303	193 is not a (prime) factor of the fourth Fermat number. (Contributed by AV, 24-Jul-2021.)
⊢ ¬ ;;193 ∥ (FermatNo‘4)
Theorem	fmtno4prm 48304	The 4-th Fermat number (65537) is a prime (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.)
⊢ (FermatNo‘4) ∈ ℙ
Theorem	65537prm 48305	65537 is a prime number (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.)
⊢ ;;;;65537 ∈ ℙ
Theorem	fmtnofz04prm 48306	The first five Fermat numbers are prime, see remark in [ApostolNT] p. 7. (Contributed by AV, 28-Jul-2021.)
⊢ (𝑁 ∈ (0...4) → (FermatNo‘𝑁) ∈ ℙ)
Theorem	fmtnole4prm 48307	The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4) → (FermatNo‘𝑁) ∈ ℙ)
Theorem	fmtno5faclem1 48308	Lemma 1 for fmtno5fac 48311. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;;;6700417 · 4) = ;;;;;;;26801668
Theorem	fmtno5faclem2 48309	Lemma 2 for fmtno5fac 48311. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;;;6700417 · 6) = ;;;;;;;40202502
Theorem	fmtno5faclem3 48310	Lemma 3 for fmtno5fac 48311. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688
Theorem	fmtno5fac 48311	The factorization of the 5 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 22-Jul-2021.)
⊢ (FermatNo‘5) = (;;;;;;6700417 · ;;641)
Theorem	fmtno5nprm 48312	The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021.)
⊢ (FermatNo‘5) ∉ ℙ
Theorem	prmdvdsfmtnof1lem1 48313*	Lemma 1 for prmdvdsfmtnof1 48316. (Contributed by AV, 3-Aug-2021.)
⊢ 𝐼 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹}, ℝ, < )    &   ⊢ 𝐽 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺}, ℝ, < )    ⇒   ⊢ ((𝐹 ∈ (ℤ≥‘2) ∧ 𝐺 ∈ (ℤ≥‘2)) → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺)))
Theorem	prmdvdsfmtnof1lem2 48314	Lemma 2 for prmdvdsfmtnof1 48316. (Contributed by AV, 3-Aug-2021.)
⊢ ((𝐹 ∈ ran FermatNo ∧ 𝐺 ∈ ran FermatNo) → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺))
Theorem	prmdvdsfmtnof 48315*	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 48316*	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 48317	The set of prime numbers is infinite. The proof of this variant of prminf 16976 is based on Goldbach's theorem goldbachth 48276 (via prmdvdsfmtnof1 48316 and prmdvdsfmtnof1lem2 48314), see Wikipedia "Fermat number", 4-Aug-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties 48314. (Contributed by AV, 4-Aug-2021.)
⊢ ℙ ∉ Fin
Theorem	2pwp1prm 48318*	For ((2↑𝑘) + 1) to be prime, 𝑘 must be a power of 2, see Wikipedia "Fermat number", section "Other theorems 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 48319*	Every prime number of the form ((2↑𝑘) + 1) must be a Fermat number. (Contributed by AV, 7-Aug-2021.)
⊢ ((𝐾 ∈ ℕ ∧ 𝑃 = ((2↑𝐾) + 1) ∧ 𝑃 ∈ ℙ) → ∃𝑛 ∈ ℕ0 𝑃 = (FermatNo‘𝑛))
21.49.12.3  Mersenne primes "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 27369. 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 48330. This is an example of sgprmdvdsmersenne 48333, 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 48333. Hence, 11 is a Sophie Germain prime and 2x11+1=23 is its associated safe prime. By sfprmdvdsmersenne 48332, 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 48340.
Theorem	m2prm 48320	The second Mersenne number M2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021.)
⊢ ((2↑2) − 1) ∈ ℙ
Theorem	m3prm 48321	The third Mersenne number M3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021.)
⊢ ((2↑3) − 1) ∈ ℙ
Theorem	flsqrt 48322	A condition equivalent to the floor of a square root. (Contributed by AV, 17-Aug-2021.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℕ0) → ((⌊‘(√‘𝐴)) = 𝐵 ↔ ((𝐵↑2) ≤ 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2))))
Theorem	flsqrt5 48323	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 48324	3 does not divide 4. (Contributed by AV, 18-Aug-2021.)
⊢ ¬ 3 ∥ 4
Theorem	139prmALT 48325	139 is a prime number. In contrast to 139prm 17185, the proof of this theorem uses 3dvds2dec 16392 for checking the divisibility by 3. Although the proof using 3dvds2dec 16392 is longer (regarding size: 1849 characters compared with 1809 for 139prm 17185), the number of essential steps is smaller (301 compared with 327 for 139prm 17185). (Contributed by Mario Carneiro, 19-Feb-2014.) (Revised by AV, 18-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ;;139 ∈ ℙ
Theorem	31prm 48326	31 is a prime number. In contrast to 37prm 17182, the proof of this theorem is not based on the "blanket" prmlem2 17181, but on isprm7 16768. 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 17182 (1810 characters compared with 1213 for 37prm 17182). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 17182). (Contributed by AV, 17-Aug-2021.) (Proof modification is discouraged.)
⊢ ;31 ∈ ℙ
Theorem	m5prm 48327	The fifth Mersenne number M5 = 31 is a prime number. (Contributed by AV, 17-Aug-2021.)
⊢ ((2↑5) − 1) ∈ ℙ
Theorem	127prm 48328	127 is a prime number. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 16-Sep-2021.)
⊢ ;;127 ∈ ℙ
Theorem	m7prm 48329	The seventh Mersenne number M7 = 127 is a prime number. (Contributed by AV, 18-Aug-2021.)
⊢ ((2↑7) − 1) ∈ ℙ
Theorem	m11nprm 48330	The eleventh Mersenne number M11 = 2047 is not a prime number. (Contributed by AV, 18-Aug-2021.)
⊢ ((2↑;11) − 1) = (;89 · ;23)
Theorem	mod42tp1mod8 48331	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 48332	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 48333	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 48334	Lemma 1 for lighneal 48340. (Contributed by AV, 11-Aug-2021.)
⊢ ((𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) − 1) ≠ (𝑃↑𝑀))
Theorem	lighneallem2 48335	Lemma 2 for lighneal 48340. (Contributed by AV, 13-Aug-2021.)
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)
Theorem	lighneallem3 48336	Lemma 3 for lighneal 48340. (Contributed by AV, 11-Aug-2021.)
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)
Theorem	lighneallem4a 48337	Lemma 1 for lighneallem4 48339. (Contributed by AV, 16-Aug-2021.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘3) ∧ 𝑆 = (((𝐴↑𝑀) + 1) / (𝐴 + 1))) → 2 ≤ 𝑆)
Theorem	lighneallem4b 48338*	Lemma 2 for lighneallem4 48339. (Contributed by AV, 16-Aug-2021.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘2) ∧ ¬ 2 ∥ 𝑀) → Σ𝑘 ∈ (0...(𝑀 − 1))((-1↑𝑘) · (𝐴↑𝑘)) ∈ (ℤ≥‘2))
Theorem	lighneallem4 48339	Lemma 3 for lighneal 48340. (Contributed by AV, 16-Aug-2021.)
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ ¬ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)
Theorem	lighneal 48340	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 27369 (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 ∧ 𝑁 ∈ ℙ))
21.49.12.4  Proth's theorem
Theorem	modexp2m1d 48341	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 48342	Lemma for proththd 48343. (Contributed by AV, 4-Jul-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1))    ⇒   ⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ))
Theorem	proththd 48343*	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 16967), 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 48344	5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020.)
⊢ (5 · (2↑3)) = ;40
Theorem	3exp4mod41 48345	3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020.)
⊢ ((3↑4) mod ;41) = (-1 mod ;41)
Theorem	41prothprmlem1 48346	Lemma 1 for 41prothprm 48348. (Contributed by AV, 4-Jul-2020.)
⊢ 𝑃 = ;41    ⇒   ⊢ ((𝑃 − 1) / 2) = ;20
Theorem	41prothprmlem2 48347	Lemma 2 for 41prothprm 48348. (Contributed by AV, 5-Jul-2020.)
⊢ 𝑃 = ;41    ⇒   ⊢ ((3↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)
Theorem	41prothprm 48348	41 is a Proth prime. (Contributed by AV, 5-Jul-2020.)
⊢ 𝑃 = ;41    ⇒   ⊢ (𝑃 = ((5 · (2↑3)) + 1) ∧ 𝑃 ∈ ℙ)
21.49.12.5  The prime-counting function according to Ján Mináč
Theorem	nprmdvdsfacm1lem1 48349	Lemma 1 for nprmdvdsfacm1 48353. (Contributed by AV, 7-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘6) ∧ 𝐴 ∈ (2..^𝑁) ∧ 𝑁 = (𝐴↑2)) → 𝑁 ∥ (𝐴 · (2 · 𝐴)))
Theorem	nprmdvdsfacm1lem2 48350	Lemma 2 for nprmdvdsfacm1 48353. (Contributed by AV, 7-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘6) ∧ 𝐴 ∈ (2..^𝑁) ∧ 𝑁 = (𝐴↑2)) → 3 ≤ 𝐴)
Theorem	nprmdvdsfacm1lem3 48351	Lemma 3 for nprmdvdsfacm1 48353. (Contributed by AV, 7-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘6) ∧ 𝐴 ∈ (2..^𝑁) ∧ 𝑁 = (𝐴↑2)) → (2 · 𝐴) < (𝑁 − 1))
Theorem	nprmdvdsfacm1lem4 48352	Lemma 4 for nprmdvdsfacm1 48353. (Contributed by AV, 7-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘6) ∧ 𝐴 ∈ (2..^𝑁) ∧ 𝑁 = (𝐴↑2)) → 𝑁 ∥ (!‘(𝑁 − 1)))
Theorem	nprmdvdsfacm1 48353	A non-prime integer greater than 5 divides the factorial of the integer decreased by 1 (see remark in [Ribenboim] p. 181). Note: not valid for 𝑁 = 4, but for 𝑁 = 1! (Contributed by AV, 7-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘6) ∧ 𝑁 ∉ ℙ) → 𝑁 ∥ (!‘(𝑁 − 1)))
Theorem	ppivalnnprm 48354	Value of a term of the prime-counting function pi for positive integers, according to Ján Mináč, for a prime number. (Contributed by AV, 10-Apr-2026.)
⊢ (𝑃 ∈ ℙ → (⌊‘((((!‘(𝑃 − 1)) + 1) / 𝑃) − (⌊‘((!‘(𝑃 − 1)) / 𝑃)))) = 1)
Theorem	ppivalnnnprmge6 48355	Value of a term of the prime-counting function pi for positive integers, according to Ján Mináč, for a non-prime number greater than 4. (Contributed by AV, 4-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘6) ∧ 𝑁 ∉ ℙ) → (⌊‘((((!‘(𝑁 − 1)) + 1) / 𝑁) − (⌊‘((!‘(𝑁 − 1)) / 𝑁)))) = 0)
Theorem	ppivalnn4 48356	Value of the term of the prime-counting function pi for positive integers, according to Ján Mináč, for 4. (Contributed by AV, 8-Apr-2026.)
⊢ (⌊‘((((!‘(4 − 1)) + 1) / 4) − (⌊‘((!‘(4 − 1)) / 4)))) = 0
Theorem	ppivalnnnprm 48357	Value of a term of the prime-counting function pi for positive integers, according to Ján Miná&ccaron, for a non-prime number greater than 1. (Contributed by AV, 8-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑁 ∉ ℙ) → (⌊‘((((!‘(𝑁 − 1)) + 1) / 𝑁) − (⌊‘((!‘(𝑁 − 1)) / 𝑁)))) = 0)
Theorem	indprm 48358	An indicator function for prime numbers, according to Ján Mináč. (Contributed by AV, 4-Apr-2026.)
⊢ ((𝟭‘(ℤ≥‘2))‘ℙ) = (𝑘 ∈ (ℤ≥‘2) ↦ (⌊‘((((!‘(𝑘 − 1)) + 1) / 𝑘) − (⌊‘((!‘(𝑘 − 1)) / 𝑘)))))
Theorem	indprmfz 48359*	An indicator function for prime numbers in a finite interval of integers, according to Ján Mináč. (Contributed by AV, 4-Apr-2026.)
⊢ 𝐼 = (2...𝐴)    ⇒   ⊢ ((𝟭‘𝐼)‘(𝐼 ∩ ℙ)) = (𝑘 ∈ 𝐼 ↦ (⌊‘((((!‘(𝑘 − 1)) + 1) / 𝑘) − (⌊‘((!‘(𝑘 − 1)) / 𝑘)))))
Theorem	ppi1sum 48360	Value of the prime-counting function pi for 1, according to Ján Mináč. (Contributed by AV, 4-Apr-2026.)
⊢ (π‘1) = Σ𝑘 ∈ ∅ (⌊‘((((!‘(𝑘 − 1)) + 1) / 𝑘) − (⌊‘((!‘(𝑘 − 1)) / 𝑘))))
Theorem	ppivalnn 48361*	Value of the prime-counting function pi for positive integers, according to Ján Mináč, see statement in [Ribenboim], p. 181. (Contributed by AV, 10-Apr-2026.)
⊢ (𝑁 ∈ ℕ → (π‘𝑁) = Σ𝑘 ∈ (2...𝑁)(⌊‘((((!‘(𝑘 − 1)) + 1) / 𝑘) − (⌊‘((!‘(𝑘 − 1)) / 𝑘)))))
21.49.12.6  Solutions of quadratic equations
Theorem	quad1 48362*	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 48363*	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 48364*	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 48365*	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 < 𝐷))
21.49.13  Even and odd numbers 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 48368 and df-odd 48369. Alternate definitions resp. characterizations are provided in dfeven2 48391, dfeven3 48400, dfeven4 48380 and in dfodd2 48378, dfodd3 48392, dfodd4 48401, dfodd5 48402, dfodd6 48379. Each characterization can be useful (and used) in an appropriate context, e.g. dfodd6 48379 in opoeALTV 48425 and dfodd3 48392 in oddprmALTV 48429. 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 48424 and divgcdodd 16770).
21.49.13.1  Definitions and basic properties
Syntax	ceven 48366	Extend the definition of a class to include the set of even numbers.
class Even
Syntax	codd 48367	Extend the definition of a class to include the set of odd numbers.
class Odd
Definition	df-even 48368	Define the set of even numbers. (Contributed by AV, 14-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ}
Definition	df-odd 48369	Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ}
Theorem	iseven 48370	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 48371	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 48372	An even number is an integer. (Contributed by AV, 14-Jun-2020.)
⊢ (𝑍 ∈ Even → 𝑍 ∈ ℤ)
Theorem	oddz 48373	An odd number is an integer. (Contributed by AV, 14-Jun-2020.)
⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ)
Theorem	evendiv2z 48374	The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 / 2) ∈ ℤ)
Theorem	oddp1div2z 48375	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 48376	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 48377	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 48378	Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 − 1) / 2) ∈ ℤ}
Theorem	dfodd6 48379*	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = ((2 · 𝑖) + 1)}
Theorem	dfeven4 48380*	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = (2 · 𝑖)}
Theorem	evenm1odd 48381	The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 − 1) ∈ Odd )
Theorem	evenp1odd 48382	The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 + 1) ∈ Odd )
Theorem	oddp1eveni 48383	The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Odd → (𝑍 + 1) ∈ Even )
Theorem	oddm1eveni 48384	The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.)
⊢ (𝑍 ∈ Odd → (𝑍 − 1) ∈ Even )
Theorem	evennodd 48385	An even number is not an odd number. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → ¬ 𝑍 ∈ Odd )
Theorem	oddneven 48386	An odd number is not an even number. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Odd → ¬ 𝑍 ∈ Even )
Theorem	enege 48387	The negative of an even number is even. (Contributed by AV, 20-Jun-2020.)
⊢ (𝐴 ∈ Even → -𝐴 ∈ Even )
Theorem	onego 48388	The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.)
⊢ (𝐴 ∈ Odd → -𝐴 ∈ Odd )
Theorem	m1expevenALTV 48389	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 48390	Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020.)
⊢ (𝑁 ∈ Odd → (-1↑𝑁) = -1)
21.49.13.2  Alternate definitions using the "divides" relation
Theorem	dfeven2 48391	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ 2 ∥ 𝑧}
Theorem	dfodd3 48392	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
Theorem	iseven2 48393	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 48394	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 48395	2 divides an even number. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Even → 2 ∥ 𝑍)
Theorem	m2even 48396	A multiple of 2 is an even number. (Contributed by AV, 5-Jun-2023.)
⊢ (𝑍 ∈ ℤ → (2 · 𝑍) ∈ Even )
Theorem	2ndvdsodd 48397	2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Odd → ¬ 2 ∥ 𝑍)
Theorem	2dvdsoddp1 48398	2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 + 1))
Theorem	2dvdsoddm1 48399	2 divides an odd number decreased by 1. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 − 1))
21.49.13.3  Alternate definitions using the "modulo" operation
Theorem	dfeven3 48400	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 0}