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 \in ℕ ⟼ if (m \in ℙ, m, 1))$
	Assertion	fvprmselelfz	$⊢ (N \in ℕ \land X \in (1 \dots N)) \to F (X) \in (1 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		fvprmselelfz.f	$⊢ F = (m \in ℕ ⟼ if (m \in ℙ, m, 1))$
2		eleq1	$⊢ m = X \to (m \in ℙ \leftrightarrow X \in ℙ)$
3		id	$⊢ m = X \to m = X$
4	2 3	ifbieq1d	$⊢ m = X \to if (m \in ℙ, m, 1) = if (X \in ℙ, X, 1)$
5		iftrue	$⊢ X \in ℙ \to if (X \in ℙ, X, 1) = X$
6	5	adantr	$⊢ (X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \to if (X \in ℙ, X, 1) = X$
7	4 6	sylan9eqr	$⊢ ((X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \land m = X) \to if (m \in ℙ, m, 1) = X$
8		elfznn	$⊢ X \in (1 \dots N) \to X \in ℕ$
9	8	adantl	$⊢ (N \in ℕ \land X \in (1 \dots N)) \to X \in ℕ$
10	9	adantl	$⊢ (X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \to X \in ℕ$
11	1 7 10 10	fvmptd2	$⊢ (X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \to F (X) = X$
12		simprr	$⊢ (X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \to X \in (1 \dots N)$
13	11 12	eqeltrd	$⊢ (X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \to F (X) \in (1 \dots N)$
14		iffalse	$⊢ \neg X \in ℙ \to if (X \in ℙ, X, 1) = 1$
15	14	adantr	$⊢ (\neg X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \to if (X \in ℙ, X, 1) = 1$
16	4 15	sylan9eqr	$⊢ ((\neg X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \land m = X) \to if (m \in ℙ, m, 1) = 1$
17	9	adantl	$⊢ (\neg X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \to X \in ℕ$
18		1nn	$⊢ 1 \in ℕ$
19	18	a1i	$⊢ (\neg X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \to 1 \in ℕ$
20	1 16 17 19	fvmptd2	$⊢ (\neg X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \to F (X) = 1$
21		elnnuz	$⊢ N \in ℕ \leftrightarrow N \in ℤ_{\geq 1}$
22		eluzfz1	$⊢ N \in ℤ_{\geq 1} \to 1 \in (1 \dots N)$
23	21 22	sylbi	$⊢ N \in ℕ \to 1 \in (1 \dots N)$
24	23	adantr	$⊢ (N \in ℕ \land X \in (1 \dots N)) \to 1 \in (1 \dots N)$
25	24	adantl	$⊢ (\neg X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \to 1 \in (1 \dots N)$
26	20 25	eqeltrd	$⊢ (\neg X \in ℙ \land (N \in ℕ \land X \in (1 \dots N))) \to F (X) \in (1 \dots N)$
27	13 26	pm2.61ian	$⊢ (N \in ℕ \land X \in (1 \dots N)) \to F (X) \in (1 \dots N)$

Metamath Proof Explorer

Theorem fvprmselelfz

Proof