Theorem exfinfldd

Description: For any prime P and any positive integer N there exists a field k such that k contains P ^ N elements. (Contributed by metakunt, 13-Jul-2025)

	Ref	Expression
Hypotheses	exfinfldd.1	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	exfinfldd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	exfinfldd	⊢ ( 𝜑 → ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑁 ) ∧ ( chr ‘ 𝑘 ) = 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		exfinfldd.1	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
2		exfinfldd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		oveq2	⊢ ( 𝑛 = 𝑁 → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑁 ) )
4	3	eqeq2d	⊢ ( 𝑛 = 𝑁 → ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑛 ) ↔ ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑁 ) ) )
5	4	anbi1d	⊢ ( 𝑛 = 𝑁 → ( ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑃 ) ↔ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑁 ) ∧ ( chr ‘ 𝑘 ) = 𝑃 ) ) )
6	5	rexbidv	⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑃 ) ↔ ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑁 ) ∧ ( chr ‘ 𝑘 ) = 𝑃 ) ) )
7		oveq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑛 ) )
8	7	eqeq2d	⊢ ( 𝑝 = 𝑃 → ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑝 ↑ 𝑛 ) ↔ ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑛 ) ) )
9		eqeq2	⊢ ( 𝑝 = 𝑃 → ( ( chr ‘ 𝑘 ) = 𝑝 ↔ ( chr ‘ 𝑘 ) = 𝑃 ) )
10	8 9	anbi12d	⊢ ( 𝑝 = 𝑃 → ( ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑝 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑝 ) ↔ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑃 ) ) )
11	10	rexbidv	⊢ ( 𝑝 = 𝑃 → ( ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑝 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑝 ) ↔ ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑃 ) ) )
12	11	ralbidv	⊢ ( 𝑝 = 𝑃 → ( ∀ 𝑛 ∈ ℕ ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑝 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑝 ) ↔ ∀ 𝑛 ∈ ℕ ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑃 ) ) )
13		ax-exfinfld	⊢ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑝 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑝 )
14	13	a1i	⊢ ( 𝜑 → ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑝 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑝 ) )
15	12 14 1	rspcdva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑃 ) )
16	6 15 2	rspcdva	⊢ ( 𝜑 → ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑃 ↑ 𝑁 ) ∧ ( chr ‘ 𝑘 ) = 𝑃 ) )