Metamath Proof Explorer

Theorem prmo6

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

Ref Expression
Assertion prmo6 ⊢ # p ⁡ 6 = 30

Proof

Step Hyp Ref Expression
1 6nn ⊢ 6 ∈ ℕ
2 prmonn2 ⊢ 6 ∈ ℕ → # p ⁡ 6 = if 6 ∈ ℙ # p ⁡ 6 − 1 ⋅ 6 # p ⁡ 6 − 1
3 1 2 ax-mp ⊢ # p ⁡ 6 = if 6 ∈ ℙ # p ⁡ 6 − 1 ⋅ 6 # p ⁡ 6 − 1
4 6nprm ⊢ ¬ 6 ∈ ℙ
5 4 iffalsei ⊢ if 6 ∈ ℙ # p ⁡ 6 − 1 ⋅ 6 # p ⁡ 6 − 1 = # p ⁡ 6 − 1
6 3 5 eqtri ⊢ # p ⁡ 6 = # p ⁡ 6 − 1
7 6m1e5 ⊢ 6 − 1 = 5
8 7 fveq2i ⊢ # p ⁡ 6 − 1 = # p ⁡ 5
9 prmo5 ⊢ # p ⁡ 5 = 30
10 8 9 eqtri ⊢ # p ⁡ 6 − 1 = 30
11 6 10 eqtri ⊢ # p ⁡ 6 = 30