prmonn2

Description: Value of the primorial function expressed recursively. (Contributed by AV, 28-Aug-2020)

		Ref	Expression
	Assertion	prmonn2	$⊢ N \in ℕ \to #_{p} (N) = if (N \in ℙ, #_{p} (N - 1) \cdot N, #_{p} (N - 1))$

Step	Hyp	Ref	Expression
1		nncn	$⊢ N \in ℕ \to N \in ℂ$
2		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
3	1 2	syl	$⊢ N \in ℕ \to N - 1 + 1 = N$
4	3	eqcomd	$⊢ N \in ℕ \to N = N - 1 + 1$
5	4	fveq2d	$⊢ N \in ℕ \to #_{p} (N) = #_{p} (N - 1 + 1)$
6		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
7		prmop1	$⊢ N - 1 \in ℕ_{0} \to #_{p} (N - 1 + 1) = if (N - 1 + 1 \in ℙ, #_{p} (N - 1) (N - 1 + 1), #_{p} (N - 1))$
8	6 7	syl	$⊢ N \in ℕ \to #_{p} (N - 1 + 1) = if (N - 1 + 1 \in ℙ, #_{p} (N - 1) (N - 1 + 1), #_{p} (N - 1))$
9	3	eleq1d	$⊢ N \in ℕ \to (N - 1 + 1 \in ℙ \leftrightarrow N \in ℙ)$
10	3	oveq2d	$⊢ N \in ℕ \to #_{p} (N - 1) (N - 1 + 1) = #_{p} (N - 1) \cdot N$
11	9 10	ifbieq1d	$⊢ N \in ℕ \to if (N - 1 + 1 \in ℙ, #_{p} (N - 1) (N - 1 + 1), #_{p} (N - 1)) = if (N \in ℙ, #_{p} (N - 1) \cdot N, #_{p} (N - 1))$
12	5 8 11	3eqtrd	$⊢ N \in ℕ \to #_{p} (N) = if (N \in ℙ, #_{p} (N - 1) \cdot N, #_{p} (N - 1))$

Metamath Proof Explorer