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 ⊢ 𝐹 = ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) )
Assertion fvprmselelfz ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 1 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 fvprmselelfz.f ⊢ 𝐹 = ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) )
2 eleq1 ⊢ ( 𝑚 = 𝑋 → ( 𝑚 ∈ ℙ ↔ 𝑋 ∈ ℙ ) )
3 id ⊢ ( 𝑚 = 𝑋 → 𝑚 = 𝑋 )
4 2 3 ifbieq1d ⊢ ( 𝑚 = 𝑋 → if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) = if ( 𝑋 ∈ ℙ , 𝑋 , 1 ) )
5 iftrue ⊢ ( 𝑋 ∈ ℙ → if ( 𝑋 ∈ ℙ , 𝑋 , 1 ) = 𝑋 )
6 5 adantr ⊢ ( ( 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) → if ( 𝑋 ∈ ℙ , 𝑋 , 1 ) = 𝑋 )
7 4 6 sylan9eqr ⊢ ( ( ( 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) ∧ 𝑚 = 𝑋 ) → if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) = 𝑋 )
8 elfznn ⊢ ( 𝑋 ∈ ( 1 ... 𝑁 ) → 𝑋 ∈ ℕ )
9 8 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ ℕ )
10 9 adantl ⊢ ( ( 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) → 𝑋 ∈ ℕ )
11 1 7 10 10 fvmptd2 ⊢ ( ( 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )
12 simprr ⊢ ( ( 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) → 𝑋 ∈ ( 1 ... 𝑁 ) )
13 11 12 eqeltrd ⊢ ( ( 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 1 ... 𝑁 ) )
14 iffalse ⊢ ( ¬ 𝑋 ∈ ℙ → if ( 𝑋 ∈ ℙ , 𝑋 , 1 ) = 1 )
15 14 adantr ⊢ ( ( ¬ 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) → if ( 𝑋 ∈ ℙ , 𝑋 , 1 ) = 1 )
16 4 15 sylan9eqr ⊢ ( ( ( ¬ 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) ∧ 𝑚 = 𝑋 ) → if ( 𝑚 ∈ ℙ , 𝑚 , 1 ) = 1 )
17 9 adantl ⊢ ( ( ¬ 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) → 𝑋 ∈ ℕ )
18 1nn ⊢ 1 ∈ ℕ
19 18 a1i ⊢ ( ( ¬ 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) → 1 ∈ ℕ )
20 1 16 17 19 fvmptd2 ⊢ ( ( ¬ 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑋 ) = 1 )
21 elnnuz ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
22 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑁 ) )
23 21 22 sylbi ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ( 1 ... 𝑁 ) )
24 23 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ( 1 ... 𝑁 ) )
25 24 adantl ⊢ ( ( ¬ 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) → 1 ∈ ( 1 ... 𝑁 ) )
26 20 25 eqeltrd ⊢ ( ( ¬ 𝑋 ∈ ℙ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 1 ... 𝑁 ) )
27 13 26 pm2.61ian ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 1 ... 𝑁 ) )