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 ⁡ 10 = 210

Proof

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