Metamath Proof Explorer

Theorem fvprmselelfz

Description: The value of the prime selection function is in a finite sequence of integers if the argument is in this finite sequence of integers. (Contributed by AV, 19-Aug-2020)

Ref Expression
Hypothesis fvprmselelfz.f 
|- F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )
Assertion fvprmselelfz 
|- ( ( N e. NN /\ X e. ( 1 ... N ) ) -> ( F ` X ) e. ( 1 ... N ) )

Proof

Step Hyp Ref Expression
1 fvprmselelfz.f 
 |-  F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )
2 eleq1 
 |-  ( m = X -> ( m e. Prime <-> X e. Prime ) )
3 id 
 |-  ( m = X -> m = X )
4 2 3 ifbieq1d 
 |-  ( m = X -> if ( m e. Prime , m , 1 ) = if ( X e. Prime , X , 1 ) )
5 iftrue 
 |-  ( X e. Prime -> if ( X e. Prime , X , 1 ) = X )
6 5 adantr 
 |-  ( ( X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) -> if ( X e. Prime , X , 1 ) = X )
7 4 6 sylan9eqr 
 |-  ( ( ( X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) /\ m = X ) -> if ( m e. Prime , m , 1 ) = X )
8 elfznn 
 |-  ( X e. ( 1 ... N ) -> X e. NN )
9 8 adantl 
 |-  ( ( N e. NN /\ X e. ( 1 ... N ) ) -> X e. NN )
10 9 adantl 
 |-  ( ( X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) -> X e. NN )
11 1 7 10 10 fvmptd2 
 |-  ( ( X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) -> ( F ` X ) = X )
12 simprr 
 |-  ( ( X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) -> X e. ( 1 ... N ) )
13 11 12 eqeltrd 
 |-  ( ( X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) -> ( F ` X ) e. ( 1 ... N ) )
14 iffalse 
 |-  ( -. X e. Prime -> if ( X e. Prime , X , 1 ) = 1 )
15 14 adantr 
 |-  ( ( -. X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) -> if ( X e. Prime , X , 1 ) = 1 )
16 4 15 sylan9eqr 
 |-  ( ( ( -. X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) /\ m = X ) -> if ( m e. Prime , m , 1 ) = 1 )
17 9 adantl 
 |-  ( ( -. X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) -> X e. NN )
18 1nn 
 |-  1 e. NN
19 18 a1i 
 |-  ( ( -. X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) -> 1 e. NN )
20 1 16 17 19 fvmptd2 
 |-  ( ( -. X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) -> ( F ` X ) = 1 )
21 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
22 eluzfz1 
 |-  ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
23 21 22 sylbi 
 |-  ( N e. NN -> 1 e. ( 1 ... N ) )
24 23 adantr 
 |-  ( ( N e. NN /\ X e. ( 1 ... N ) ) -> 1 e. ( 1 ... N ) )
25 24 adantl 
 |-  ( ( -. X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) -> 1 e. ( 1 ... N ) )
26 20 25 eqeltrd 
 |-  ( ( -. X e. Prime /\ ( N e. NN /\ X e. ( 1 ... N ) ) ) -> ( F ` X ) e. ( 1 ... N ) )
27 13 26 pm2.61ian 
 |-  ( ( N e. NN /\ X e. ( 1 ... N ) ) -> ( F ` X ) e. ( 1 ... N ) )