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=if10∈ℙ#p⁡10−1⋅10#p⁡10−1
3 1 2 ax-mp ⊢#p⁡10=if10∈ℙ#p⁡10−1⋅10#p⁡10−1
4 10nprm ⊢¬10∈ℙ
5 4 iffalsei ⊢if10∈ℙ#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=if9∈ℙ#p⁡9−1⋅9#p⁡9−1
11 9 10 ax-mp ⊢#p⁡9=if9∈ℙ#p⁡9−1⋅9#p⁡9−1
12 9nprm ⊢¬9∈ℙ
13 12 iffalsei ⊢if9∈ℙ#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=if8∈ℙ#p⁡8−1⋅8#p⁡8−1
19 17 18 ax-mp ⊢#p⁡8=if8∈ℙ#p⁡8−1⋅8#p⁡8−1
20 8nprm ⊢¬8∈ℙ
21 20 iffalsei ⊢if8∈ℙ#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=if7∈ℙ#p⁡7−1⋅7#p⁡7−1
27 25 26 ax-mp ⊢#p⁡7=if7∈ℙ#p⁡7−1⋅7#p⁡7−1
28 7prm ⊢7∈ℙ
29 28 iftruei ⊢if7∈ℙ#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