P. 124 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12301-12400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pcndvds2 12301	The remainder after dividing out all factors of 𝑃 is not divisible by 𝑃. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁))))
Theorem	pcdvdsb 12302	𝑃↑𝐴 divides 𝑁 if and only if 𝐴 is at most the count of 𝑃. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁))
Theorem	pcelnn 12303	There are a positive number of powers of a prime 𝑃 in 𝑁 iff 𝑃 divides 𝑁. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) ∈ ℕ ↔ 𝑃 ∥ 𝑁))
Theorem	pceq0 12304	There are zero powers of a prime 𝑃 in 𝑁 iff 𝑃 does not divide 𝑁. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) = 0 ↔ ¬ 𝑃 ∥ 𝑁))
Theorem	pcidlem 12305	The prime count of a prime power. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴)
Theorem	pcid 12306	The prime count of a prime power. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴)
Theorem	pcneg 12307	The prime count of a negative number. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴))
Theorem	pcabs 12308	The prime count of an absolute value. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt (abs‘𝐴)) = (𝑃 pCnt 𝐴))
Theorem	pcdvdstr 12309	The prime count increases under the divisibility relation. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵))
Theorem	pcgcd1 12310	The prime count of a GCD is the minimum of the prime counts of the arguments. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) → (𝑃 pCnt (𝐴 gcd 𝐵)) = (𝑃 pCnt 𝐴))
Theorem	pcgcd 12311	The prime count of a GCD is the minimum of the prime counts of the arguments. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑃 pCnt (𝐴 gcd 𝐵)) = if((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵), (𝑃 pCnt 𝐴), (𝑃 pCnt 𝐵)))
Theorem	pc2dvds 12312*	A characterization of divisibility in terms of prime count. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
Theorem	pc11 12313*	The prime count function, viewed as a function from ℕ to (ℕ ↑𝑚 ℙ), is one-to-one. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵)))
Theorem	pcz 12314*	The prime count function can be used as an indicator that a given rational number is an integer. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝐴 ∈ ℚ → (𝐴 ∈ ℤ ↔ ∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt 𝐴)))
Theorem	pcprmpw2 12315*	Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0 𝐴 ∥ (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴))))
Theorem	pcprmpw 12316*	Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴))))
Theorem	dvdsprmpweq 12317*	If a positive integer divides a prime power, it is a prime power. (Contributed by AV, 25-Jul-2021.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛)))
Theorem	dvdsprmpweqnn 12318*	If an integer greater than 1 divides a prime power, it is a (proper) prime power. (Contributed by AV, 13-Aug-2021.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ 𝐴 = (𝑃↑𝑛)))
Theorem	dvdsprmpweqle 12319*	If a positive integer divides a prime power, it is a prime power with a smaller exponent. (Contributed by AV, 25-Jul-2021.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛))))
Theorem	difsqpwdvds 12320	If the difference of two squares is a power of a prime, the prime divides twice the second squared number. (Contributed by AV, 13-Aug-2021.)
⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ (𝐵 + 1) < 𝐴) ∧ (𝐶 ∈ ℙ ∧ 𝐷 ∈ ℕ0)) → ((𝐶↑𝐷) = ((𝐴↑2) − (𝐵↑2)) → 𝐶 ∥ (2 · 𝐵)))
Theorem	pcaddlem 12321	Lemma for pcadd 12322. The original numbers 𝐴 and 𝐵 have been decomposed using the prime count function as (𝑃↑𝑀) · (𝑅 / 𝑆) where 𝑅, 𝑆 are both not divisible by 𝑃 and 𝑀 = (𝑃 pCnt 𝐴), and similarly for 𝐵. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 = ((𝑃↑𝑀) · (𝑅 / 𝑆)))    &   ⊢ (𝜑 → 𝐵 = ((𝑃↑𝑁) · (𝑇 / 𝑈)))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑅))    &   ⊢ (𝜑 → (𝑆 ∈ ℕ ∧ ¬ 𝑃 ∥ 𝑆))    &   ⊢ (𝜑 → (𝑇 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑇))    &   ⊢ (𝜑 → (𝑈 ∈ ℕ ∧ ¬ 𝑃 ∥ 𝑈))    ⇒   ⊢ (𝜑 → 𝑀 ≤ (𝑃 pCnt (𝐴 + 𝐵)))
Theorem	pcadd 12322	An inequality for the prime count of a sum. This is the source of the ultrametric inequality for the p-adic metric. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 ∈ ℚ)    &   ⊢ (𝜑 → 𝐵 ∈ ℚ)    &   ⊢ (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵))    ⇒   ⊢ (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵)))
Theorem	pcmptcl 12323	Closure for the prime power map. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
Theorem	pcmpt 12324*	Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0))
Theorem	pcmpt2 12325*	Dividing two prime count maps yields a number with all dividing primes confined to an interval. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑁))    ⇒   ⊢ (𝜑 → (𝑃 pCnt ((seq1( · , 𝐹)‘𝑀) / (seq1( · , 𝐹)‘𝑁))) = if((𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁), 𝐵, 0))
Theorem	pcmptdvds 12326	The partial products of the prime power map form a divisibility chain. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑁))    ⇒   ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑁) ∥ (seq1( · , 𝐹)‘𝑀))
Theorem	pcprod 12327*	The product of the primes taken to their respective powers reconstructs the original number. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ (𝑁 ∈ ℕ → (seq1( · , 𝐹)‘𝑁) = 𝑁)
Theorem	sumhashdc 12328*	The sum of 1 over a set is the size of the set. (Contributed by Mario Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro, 20-May-2014.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐵 DECID 𝑥 ∈ 𝐴) → Σ𝑘 ∈ 𝐵 if(𝑘 ∈ 𝐴, 1, 0) = (♯‘𝐴))
Theorem	fldivp1 12329	The difference between the floors of adjacent fractions is either 1 or 0. (Contributed by Mario Carneiro, 8-Mar-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0))
Theorem	pcfaclem 12330	Lemma for pcfac 12331. (Contributed by Mario Carneiro, 20-May-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) → (⌊‘(𝑁 / (𝑃↑𝑀))) = 0)
Theorem	pcfac 12331*	Calculate the prime count of a factorial. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘))))
Theorem	pcbc 12332*	Calculate the prime count of a binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁) ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (𝑁C𝐾)) = Σ𝑘 ∈ (1...𝑁)((⌊‘(𝑁 / (𝑃↑𝑘))) − ((⌊‘((𝑁 − 𝐾) / (𝑃↑𝑘))) + (⌊‘(𝐾 / (𝑃↑𝑘))))))
Theorem	qexpz 12333	If a power of a rational number is an integer, then the number is an integer. (Contributed by Mario Carneiro, 10-Aug-2015.)
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) → 𝐴 ∈ ℤ)
Theorem	expnprm 12334	A second or higher power of a rational number is not a prime number. Or by contraposition, the n-th root of a prime number is not rational. Suggested by Norm Megill. (Contributed by Mario Carneiro, 10-Aug-2015.)
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ (ℤ≥‘2)) → ¬ (𝐴↑𝑁) ∈ ℙ)
Theorem	oddprmdvds 12335*	Every positive integer which is not a power of two is divisible by an odd prime number. (Contributed by AV, 6-Aug-2021.)
⊢ ((𝐾 ∈ ℕ ∧ ¬ ∃𝑛 ∈ ℕ0 𝐾 = (2↑𝑛)) → ∃𝑝 ∈ (ℙ ∖ {2})𝑝 ∥ 𝐾)
5.2.9  Pocklington's theorem
Theorem	prmpwdvds 12336	A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.)
⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷)
Theorem	pockthlem 12337	Lemma for pockthg 12338. (Contributed by Mario Carneiro, 2-Mar-2014.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 < 𝐴)    &   ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑃 ∥ 𝑁)    &   ⊢ (𝜑 → 𝑄 ∈ ℙ)    &   ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1)    &   ⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1)    ⇒   ⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)))
Theorem	pockthg 12338*	The generalized Pocklington's theorem. If 𝑁 − 1 = 𝐴 · 𝐵 where 𝐵 < 𝐴, then 𝑁 is prime if and only if for every prime factor 𝑝 of 𝐴, there is an 𝑥 such that 𝑥↑(𝑁 − 1) = 1( mod 𝑁) and gcd (𝑥↑((𝑁 − 1) / 𝑝) − 1, 𝑁) = 1. (Contributed by Mario Carneiro, 2-Mar-2014.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 < 𝐴)    &   ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1))    &   ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1)))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℙ)
Theorem	pockthi 12339	Pocklington's theorem, which gives a sufficient criterion for a number 𝑁 to be prime. This is the preferred method for verifying large primes, being much more efficient to compute than trial division. This form has been optimized for application to specific large primes; see pockthg 12338 for a more general closed-form version. (Contributed by Mario Carneiro, 2-Mar-2014.)
⊢ 𝑃 ∈ ℙ    &   ⊢ 𝐺 ∈ ℕ    &   ⊢ 𝑀 = (𝐺 · 𝑃)    &   ⊢ 𝑁 = (𝑀 + 1)    &   ⊢ 𝐷 ∈ ℕ    &   ⊢ 𝐸 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝑀 = (𝐷 · (𝑃↑𝐸))    &   ⊢ 𝐷 < (𝑃↑𝐸)    &   ⊢ ((𝐴↑𝑀) mod 𝑁) = (1 mod 𝑁)    &   ⊢ (((𝐴↑𝐺) − 1) gcd 𝑁) = 1    ⇒   ⊢ 𝑁 ∈ ℙ
5.2.10  Infinite primes theorem
Theorem	infpnlem1 12340*	Lemma for infpn 12342. The smallest divisor (greater than 1) 𝑀 of 𝑁! + 1 is a prime greater than 𝑁. (Contributed by NM, 5-May-2005.)
⊢ 𝐾 = ((!‘𝑁) + 1)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (((1 < 𝑀 ∧ (𝐾 / 𝑀) ∈ ℕ) ∧ ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗)) → (𝑁 < 𝑀 ∧ ∀𝑗 ∈ ℕ ((𝑀 / 𝑗) ∈ ℕ → (𝑗 = 1 ∨ 𝑗 = 𝑀)))))
Theorem	infpnlem2 12341*	Lemma for infpn 12342. For any positive integer 𝑁, there exists a prime number 𝑗 greater than 𝑁. (Contributed by NM, 5-May-2005.)
⊢ 𝐾 = ((!‘𝑁) + 1)    ⇒   ⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗))))
Theorem	infpn 12342*	There exist infinitely many prime numbers: for any positive integer 𝑁, there exists a prime number 𝑗 greater than 𝑁. (See infpn2 12440 for the equinumerosity version.) (Contributed by NM, 1-Jun-2006.)
⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗))))
Theorem	prmunb 12343*	The primes are unbounded. (Contributed by Paul Chapman, 28-Nov-2012.)
⊢ (𝑁 ∈ ℕ → ∃𝑝 ∈ ℙ 𝑁 < 𝑝)
5.2.11  Fundamental theorem of arithmetic
Theorem	1arithlem1 12344*	Lemma for 1arith 12348. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑁)))
Theorem	1arithlem2 12345*	Lemma for 1arith 12348. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((𝑀‘𝑁)‘𝑃) = (𝑃 pCnt 𝑁))
Theorem	1arithlem3 12346*	Lemma for 1arith 12348. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁):ℙ⟶ℕ0)
Theorem	1arithlem4 12347*	Lemma for 1arith 12348. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    &   ⊢ 𝐺 = (𝑦 ∈ ℕ ↦ if(𝑦 ∈ ℙ, (𝑦↑(𝐹‘𝑦)), 1))    &   ⊢ (𝜑 → 𝐹:ℙ⟶ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑁 ≤ 𝑞)) → (𝐹‘𝑞) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℕ 𝐹 = (𝑀‘𝑥))
Theorem	1arith 12348*	Fundamental theorem of arithmetic, where a prime factorization is represented as a sequence of prime exponents, for which only finitely many primes have nonzero exponent. The function 𝑀 maps the set of positive integers one-to-one onto the set of prime factorizations 𝑅. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    &   ⊢ 𝑅 = {𝑒 ∈ (ℕ0 ↑𝑚 ℙ) ∣ (◡𝑒 “ ℕ) ∈ Fin}    ⇒   ⊢ 𝑀:ℕ–1-1-onto→𝑅
Theorem	1arith2 12349*	Fundamental theorem of arithmetic, where a prime factorization is represented as a finite monotonic 1-based sequence of primes. Every positive integer has a unique prime factorization. Theorem 1.10 in [ApostolNT] p. 17. This is Metamath 100 proof #80. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    &   ⊢ 𝑅 = {𝑒 ∈ (ℕ0 ↑𝑚 ℙ) ∣ (◡𝑒 “ ℕ) ∈ Fin}    ⇒   ⊢ ∀𝑧 ∈ ℕ ∃!𝑔 ∈ 𝑅 (𝑀‘𝑧) = 𝑔
5.2.12  Lagrange's four-square theorem
Syntax	cgz 12350	Extend class notation with the set of gaussian integers.
class ℤ[i]
Definition	df-gz 12351	Define the set of gaussian integers, which are complex numbers whose real and imaginary parts are integers. (Note that the [i] is actually part of the symbol token and has no independent meaning.) (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ ℤ[i] = {𝑥 ∈ ℂ ∣ ((ℜ‘𝑥) ∈ ℤ ∧ (ℑ‘𝑥) ∈ ℤ)}
Theorem	elgz 12352	Elementhood in the gaussian integers. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] ↔ (𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℤ ∧ (ℑ‘𝐴) ∈ ℤ))
Theorem	gzcn 12353	A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
Theorem	zgz 12354	An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℤ[i])
Theorem	igz 12355	i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ i ∈ ℤ[i]
Theorem	gznegcl 12356	The gaussian integers are closed under negation. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → -𝐴 ∈ ℤ[i])
Theorem	gzcjcl 12357	The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
Theorem	gzaddcl 12358	The gaussian integers are closed under addition. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 + 𝐵) ∈ ℤ[i])
Theorem	gzmulcl 12359	The gaussian integers are closed under multiplication. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 · 𝐵) ∈ ℤ[i])
Theorem	gzreim 12360	Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
Theorem	gzsubcl 12361	The gaussian integers are closed under subtraction. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 − 𝐵) ∈ ℤ[i])
Theorem	gzabssqcl 12362	The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → ((abs‘𝐴)↑2) ∈ ℕ0)
Theorem	4sqlem5 12363	Lemma for 4sq (not yet proved here). (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (𝐵 ∈ ℤ ∧ ((𝐴 − 𝐵) / 𝑀) ∈ ℤ))
Theorem	4sqlem6 12364	Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (-(𝑀 / 2) ≤ 𝐵 ∧ 𝐵 < (𝑀 / 2)))
Theorem	4sqlem7 12365	Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (𝐵↑2) ≤ (((𝑀↑2) / 2) / 2))
Theorem	4sqlem8 12366	Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐵↑2)))
Theorem	4sqlem9 12367	Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) = 0)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ (𝐴↑2))
Theorem	4sqlem10 12368	Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ ((𝜑 ∧ 𝜓) → ((((𝑀↑2) / 2) / 2) − (𝐵↑2)) = 0)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴↑2) − (((𝑀↑2) / 2) / 2)))
Theorem	4sqlem1 12369*	Lemma for 4sq (not yet proved here) . The set 𝑆 is the set of all numbers that are expressible as a sum of four squares. Our goal is to show that 𝑆 = ℕ0; here we show one subset direction. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ 𝑆 ⊆ ℕ0
Theorem	4sqlem2 12370*	Lemma for 4sq (not yet proved here) . Change bound variables in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
Theorem	4sqlem3 12371*	Lemma for 4sq (not yet proved here) . Sufficient condition to be in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) ∈ 𝑆)
Theorem	4sqlem4a 12372*	Lemma for 4sqlem4 12373. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ 𝑆)
Theorem	4sqlem4 12373*	Lemma for 4sq (not yet proved here) . We can express the four-square property more compactly in terms of gaussian integers, because the norms of gaussian integers are exactly sums of two squares. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] 𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)))
Theorem	mul4sqlem 12374*	Lemma for mul4sq 12375: algebraic manipulations. The extra assumptions involving 𝑀 would let us know not just that the product is a sum of squares, but also that it preserves divisibility by 𝑀. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝐴 ∈ ℤ[i])    &   ⊢ (𝜑 → 𝐵 ∈ ℤ[i])    &   ⊢ (𝜑 → 𝐶 ∈ ℤ[i])    &   ⊢ (𝜑 → 𝐷 ∈ ℤ[i])    &   ⊢ 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))    &   ⊢ 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i])    &   ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i])    &   ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)
Theorem	mul4sq 12375*	Euler's four-square identity: The product of two sums of four squares is also a sum of four squares. This is usually quoted as an explicit formula involving eight real variables; we save some time by working with complex numbers (gaussian integers) instead, so that we only have to work with four variables, and also hiding the actual formula for the product in the proof of mul4sqlem 12374. (For the curious, the explicit formula that is used is ( ∣ 𝑎 ∣ ↑2 + ∣ 𝑏 ∣ ↑2)( ∣ 𝑐 ∣ ↑2 + ∣ 𝑑 ∣ ↑2) = ∣ 𝑎∗ · 𝑐 + 𝑏 · 𝑑∗ ∣ ↑2 + ∣ 𝑎∗ · 𝑑 − 𝑏 · 𝑐∗ ∣ ↑2.) (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 · 𝐵) ∈ 𝑆)
5.3  Cardinality of real and complex number subsets
5.3.1  Countability of integers and rationals
Theorem	oddennn 12376	There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.)
⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ≈ ℕ
Theorem	evenennn 12377	There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.)
⊢ {𝑧 ∈ ℕ ∣ 2 ∥ 𝑧} ≈ ℕ
Theorem	xpnnen 12378	The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.)
⊢ (ℕ × ℕ) ≈ ℕ
Theorem	xpomen 12379	The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.)
⊢ (ω × ω) ≈ ω
Theorem	xpct 12380	The cartesian product of two sets dominated by ω is dominated by ω. (Contributed by Thierry Arnoux, 24-Sep-2017.)
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω)
Theorem	unennn 12381	The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.)
⊢ ((𝐴 ≈ ℕ ∧ 𝐵 ≈ ℕ ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ≈ ℕ)
Theorem	znnen 12382	The set of integers and the set of positive integers are equinumerous. Corollary 8.1.23 of [AczelRathjen], p. 75. (Contributed by NM, 31-Jul-2004.)
⊢ ℤ ≈ ℕ
Theorem	ennnfonelemdc 12383*	Lemma for ennnfone 12409. A direct consequence of fidcenumlemrk 6947. (Contributed by Jim Kingdon, 15-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → 𝑃 ∈ ω)    ⇒   ⊢ (𝜑 → DECID (𝐹‘𝑃) ∈ (𝐹 “ 𝑃))
Theorem	ennnfonelemk 12384*	Lemma for ennnfone 12409. (Contributed by Jim Kingdon, 15-Jul-2023.)
⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → ∀𝑗 ∈ suc 𝑁(𝐹‘𝐾) ≠ (𝐹‘𝑗))    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝐾)
Theorem	ennnfonelemj0 12385*	Lemma for ennnfone 12409. Initial state for 𝐽. (Contributed by Jim Kingdon, 20-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    ⇒   ⊢ (𝜑 → (𝐽‘0) ∈ {𝑔 ∈ (𝐴 ↑pm ω) ∣ dom 𝑔 ∈ ω})
Theorem	ennnfonelemjn 12386*	Lemma for ennnfone 12409. Non-initial state for 𝐽. (Contributed by Jim Kingdon, 20-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    ⇒   ⊢ ((𝜑 ∧ 𝑓 ∈ (ℤ≥‘(0 + 1))) → (𝐽‘𝑓) ∈ ω)
Theorem	ennnfonelemg 12387*	Lemma for ennnfone 12409. Closure for 𝐺. (Contributed by Jim Kingdon, 20-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    ⇒   ⊢ ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴 ↑pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → (𝑓𝐺𝑗) ∈ {𝑔 ∈ (𝐴 ↑pm ω) ∣ dom 𝑔 ∈ ω})
Theorem	ennnfonelemh 12388*	Lemma for ennnfone 12409. (Contributed by Jim Kingdon, 8-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    ⇒   ⊢ (𝜑 → 𝐻:ℕ0⟶(𝐴 ↑pm ω))
Theorem	ennnfonelem0 12389*	Lemma for ennnfone 12409. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    ⇒   ⊢ (𝜑 → (𝐻‘0) = ∅)
Theorem	ennnfonelemp1 12390*	Lemma for ennnfone 12409. Value of 𝐻 at a successor. (Contributed by Jim Kingdon, 23-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘(𝑃 + 1)) = if((𝐹‘(◡𝑁‘𝑃)) ∈ (𝐹 “ (◡𝑁‘𝑃)), (𝐻‘𝑃), ((𝐻‘𝑃) ∪ {⟨dom (𝐻‘𝑃), (𝐹‘(◡𝑁‘𝑃))⟩})))
Theorem	ennnfonelem1 12391*	Lemma for ennnfone 12409. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    ⇒   ⊢ (𝜑 → (𝐻‘1) = {⟨∅, (𝐹‘∅)⟩})
Theorem	ennnfonelemom 12392*	Lemma for ennnfone 12409. 𝐻 yields finite sequences. (Contributed by Jim Kingdon, 19-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    ⇒   ⊢ (𝜑 → dom (𝐻‘𝑃) ∈ ω)
Theorem	ennnfonelemhdmp1 12393*	Lemma for ennnfone 12409. Domain at a successor where we need to add an element to the sequence. (Contributed by Jim Kingdon, 23-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    &   ⊢ (𝜑 → ¬ (𝐹‘(◡𝑁‘𝑃)) ∈ (𝐹 “ (◡𝑁‘𝑃)))    ⇒   ⊢ (𝜑 → dom (𝐻‘(𝑃 + 1)) = suc dom (𝐻‘𝑃))
Theorem	ennnfonelemss 12394*	Lemma for ennnfone 12409. We only add elements to 𝐻 as the index increases. (Contributed by Jim Kingdon, 15-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑃) ⊆ (𝐻‘(𝑃 + 1)))
Theorem	ennnfoneleminc 12395*	Lemma for ennnfone 12409. We only add elements to 𝐻 as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑄 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑃 ≤ 𝑄)    ⇒   ⊢ (𝜑 → (𝐻‘𝑃) ⊆ (𝐻‘𝑄))
Theorem	ennnfonelemkh 12396*	Lemma for ennnfone 12409. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    ⇒   ⊢ (𝜑 → dom (𝐻‘𝑃) ⊆ (◡𝑁‘𝑃))
Theorem	ennnfonelemhf1o 12397*	Lemma for ennnfone 12409. Each of the functions in 𝐻 is one to one and onto an image of 𝐹. (Contributed by Jim Kingdon, 17-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (◡𝑁‘𝑃)))
Theorem	ennnfonelemex 12398*	Lemma for ennnfone 12409. Extending the sequence (𝐻‘𝑃) to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ∃𝑖 ∈ ℕ0 dom (𝐻‘𝑃) ∈ dom (𝐻‘𝑖))
Theorem	ennnfonelemhom 12399*	Lemma for ennnfone 12409. The sequences in 𝐻 increase in length without bound if you go out far enough. (Contributed by Jim Kingdon, 19-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    ⇒   ⊢ (𝜑 → ∃𝑖 ∈ ℕ0 𝑀 ∈ dom (𝐻‘𝑖))
Theorem	ennnfonelemrnh 12400*	Lemma for ennnfone 12409. A consequence of ennnfonelemss 12394. (Contributed by Jim Kingdon, 16-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐻)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐻)    ⇒   ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ∨ 𝑌 ⊆ 𝑋))