Metamath Proof Explorer

Theorem prmo3

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

Ref Expression
Assertion prmo3 ⊢ # p ⁡ 3 = 6

Proof

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