This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℕ
2 prmonn2 ⊢ ( 1 0 ∈ ℕ → ( #p ‘ 1 0 ) = if ( 1 0 ∈ ℙ , ( ( #p ‘ ( 1 0 − 1 ) ) · 1 0 ) , ( #p ‘ ( 1 0 − 1 ) ) ) )
3 1 2 ax-mp ⊢ ( #p ‘ 1 0 ) = if ( 1 0 ∈ ℙ , ( ( #p ‘ ( 1 0 − 1 ) ) · 1 0 ) , ( #p ‘ ( 1 0 − 1 ) ) )
4 10nprm ⊢ ¬ 1 0 ∈ ℙ
5 4 iffalsei ⊢ if ( 1 0 ∈ ℙ , ( ( #p ‘ ( 1 0 − 1 ) ) · 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 ∈ ℕ
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 ) = 3 0
36 34 35 eqtri ⊢ ( #p ‘ ( 7 − 1 ) ) = 3 0
37 7cn ⊢ 7 ∈ ℂ
38 3cn ⊢ 3 ∈ ℂ
39 7t3e21 ⊢ ( 7 · 3 ) = 2 1
40 37 38 39 mulcomli ⊢ ( 3 · 7 ) = 2 1
41 37 mul02i ⊢ ( 0 · 7 ) = 0
42 30 31 32 36 40 41 decmul1 ⊢ ( ( #p ‘ ( 7 − 1 ) ) · 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