Metamath Proof Explorer

Theorem 1arithlem4

Description: Lemma for 1arith . (Contributed by Mario Carneiro, 30-May-2014)

Ref Expression
Hypotheses 1arith.1 
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )
1arithlem4.2 
|- G = ( y e. NN |-> if ( y e. Prime , ( y ^ ( F ` y ) ) , 1 ) )
1arithlem4.3 
|- ( ph -> F : Prime --> NN0 )
1arithlem4.4 
|- ( ph -> N e. NN )
1arithlem4.5 
|- ( ( ph /\ ( q e. Prime /\ N <_ q ) ) -> ( F ` q ) = 0 )
Assertion 1arithlem4 
|- ( ph -> E. x e. NN F = ( M ` x ) )

Proof

Step Hyp Ref Expression
1 1arith.1 
 |-  M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )
2 1arithlem4.2 
 |-  G = ( y e. NN |-> if ( y e. Prime , ( y ^ ( F ` y ) ) , 1 ) )
3 1arithlem4.3 
 |-  ( ph -> F : Prime --> NN0 )
4 1arithlem4.4 
 |-  ( ph -> N e. NN )
5 1arithlem4.5 
 |-  ( ( ph /\ ( q e. Prime /\ N <_ q ) ) -> ( F ` q ) = 0 )
6 3 ffvelrnda 
 |-  ( ( ph /\ y e. Prime ) -> ( F ` y ) e. NN0 )
7 6 ralrimiva 
 |-  ( ph -> A. y e. Prime ( F ` y ) e. NN0 )
8 2 7 pcmptcl 
 |-  ( ph -> ( G : NN --> NN /\ seq 1 ( x. , G ) : NN --> NN ) )
9 8 simprd 
 |-  ( ph -> seq 1 ( x. , G ) : NN --> NN )
10 9 4 ffvelrnd 
 |-  ( ph -> ( seq 1 ( x. , G ) ` N ) e. NN )
11 1 1arithlem2 
 |-  ( ( ( seq 1 ( x. , G ) ` N ) e. NN /\ q e. Prime ) -> ( ( M ` ( seq 1 ( x. , G ) ` N ) ) ` q ) = ( q pCnt ( seq 1 ( x. , G ) ` N ) ) )
12 10 11 sylan 
 |-  ( ( ph /\ q e. Prime ) -> ( ( M ` ( seq 1 ( x. , G ) ` N ) ) ` q ) = ( q pCnt ( seq 1 ( x. , G ) ` N ) ) )
13 7 adantr 
 |-  ( ( ph /\ q e. Prime ) -> A. y e. Prime ( F ` y ) e. NN0 )
14 4 adantr 
 |-  ( ( ph /\ q e. Prime ) -> N e. NN )
15 simpr 
 |-  ( ( ph /\ q e. Prime ) -> q e. Prime )
16 fveq2 
 |-  ( y = q -> ( F ` y ) = ( F ` q ) )
17 2 13 14 15 16 pcmpt 
 |-  ( ( ph /\ q e. Prime ) -> ( q pCnt ( seq 1 ( x. , G ) ` N ) ) = if ( q <_ N , ( F ` q ) , 0 ) )
18 14 nnred 
 |-  ( ( ph /\ q e. Prime ) -> N e. RR )
19 prmz 
 |-  ( q e. Prime -> q e. ZZ )
20 19 zred 
 |-  ( q e. Prime -> q e. RR )
21 20 adantl 
 |-  ( ( ph /\ q e. Prime ) -> q e. RR )
22 5 anassrs 
 |-  ( ( ( ph /\ q e. Prime ) /\ N <_ q ) -> ( F ` q ) = 0 )
23 22 ifeq2d 
 |-  ( ( ( ph /\ q e. Prime ) /\ N <_ q ) -> if ( q <_ N , ( F ` q ) , ( F ` q ) ) = if ( q <_ N , ( F ` q ) , 0 ) )
24 ifid 
 |-  if ( q <_ N , ( F ` q ) , ( F ` q ) ) = ( F ` q )
25 23 24 eqtr3di 
 |-  ( ( ( ph /\ q e. Prime ) /\ N <_ q ) -> if ( q <_ N , ( F ` q ) , 0 ) = ( F ` q ) )
26 iftrue 
 |-  ( q <_ N -> if ( q <_ N , ( F ` q ) , 0 ) = ( F ` q ) )
27 26 adantl 
 |-  ( ( ( ph /\ q e. Prime ) /\ q <_ N ) -> if ( q <_ N , ( F ` q ) , 0 ) = ( F ` q ) )
28 18 21 25 27 lecasei 
 |-  ( ( ph /\ q e. Prime ) -> if ( q <_ N , ( F ` q ) , 0 ) = ( F ` q ) )
29 12 17 28 3eqtrrd 
 |-  ( ( ph /\ q e. Prime ) -> ( F ` q ) = ( ( M ` ( seq 1 ( x. , G ) ` N ) ) ` q ) )
30 29 ralrimiva 
 |-  ( ph -> A. q e. Prime ( F ` q ) = ( ( M ` ( seq 1 ( x. , G ) ` N ) ) ` q ) )
31 1 1arithlem3 
 |-  ( ( seq 1 ( x. , G ) ` N ) e. NN -> ( M ` ( seq 1 ( x. , G ) ` N ) ) : Prime --> NN0 )
32 10 31 syl 
 |-  ( ph -> ( M ` ( seq 1 ( x. , G ) ` N ) ) : Prime --> NN0 )
33 ffn 
 |-  ( F : Prime --> NN0 -> F Fn Prime )
34 ffn 
 |-  ( ( M ` ( seq 1 ( x. , G ) ` N ) ) : Prime --> NN0 -> ( M ` ( seq 1 ( x. , G ) ` N ) ) Fn Prime )
35 eqfnfv 
 |-  ( ( F Fn Prime /\ ( M ` ( seq 1 ( x. , G ) ` N ) ) Fn Prime ) -> ( F = ( M ` ( seq 1 ( x. , G ) ` N ) ) <-> A. q e. Prime ( F ` q ) = ( ( M ` ( seq 1 ( x. , G ) ` N ) ) ` q ) ) )
36 33 34 35 syl2an 
 |-  ( ( F : Prime --> NN0 /\ ( M ` ( seq 1 ( x. , G ) ` N ) ) : Prime --> NN0 ) -> ( F = ( M ` ( seq 1 ( x. , G ) ` N ) ) <-> A. q e. Prime ( F ` q ) = ( ( M ` ( seq 1 ( x. , G ) ` N ) ) ` q ) ) )
37 3 32 36 syl2anc 
 |-  ( ph -> ( F = ( M ` ( seq 1 ( x. , G ) ` N ) ) <-> A. q e. Prime ( F ` q ) = ( ( M ` ( seq 1 ( x. , G ) ` N ) ) ` q ) ) )
38 30 37 mpbird 
 |-  ( ph -> F = ( M ` ( seq 1 ( x. , G ) ` N ) ) )
39 fveq2 
 |-  ( x = ( seq 1 ( x. , G ) ` N ) -> ( M ` x ) = ( M ` ( seq 1 ( x. , G ) ` N ) ) )
40 39 rspceeqv 
 |-  ( ( ( seq 1 ( x. , G ) ` N ) e. NN /\ F = ( M ` ( seq 1 ( x. , G ) ` N ) ) ) -> E. x e. NN F = ( M ` x ) )
41 10 38 40 syl2anc 
 |-  ( ph -> E. x e. NN F = ( M ` x ) )