Metamath Proof Explorer


Theorem lgsdilem2

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

Ref Expression
Hypotheses lgsdilem2.1 φ A
lgsdilem2.2 φ M
lgsdilem2.3 φ N
lgsdilem2.4 φ M 0
lgsdilem2.5 φ N 0
lgsdilem2.6 F = n if n A / L n n pCnt M 1
Assertion lgsdilem2 φ seq 1 × F M = seq 1 × F M N

Proof

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