Metamath Proof Explorer

Theorem prmo2

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

Ref Expression
Assertion prmo2 ⊢ # p ⁡ 2 = 2

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 prmonn2 ⊢ 2 ∈ ℕ → # p ⁡ 2 = if 2 ∈ ℙ # p ⁡ 2 − 1 ⋅ 2 # p ⁡ 2 − 1
3 1 2 ax-mp ⊢ # p ⁡ 2 = if 2 ∈ ℙ # p ⁡ 2 − 1 ⋅ 2 # p ⁡ 2 − 1
4 2prm ⊢ 2 ∈ ℙ
5 4 iftruei ⊢ if 2 ∈ ℙ # p ⁡ 2 − 1 ⋅ 2 # p ⁡ 2 − 1 = # p ⁡ 2 − 1 ⋅ 2
6 2m1e1 ⊢ 2 − 1 = 1
7 6 fveq2i ⊢ # p ⁡ 2 − 1 = # p ⁡ 1
8 prmo1 ⊢ # p ⁡ 1 = 1
9 7 8 eqtri ⊢ # p ⁡ 2 − 1 = 1
10 9 oveq1i ⊢ # p ⁡ 2 − 1 ⋅ 2 = 1 ⋅ 2
11 2cn ⊢ 2 ∈ ℂ
12 11 mulid2i ⊢ 1 ⋅ 2 = 2
13 10 12 eqtri ⊢ # p ⁡ 2 − 1 ⋅ 2 = 2
14 5 13 eqtri ⊢ if 2 ∈ ℙ # p ⁡ 2 − 1 ⋅ 2 # p ⁡ 2 − 1 = 2
15 3 14 eqtri ⊢ # p ⁡ 2 = 2