Step |
Hyp |
Ref |
Expression |
1 |
|
climsubmpt.k |
⊢ Ⅎ 𝑘 𝜑 |
2 |
|
climsubmpt.z |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
3 |
|
climsubmpt.m |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
4 |
|
climsubmpt.a |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ ) |
5 |
|
climsubmpt.b |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ ) |
6 |
|
climsubmpt.c |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ⇝ 𝐶 ) |
7 |
|
climsubmpt.d |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐷 ) |
8 |
2
|
fvexi |
⊢ 𝑍 ∈ V |
9 |
8
|
mptex |
⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 − 𝐵 ) ) ∈ V |
10 |
9
|
a1i |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 − 𝐵 ) ) ∈ V ) |
11 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 ) |
12 |
|
nfv |
⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍 |
13 |
1 12
|
nfan |
⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) |
14 |
|
nfcv |
⊢ Ⅎ 𝑘 𝑗 |
15 |
14
|
nfcsb1 |
⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴 |
16 |
15
|
nfel1 |
⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ |
17 |
13 16
|
nfim |
⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ ) |
18 |
|
eleq1w |
⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) ) |
19 |
18
|
anbi2d |
⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) ) |
20 |
|
csbeq1a |
⊢ ( 𝑘 = 𝑗 → 𝐴 = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ) |
21 |
20
|
eleq1d |
⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ ) ) |
22 |
19 21
|
imbi12d |
⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ ) ) ) |
23 |
17 22 4
|
chvarfv |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ ) |
24 |
|
eqid |
⊢ ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) = ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) |
25 |
14 15 20 24
|
fvmptf |
⊢ ( ( 𝑗 ∈ 𝑍 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ) |
26 |
11 23 25
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ) |
27 |
26 23
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑗 ) ∈ ℂ ) |
28 |
14
|
nfcsb1 |
⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 |
29 |
|
nfcv |
⊢ Ⅎ 𝑘 ℂ |
30 |
28 29
|
nfel |
⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ |
31 |
13 30
|
nfim |
⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) |
32 |
|
csbeq1a |
⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) |
33 |
32
|
eleq1d |
⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) |
34 |
19 33
|
imbi12d |
⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) ) |
35 |
31 34 5
|
chvarfv |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) |
36 |
|
eqid |
⊢ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) |
37 |
14 28 32 36
|
fvmptf |
⊢ ( ( 𝑗 ∈ 𝑍 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) |
38 |
11 35 37
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) |
39 |
38 35
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ∈ ℂ ) |
40 |
|
ovexd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 − ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ∈ V ) |
41 |
|
nfcv |
⊢ Ⅎ 𝑘 − |
42 |
15 41 28
|
nfov |
⊢ Ⅎ 𝑘 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 − ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) |
43 |
20 32
|
oveq12d |
⊢ ( 𝑘 = 𝑗 → ( 𝐴 − 𝐵 ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 − ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) |
44 |
|
eqid |
⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 − 𝐵 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 − 𝐵 ) ) |
45 |
14 42 43 44
|
fvmptf |
⊢ ( ( 𝑗 ∈ 𝑍 ∧ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 − ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ∈ V ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 − 𝐵 ) ) ‘ 𝑗 ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 − ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) |
46 |
11 40 45
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 − 𝐵 ) ) ‘ 𝑗 ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 − ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) |
47 |
26 38
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑗 ) − ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 − ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) |
48 |
46 47
|
eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 − 𝐵 ) ) ‘ 𝑗 ) = ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑗 ) − ( ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ) ) |
49 |
2 3 6 10 7 27 39 48
|
climsub |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 − 𝐵 ) ) ⇝ ( 𝐶 − 𝐷 ) ) |