prmop1

		Ref	Expression
	Assertion	prmop1	$⊢ N \in ℕ_{0} \to #_{p} (N + 1) = if (N + 1 \in ℙ, #_{p} (N) (N + 1), #_{p} (N))$

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
2		prmoval	$⊢ N + 1 \in ℕ_{0} \to #_{p} (N + 1) = \prod_{k = 1}^{N + 1} if (k \in ℙ, k, 1)$
3	1 2	syl	$⊢ N \in ℕ_{0} \to #_{p} (N + 1) = \prod_{k = 1}^{N + 1} if (k \in ℙ, k, 1)$
4		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
5		elnnuz	$⊢ N + 1 \in ℕ \leftrightarrow N + 1 \in ℤ_{\geq 1}$
6	4 5	sylib	$⊢ N \in ℕ_{0} \to N + 1 \in ℤ_{\geq 1}$
7		elfzelz	$⊢ k \in (1 \dots N + 1) \to k \in ℤ$
8	7	zcnd	$⊢ k \in (1 \dots N + 1) \to k \in ℂ$
9	8	adantl	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N + 1)) \to k \in ℂ$
10		1cnd	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N + 1)) \to 1 \in ℂ$
11	9 10	ifcld	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N + 1)) \to if (k \in ℙ, k, 1) \in ℂ$
12		eleq1	$⊢ k = N + 1 \to (k \in ℙ \leftrightarrow N + 1 \in ℙ)$
13		id	$⊢ k = N + 1 \to k = N + 1$
14	12 13	ifbieq1d	$⊢ k = N + 1 \to if (k \in ℙ, k, 1) = if (N + 1 \in ℙ, N + 1, 1)$
15	6 11 14	fprodm1	$⊢ N \in ℕ_{0} \to \prod_{k = 1}^{N + 1} if (k \in ℙ, k, 1) = \prod_{k = 1}^{N + 1 - 1} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1)$
16		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
17		pncan1	$⊢ N \in ℂ \to N + 1 - 1 = N$
18	16 17	syl	$⊢ N \in ℕ_{0} \to N + 1 - 1 = N$
19	18	oveq2d	$⊢ N \in ℕ_{0} \to (1 \dots N + 1 - 1) = (1 \dots N)$
20	19	prodeq1d	$⊢ N \in ℕ_{0} \to \prod_{k = 1}^{N + 1 - 1} if (k \in ℙ, k, 1) = \prod_{k = 1}^{N} if (k \in ℙ, k, 1)$
21	20	oveq1d	$⊢ N \in ℕ_{0} \to \prod_{k = 1}^{N + 1 - 1} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1) = \prod_{k = 1}^{N} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1)$
22		prmoval	$⊢ N \in ℕ_{0} \to #_{p} (N) = \prod_{k = 1}^{N} if (k \in ℙ, k, 1)$
23	22	eqcomd	$⊢ N \in ℕ_{0} \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) = #_{p} (N)$
24	23	adantl	$⊢ (N + 1 \in ℙ \land N \in ℕ_{0}) \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) = #_{p} (N)$
25	24	oveq1d	$⊢ (N + 1 \in ℙ \land N \in ℕ_{0}) \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) (N + 1) = #_{p} (N) (N + 1)$
26		iftrue	$⊢ N + 1 \in ℙ \to if (N + 1 \in ℙ, N + 1, 1) = N + 1$
27	26	oveq2d	$⊢ N + 1 \in ℙ \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1) = \prod_{k = 1}^{N} if (k \in ℙ, k, 1) (N + 1)$
28		iftrue	$⊢ N + 1 \in ℙ \to if (N + 1 \in ℙ, #_{p} (N) (N + 1), #_{p} (N)) = #_{p} (N) (N + 1)$
29	27 28	eqeq12d	$⊢ N + 1 \in ℙ \to (\prod_{k = 1}^{N} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1) = if (N + 1 \in ℙ, #_{p} (N) (N + 1), #_{p} (N)) \leftrightarrow \prod_{k = 1}^{N} if (k \in ℙ, k, 1) (N + 1) = #_{p} (N) (N + 1))$
30	29	adantr	$⊢ (N + 1 \in ℙ \land N \in ℕ_{0}) \to (\prod_{k = 1}^{N} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1) = if (N + 1 \in ℙ, #_{p} (N) (N + 1), #_{p} (N)) \leftrightarrow \prod_{k = 1}^{N} if (k \in ℙ, k, 1) (N + 1) = #_{p} (N) (N + 1))$
31	25 30	mpbird	$⊢ (N + 1 \in ℙ \land N \in ℕ_{0}) \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1) = if (N + 1 \in ℙ, #_{p} (N) (N + 1), #_{p} (N))$
32		fzfid	$⊢ N \in ℕ_{0} \to (1 \dots N) \in Fin$
33		elfznn	$⊢ k \in (1 \dots N) \to k \in ℕ$
34		1nn	$⊢ 1 \in ℕ$
35	34	a1i	$⊢ k \in (1 \dots N) \to 1 \in ℕ$
36	33 35	ifcld	$⊢ k \in (1 \dots N) \to if (k \in ℙ, k, 1) \in ℕ$
37	36	adantl	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to if (k \in ℙ, k, 1) \in ℕ$
38	32 37	fprodnncl	$⊢ N \in ℕ_{0} \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) \in ℕ$
39	38	nncnd	$⊢ N \in ℕ_{0} \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) \in ℂ$
40	39	adantl	$⊢ (\neg N + 1 \in ℙ \land N \in ℕ_{0}) \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) \in ℂ$
41	40	mulid1d	$⊢ (\neg N + 1 \in ℙ \land N \in ℕ_{0}) \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) \cdot 1 = \prod_{k = 1}^{N} if (k \in ℙ, k, 1)$
42	22	adantl	$⊢ (\neg N + 1 \in ℙ \land N \in ℕ_{0}) \to #_{p} (N) = \prod_{k = 1}^{N} if (k \in ℙ, k, 1)$
43	41 42	eqtr4d	$⊢ (\neg N + 1 \in ℙ \land N \in ℕ_{0}) \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) \cdot 1 = #_{p} (N)$
44		iffalse	$⊢ \neg N + 1 \in ℙ \to if (N + 1 \in ℙ, N + 1, 1) = 1$
45	44	oveq2d	$⊢ \neg N + 1 \in ℙ \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1) = \prod_{k = 1}^{N} if (k \in ℙ, k, 1) \cdot 1$
46		iffalse	$⊢ \neg N + 1 \in ℙ \to if (N + 1 \in ℙ, #_{p} (N) (N + 1), #_{p} (N)) = #_{p} (N)$
47	45 46	eqeq12d	$⊢ \neg N + 1 \in ℙ \to (\prod_{k = 1}^{N} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1) = if (N + 1 \in ℙ, #_{p} (N) (N + 1), #_{p} (N)) \leftrightarrow \prod_{k = 1}^{N} if (k \in ℙ, k, 1) \cdot 1 = #_{p} (N))$
48	47	adantr	$⊢ (\neg N + 1 \in ℙ \land N \in ℕ_{0}) \to (\prod_{k = 1}^{N} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1) = if (N + 1 \in ℙ, #_{p} (N) (N + 1), #_{p} (N)) \leftrightarrow \prod_{k = 1}^{N} if (k \in ℙ, k, 1) \cdot 1 = #_{p} (N))$
49	43 48	mpbird	$⊢ (\neg N + 1 \in ℙ \land N \in ℕ_{0}) \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1) = if (N + 1 \in ℙ, #_{p} (N) (N + 1), #_{p} (N))$
50	31 49	pm2.61ian	$⊢ N \in ℕ_{0} \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1) = if (N + 1 \in ℙ, #_{p} (N) (N + 1), #_{p} (N))$
51	21 50	eqtrd	$⊢ N \in ℕ_{0} \to \prod_{k = 1}^{N + 1 - 1} if (k \in ℙ, k, 1) if (N + 1 \in ℙ, N + 1, 1) = if (N + 1 \in ℙ, #_{p} (N) (N + 1), #_{p} (N))$
52	3 15 51	3eqtrd	$⊢ N \in ℕ_{0} \to #_{p} (N + 1) = if (N + 1 \in ℙ, #_{p} (N) (N + 1), #_{p} (N))$

Metamath Proof Explorer

Theorem prmop1

Proof