Metamath Proof Explorer

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 ⊢ φ → P ∈ ℙ
exfinfldd.2 ⊢ φ → N ∈ ℕ
Assertion exfinfldd ⊢ φ → ∃ k ∈ Field Base k = P N ∧ chr ⁡ k = P

Proof

Step Hyp Ref Expression
1 exfinfldd.1 ⊢ φ → P ∈ ℙ
2 exfinfldd.2 ⊢ φ → N ∈ ℕ
3 oveq2 ⊢ n = N → P n = P N
4 3 eqeq2d ⊢ n = N → Base k = P n ↔ Base k = P N
5 4 anbi1d ⊢ n = N → Base k = P n ∧ chr ⁡ k = P ↔ Base k = P N ∧ chr ⁡ k = P
6 5 rexbidv ⊢ n = N → ∃ k ∈ Field Base k = P n ∧ chr ⁡ k = P ↔ ∃ k ∈ Field Base k = P N ∧ chr ⁡ k = P
7 oveq1 ⊢ p = P → p n = P n
8 7 eqeq2d ⊢ p = P → Base k = p n ↔ Base k = P n
9 eqeq2 ⊢ p = P → chr ⁡ k = p ↔ chr ⁡ k = P
10 8 9 anbi12d ⊢ p = P → Base k = p n ∧ chr ⁡ k = p ↔ Base k = P n ∧ chr ⁡ k = P
11 10 rexbidv ⊢ p = P → ∃ k ∈ Field Base k = p n ∧ chr ⁡ k = p ↔ ∃ k ∈ Field Base k = P n ∧ chr ⁡ k = P
12 11 ralbidv ⊢ p = P → ∀ n ∈ ℕ ∃ k ∈ Field Base k = p n ∧ chr ⁡ k = p ↔ ∀ n ∈ ℕ ∃ k ∈ Field Base k = P n ∧ chr ⁡ k = P
13 ax-exfinfld ⊢ ∀ p ∈ ℙ ∀ n ∈ ℕ ∃ k ∈ Field Base k = p n ∧ chr ⁡ k = p
14 13 a1i ⊢ φ → ∀ p ∈ ℙ ∀ n ∈ ℕ ∃ k ∈ Field Base k = p n ∧ chr ⁡ k = p
15 12 14 1 rspcdva ⊢ φ → ∀ n ∈ ℕ ∃ k ∈ Field Base k = P n ∧ chr ⁡ k = P
16 6 15 2 rspcdva ⊢ φ → ∃ k ∈ Field Base k = P N ∧ chr ⁡ k = P