Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  psercn Structured version   Visualization version   GIF version

Theorem psercn 24118
 Description: An infinite series converges to a continuous function on the open disk of radius 𝑅, where 𝑅 is the radius of convergence of the series. (Contributed by Mario Carneiro, 4-Mar-2015.)
Hypotheses
Ref Expression
pserf.g 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
pserf.f 𝐹 = (𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗))
pserf.a (𝜑𝐴:ℕ0⟶ℂ)
pserf.r 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
psercn.s 𝑆 = (abs “ (0[,)𝑅))
psercn.m 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))
Assertion
Ref Expression
psercn (𝜑𝐹 ∈ (𝑆cn→ℂ))
Distinct variable groups:   𝑗,𝑎,𝑛,𝑟,𝑥,𝑦,𝐴   𝑗,𝑀,𝑦   𝑗,𝐺,𝑟,𝑦   𝑆,𝑎,𝑗,𝑦   𝐹,𝑎   𝜑,𝑎,𝑗,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑛,𝑟)   𝑅(𝑥,𝑦,𝑗,𝑛,𝑟,𝑎)   𝑆(𝑥,𝑛,𝑟)   𝐹(𝑥,𝑦,𝑗,𝑛,𝑟)   𝐺(𝑥,𝑛,𝑎)   𝑀(𝑥,𝑛,𝑟,𝑎)

