Theorem prmop1

Description: The primorial of a successor. (Contributed by AV, 28-Aug-2020)

	Ref	Expression
Assertion	prmop1	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ ( 𝑁 + 1 ) ) = if ( ( 𝑁 + 1 ) ∈ ℙ , ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) , ( #p ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
2		prmoval	⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( #p ‘ ( 𝑁 + 1 ) ) = ∏ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ ( 𝑁 + 1 ) ) = ∏ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
4		nn0p1nn	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
5		elnnuz	⊢ ( ( 𝑁 + 1 ) ∈ ℕ ↔ ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
6	4 5	sylib	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
7		elfzelz	⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
8	7	zcnd	⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℂ )
9	8	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℂ )
10		1cnd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 1 ∈ ℂ )
11	9 10	ifcld	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℂ )
12		eleq1	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝑘 ∈ ℙ ↔ ( 𝑁 + 1 ) ∈ ℙ ) )
13		id	⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝑘 = ( 𝑁 + 1 ) )
14	12 13	ifbieq1d	⊢ ( 𝑘 = ( 𝑁 + 1 ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) )
15	6 11 14	fprodm1	⊢ ( 𝑁 ∈ ℕ0 → ∏ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = ( ∏ 𝑘 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) )
16		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
17		pncan1	⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
18	16 17	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
19	18	oveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 1 ... 𝑁 ) )
20	19	prodeq1d	⊢ ( 𝑁 ∈ ℕ0 → ∏ 𝑘 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
21	20	oveq1d	⊢ ( 𝑁 ∈ ℕ0 → ( ∏ 𝑘 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) )
22		prmoval	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
23	22	eqcomd	⊢ ( 𝑁 ∈ ℕ0 → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = ( #p ‘ 𝑁 ) )
24	23	adantl	⊢ ( ( ( 𝑁 + 1 ) ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = ( #p ‘ 𝑁 ) )
25	24	oveq1d	⊢ ( ( ( 𝑁 + 1 ) ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · ( 𝑁 + 1 ) ) = ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )
26		iftrue	⊢ ( ( 𝑁 + 1 ) ∈ ℙ → if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) = ( 𝑁 + 1 ) )
27	26	oveq2d	⊢ ( ( 𝑁 + 1 ) ∈ ℙ → ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · ( 𝑁 + 1 ) ) )
28		iftrue	⊢ ( ( 𝑁 + 1 ) ∈ ℙ → if ( ( 𝑁 + 1 ) ∈ ℙ , ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) , ( #p ‘ 𝑁 ) ) = ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )
29	27 28	eqeq12d	⊢ ( ( 𝑁 + 1 ) ∈ ℙ → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) = if ( ( 𝑁 + 1 ) ∈ ℙ , ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) , ( #p ‘ 𝑁 ) ) ↔ ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · ( 𝑁 + 1 ) ) = ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) ) )
30	29	adantr	⊢ ( ( ( 𝑁 + 1 ) ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) = if ( ( 𝑁 + 1 ) ∈ ℙ , ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) , ( #p ‘ 𝑁 ) ) ↔ ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · ( 𝑁 + 1 ) ) = ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) ) )
31	25 30	mpbird	⊢ ( ( ( 𝑁 + 1 ) ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) = if ( ( 𝑁 + 1 ) ∈ ℙ , ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) , ( #p ‘ 𝑁 ) ) )
32		fzfid	⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ∈ Fin )
33		elfznn	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
34		1nn	⊢ 1 ∈ ℕ
35	34	a1i	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 1 ∈ ℕ )
36	33 35	ifcld	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℕ )
37	36	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℕ )
38	32 37	fprodnncl	⊢ ( 𝑁 ∈ ℕ0 → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℕ )
39	38	nncnd	⊢ ( 𝑁 ∈ ℕ0 → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℂ )
40	39	adantl	⊢ ( ( ¬ ( 𝑁 + 1 ) ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℂ )
41	40	mulridd	⊢ ( ( ¬ ( 𝑁 + 1 ) ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · 1 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
42	22	adantl	⊢ ( ( ¬ ( 𝑁 + 1 ) ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( #p ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
43	41 42	eqtr4d	⊢ ( ( ¬ ( 𝑁 + 1 ) ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · 1 ) = ( #p ‘ 𝑁 ) )
44		iffalse	⊢ ( ¬ ( 𝑁 + 1 ) ∈ ℙ → if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) = 1 )
45	44	oveq2d	⊢ ( ¬ ( 𝑁 + 1 ) ∈ ℙ → ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · 1 ) )
46		iffalse	⊢ ( ¬ ( 𝑁 + 1 ) ∈ ℙ → if ( ( 𝑁 + 1 ) ∈ ℙ , ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) , ( #p ‘ 𝑁 ) ) = ( #p ‘ 𝑁 ) )
47	45 46	eqeq12d	⊢ ( ¬ ( 𝑁 + 1 ) ∈ ℙ → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) = if ( ( 𝑁 + 1 ) ∈ ℙ , ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) , ( #p ‘ 𝑁 ) ) ↔ ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · 1 ) = ( #p ‘ 𝑁 ) ) )
48	47	adantr	⊢ ( ( ¬ ( 𝑁 + 1 ) ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) = if ( ( 𝑁 + 1 ) ∈ ℙ , ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) , ( #p ‘ 𝑁 ) ) ↔ ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · 1 ) = ( #p ‘ 𝑁 ) ) )
49	43 48	mpbird	⊢ ( ( ¬ ( 𝑁 + 1 ) ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) = if ( ( 𝑁 + 1 ) ∈ ℙ , ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) , ( #p ‘ 𝑁 ) ) )
50	31 49	pm2.61ian	⊢ ( 𝑁 ∈ ℕ0 → ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) = if ( ( 𝑁 + 1 ) ∈ ℙ , ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) , ( #p ‘ 𝑁 ) ) )
51	21 50	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( ∏ 𝑘 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · if ( ( 𝑁 + 1 ) ∈ ℙ , ( 𝑁 + 1 ) , 1 ) ) = if ( ( 𝑁 + 1 ) ∈ ℙ , ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) , ( #p ‘ 𝑁 ) ) )
52	3 15 51	3eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ ( 𝑁 + 1 ) ) = if ( ( 𝑁 + 1 ) ∈ ℙ , ( ( #p ‘ 𝑁 ) · ( 𝑁 + 1 ) ) , ( #p ‘ 𝑁 ) ) )