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 |