Metamath Proof Explorer


Theorem lgsdilem2

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

Ref Expression
Hypotheses lgsdilem2.1 ( 𝜑𝐴 ∈ ℤ )
lgsdilem2.2 ( 𝜑𝑀 ∈ ℤ )
lgsdilem2.3 ( 𝜑𝑁 ∈ ℤ )
lgsdilem2.4 ( 𝜑𝑀 ≠ 0 )
lgsdilem2.5 ( 𝜑𝑁 ≠ 0 )
lgsdilem2.6 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) )
Assertion lgsdilem2 ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑀 ) ) = ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 lgsdilem2.1 ( 𝜑𝐴 ∈ ℤ )
2 lgsdilem2.2 ( 𝜑𝑀 ∈ ℤ )
3 lgsdilem2.3 ( 𝜑𝑁 ∈ ℤ )
4 lgsdilem2.4 ( 𝜑𝑀 ≠ 0 )
5 lgsdilem2.5 ( 𝜑𝑁 ≠ 0 )
6 lgsdilem2.6 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) )
7 mulid1 ( 𝑘 ∈ ℂ → ( 𝑘 · 1 ) = 𝑘 )
8 7 adantl ( ( 𝜑𝑘 ∈ ℂ ) → ( 𝑘 · 1 ) = 𝑘 )
9 nnabscl ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ( abs ‘ 𝑀 ) ∈ ℕ )
10 2 4 9 syl2anc ( 𝜑 → ( abs ‘ 𝑀 ) ∈ ℕ )
11 nnuz ℕ = ( ℤ ‘ 1 )
12 10 11 eleqtrdi ( 𝜑 → ( abs ‘ 𝑀 ) ∈ ( ℤ ‘ 1 ) )
13 10 nnzd ( 𝜑 → ( abs ‘ 𝑀 ) ∈ ℤ )
14 2 3 zmulcld ( 𝜑 → ( 𝑀 · 𝑁 ) ∈ ℤ )
15 2 zcnd ( 𝜑𝑀 ∈ ℂ )
16 3 zcnd ( 𝜑𝑁 ∈ ℂ )
17 15 16 4 5 mulne0d ( 𝜑 → ( 𝑀 · 𝑁 ) ≠ 0 )
18 nnabscl ( ( ( 𝑀 · 𝑁 ) ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ≠ 0 ) → ( abs ‘ ( 𝑀 · 𝑁 ) ) ∈ ℕ )
19 14 17 18 syl2anc ( 𝜑 → ( abs ‘ ( 𝑀 · 𝑁 ) ) ∈ ℕ )
20 19 nnzd ( 𝜑 → ( abs ‘ ( 𝑀 · 𝑁 ) ) ∈ ℤ )
21 15 abscld ( 𝜑 → ( abs ‘ 𝑀 ) ∈ ℝ )
22 16 abscld ( 𝜑 → ( abs ‘ 𝑁 ) ∈ ℝ )
23 15 absge0d ( 𝜑 → 0 ≤ ( abs ‘ 𝑀 ) )
24 nnabscl ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( abs ‘ 𝑁 ) ∈ ℕ )
25 3 5 24 syl2anc ( 𝜑 → ( abs ‘ 𝑁 ) ∈ ℕ )
26 25 nnge1d ( 𝜑 → 1 ≤ ( abs ‘ 𝑁 ) )
27 21 22 23 26 lemulge11d ( 𝜑 → ( abs ‘ 𝑀 ) ≤ ( ( abs ‘ 𝑀 ) · ( abs ‘ 𝑁 ) ) )
28 15 16 absmuld ( 𝜑 → ( abs ‘ ( 𝑀 · 𝑁 ) ) = ( ( abs ‘ 𝑀 ) · ( abs ‘ 𝑁 ) ) )
29 27 28 breqtrrd ( 𝜑 → ( abs ‘ 𝑀 ) ≤ ( abs ‘ ( 𝑀 · 𝑁 ) ) )
30 eluz2 ( ( abs ‘ ( 𝑀 · 𝑁 ) ) ∈ ( ℤ ‘ ( abs ‘ 𝑀 ) ) ↔ ( ( abs ‘ 𝑀 ) ∈ ℤ ∧ ( abs ‘ ( 𝑀 · 𝑁 ) ) ∈ ℤ ∧ ( abs ‘ 𝑀 ) ≤ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )
31 13 20 29 30 syl3anbrc ( 𝜑 → ( abs ‘ ( 𝑀 · 𝑁 ) ) ∈ ( ℤ ‘ ( abs ‘ 𝑀 ) ) )
32 6 lgsfcl3 ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → 𝐹 : ℕ ⟶ ℤ )
33 1 2 4 32 syl3anc ( 𝜑𝐹 : ℕ ⟶ ℤ )
34 elfznn ( 𝑘 ∈ ( 1 ... ( abs ‘ 𝑀 ) ) → 𝑘 ∈ ℕ )
35 ffvelrn ( ( 𝐹 : ℕ ⟶ ℤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) ∈ ℤ )
36 33 34 35 syl2an ( ( 𝜑𝑘 ∈ ( 1 ... ( abs ‘ 𝑀 ) ) ) → ( 𝐹𝑘 ) ∈ ℤ )
37 36 zcnd ( ( 𝜑𝑘 ∈ ( 1 ... ( abs ‘ 𝑀 ) ) ) → ( 𝐹𝑘 ) ∈ ℂ )
38 mulcl ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
39 38 adantl ( ( 𝜑 ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
40 12 37 39 seqcl ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑀 ) ) ∈ ℂ )
41 10 peano2nnd ( 𝜑 → ( ( abs ‘ 𝑀 ) + 1 ) ∈ ℕ )
42 elfzuz ( 𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) → 𝑘 ∈ ( ℤ ‘ ( ( abs ‘ 𝑀 ) + 1 ) ) )
43 eluznn ( ( ( ( abs ‘ 𝑀 ) + 1 ) ∈ ℕ ∧ 𝑘 ∈ ( ℤ ‘ ( ( abs ‘ 𝑀 ) + 1 ) ) ) → 𝑘 ∈ ℕ )
44 41 42 43 syl2an ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → 𝑘 ∈ ℕ )
45 eleq1w ( 𝑛 = 𝑘 → ( 𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ ) )
46 oveq2 ( 𝑛 = 𝑘 → ( 𝐴 /L 𝑛 ) = ( 𝐴 /L 𝑘 ) )
47 oveq1 ( 𝑛 = 𝑘 → ( 𝑛 pCnt 𝑀 ) = ( 𝑘 pCnt 𝑀 ) )
48 46 47 oveq12d ( 𝑛 = 𝑘 → ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) = ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) )
49 45 48 ifbieq1d ( 𝑛 = 𝑘 → if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑀 ) ) , 1 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) )
50 ovex ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) ∈ V
51 1ex 1 ∈ V
52 50 51 ifex if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) ∈ V
53 49 6 52 fvmpt ( 𝑘 ∈ ℕ → ( 𝐹𝑘 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) )
54 44 53 syl ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( 𝐹𝑘 ) = if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) )
55 simpr ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝑘 ∈ ℙ )
56 2 ad2antrr ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝑀 ∈ ℤ )
57 zq ( 𝑀 ∈ ℤ → 𝑀 ∈ ℚ )
58 56 57 syl ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝑀 ∈ ℚ )
59 pcabs ( ( 𝑘 ∈ ℙ ∧ 𝑀 ∈ ℚ ) → ( 𝑘 pCnt ( abs ‘ 𝑀 ) ) = ( 𝑘 pCnt 𝑀 ) )
60 55 58 59 syl2anc ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( 𝑘 pCnt ( abs ‘ 𝑀 ) ) = ( 𝑘 pCnt 𝑀 ) )
61 elfzle1 ( 𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) → ( ( abs ‘ 𝑀 ) + 1 ) ≤ 𝑘 )
62 61 adantl ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( ( abs ‘ 𝑀 ) + 1 ) ≤ 𝑘 )
63 elfzelz ( 𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) → 𝑘 ∈ ℤ )
64 zltp1le ( ( ( abs ‘ 𝑀 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) < 𝑘 ↔ ( ( abs ‘ 𝑀 ) + 1 ) ≤ 𝑘 ) )
65 13 63 64 syl2an ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( ( abs ‘ 𝑀 ) < 𝑘 ↔ ( ( abs ‘ 𝑀 ) + 1 ) ≤ 𝑘 ) )
66 62 65 mpbird ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( abs ‘ 𝑀 ) < 𝑘 )
67 21 adantr ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( abs ‘ 𝑀 ) ∈ ℝ )
68 63 adantl ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → 𝑘 ∈ ℤ )
69 68 zred ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → 𝑘 ∈ ℝ )
70 67 69 ltnled ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( ( abs ‘ 𝑀 ) < 𝑘 ↔ ¬ 𝑘 ≤ ( abs ‘ 𝑀 ) ) )
71 66 70 mpbid ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ¬ 𝑘 ≤ ( abs ‘ 𝑀 ) )
72 71 adantr ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ¬ 𝑘 ≤ ( abs ‘ 𝑀 ) )
73 prmz ( 𝑘 ∈ ℙ → 𝑘 ∈ ℤ )
74 73 adantl ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝑘 ∈ ℤ )
75 4 ad2antrr ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝑀 ≠ 0 )
76 56 75 9 syl2anc ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( abs ‘ 𝑀 ) ∈ ℕ )
77 dvdsle ( ( 𝑘 ∈ ℤ ∧ ( abs ‘ 𝑀 ) ∈ ℕ ) → ( 𝑘 ∥ ( abs ‘ 𝑀 ) → 𝑘 ≤ ( abs ‘ 𝑀 ) ) )
78 74 76 77 syl2anc ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( 𝑘 ∥ ( abs ‘ 𝑀 ) → 𝑘 ≤ ( abs ‘ 𝑀 ) ) )
79 72 78 mtod ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ¬ 𝑘 ∥ ( abs ‘ 𝑀 ) )
80 pceq0 ( ( 𝑘 ∈ ℙ ∧ ( abs ‘ 𝑀 ) ∈ ℕ ) → ( ( 𝑘 pCnt ( abs ‘ 𝑀 ) ) = 0 ↔ ¬ 𝑘 ∥ ( abs ‘ 𝑀 ) ) )
81 55 76 80 syl2anc ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( ( 𝑘 pCnt ( abs ‘ 𝑀 ) ) = 0 ↔ ¬ 𝑘 ∥ ( abs ‘ 𝑀 ) ) )
82 79 81 mpbird ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( 𝑘 pCnt ( abs ‘ 𝑀 ) ) = 0 )
83 60 82 eqtr3d ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( 𝑘 pCnt 𝑀 ) = 0 )
84 83 oveq2d ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) = ( ( 𝐴 /L 𝑘 ) ↑ 0 ) )
85 1 ad2antrr ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → 𝐴 ∈ ℤ )
86 lgscl ( ( 𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝐴 /L 𝑘 ) ∈ ℤ )
87 85 74 86 syl2anc ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( 𝐴 /L 𝑘 ) ∈ ℤ )
88 87 zcnd ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( 𝐴 /L 𝑘 ) ∈ ℂ )
89 88 exp0d ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( ( 𝐴 /L 𝑘 ) ↑ 0 ) = 1 )
90 84 89 eqtrd ( ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℙ ) → ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) = 1 )
91 90 ifeq1da ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) = if ( 𝑘 ∈ ℙ , 1 , 1 ) )
92 ifid if ( 𝑘 ∈ ℙ , 1 , 1 ) = 1
93 91 92 eqtrdi ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → if ( 𝑘 ∈ ℙ , ( ( 𝐴 /L 𝑘 ) ↑ ( 𝑘 pCnt 𝑀 ) ) , 1 ) = 1 )
94 54 93 eqtrd ( ( 𝜑𝑘 ∈ ( ( ( abs ‘ 𝑀 ) + 1 ) ... ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ( 𝐹𝑘 ) = 1 )
95 8 12 31 40 94 seqid2 ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑀 ) ) = ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )