Metamath Proof Explorer

Theorem lgsdilem2

Description: Lemma for lgsdi . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypotheses lgsdilem2.1 
|- ( ph -> A e. ZZ )
lgsdilem2.2 
|- ( ph -> M e. ZZ )
lgsdilem2.3 
|- ( ph -> N e. ZZ )
lgsdilem2.4 
|- ( ph -> M =/= 0 )
lgsdilem2.5 
|- ( ph -> N =/= 0 )
lgsdilem2.6 
|- F = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) )
Assertion lgsdilem2 
|- ( ph -> ( seq 1 ( x. , F ) ` ( abs ` M ) ) = ( seq 1 ( x. , F ) ` ( abs ` ( M x. N ) ) ) )

Proof

Step Hyp Ref Expression
1 lgsdilem2.1 
 |-  ( ph -> A e. ZZ )
2 lgsdilem2.2 
 |-  ( ph -> M e. ZZ )
3 lgsdilem2.3 
 |-  ( ph -> N e. ZZ )
4 lgsdilem2.4 
 |-  ( ph -> M =/= 0 )
5 lgsdilem2.5 
 |-  ( ph -> N =/= 0 )
6 lgsdilem2.6 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) )
7 mulrid 
 |-  ( k e. CC -> ( k x. 1 ) = k )
8 7 adantl 
 |-  ( ( ph /\ k e. CC ) -> ( k x. 1 ) = k )
9 nnabscl 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( abs ` M ) e. NN )
10 2 4 9 syl2anc 
 |-  ( ph -> ( abs ` M ) e. NN )
11 nnuz 
 |-  NN = ( ZZ>= ` 1 )
12 10 11 eleqtrdi 
 |-  ( ph -> ( abs ` M ) e. ( ZZ>= ` 1 ) )
13 10 nnzd 
 |-  ( ph -> ( abs ` M ) e. ZZ )
14 2 3 zmulcld 
 |-  ( ph -> ( M x. N ) e. ZZ )
15 2 zcnd 
 |-  ( ph -> M e. CC )
16 3 zcnd 
 |-  ( ph -> N e. CC )
17 15 16 4 5 mulne0d 
 |-  ( ph -> ( M x. N ) =/= 0 )
18 nnabscl 
 |-  ( ( ( M x. N ) e. ZZ /\ ( M x. N ) =/= 0 ) -> ( abs ` ( M x. N ) ) e. NN )
19 14 17 18 syl2anc 
 |-  ( ph -> ( abs ` ( M x. N ) ) e. NN )
20 19 nnzd 
 |-  ( ph -> ( abs ` ( M x. N ) ) e. ZZ )
21 15 abscld 
 |-  ( ph -> ( abs ` M ) e. RR )
22 16 abscld 
 |-  ( ph -> ( abs ` N ) e. RR )
23 15 absge0d 
 |-  ( ph -> 0 <_ ( abs ` M ) )
24 nnabscl 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN )
25 3 5 24 syl2anc 
 |-  ( ph -> ( abs ` N ) e. NN )
26 25 nnge1d 
 |-  ( ph -> 1 <_ ( abs ` N ) )
27 21 22 23 26 lemulge11d 
 |-  ( ph -> ( abs ` M ) <_ ( ( abs ` M ) x. ( abs ` N ) ) )
28 15 16 absmuld 
 |-  ( ph -> ( abs ` ( M x. N ) ) = ( ( abs ` M ) x. ( abs ` N ) ) )
29 27 28 breqtrrd 
 |-  ( ph -> ( abs ` M ) <_ ( abs ` ( M x. N ) ) )
30 eluz2 
 |-  ( ( abs ` ( M x. N ) ) e. ( ZZ>= ` ( abs ` M ) ) <-> ( ( abs ` M ) e. ZZ /\ ( abs ` ( M x. N ) ) e. ZZ /\ ( abs ` M ) <_ ( abs ` ( M x. N ) ) ) )
31 13 20 29 30 syl3anbrc 
 |-  ( ph -> ( abs ` ( M x. N ) ) e. ( ZZ>= ` ( abs ` M ) ) )
32 6 lgsfcl3 
 |-  ( ( A e. ZZ /\ M e. ZZ /\ M =/= 0 ) -> F : NN --> ZZ )
33 1 2 4 32 syl3anc 
 |-  ( ph -> F : NN --> ZZ )
34 elfznn 
 |-  ( k e. ( 1 ... ( abs ` M ) ) -> k e. NN )
35 ffvelcdm 
 |-  ( ( F : NN --> ZZ /\ k e. NN ) -> ( F ` k ) e. ZZ )
36 33 34 35 syl2an 
 |-  ( ( ph /\ k e. ( 1 ... ( abs ` M ) ) ) -> ( F ` k ) e. ZZ )
37 36 zcnd 
 |-  ( ( ph /\ k e. ( 1 ... ( abs ` M ) ) ) -> ( F ` k ) e. CC )
38 mulcl 
 |-  ( ( k e. CC /\ x e. CC ) -> ( k x. x ) e. CC )
39 38 adantl 
 |-  ( ( ph /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
40 12 37 39 seqcl 
 |-  ( ph -> ( seq 1 ( x. , F ) ` ( abs ` M ) ) e. CC )
41 10 peano2nnd 
 |-  ( ph -> ( ( abs ` M ) + 1 ) e. NN )
42 elfzuz 
 |-  ( k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) -> k e. ( ZZ>= ` ( ( abs ` M ) + 1 ) ) )
43 eluznn 
 |-  ( ( ( ( abs ` M ) + 1 ) e. NN /\ k e. ( ZZ>= ` ( ( abs ` M ) + 1 ) ) ) -> k e. NN )
44 41 42 43 syl2an 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> k e. NN )
45 eleq1w 
 |-  ( n = k -> ( n e. Prime <-> k e. Prime ) )
46 oveq2 
 |-  ( n = k -> ( A /L n ) = ( A /L k ) )
47 oveq1 
 |-  ( n = k -> ( n pCnt M ) = ( k pCnt M ) )
48 46 47 oveq12d 
 |-  ( n = k -> ( ( A /L n ) ^ ( n pCnt M ) ) = ( ( A /L k ) ^ ( k pCnt M ) ) )
49 45 48 ifbieq1d 
 |-  ( n = k -> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) )
50 ovex 
 |-  ( ( A /L k ) ^ ( k pCnt M ) ) e. _V
51 1ex 
 |-  1 e. _V
52 50 51 ifex 
 |-  if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) e. _V
53 49 6 52 fvmpt 
 |-  ( k e. NN -> ( F ` k ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) )
54 44 53 syl 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> ( F ` k ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) )
55 simpr 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> k e. Prime )
56 2 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> M e. ZZ )
57 zq 
 |-  ( M e. ZZ -> M e. QQ )
58 56 57 syl 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> M e. QQ )
59 pcabs 
 |-  ( ( k e. Prime /\ M e. QQ ) -> ( k pCnt ( abs ` M ) ) = ( k pCnt M ) )
60 55 58 59 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( k pCnt ( abs ` M ) ) = ( k pCnt M ) )
61 elfzle1 
 |-  ( k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) -> ( ( abs ` M ) + 1 ) <_ k )
62 61 adantl 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> ( ( abs ` M ) + 1 ) <_ k )
63 elfzelz 
 |-  ( k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) -> k e. ZZ )
64 zltp1le 
 |-  ( ( ( abs ` M ) e. ZZ /\ k e. ZZ ) -> ( ( abs ` M ) < k <-> ( ( abs ` M ) + 1 ) <_ k ) )
65 13 63 64 syl2an 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> ( ( abs ` M ) < k <-> ( ( abs ` M ) + 1 ) <_ k ) )
66 62 65 mpbird 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> ( abs ` M ) < k )
67 21 adantr 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> ( abs ` M ) e. RR )
68 63 adantl 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> k e. ZZ )
69 68 zred 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> k e. RR )
70 67 69 ltnled 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> ( ( abs ` M ) < k <-> -. k <_ ( abs ` M ) ) )
71 66 70 mpbid 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> -. k <_ ( abs ` M ) )
72 71 adantr 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> -. k <_ ( abs ` M ) )
73 prmz 
 |-  ( k e. Prime -> k e. ZZ )
74 73 adantl 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> k e. ZZ )
75 4 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> M =/= 0 )
76 56 75 9 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( abs ` M ) e. NN )
77 dvdsle 
 |-  ( ( k e. ZZ /\ ( abs ` M ) e. NN ) -> ( k || ( abs ` M ) -> k <_ ( abs ` M ) ) )
78 74 76 77 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( k || ( abs ` M ) -> k <_ ( abs ` M ) ) )
79 72 78 mtod 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> -. k || ( abs ` M ) )
80 pceq0 
 |-  ( ( k e. Prime /\ ( abs ` M ) e. NN ) -> ( ( k pCnt ( abs ` M ) ) = 0 <-> -. k || ( abs ` M ) ) )
81 55 76 80 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( ( k pCnt ( abs ` M ) ) = 0 <-> -. k || ( abs ` M ) ) )
82 79 81 mpbird 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( k pCnt ( abs ` M ) ) = 0 )
83 60 82 eqtr3d 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( k pCnt M ) = 0 )
84 83 oveq2d 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( ( A /L k ) ^ ( k pCnt M ) ) = ( ( A /L k ) ^ 0 ) )
85 1 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> A e. ZZ )
86 lgscl 
 |-  ( ( A e. ZZ /\ k e. ZZ ) -> ( A /L k ) e. ZZ )
87 85 74 86 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( A /L k ) e. ZZ )
88 87 zcnd 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( A /L k ) e. CC )
89 88 exp0d 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( ( A /L k ) ^ 0 ) = 1 )
90 84 89 eqtrd 
 |-  ( ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( ( A /L k ) ^ ( k pCnt M ) ) = 1 )
91 90 ifeq1da 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) = if ( k e. Prime , 1 , 1 ) )
92 ifid 
 |-  if ( k e. Prime , 1 , 1 ) = 1
93 91 92 eqtrdi 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) = 1 )
94 54 93 eqtrd 
 |-  ( ( ph /\ k e. ( ( ( abs ` M ) + 1 ) ... ( abs ` ( M x. N ) ) ) ) -> ( F ` k ) = 1 )
95 8 12 31 40 94 seqid2 
 |-  ( ph -> ( seq 1 ( x. , F ) ` ( abs ` M ) ) = ( seq 1 ( x. , F ) ` ( abs ` ( M x. N ) ) ) )