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