Step |
Hyp |
Ref |
Expression |
1 |
|
plyaddlem.1 |
⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) ) |
2 |
|
plyaddlem.2 |
⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) ) |
3 |
|
plyaddlem.m |
⊢ ( 𝜑 → 𝑀 ∈ ℕ0 ) |
4 |
|
plyaddlem.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
5 |
|
plyaddlem.a |
⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ ) |
6 |
|
plyaddlem.b |
⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ ℂ ) |
7 |
|
plyaddlem.a2 |
⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) |
8 |
|
plyaddlem.b2 |
⊢ ( 𝜑 → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) |
9 |
|
plyaddlem.f |
⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
10 |
|
plyaddlem.g |
⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
11 |
|
cnex |
⊢ ℂ ∈ V |
12 |
11
|
a1i |
⊢ ( 𝜑 → ℂ ∈ V ) |
13 |
|
sumex |
⊢ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ V |
14 |
13
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ V ) |
15 |
|
sumex |
⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ V |
16 |
15
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ V ) |
17 |
12 14 16 9 10
|
offval2 |
⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) = ( 𝑧 ∈ ℂ ↦ ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
18 |
|
fzfid |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∈ Fin ) |
19 |
|
elfznn0 |
⊢ ( 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ∈ ℕ0 ) |
20 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ ) |
21 |
20
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ ) |
22 |
|
expcl |
⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ ) |
23 |
22
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ ) |
24 |
21 23
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ ) |
25 |
19 24
|
sylan2 |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ ) |
26 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐵 : ℕ0 ⟶ ℂ ) |
27 |
26
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℂ ) |
28 |
27 23
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ ) |
29 |
19 28
|
sylan2 |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ ) |
30 |
18 25 29
|
fsumadd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
31 |
5
|
ffnd |
⊢ ( 𝜑 → 𝐴 Fn ℕ0 ) |
32 |
6
|
ffnd |
⊢ ( 𝜑 → 𝐵 Fn ℕ0 ) |
33 |
|
nn0ex |
⊢ ℕ0 ∈ V |
34 |
33
|
a1i |
⊢ ( 𝜑 → ℕ0 ∈ V ) |
35 |
|
inidm |
⊢ ( ℕ0 ∩ ℕ0 ) = ℕ0 |
36 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) ) |
37 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) ) |
38 |
31 32 34 34 35 36 37
|
ofval |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) + ( 𝐵 ‘ 𝑘 ) ) ) |
39 |
38
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) + ( 𝐵 ‘ 𝑘 ) ) ) |
40 |
39
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) + ( 𝐵 ‘ 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) |
41 |
21 27 23
|
adddird |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ‘ 𝑘 ) + ( 𝐵 ‘ 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
42 |
40 41
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
43 |
19 42
|
sylan2 |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) → ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
44 |
43
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
45 |
3
|
nn0zd |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
46 |
4 3
|
ifcld |
⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℕ0 ) |
47 |
46
|
nn0zd |
⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ ) |
48 |
3
|
nn0red |
⊢ ( 𝜑 → 𝑀 ∈ ℝ ) |
49 |
4
|
nn0red |
⊢ ( 𝜑 → 𝑁 ∈ ℝ ) |
50 |
|
max1 |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) |
51 |
48 49 50
|
syl2anc |
⊢ ( 𝜑 → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) |
52 |
|
eluz2 |
⊢ ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ ∧ 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) |
53 |
45 47 51 52
|
syl3anbrc |
⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
54 |
|
fzss2 |
⊢ ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 0 ... 𝑀 ) ⊆ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) |
55 |
53 54
|
syl |
⊢ ( 𝜑 → ( 0 ... 𝑀 ) ⊆ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) |
56 |
55
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑀 ) ⊆ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) |
57 |
|
elfznn0 |
⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ℕ0 ) |
58 |
57 24
|
sylan2 |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ ) |
59 |
|
eldifn |
⊢ ( 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑀 ) ) |
60 |
59
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑀 ) ) |
61 |
|
eldifi |
⊢ ( 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) |
62 |
61 19
|
syl |
⊢ ( 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ℕ0 ) |
63 |
62
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → 𝑘 ∈ ℕ0 ) |
64 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
65 |
|
peano2nn0 |
⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 ) |
66 |
3 65
|
syl |
⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ0 ) |
67 |
66 64
|
eleqtrdi |
⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 0 ) ) |
68 |
|
uzsplit |
⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( ℤ≥ ‘ 0 ) = ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) |
69 |
67 68
|
syl |
⊢ ( 𝜑 → ( ℤ≥ ‘ 0 ) = ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) |
70 |
64 69
|
syl5eq |
⊢ ( 𝜑 → ℕ0 = ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) |
71 |
3
|
nn0cnd |
⊢ ( 𝜑 → 𝑀 ∈ ℂ ) |
72 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
73 |
|
pncan |
⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 ) |
74 |
71 72 73
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 ) |
75 |
74
|
oveq2d |
⊢ ( 𝜑 → ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) = ( 0 ... 𝑀 ) ) |
76 |
75
|
uneq1d |
⊢ ( 𝜑 → ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = ( ( 0 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) |
77 |
70 76
|
eqtrd |
⊢ ( 𝜑 → ℕ0 = ( ( 0 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) |
78 |
77
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ℕ0 = ( ( 0 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) |
79 |
63 78
|
eleqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → 𝑘 ∈ ( ( 0 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) |
80 |
|
elun |
⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... 𝑀 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) |
81 |
79 80
|
sylib |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑀 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) |
82 |
81
|
ord |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) |
83 |
60 82
|
mpd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) |
84 |
5
|
ffund |
⊢ ( 𝜑 → Fun 𝐴 ) |
85 |
|
ssun2 |
⊢ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ⊆ ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) |
86 |
85 70
|
sseqtrrid |
⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ⊆ ℕ0 ) |
87 |
5
|
fdmd |
⊢ ( 𝜑 → dom 𝐴 = ℕ0 ) |
88 |
86 87
|
sseqtrrd |
⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ⊆ dom 𝐴 ) |
89 |
|
funfvima2 |
⊢ ( ( Fun 𝐴 ∧ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ⊆ dom 𝐴 ) → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) |
90 |
84 88 89
|
syl2anc |
⊢ ( 𝜑 → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) |
91 |
90
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) ) |
92 |
83 91
|
mpd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) |
93 |
7
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) |
94 |
92 93
|
eleqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ { 0 } ) |
95 |
|
elsni |
⊢ ( ( 𝐴 ‘ 𝑘 ) ∈ { 0 } → ( 𝐴 ‘ 𝑘 ) = 0 ) |
96 |
94 95
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴 ‘ 𝑘 ) = 0 ) |
97 |
96
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 0 · ( 𝑧 ↑ 𝑘 ) ) ) |
98 |
62 23
|
sylan2 |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ ) |
99 |
98
|
mul02d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 0 · ( 𝑧 ↑ 𝑘 ) ) = 0 ) |
100 |
97 99
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 ) |
101 |
56 58 100 18
|
fsumss |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) |
102 |
4
|
nn0zd |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
103 |
|
max2 |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) |
104 |
48 49 103
|
syl2anc |
⊢ ( 𝜑 → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) |
105 |
|
eluz2 |
⊢ ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ ∧ 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) |
106 |
102 47 104 105
|
syl3anbrc |
⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) |
107 |
|
fzss2 |
⊢ ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) |
108 |
106 107
|
syl |
⊢ ( 𝜑 → ( 0 ... 𝑁 ) ⊆ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) |
109 |
108
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) |
110 |
|
elfznn0 |
⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 ) |
111 |
110 28
|
sylan2 |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ ) |
112 |
|
eldifn |
⊢ ( 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) ) |
113 |
112
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) ) |
114 |
|
eldifi |
⊢ ( 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) |
115 |
114 19
|
syl |
⊢ ( 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 ) |
116 |
115
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑘 ∈ ℕ0 ) |
117 |
|
peano2nn0 |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 ) |
118 |
4 117
|
syl |
⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 ) |
119 |
118 64
|
eleqtrdi |
⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 0 ) ) |
120 |
|
uzsplit |
⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( ℤ≥ ‘ 0 ) = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
121 |
119 120
|
syl |
⊢ ( 𝜑 → ( ℤ≥ ‘ 0 ) = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
122 |
64 121
|
syl5eq |
⊢ ( 𝜑 → ℕ0 = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
123 |
4
|
nn0cnd |
⊢ ( 𝜑 → 𝑁 ∈ ℂ ) |
124 |
|
pncan |
⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 ) |
125 |
123 72 124
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 ) |
126 |
125
|
oveq2d |
⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ... 𝑁 ) ) |
127 |
126
|
uneq1d |
⊢ ( 𝜑 → ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
128 |
122 127
|
eqtrd |
⊢ ( 𝜑 → ℕ0 = ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
129 |
128
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ℕ0 = ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
130 |
116 129
|
eleqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑘 ∈ ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
131 |
|
elun |
⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
132 |
130 131
|
sylib |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
133 |
132
|
ord |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
134 |
113 133
|
mpd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) |
135 |
6
|
ffund |
⊢ ( 𝜑 → Fun 𝐵 ) |
136 |
|
ssun2 |
⊢ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) |
137 |
136 122
|
sseqtrrid |
⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ ℕ0 ) |
138 |
6
|
fdmd |
⊢ ( 𝜑 → dom 𝐵 = ℕ0 ) |
139 |
137 138
|
sseqtrrd |
⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ dom 𝐵 ) |
140 |
|
funfvima2 |
⊢ ( ( Fun 𝐵 ∧ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ dom 𝐵 ) → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) |
141 |
135 139 140
|
syl2anc |
⊢ ( 𝜑 → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) |
142 |
141
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) |
143 |
134 142
|
mpd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
144 |
8
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) |
145 |
143 144
|
eleqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵 ‘ 𝑘 ) ∈ { 0 } ) |
146 |
|
elsni |
⊢ ( ( 𝐵 ‘ 𝑘 ) ∈ { 0 } → ( 𝐵 ‘ 𝑘 ) = 0 ) |
147 |
145 146
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵 ‘ 𝑘 ) = 0 ) |
148 |
147
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 0 · ( 𝑧 ↑ 𝑘 ) ) ) |
149 |
115 23
|
sylan2 |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ ) |
150 |
149
|
mul02d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 0 · ( 𝑧 ↑ 𝑘 ) ) = 0 ) |
151 |
148 150
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 ) |
152 |
109 111 151 18
|
fsumss |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) |
153 |
101 152
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
154 |
30 44 153
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
155 |
154
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
156 |
17 155
|
eqtr4d |
⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |