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 ‘ ( 𝑀 · 𝑁 ) ) ) )