Metamath Proof Explorer

Theorem prmo4

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

Ref Expression
Assertion prmo4 ⊢ # p ⁡ 4 = 6

Proof

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