Proof of Theorem psercn
Dummy variables 𝑘 𝑠 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sumex 14368 . . . . . 6 Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗) ∈ V
21rgenw 2920 . . . . 5 𝑦𝑆 Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗) ∈ V
3 pserf.f . . . . . 6 𝐹 = (𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗))
43fnmpt 5987 . . . . 5 (∀𝑦𝑆 Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗) ∈ V → 𝐹 Fn 𝑆)
52, 4mp1i 13 . . . 4 (𝜑𝐹 Fn 𝑆)
6 psercn.s . . . . . . . . . . 11 𝑆 = (abs “ (0[,)𝑅))
7 cnvimass 5454 . . . . . . . . . . . 12 (abs “ (0[,)𝑅)) ⊆ dom abs
8 absf 14027 . . . . . . . . . . . . 13 abs:ℂ⟶ℝ
98fdmi 6019 . . . . . . . . . . . 12 dom abs = ℂ
107, 9sseqtri 3622 . . . . . . . . . . 11 (abs “ (0[,)𝑅)) ⊆ ℂ
116, 10eqsstri 3620 . . . . . . . . . 10 𝑆 ⊆ ℂ
1211a1i 11 . . . . . . . . 9 (𝜑𝑆 ⊆ ℂ)
1312sselda 3588 . . . . . . . 8 ((𝜑𝑎𝑆) → 𝑎 ∈ ℂ)
14 0cn 9992 . . . . . . . . . . 11 0 ∈ ℂ
15 eqid 2621 . . . . . . . . . . . 12 (abs ∘ − ) = (abs ∘ − )
1615cnmetdval 22514 . . . . . . . . . . 11 ((0 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (0(abs ∘ − )𝑎) = (abs‘(0 − 𝑎)))
1714, 13, 16sylancr 694 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (0(abs ∘ − )𝑎) = (abs‘(0 − 𝑎)))
18 abssub 14016 . . . . . . . . . . 11 ((0 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (abs‘(0 − 𝑎)) = (abs‘(𝑎 − 0)))
1914, 13, 18sylancr 694 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘(0 − 𝑎)) = (abs‘(𝑎 − 0)))
2013subid1d 10341 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (𝑎 − 0) = 𝑎)
2120fveq2d 6162 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘(𝑎 − 0)) = (abs‘𝑎))
2217, 19, 213eqtrd 2659 . . . . . . . . 9 ((𝜑𝑎𝑆) → (0(abs ∘ − )𝑎) = (abs‘𝑎))
23 breq2 4627 . . . . . . . . . . 11 ((((abs‘𝑎) + 𝑅) / 2) = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2) ↔ (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))))
24 breq2 4627 . . . . . . . . . . 11 (((abs‘𝑎) + 1) = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((abs‘𝑎) < ((abs‘𝑎) + 1) ↔ (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))))
25 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎𝑆) → 𝑎𝑆)
2625, 6syl6eleq 2708 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎𝑆) → 𝑎 ∈ (abs “ (0[,)𝑅)))
27 ffn 6012 . . . . . . . . . . . . . . . . . 18 (abs:ℂ⟶ℝ → abs Fn ℂ)
28 elpreima 6303 . . . . . . . . . . . . . . . . . 18 (abs Fn ℂ → (𝑎 ∈ (abs “ (0[,)𝑅)) ↔ (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅))))
298, 27, 28mp2b 10 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (abs “ (0[,)𝑅)) ↔ (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅)))
3026, 29sylib 208 . . . . . . . . . . . . . . . 16 ((𝜑𝑎𝑆) → (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅)))
3130simprd 479 . . . . . . . . . . . . . . 15 ((𝜑𝑎𝑆) → (abs‘𝑎) ∈ (0[,)𝑅))
32 0re 10000 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
33 iccssxr 12214 . . . . . . . . . . . . . . . . 17 (0[,]+∞) ⊆ ℝ*
34 pserf.g . . . . . . . . . . . . . . . . . . 19 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
35 pserf.a . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴:ℕ0⟶ℂ)
36 pserf.r . . . . . . . . . . . . . . . . . . 19 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
3734, 35, 36radcnvcl 24109 . . . . . . . . . . . . . . . . . 18 (𝜑𝑅 ∈ (0[,]+∞))
3837adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎𝑆) → 𝑅 ∈ (0[,]+∞))
3933, 38sseldi 3586 . . . . . . . . . . . . . . . 16 ((𝜑𝑎𝑆) → 𝑅 ∈ ℝ*)
40 elico2 12195 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ 𝑅 ∈ ℝ*) → ((abs‘𝑎) ∈ (0[,)𝑅) ↔ ((abs‘𝑎) ∈ ℝ ∧ 0 ≤ (abs‘𝑎) ∧ (abs‘𝑎) < 𝑅)))
4132, 39, 40sylancr 694 . . . . . . . . . . . . . . 15 ((𝜑𝑎𝑆) → ((abs‘𝑎) ∈ (0[,)𝑅) ↔ ((abs‘𝑎) ∈ ℝ ∧ 0 ≤ (abs‘𝑎) ∧ (abs‘𝑎) < 𝑅)))
4231, 41mpbid 222 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑆) → ((abs‘𝑎) ∈ ℝ ∧ 0 ≤ (abs‘𝑎) ∧ (abs‘𝑎) < 𝑅))
4342simp3d 1073 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → (abs‘𝑎) < 𝑅)
4443adantr 481 . . . . . . . . . . . 12 (((𝜑𝑎𝑆) ∧ 𝑅 ∈ ℝ) → (abs‘𝑎) < 𝑅)
4513abscld 14125 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → (abs‘𝑎) ∈ ℝ)
46 avglt1 11230 . . . . . . . . . . . . 13 (((abs‘𝑎) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2)))
4745, 46sylan 488 . . . . . . . . . . . 12 (((𝜑𝑎𝑆) ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2)))
4844, 47mpbid 222 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ 𝑅 ∈ ℝ) → (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2))
4945ltp1d 10914 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → (abs‘𝑎) < ((abs‘𝑎) + 1))
5049adantr 481 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ ¬ 𝑅 ∈ ℝ) → (abs‘𝑎) < ((abs‘𝑎) + 1))
5123, 24, 48, 50ifbothda 4101 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)))
52 psercn.m . . . . . . . . . 10 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))
5351, 52syl6breqr 4665 . . . . . . . . 9 ((𝜑𝑎𝑆) → (abs‘𝑎) < 𝑀)
5422, 53eqbrtrd 4645 . . . . . . . 8 ((𝜑𝑎𝑆) → (0(abs ∘ − )𝑎) < 𝑀)
55 cnxmet 22516 . . . . . . . . . 10 (abs ∘ − ) ∈ (∞Met‘ℂ)
5655a1i 11 . . . . . . . . 9 ((𝜑𝑎𝑆) → (abs ∘ − ) ∈ (∞Met‘ℂ))
5714a1i 11 . . . . . . . . 9 ((𝜑𝑎𝑆) → 0 ∈ ℂ)
5834, 3, 35, 36, 6, 52psercnlem1 24117 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀𝑀 < 𝑅))
5958simp1d 1071 . . . . . . . . . 10 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ+)
6059rpxrd 11833 . . . . . . . . 9 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ*)
61 elbl 22133 . . . . . . . . 9 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 𝑀 ∈ ℝ*) → (𝑎 ∈ (0(ball‘(abs ∘ − ))𝑀) ↔ (𝑎 ∈ ℂ ∧ (0(abs ∘ − )𝑎) < 𝑀)))
6256, 57, 60, 61syl3anc 1323 . . . . . . . 8 ((𝜑𝑎𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ − ))𝑀) ↔ (𝑎 ∈ ℂ ∧ (0(abs ∘ − )𝑎) < 𝑀)))
6313, 54, 62mpbir2and 956 . . . . . . 7 ((𝜑𝑎𝑆) → 𝑎 ∈ (0(ball‘(abs ∘ − ))𝑀))
64 fvres 6174 . . . . . . 7 (𝑎 ∈ (0(ball‘(abs ∘ − ))𝑀) → ((𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀))‘𝑎) = (𝐹𝑎))
6563, 64syl 17 . . . . . 6 ((𝜑𝑎𝑆) → ((𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀))‘𝑎) = (𝐹𝑎))
663reseq1i 5362 . . . . . . . . . 10 (𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)) = ((𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗)) ↾ (0(ball‘(abs ∘ − ))𝑀))
6734, 3, 35, 36, 6, 58psercnlem2 24116 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ − ))𝑀) ∧ (0(ball‘(abs ∘ − ))𝑀) ⊆ (abs “ (0[,]𝑀)) ∧ (abs “ (0[,]𝑀)) ⊆ 𝑆))
6867simp2d 1072 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))𝑀) ⊆ (abs “ (0[,]𝑀)))
6967simp3d 1073 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → (abs “ (0[,]𝑀)) ⊆ 𝑆)
7068, 69sstrd 3598 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))𝑀) ⊆ 𝑆)
7170resmptd 5421 . . . . . . . . . 10 ((𝜑𝑎𝑆) → ((𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗)) ↾ (0(ball‘(abs ∘ − ))𝑀)) = (𝑦 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗)))
7266, 71syl5eq 2667 . . . . . . . . 9 ((𝜑𝑎𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)) = (𝑦 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗)))
73 eqid 2621 . . . . . . . . . 10 (𝑦 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗)) = (𝑦 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗))
7435adantr 481 . . . . . . . . . 10 ((𝜑𝑎𝑆) → 𝐴:ℕ0⟶ℂ)
75 fveq2 6158 . . . . . . . . . . . . . . 15 (𝑘 = 𝑦 → (𝐺𝑘) = (𝐺𝑦))
7675seqeq3d 12765 . . . . . . . . . . . . . 14 (𝑘 = 𝑦 → seq0( + , (𝐺𝑘)) = seq0( + , (𝐺𝑦)))
7776fveq1d 6160 . . . . . . . . . . . . 13 (𝑘 = 𝑦 → (seq0( + , (𝐺𝑘))‘𝑠) = (seq0( + , (𝐺𝑦))‘𝑠))
7877cbvmptv 4720 . . . . . . . . . . . 12 (𝑘 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ (seq0( + , (𝐺𝑘))‘𝑠)) = (𝑦 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ (seq0( + , (𝐺𝑦))‘𝑠))
79 fveq2 6158 . . . . . . . . . . . . 13 (𝑠 = 𝑖 → (seq0( + , (𝐺𝑦))‘𝑠) = (seq0( + , (𝐺𝑦))‘𝑖))
8079mpteq2dv 4715 . . . . . . . . . . . 12 (𝑠 = 𝑖 → (𝑦 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ (seq0( + , (𝐺𝑦))‘𝑠)) = (𝑦 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ (seq0( + , (𝐺𝑦))‘𝑖)))
8178, 80syl5eq 2667 . . . . . . . . . . 11 (𝑠 = 𝑖 → (𝑘 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ (seq0( + , (𝐺𝑘))‘𝑠)) = (𝑦 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ (seq0( + , (𝐺𝑦))‘𝑖)))
8281cbvmptv 4720 . . . . . . . . . 10 (𝑠 ∈ ℕ0 ↦ (𝑘 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ (seq0( + , (𝐺𝑘))‘𝑠))) = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ (seq0( + , (𝐺𝑦))‘𝑖)))
8359rpred 11832 . . . . . . . . . 10 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ)
8458simp3d 1073 . . . . . . . . . 10 ((𝜑𝑎𝑆) → 𝑀 < 𝑅)
8534, 73, 74, 36, 82, 83, 84, 68psercn2 24115 . . . . . . . . 9 ((𝜑𝑎𝑆) → (𝑦 ∈ (0(ball‘(abs ∘ − ))𝑀) ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗)) ∈ ((0(ball‘(abs ∘ − ))𝑀)–cn→ℂ))
8672, 85eqeltrd 2698 . . . . . . . 8 ((𝜑𝑎𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)) ∈ ((0(ball‘(abs ∘ − ))𝑀)–cn→ℂ))
87 cncff 22636 . . . . . . . 8 ((𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)) ∈ ((0(ball‘(abs ∘ − ))𝑀)–cn→ℂ) → (𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)):(0(ball‘(abs ∘ − ))𝑀)⟶ℂ)
8886, 87syl 17 . . . . . . 7 ((𝜑𝑎𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)):(0(ball‘(abs ∘ − ))𝑀)⟶ℂ)
8988, 63ffvelrnd 6326 . . . . . 6 ((𝜑𝑎𝑆) → ((𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀))‘𝑎) ∈ ℂ)
9065, 89eqeltrrd 2699 . . . . 5 ((𝜑𝑎𝑆) → (𝐹𝑎) ∈ ℂ)
9190ralrimiva 2962 . . . 4 (𝜑 → ∀𝑎𝑆 (𝐹𝑎) ∈ ℂ)
92 ffnfv 6354 . . . 4 (𝐹:𝑆⟶ℂ ↔ (𝐹 Fn 𝑆 ∧ ∀𝑎𝑆 (𝐹𝑎) ∈ ℂ))
935, 91, 92sylanbrc 697 . . 3 (𝜑𝐹:𝑆⟶ℂ)
9470, 11syl6ss 3600 . . . . . . . . 9 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))𝑀) ⊆ ℂ)
95 ssid 3609 . . . . . . . . 9 ℂ ⊆ ℂ
96 eqid 2621 . . . . . . . . . 10 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
97 eqid 2621 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)) = ((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀))
9896cnfldtop 22527 . . . . . . . . . . . 12 (TopOpen‘ℂfld) ∈ Top
9996cnfldtopon 22526 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
10099toponunii 20661 . . . . . . . . . . . . 13 ℂ = (TopOpen‘ℂfld)
101100restid 16034 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
10298, 101ax-mp 5 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
103102eqcomi 2630 . . . . . . . . . 10 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
10496, 97, 103cncfcn 22652 . . . . . . . . 9 (((0(ball‘(abs ∘ − ))𝑀) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((0(ball‘(abs ∘ − ))𝑀)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)) Cn (TopOpen‘ℂfld)))
10594, 95, 104sylancl 693 . . . . . . . 8 ((𝜑𝑎𝑆) → ((0(ball‘(abs ∘ − ))𝑀)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)) Cn (TopOpen‘ℂfld)))
10686, 105eleqtrd 2700 . . . . . . 7 ((𝜑𝑎𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)) ∈ (((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)) Cn (TopOpen‘ℂfld)))
107100restuni 20906 . . . . . . . . 9 (((TopOpen‘ℂfld) ∈ Top ∧ (0(ball‘(abs ∘ − ))𝑀) ⊆ ℂ) → (0(ball‘(abs ∘ − ))𝑀) = ((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)))
10898, 94, 107sylancr 694 . . . . . . . 8 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))𝑀) = ((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)))
10963, 108eleqtrd 2700 . . . . . . 7 ((𝜑𝑎𝑆) → 𝑎 ((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)))
110 eqid 2621 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)) = ((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀))
111110cncnpi 21022 . . . . . . 7 (((𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)) ∈ (((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)) Cn (TopOpen‘ℂfld)) ∧ 𝑎 ((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀))) → (𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)) ∈ ((((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)) CnP (TopOpen‘ℂfld))‘𝑎))
112106, 109, 111syl2anc 692 . . . . . 6 ((𝜑𝑎𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)) ∈ ((((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)) CnP (TopOpen‘ℂfld))‘𝑎))
11398a1i 11 . . . . . . . . 9 ((𝜑𝑎𝑆) → (TopOpen‘ℂfld) ∈ Top)
114 cnex 9977 . . . . . . . . . . 11 ℂ ∈ V
115114, 11ssexi 4773 . . . . . . . . . 10 𝑆 ∈ V
116115a1i 11 . . . . . . . . 9 ((𝜑𝑎𝑆) → 𝑆 ∈ V)
117 restabs 20909 . . . . . . . . 9 (((TopOpen‘ℂfld) ∈ Top ∧ (0(ball‘(abs ∘ − ))𝑀) ⊆ 𝑆𝑆 ∈ V) → (((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs ∘ − ))𝑀)) = ((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)))
118113, 70, 116, 117syl3anc 1323 . . . . . . . 8 ((𝜑𝑎𝑆) → (((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs ∘ − ))𝑀)) = ((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)))
119118oveq1d 6630 . . . . . . 7 ((𝜑𝑎𝑆) → ((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs ∘ − ))𝑀)) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)) CnP (TopOpen‘ℂfld)))
120119fveq1d 6160 . . . . . 6 ((𝜑𝑎𝑆) → (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs ∘ − ))𝑀)) CnP (TopOpen‘ℂfld))‘𝑎) = ((((TopOpen‘ℂfld) ↾t (0(ball‘(abs ∘ − ))𝑀)) CnP (TopOpen‘ℂfld))‘𝑎))
121112, 120eleqtrrd 2701 . . . . 5 ((𝜑𝑎𝑆) → (𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)) ∈ (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs ∘ − ))𝑀)) CnP (TopOpen‘ℂfld))‘𝑎))
122 resttop 20904 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈ V) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
12398, 115, 122mp2an 707 . . . . . . 7 ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top
124123a1i 11 . . . . . 6 ((𝜑𝑎𝑆) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
125 df-ss 3574 . . . . . . . . . 10 ((0(ball‘(abs ∘ − ))𝑀) ⊆ 𝑆 ↔ ((0(ball‘(abs ∘ − ))𝑀) ∩ 𝑆) = (0(ball‘(abs ∘ − ))𝑀))
12670, 125sylib 208 . . . . . . . . 9 ((𝜑𝑎𝑆) → ((0(ball‘(abs ∘ − ))𝑀) ∩ 𝑆) = (0(ball‘(abs ∘ − ))𝑀))
12796cnfldtopn 22525 . . . . . . . . . . . 12 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
128127blopn 22245 . . . . . . . . . . 11 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 𝑀 ∈ ℝ*) → (0(ball‘(abs ∘ − ))𝑀) ∈ (TopOpen‘ℂfld))
12956, 57, 60, 128syl3anc 1323 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))𝑀) ∈ (TopOpen‘ℂfld))
130 elrestr 16029 . . . . . . . . . 10 (((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈ V ∧ (0(ball‘(abs ∘ − ))𝑀) ∈ (TopOpen‘ℂfld)) → ((0(ball‘(abs ∘ − ))𝑀) ∩ 𝑆) ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
131113, 116, 129, 130syl3anc 1323 . . . . . . . . 9 ((𝜑𝑎𝑆) → ((0(ball‘(abs ∘ − ))𝑀) ∩ 𝑆) ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
132126, 131eqeltrrd 2699 . . . . . . . 8 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))𝑀) ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
133 isopn3i 20826 . . . . . . . 8 ((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ (0(ball‘(abs ∘ − ))𝑀) ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(0(ball‘(abs ∘ − ))𝑀)) = (0(ball‘(abs ∘ − ))𝑀))
134123, 132, 133sylancr 694 . . . . . . 7 ((𝜑𝑎𝑆) → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(0(ball‘(abs ∘ − ))𝑀)) = (0(ball‘(abs ∘ − ))𝑀))
13563, 134eleqtrrd 2701 . . . . . 6 ((𝜑𝑎𝑆) → 𝑎 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(0(ball‘(abs ∘ − ))𝑀)))
13693adantr 481 . . . . . 6 ((𝜑𝑎𝑆) → 𝐹:𝑆⟶ℂ)
137100restuni 20906 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ⊆ ℂ) → 𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆))
13898, 11, 137mp2an 707 . . . . . . 7 𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆)
139138, 100cnprest 21033 . . . . . 6 (((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ (0(ball‘(abs ∘ − ))𝑀) ⊆ 𝑆) ∧ (𝑎 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(0(ball‘(abs ∘ − ))𝑀)) ∧ 𝐹:𝑆⟶ℂ)) → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑎) ↔ (𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)) ∈ (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs ∘ − ))𝑀)) CnP (TopOpen‘ℂfld))‘𝑎)))
140124, 70, 135, 136, 139syl22anc 1324 . . . . 5 ((𝜑𝑎𝑆) → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑎) ↔ (𝐹 ↾ (0(ball‘(abs ∘ − ))𝑀)) ∈ (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (0(ball‘(abs ∘ − ))𝑀)) CnP (TopOpen‘ℂfld))‘𝑎)))
141121, 140mpbird 247 . . . 4 ((𝜑𝑎𝑆) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑎))
142141ralrimiva 2962 . . 3 (𝜑 → ∀𝑎𝑆 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑎))
143 resttopon 20905 . . . . 5 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
14499, 11, 143mp2an 707 . . . 4 ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)
145 cncnp 21024 . . . 4 ((((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld)) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑎𝑆 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑎))))
146144, 99, 145mp2an 707 . . 3 (𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld)) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑎𝑆 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑎)))
14793, 142, 146sylanbrc 697 . 2 (𝜑𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld)))
148 eqid 2621 . . . 4 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
14996, 148, 103cncfcn 22652 . . 3 ((𝑆 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑆cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld)))
15011, 95, 149mp2an 707 . 2 (𝑆cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
151147, 150syl6eleqr 2709 1 (𝜑𝐹 ∈ (𝑆cn→ℂ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987  ∀wral 2908  {crab 2912  Vcvv 3190   ∩ cin 3559   ⊆ wss 3560  ifcif 4064  ∪ cuni 4409   class class class wbr 4623   ↦ cmpt 4683  ◡ccnv 5083  dom cdm 5084   ↾ cres 5086   “ cima 5087   ∘ ccom 5088   Fn wfn 5852  ⟶wf 5853  ‘cfv 5857  (class class class)co 6615  supcsup 8306  ℂcc 9894  ℝcr 9895  0cc0 9896  1c1 9897   + caddc 9899   · cmul 9901  +∞cpnf 10031  ℝ*cxr 10033   < clt 10034   ≤ cle 10035   − cmin 10226   / cdiv 10644  2c2 11030  ℕ0cn0 11252  ℝ+crp 11792  [,)cico 12135  [,]cicc 12136  seqcseq 12757  ↑cexp 12816  abscabs 13924   ⇝ cli 14165  Σcsu 14366   ↾t crest 16021  TopOpenctopn 16022  ∞Metcxmt 19671  ballcbl 19673  ℂfldccnfld 19686  Topctop 20638  TopOnctopon 20655  intcnt 20761   Cn ccn 20968   CnP ccnp 20969  –cn→ccncf 22619 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974  ax-addf 9975  ax-mulf 9976 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-supp 7256  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-ixp 7869  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fsupp 8236  df-fi 8277  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-cda 8950  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-z 11338  df-dec 11454  df-uz 11648  df-q 11749  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-ico 12139  df-icc 12140  df-fz 12285  df-fzo 12423  df-fl 12549  df-seq 12758  df-exp 12817  df-hash 13074  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-limsup 14152  df-clim 14169  df-rlim 14170  df-sum 14367  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-mulr 15895  df-starv 15896  df-sca 15897  df-vsca 15898  df-ip 15899  df-tset 15900  df-ple 15901  df-ds 15904  df-unif 15905  df-hom 15906  df-cco 15907  df-rest 16023  df-topn 16024  df-0g 16042  df-gsum 16043  df-topgen 16044  df-pt 16045  df-prds 16048  df-xrs 16102  df-qtop 16107  df-imas 16108  df-xps 16110  df-mre 16186  df-mrc 16187  df-acs 16189  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-submnd 17276  df-mulg 17481  df-cntz 17690  df-cmn 18135  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-mopn 19682  df-cnfld 19687  df-top 20639  df-topon 20656  df-topsp 20677  df-bases 20690  df-ntr 20764  df-cn 20971  df-cnp 20972  df-tx 21305  df-hmeo 21498  df-xms 22065  df-ms 22066  df-tms 22067  df-cncf 22621  df-ulm 24069 This theorem is referenced by:  pserdvlem2  24120  pserdv  24121  abelth  24133  logtayl  24340
 Copyright terms: Public domain W3C validator