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 ` ; 1 0 ) = ; ; 2 1 0

Proof

Step Hyp Ref Expression
1 10nn
 |-  ; 1 0 e. NN
2 prmonn2
 |-  ( ; 1 0 e. NN -> ( #p ` ; 1 0 ) = if ( ; 1 0 e. Prime , ( ( #p ` ( ; 1 0 - 1 ) ) x. ; 1 0 ) , ( #p ` ( ; 1 0 - 1 ) ) ) )
3 1 2 ax-mp
 |-  ( #p ` ; 1 0 ) = if ( ; 1 0 e. Prime , ( ( #p ` ( ; 1 0 - 1 ) ) x. ; 1 0 ) , ( #p ` ( ; 1 0 - 1 ) ) )
4 10nprm
 |-  -. ; 1 0 e. Prime
5 4 iffalsei
 |-  if ( ; 1 0 e. Prime , ( ( #p ` ( ; 1 0 - 1 ) ) x. ; 1 0 ) , ( #p ` ( ; 1 0 - 1 ) ) ) = ( #p ` ( ; 1 0 - 1 ) )
6 3 5 eqtri
 |-  ( #p ` ; 1 0 ) = ( #p ` ( ; 1 0 - 1 ) )
7 10m1e9
 |-  ( ; 1 0 - 1 ) = 9
8 7 fveq2i
 |-  ( #p ` ( ; 1 0 - 1 ) ) = ( #p ` 9 )
9 9nn
 |-  9 e. NN
10 prmonn2
 |-  ( 9 e. NN -> ( #p ` 9 ) = if ( 9 e. Prime , ( ( #p ` ( 9 - 1 ) ) x. 9 ) , ( #p ` ( 9 - 1 ) ) ) )
11 9 10 ax-mp
 |-  ( #p ` 9 ) = if ( 9 e. Prime , ( ( #p ` ( 9 - 1 ) ) x. 9 ) , ( #p ` ( 9 - 1 ) ) )
12 9nprm
 |-  -. 9 e. Prime
13 12 iffalsei
 |-  if ( 9 e. Prime , ( ( #p ` ( 9 - 1 ) ) x. 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 e. NN
18 prmonn2
 |-  ( 8 e. NN -> ( #p ` 8 ) = if ( 8 e. Prime , ( ( #p ` ( 8 - 1 ) ) x. 8 ) , ( #p ` ( 8 - 1 ) ) ) )
19 17 18 ax-mp
 |-  ( #p ` 8 ) = if ( 8 e. Prime , ( ( #p ` ( 8 - 1 ) ) x. 8 ) , ( #p ` ( 8 - 1 ) ) )
20 8nprm
 |-  -. 8 e. Prime
21 20 iffalsei
 |-  if ( 8 e. Prime , ( ( #p ` ( 8 - 1 ) ) x. 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 e. NN
26 prmonn2
 |-  ( 7 e. NN -> ( #p ` 7 ) = if ( 7 e. Prime , ( ( #p ` ( 7 - 1 ) ) x. 7 ) , ( #p ` ( 7 - 1 ) ) ) )
27 25 26 ax-mp
 |-  ( #p ` 7 ) = if ( 7 e. Prime , ( ( #p ` ( 7 - 1 ) ) x. 7 ) , ( #p ` ( 7 - 1 ) ) )
28 7prm
 |-  7 e. Prime
29 28 iftruei
 |-  if ( 7 e. Prime , ( ( #p ` ( 7 - 1 ) ) x. 7 ) , ( #p ` ( 7 - 1 ) ) ) = ( ( #p ` ( 7 - 1 ) ) x. 7 )
30 7nn0
 |-  7 e. NN0
31 3nn0
 |-  3 e. NN0
32 0nn0
 |-  0 e. NN0
33 7m1e6
 |-  ( 7 - 1 ) = 6
34 33 fveq2i
 |-  ( #p ` ( 7 - 1 ) ) = ( #p ` 6 )
35 prmo6
 |-  ( #p ` 6 ) = ; 3 0
36 34 35 eqtri
 |-  ( #p ` ( 7 - 1 ) ) = ; 3 0
37 7cn
 |-  7 e. CC
38 3cn
 |-  3 e. CC
39 7t3e21
 |-  ( 7 x. 3 ) = ; 2 1
40 37 38 39 mulcomli
 |-  ( 3 x. 7 ) = ; 2 1
41 37 mul02i
 |-  ( 0 x. 7 ) = 0
42 30 31 32 36 40 41 decmul1
 |-  ( ( #p ` ( 7 - 1 ) ) x. 7 ) = ; ; 2 1 0
43 27 29 42 3eqtri
 |-  ( #p ` 7 ) = ; ; 2 1 0
44 22 24 43 3eqtri
 |-  ( #p ` 8 ) = ; ; 2 1 0
45 14 16 44 3eqtri
 |-  ( #p ` 9 ) = ; ; 2 1 0
46 6 8 45 3eqtri
 |-  ( #p ` ; 1 0 ) = ; ; 2 1 0