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 
|- ( ph -> P e. Prime )
exfinfldd.2 
|- ( ph -> N e. NN )
Assertion exfinfldd 
|- ( ph -> E. k e. Field ( ( # ` ( Base ` k ) ) = ( P ^ N ) /\ ( chr ` k ) = P ) )

Proof

Step Hyp Ref Expression
1 exfinfldd.1 
 |-  ( ph -> P e. Prime )
2 exfinfldd.2 
 |-  ( ph -> N e. NN )
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 -> ( E. k e. Field ( ( # ` ( Base ` k ) ) = ( P ^ n ) /\ ( chr ` k ) = P ) <-> E. k e. 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 -> ( E. k e. Field ( ( # ` ( Base ` k ) ) = ( p ^ n ) /\ ( chr ` k ) = p ) <-> E. k e. Field ( ( # ` ( Base ` k ) ) = ( P ^ n ) /\ ( chr ` k ) = P ) ) )
12 11 ralbidv 
 |-  ( p = P -> ( A. n e. NN E. k e. Field ( ( # ` ( Base ` k ) ) = ( p ^ n ) /\ ( chr ` k ) = p ) <-> A. n e. NN E. k e. Field ( ( # ` ( Base ` k ) ) = ( P ^ n ) /\ ( chr ` k ) = P ) ) )
13 ax-exfinfld 
 |-  A. p e. Prime A. n e. NN E. k e. Field ( ( # ` ( Base ` k ) ) = ( p ^ n ) /\ ( chr ` k ) = p )
14 13 a1i 
 |-  ( ph -> A. p e. Prime A. n e. NN E. k e. Field ( ( # ` ( Base ` k ) ) = ( p ^ n ) /\ ( chr ` k ) = p ) )
15 12 14 1 rspcdva 
 |-  ( ph -> A. n e. NN E. k e. Field ( ( # ` ( Base ` k ) ) = ( P ^ n ) /\ ( chr ` k ) = P ) )
16 6 15 2 rspcdva 
 |-  ( ph -> E. k e. Field ( ( # ` ( Base ` k ) ) = ( P ^ N ) /\ ( chr ` k ) = P ) )