Metamath Proof Explorer

Theorem prmo5

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

Ref Expression
Assertion prmo5 ⊢ # p ⁡ 5 = 30

Proof

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