Metamath Proof Explorer

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 mulid1d ⊢ ( ( ¬ ( 𝑁 + 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 ‘ 𝑁 ) ) )