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