# Metamath Proof Explorer

## Theorem ex-prmo

Description: Example for df-prmo : ( #p1 0 ) = 2 x. 3 x. 5 x. 7 . (Contributed by AV, 6-Sep-2021)

Ref Expression
Assertion ex-prmo ${⊢}{#}_{p}\left(10\right)=210$

### Proof

Step Hyp Ref Expression
1 10nn ${⊢}10\in ℕ$
2 prmonn2 ${⊢}10\in ℕ\to {#}_{p}\left(10\right)=if\left(10\in ℙ,{#}_{p}\left(10-1\right)\cdot 10,{#}_{p}\left(10-1\right)\right)$
3 1 2 ax-mp ${⊢}{#}_{p}\left(10\right)=if\left(10\in ℙ,{#}_{p}\left(10-1\right)\cdot 10,{#}_{p}\left(10-1\right)\right)$
4 10nprm ${⊢}¬10\in ℙ$
5 4 iffalsei ${⊢}if\left(10\in ℙ,{#}_{p}\left(10-1\right)\cdot 10,{#}_{p}\left(10-1\right)\right)={#}_{p}\left(10-1\right)$
6 3 5 eqtri ${⊢}{#}_{p}\left(10\right)={#}_{p}\left(10-1\right)$
7 10m1e9 ${⊢}10-1=9$
8 7 fveq2i ${⊢}{#}_{p}\left(10-1\right)={#}_{p}\left(9\right)$
9 9nn ${⊢}9\in ℕ$
10 prmonn2 ${⊢}9\in ℕ\to {#}_{p}\left(9\right)=if\left(9\in ℙ,{#}_{p}\left(9-1\right)\cdot 9,{#}_{p}\left(9-1\right)\right)$
11 9 10 ax-mp ${⊢}{#}_{p}\left(9\right)=if\left(9\in ℙ,{#}_{p}\left(9-1\right)\cdot 9,{#}_{p}\left(9-1\right)\right)$
12 9nprm ${⊢}¬9\in ℙ$
13 12 iffalsei ${⊢}if\left(9\in ℙ,{#}_{p}\left(9-1\right)\cdot 9,{#}_{p}\left(9-1\right)\right)={#}_{p}\left(9-1\right)$
14 11 13 eqtri ${⊢}{#}_{p}\left(9\right)={#}_{p}\left(9-1\right)$
15 9m1e8 ${⊢}9-1=8$
16 15 fveq2i ${⊢}{#}_{p}\left(9-1\right)={#}_{p}\left(8\right)$
17 8nn ${⊢}8\in ℕ$
18 prmonn2 ${⊢}8\in ℕ\to {#}_{p}\left(8\right)=if\left(8\in ℙ,{#}_{p}\left(8-1\right)\cdot 8,{#}_{p}\left(8-1\right)\right)$
19 17 18 ax-mp ${⊢}{#}_{p}\left(8\right)=if\left(8\in ℙ,{#}_{p}\left(8-1\right)\cdot 8,{#}_{p}\left(8-1\right)\right)$
20 8nprm ${⊢}¬8\in ℙ$
21 20 iffalsei ${⊢}if\left(8\in ℙ,{#}_{p}\left(8-1\right)\cdot 8,{#}_{p}\left(8-1\right)\right)={#}_{p}\left(8-1\right)$
22 19 21 eqtri ${⊢}{#}_{p}\left(8\right)={#}_{p}\left(8-1\right)$
23 8m1e7 ${⊢}8-1=7$
24 23 fveq2i ${⊢}{#}_{p}\left(8-1\right)={#}_{p}\left(7\right)$
25 7nn ${⊢}7\in ℕ$
26 prmonn2 ${⊢}7\in ℕ\to {#}_{p}\left(7\right)=if\left(7\in ℙ,{#}_{p}\left(7-1\right)\cdot 7,{#}_{p}\left(7-1\right)\right)$
27 25 26 ax-mp ${⊢}{#}_{p}\left(7\right)=if\left(7\in ℙ,{#}_{p}\left(7-1\right)\cdot 7,{#}_{p}\left(7-1\right)\right)$
28 7prm ${⊢}7\in ℙ$
29 28 iftruei ${⊢}if\left(7\in ℙ,{#}_{p}\left(7-1\right)\cdot 7,{#}_{p}\left(7-1\right)\right)={#}_{p}\left(7-1\right)\cdot 7$
30 7nn0 ${⊢}7\in {ℕ}_{0}$
31 3nn0 ${⊢}3\in {ℕ}_{0}$
32 0nn0 ${⊢}0\in {ℕ}_{0}$
33 7m1e6 ${⊢}7-1=6$
34 33 fveq2i ${⊢}{#}_{p}\left(7-1\right)={#}_{p}\left(6\right)$
35 prmo6 ${⊢}{#}_{p}\left(6\right)=30$
36 34 35 eqtri ${⊢}{#}_{p}\left(7-1\right)=30$
37 7cn ${⊢}7\in ℂ$
38 3cn ${⊢}3\in ℂ$
39 7t3e21 ${⊢}7\cdot 3=21$
40 37 38 39 mulcomli ${⊢}3\cdot 7=21$
41 37 mul02i ${⊢}0\cdot 7=0$
42 30 31 32 36 40 41 decmul1 ${⊢}{#}_{p}\left(7-1\right)\cdot 7=210$
43 27 29 42 3eqtri ${⊢}{#}_{p}\left(7\right)=210$
44 22 24 43 3eqtri ${⊢}{#}_{p}\left(8\right)=210$
45 14 16 44 3eqtri ${⊢}{#}_{p}\left(9\right)=210$
46 6 8 45 3eqtri ${⊢}{#}_{p}\left(10\right)=210$