Metamath Proof Explorer


Theorem lgsval4a

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

Ref Expression
Hypothesis lgsval4.1 โŠข ๐น = ( ๐‘› โˆˆ โ„• โ†ฆ if ( ๐‘› โˆˆ โ„™ , ( ( ๐ด /L ๐‘› ) โ†‘ ( ๐‘› pCnt ๐‘ ) ) , 1 ) )
Assertion lgsval4a ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ( ๐ด /L ๐‘ ) = ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ ) )

Proof

Step Hyp Ref Expression
1 lgsval4.1 โŠข ๐น = ( ๐‘› โˆˆ โ„• โ†ฆ if ( ๐‘› โˆˆ โ„™ , ( ( ๐ด /L ๐‘› ) โ†‘ ( ๐‘› pCnt ๐‘ ) ) , 1 ) )
2 simpl โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ๐ด โˆˆ โ„ค )
3 nnz โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ค )
4 3 adantl โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ๐‘ โˆˆ โ„ค )
5 nnne0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โ‰  0 )
6 5 adantl โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ๐‘ โ‰  0 )
7 1 lgsval4 โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0 ) โ†’ ( ๐ด /L ๐‘ ) = ( if ( ( ๐‘ < 0 โˆง ๐ด < 0 ) , - 1 , 1 ) ยท ( seq 1 ( ยท , ๐น ) โ€˜ ( abs โ€˜ ๐‘ ) ) ) )
8 2 4 6 7 syl3anc โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ( ๐ด /L ๐‘ ) = ( if ( ( ๐‘ < 0 โˆง ๐ด < 0 ) , - 1 , 1 ) ยท ( seq 1 ( ยท , ๐น ) โ€˜ ( abs โ€˜ ๐‘ ) ) ) )
9 nngt0 โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 < ๐‘ )
10 9 adantl โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ 0 < ๐‘ )
11 0re โŠข 0 โˆˆ โ„
12 nnre โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ )
13 12 adantl โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ๐‘ โˆˆ โ„ )
14 ltnsym โŠข ( ( 0 โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ ) โ†’ ( 0 < ๐‘ โ†’ ยฌ ๐‘ < 0 ) )
15 11 13 14 sylancr โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ( 0 < ๐‘ โ†’ ยฌ ๐‘ < 0 ) )
16 10 15 mpd โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ยฌ ๐‘ < 0 )
17 16 intnanrd โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ยฌ ( ๐‘ < 0 โˆง ๐ด < 0 ) )
18 17 iffalsed โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ if ( ( ๐‘ < 0 โˆง ๐ด < 0 ) , - 1 , 1 ) = 1 )
19 nnnn0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„•0 )
20 19 adantl โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ๐‘ โˆˆ โ„•0 )
21 20 nn0ge0d โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ 0 โ‰ค ๐‘ )
22 13 21 absidd โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ( abs โ€˜ ๐‘ ) = ๐‘ )
23 22 fveq2d โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( abs โ€˜ ๐‘ ) ) = ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ ) )
24 18 23 oveq12d โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ( if ( ( ๐‘ < 0 โˆง ๐ด < 0 ) , - 1 , 1 ) ยท ( seq 1 ( ยท , ๐น ) โ€˜ ( abs โ€˜ ๐‘ ) ) ) = ( 1 ยท ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ ) ) )
25 simpr โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ๐‘ โˆˆ โ„• )
26 nnuz โŠข โ„• = ( โ„คโ‰ฅ โ€˜ 1 )
27 25 26 eleqtrdi โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) )
28 1 lgsfcl3 โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0 ) โ†’ ๐น : โ„• โŸถ โ„ค )
29 2 4 6 28 syl3anc โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ๐น : โ„• โŸถ โ„ค )
30 elfznn โŠข ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) โ†’ ๐‘ฅ โˆˆ โ„• )
31 ffvelcdm โŠข ( ( ๐น : โ„• โŸถ โ„ค โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐น โ€˜ ๐‘ฅ ) โˆˆ โ„ค )
32 29 30 31 syl2an โŠข ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐น โ€˜ ๐‘ฅ ) โˆˆ โ„ค )
33 zmulcl โŠข ( ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ โ„ค )
34 33 adantl โŠข ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ โ„ค )
35 27 32 34 seqcl โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ ) โˆˆ โ„ค )
36 35 zcnd โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ ) โˆˆ โ„‚ )
37 36 mullidd โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ( 1 ยท ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ ) ) = ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ ) )
38 8 24 37 3eqtrd โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„• ) โ†’ ( ๐ด /L ๐‘ ) = ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ ) )