Metamath Proof Explorer

Theorem lgsval4a

Description: Same as lgsval4 for positive N . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis lgsval4.1 
|- F = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) )
Assertion lgsval4a 
|- ( ( A e. ZZ /\ N e. NN ) -> ( A /L N ) = ( seq 1 ( x. , F ) ` N ) )

Proof

Step Hyp Ref Expression
1 lgsval4.1 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) )
2 simpl 
 |-  ( ( A e. ZZ /\ N e. NN ) -> A e. ZZ )
3 nnz 
 |-  ( N e. NN -> N e. ZZ )
4 3 adantl 
 |-  ( ( A e. ZZ /\ N e. NN ) -> N e. ZZ )
5 nnne0 
 |-  ( N e. NN -> N =/= 0 )
6 5 adantl 
 |-  ( ( A e. ZZ /\ N e. NN ) -> N =/= 0 )
7 1 lgsval4 
 |-  ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( A /L N ) = ( if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , F ) ` ( abs ` N ) ) ) )
8 2 4 6 7 syl3anc 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( A /L N ) = ( if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , F ) ` ( abs ` N ) ) ) )
9 nngt0 
 |-  ( N e. NN -> 0 < N )
10 9 adantl 
 |-  ( ( A e. ZZ /\ N e. NN ) -> 0 < N )
11 0re 
 |-  0 e. RR
12 nnre 
 |-  ( N e. NN -> N e. RR )
13 12 adantl 
 |-  ( ( A e. ZZ /\ N e. NN ) -> N e. RR )
14 ltnsym 
 |-  ( ( 0 e. RR /\ N e. RR ) -> ( 0 < N -> -. N < 0 ) )
15 11 13 14 sylancr 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( 0 < N -> -. N < 0 ) )
16 10 15 mpd 
 |-  ( ( A e. ZZ /\ N e. NN ) -> -. N < 0 )
17 16 intnanrd 
 |-  ( ( A e. ZZ /\ N e. NN ) -> -. ( N < 0 /\ A < 0 ) )
18 17 iffalsed 
 |-  ( ( A e. ZZ /\ N e. NN ) -> if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) = 1 )
19 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
20 19 adantl 
 |-  ( ( A e. ZZ /\ N e. NN ) -> N e. NN0 )
21 20 nn0ge0d 
 |-  ( ( A e. ZZ /\ N e. NN ) -> 0 <_ N )
22 13 21 absidd 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( abs ` N ) = N )
23 22 fveq2d 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( seq 1 ( x. , F ) ` ( abs ` N ) ) = ( seq 1 ( x. , F ) ` N ) )
24 18 23 oveq12d 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , F ) ` ( abs ` N ) ) ) = ( 1 x. ( seq 1 ( x. , F ) ` N ) ) )
25 simpr 
 |-  ( ( A e. ZZ /\ N e. NN ) -> N e. NN )
26 nnuz 
 |-  NN = ( ZZ>= ` 1 )
27 25 26 eleqtrdi 
 |-  ( ( A e. ZZ /\ N e. NN ) -> N e. ( ZZ>= ` 1 ) )
28 1 lgsfcl3 
 |-  ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> F : NN --> ZZ )
29 2 4 6 28 syl3anc 
 |-  ( ( A e. ZZ /\ N e. NN ) -> F : NN --> ZZ )
30 elfznn 
 |-  ( x e. ( 1 ... N ) -> x e. NN )
31 ffvelrn 
 |-  ( ( F : NN --> ZZ /\ x e. NN ) -> ( F ` x ) e. ZZ )
32 29 30 31 syl2an 
 |-  ( ( ( A e. ZZ /\ N e. NN ) /\ x e. ( 1 ... N ) ) -> ( F ` x ) e. ZZ )
33 zmulcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x x. y ) e. ZZ )
34 33 adantl 
 |-  ( ( ( A e. ZZ /\ N e. NN ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x x. y ) e. ZZ )
35 27 32 34 seqcl 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( seq 1 ( x. , F ) ` N ) e. ZZ )
36 35 zcnd 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( seq 1 ( x. , F ) ` N ) e. CC )
37 36 mulid2d 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( 1 x. ( seq 1 ( x. , F ) ` N ) ) = ( seq 1 ( x. , F ) ` N ) )
38 8 24 37 3eqtrd 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( A /L N ) = ( seq 1 ( x. , F ) ` N ) )