| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | taylthlem1.n | . . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 2 |  | elfz1end 13595 | . . . 4
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁)) | 
| 3 | 1, 2 | sylib 218 | . . 3
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) | 
| 4 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑚 = 1 → (𝑁 − 𝑚) = (𝑁 − 1)) | 
| 5 | 4 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑚 = 1 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) | 
| 6 | 5 | fveq1d 6907 | . . . . . . . . . 10
⊢ (𝑚 = 1 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥)) | 
| 7 | 4 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑚 = 1 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 1))) | 
| 8 | 7 | fveq1d 6907 | . . . . . . . . . 10
⊢ (𝑚 = 1 → (((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) | 
| 9 | 6, 8 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑚 = 1 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥))) | 
| 10 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑚 = 1 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑1)) | 
| 11 | 9, 10 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑚 = 1 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) | 
| 12 | 11 | mpteq2dv 5243 | . . . . . . 7
⊢ (𝑚 = 1 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)))) | 
| 13 | 12 | oveq1d 7447 | . . . . . 6
⊢ (𝑚 = 1 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵)) | 
| 14 | 13 | eleq2d 2826 | . . . . 5
⊢ (𝑚 = 1 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵))) | 
| 15 | 14 | imbi2d 340 | . . . 4
⊢ (𝑚 = 1 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵)))) | 
| 16 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑁 − 𝑚) = (𝑁 − 𝑛)) | 
| 17 | 16 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))) | 
| 18 | 17 | fveq1d 6907 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥)) | 
| 19 | 16 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑛))) | 
| 20 | 19 | fveq1d 6907 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) | 
| 21 | 18, 20 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥))) | 
| 22 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑛)) | 
| 23 | 21, 22 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))) | 
| 24 | 23 | mpteq2dv 5243 | . . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)))) | 
| 25 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦)) | 
| 26 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) | 
| 27 | 25, 26 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦))) | 
| 28 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 − 𝐵) = (𝑦 − 𝐵)) | 
| 29 | 28 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 − 𝐵)↑𝑛) = ((𝑦 − 𝐵)↑𝑛)) | 
| 30 | 27, 29 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) | 
| 31 | 30 | cbvmptv 5254 | . . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) | 
| 32 | 24, 31 | eqtrdi 2792 | . . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛)))) | 
| 33 | 32 | oveq1d 7447 | . . . . . 6
⊢ (𝑚 = 𝑛 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) = ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵)) | 
| 34 | 33 | eleq2d 2826 | . . . . 5
⊢ (𝑚 = 𝑛 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) ↔ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵))) | 
| 35 | 34 | imbi2d 340 | . . . 4
⊢ (𝑚 = 𝑛 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵)))) | 
| 36 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (𝑁 − 𝑚) = (𝑁 − (𝑛 + 1))) | 
| 37 | 36 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))) | 
| 38 | 37 | fveq1d 6907 | . . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥)) | 
| 39 | 36 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → ((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))) | 
| 40 | 39 | fveq1d 6907 | . . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) | 
| 41 | 38, 40 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥))) | 
| 42 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑(𝑛 + 1))) | 
| 43 | 41, 42 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) | 
| 44 | 43 | mpteq2dv 5243 | . . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1))))) | 
| 45 | 44 | oveq1d 7447 | . . . . . 6
⊢ (𝑚 = (𝑛 + 1) → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)) | 
| 46 | 45 | eleq2d 2826 | . . . . 5
⊢ (𝑚 = (𝑛 + 1) → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵))) | 
| 47 | 46 | imbi2d 340 | . . . 4
⊢ (𝑚 = (𝑛 + 1) → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)))) | 
| 48 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑁 → (𝑁 − 𝑚) = (𝑁 − 𝑁)) | 
| 49 | 48 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑁 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))) | 
| 50 | 49 | fveq1d 6907 | . . . . . . . . . 10
⊢ (𝑚 = 𝑁 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥)) | 
| 51 | 48 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑁 → ((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑁))) | 
| 52 | 51 | fveq1d 6907 | . . . . . . . . . 10
⊢ (𝑚 = 𝑁 → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) | 
| 53 | 50, 52 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑚 = 𝑁 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥))) | 
| 54 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑚 = 𝑁 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑁)) | 
| 55 | 53, 54 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑚 = 𝑁 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) | 
| 56 | 55 | mpteq2dv 5243 | . . . . . . 7
⊢ (𝑚 = 𝑁 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))) | 
| 57 | 56 | oveq1d 7447 | . . . . . 6
⊢ (𝑚 = 𝑁 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵)) | 
| 58 | 57 | eleq2d 2826 | . . . . 5
⊢ (𝑚 = 𝑁 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵))) | 
| 59 | 58 | imbi2d 340 | . . . 4
⊢ (𝑚 = 𝑁 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵)))) | 
| 60 |  | taylthlem1.b | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ 𝐴) | 
| 61 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐵 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) = (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)) | 
| 62 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐵 → (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦) = (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)) | 
| 63 | 61, 62 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵))) | 
| 64 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) | 
| 65 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵)) ∈ V | 
| 66 | 63, 64, 65 | fvmpt 7015 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵))) | 
| 67 | 60, 66 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵))) | 
| 68 |  | taylthlem1.s | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) | 
| 69 |  | taylthlem1.f | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) | 
| 70 |  | taylthlem1.a | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆ 𝑆) | 
| 71 | 1 | nnnn0d 12589 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 72 |  | nn0uz 12921 | . . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) | 
| 73 | 71, 72 | eleqtrdi 2850 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) | 
| 74 |  | eluzfz2b 13574 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘0) ↔ 𝑁 ∈ (0...𝑁)) | 
| 75 | 73, 74 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) | 
| 76 |  | taylthlem1.d | . . . . . . . . . . . . . 14
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) = 𝐴) | 
| 77 | 60, 76 | eleqtrrd 2843 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 78 |  | taylthlem1.t | . . . . . . . . . . . . 13
⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) | 
| 79 | 68, 69, 70, 75, 77, 78 | dvntaylp0 26415 | . . . . . . . . . . . 12
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘𝑁)‘𝐵) = (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)) | 
| 80 | 79 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵)) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵))) | 
| 81 |  | cnex 11237 | . . . . . . . . . . . . . . . 16
⊢ ℂ
∈ V | 
| 82 | 81 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ℂ ∈
V) | 
| 83 |  | elpm2r 8886 | . . . . . . . . . . . . . . 15
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆)) | 
| 84 | 82, 68, 69, 70, 83 | syl22anc 838 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm 𝑆)) | 
| 85 |  | dvnf 25964 | . . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ 𝑁 ∈
ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ) | 
| 86 | 68, 84, 71, 85 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ) | 
| 87 | 86, 77 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) ∈ ℂ) | 
| 88 | 87 | subidd 11609 | . . . . . . . . . . 11
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)) = 0) | 
| 89 | 67, 80, 88 | 3eqtrd 2780 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0) | 
| 90 |  | funmpt 6603 | . . . . . . . . . . 11
⊢ Fun
(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) | 
| 91 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)) ∈ V | 
| 92 | 91, 64 | dmmpti 6711 | . . . . . . . . . . . 12
⊢ dom
(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) = 𝐴 | 
| 93 | 60, 92 | eleqtrrdi 2851 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))) | 
| 94 |  | funbrfvb 6961 | . . . . . . . . . . 11
⊢ ((Fun
(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) ∧ 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))0)) | 
| 95 | 90, 93, 94 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))0)) | 
| 96 | 89, 95 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))0) | 
| 97 |  | nnm1nn0 12569 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) | 
| 98 | 1, 97 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) | 
| 99 |  | dvnf 25964 | . . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ (𝑁 − 1) ∈
ℕ0) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 −
1))⟶ℂ) | 
| 100 | 68, 84, 98, 99 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 −
1))⟶ℂ) | 
| 101 |  | dvnbss 25965 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ (𝑁 − 1) ∈
ℕ0) → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹) | 
| 102 | 68, 84, 98, 101 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹) | 
| 103 | 69, 102 | fssdmd 6753 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ 𝐴) | 
| 104 |  | fzo0end 13798 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁)) | 
| 105 |  | elfzofz 13716 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 − 1) ∈ (0..^𝑁) → (𝑁 − 1) ∈ (0...𝑁)) | 
| 106 | 1, 104, 105 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 − 1) ∈ (0...𝑁)) | 
| 107 |  | dvn2bss 25967 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ (𝑁 − 1) ∈
(0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) | 
| 108 | 68, 84, 106, 107 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) | 
| 109 | 76, 108 | eqsstrrd 4018 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) | 
| 110 | 103, 109 | eqssd 4000 | . . . . . . . . . . . . . 14
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) = 𝐴) | 
| 111 | 110 | feq2d 6721 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))⟶ℂ ↔ ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ)) | 
| 112 | 100, 111 | mpbid 232 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ) | 
| 113 | 112 | ffvelcdmda 7103 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) ∈ ℂ) | 
| 114 | 76 | feq2d 6721 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ ↔ ((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ)) | 
| 115 | 86, 114 | mpbid 232 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ) | 
| 116 | 115 | ffvelcdmda 7103 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) ∈ ℂ) | 
| 117 | 1 | nncnd 12283 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 118 |  | 1cnd 11257 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℂ) | 
| 119 | 117, 118 | npcand 11625 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) | 
| 120 | 119 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 121 |  | recnprss 25940 | . . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) | 
| 122 | 68, 121 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ⊆ ℂ) | 
| 123 |  | dvnp1 25962 | . . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)
∧ (𝑁 − 1) ∈
ℕ0) → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) | 
| 124 | 122, 84, 98, 123 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) | 
| 125 | 120, 124 | eqtr3d 2778 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) | 
| 126 | 115 | feqmptd 6976 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦))) | 
| 127 | 112 | feqmptd 6976 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) | 
| 128 | 127 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦)))) | 
| 129 | 125, 126,
128 | 3eqtr3rd 2785 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦))) | 
| 130 | 70, 122 | sstrd 3993 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆ ℂ) | 
| 131 | 130 | sselda 3982 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ) | 
| 132 |  | 1nn0 12544 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 | 
| 133 | 132 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℕ0) | 
| 134 |  | elpm2r 8886 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ
↑pm 𝑆)) | 
| 135 | 82, 68, 112, 70, 134 | syl22anc 838 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ
↑pm 𝑆)) | 
| 136 |  | dvn1 25963 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ
↑pm 𝑆))
→ ((𝑆
D𝑛 ((𝑆
D𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) | 
| 137 | 122, 135,
136 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) | 
| 138 | 124, 120 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 139 | 137, 138 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 140 | 139 | dmeqd 5915 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 141 | 77, 140 | eleqtrrd 2843 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1)) | 
| 142 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵) | 
| 143 | 68, 112, 70, 133, 141, 142 | taylpf 26408 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ) | 
| 144 | 118, 117 | pncan3d 11624 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 + (𝑁 − 1)) = 𝑁) | 
| 145 | 144 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵)) | 
| 146 | 78, 145 | eqtr4id 2795 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 = ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵)) | 
| 147 | 146 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℂ
D𝑛 𝑇) =
(ℂ D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))) | 
| 148 | 147 | fveq1d 6907 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)) = ((ℂ
D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1))) | 
| 149 | 144 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 150 | 149 | dmeqd 5915 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 151 | 77, 150 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1)))) | 
| 152 | 68, 69, 70, 98, 133, 151 | dvntaylp 26414 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℂ
D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵)) | 
| 153 | 148, 152 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵)) | 
| 154 | 153 | feq1d 6719 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ ↔
(1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ)) | 
| 155 | 143, 154 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 −
1)):ℂ⟶ℂ) | 
| 156 | 155 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ
D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ) | 
| 157 | 131, 156 | syldan 591 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ) | 
| 158 |  | 0nn0 12543 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℕ0 | 
| 159 | 158 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈
ℕ0) | 
| 160 |  | elpm2r 8886 | . . . . . . . . . . . . . . . . . . 19
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆)) | 
| 161 | 82, 68, 115, 70, 160 | syl22anc 838 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆)) | 
| 162 |  | dvn0 25961 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 163 | 122, 161,
162 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 164 | 163 | dmeqd 5915 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 165 | 77, 164 | eleqtrrd 2843 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0)) | 
| 166 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵) | 
| 167 | 68, 115, 70, 159, 165, 166 | taylpf 26408 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ) | 
| 168 | 117 | addlidd 11463 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (0 + 𝑁) = 𝑁) | 
| 169 | 168 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵)) | 
| 170 | 169, 78 | eqtr4di 2794 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = 𝑇) | 
| 171 | 170 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℂ
D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵)) = (ℂ D𝑛 𝑇)) | 
| 172 | 171 | fveq1d 6907 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℂ
D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = ((ℂ D𝑛 𝑇)‘𝑁)) | 
| 173 | 168 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)) = ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 174 | 173 | dmeqd 5915 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 175 | 77, 174 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(0 + 𝑁))) | 
| 176 | 68, 69, 70, 71, 159, 175 | dvntaylp 26414 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℂ
D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵)) | 
| 177 | 172, 176 | eqtr3d 2778 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘𝑁) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵)) | 
| 178 | 177 | feq1d 6719 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘𝑁):ℂ⟶ℂ ↔ (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ)) | 
| 179 | 167, 178 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘𝑁):ℂ⟶ℂ) | 
| 180 | 179 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ
D𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ) | 
| 181 | 131, 180 | syldan 591 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦) ∈ ℂ) | 
| 182 | 122 | sselda 3982 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ) | 
| 183 | 182, 156 | syldan 591 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ) | 
| 184 | 182, 180 | syldan 591 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦) ∈ ℂ) | 
| 185 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 186 | 185 | cnfldtopon 24804 | . . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) | 
| 187 |  | toponmax 22933 | . . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ℂ ∈ (TopOpen‘ℂfld)) | 
| 188 | 186, 187 | mp1i 13 | . . . . . . . . . . . . 13
⊢ (𝜑 → ℂ ∈
(TopOpen‘ℂfld)) | 
| 189 |  | dfss2 3968 | . . . . . . . . . . . . . 14
⊢ (𝑆 ⊆ ℂ ↔ (𝑆 ∩ ℂ) = 𝑆) | 
| 190 | 122, 189 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ∩ ℂ) = 𝑆) | 
| 191 |  | ssid 4005 | . . . . . . . . . . . . . . . . 17
⊢ ℂ
⊆ ℂ | 
| 192 | 191 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 193 |  | mapsspm 8917 | . . . . . . . . . . . . . . . . 17
⊢ (ℂ
↑m ℂ) ⊆ (ℂ ↑pm
ℂ) | 
| 194 | 68, 69, 70, 71, 77, 78 | taylpf 26408 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇:ℂ⟶ℂ) | 
| 195 | 81, 81 | elmap 8912 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ (ℂ
↑m ℂ) ↔ 𝑇:ℂ⟶ℂ) | 
| 196 | 194, 195 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 ∈ (ℂ ↑m
ℂ)) | 
| 197 | 193, 196 | sselid 3980 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑇 ∈ (ℂ ↑pm
ℂ)) | 
| 198 |  | dvnp1 25962 | . . . . . . . . . . . . . . . 16
⊢ ((ℂ
⊆ ℂ ∧ 𝑇
∈ (ℂ ↑pm ℂ) ∧ (𝑁 − 1) ∈ ℕ0)
→ ((ℂ D𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)))) | 
| 199 | 192, 197,
98, 198 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)))) | 
| 200 | 119 | fveq2d 6909 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘((𝑁 − 1) + 1)) = ((ℂ
D𝑛 𝑇)‘𝑁)) | 
| 201 | 199, 200 | eqtr3d 2778 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − 1))) = ((ℂ
D𝑛 𝑇)‘𝑁)) | 
| 202 | 155 | feqmptd 6976 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)) = (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) | 
| 203 | 202 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − 1))) = (ℂ D (𝑦 ∈ ℂ ↦
(((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))) | 
| 204 | 179 | feqmptd 6976 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘𝑁) = (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘𝑁)‘𝑦))) | 
| 205 | 201, 203,
204 | 3eqtr3d 2784 | . . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘𝑁)‘𝑦))) | 
| 206 | 185, 68, 188, 190, 156, 180, 205 | dvmptres3 25995 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝑆 ↦ (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) | 
| 207 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t 𝑆) =
((TopOpen‘ℂfld) ↾t 𝑆) | 
| 208 |  | resttopon 23170 | . . . . . . . . . . . . . . . 16
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) | 
| 209 | 186, 122,
208 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) | 
| 210 |  | topontop 22920 | . . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) | 
| 211 | 209, 210 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) | 
| 212 |  | toponuni 22921 | . . . . . . . . . . . . . . . 16
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) | 
| 213 | 209, 212 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) | 
| 214 | 70, 213 | sseqtrd 4019 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ∪
((TopOpen‘ℂfld) ↾t 𝑆)) | 
| 215 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ ∪ ((TopOpen‘ℂfld)
↾t 𝑆) =
∪ ((TopOpen‘ℂfld)
↾t 𝑆) | 
| 216 | 215 | ntrss2 23066 | . . . . . . . . . . . . . 14
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ 𝐴 ⊆ ∪ ((TopOpen‘ℂfld)
↾t 𝑆))
→ ((int‘((TopOpen‘ℂfld) ↾t
𝑆))‘𝐴) ⊆ 𝐴) | 
| 217 | 211, 214,
216 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ⊆ 𝐴) | 
| 218 | 138 | dmeqd 5915 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 219 | 218, 76 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = 𝐴) | 
| 220 | 122, 112,
70, 207, 185 | dvbssntr 25936 | . . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) ⊆
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴)) | 
| 221 | 219, 220 | eqsstrrd 4018 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴)) | 
| 222 | 217, 221 | eqssd 4000 | . . . . . . . . . . . 12
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) = 𝐴) | 
| 223 | 68, 183, 184, 206, 70, 207, 185, 222 | dvmptres2 26001 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) | 
| 224 | 68, 113, 116, 129, 157, 181, 223 | dvmptsub 26006 | . . . . . . . . . 10
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))) | 
| 225 | 224 | breqd 5153 | . . . . . . . . 9
⊢ (𝜑 → (𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))0)) | 
| 226 | 96, 225 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → 𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))))0) | 
| 227 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) | 
| 228 | 113, 157 | subcld 11621 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)) ∈ ℂ) | 
| 229 | 228 | fmpttd 7134 | . . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))):𝐴⟶ℂ) | 
| 230 | 207, 185,
227, 122, 229, 70 | eldv 25934 | . . . . . . . 8
⊢ (𝜑 → (𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ (𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) limℂ 𝐵)))) | 
| 231 | 226, 230 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) limℂ 𝐵))) | 
| 232 | 231 | simprd 495 | . . . . . 6
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) limℂ 𝐵)) | 
| 233 |  | eldifi 4130 | . . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ 𝐴) | 
| 234 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥)) | 
| 235 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) | 
| 236 | 234, 235 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥))) | 
| 237 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))) | 
| 238 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) ∈ V | 
| 239 | 236, 237,
238 | fvmpt 7015 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥))) | 
| 240 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐵 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) | 
| 241 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐵 → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) | 
| 242 | 240, 241 | oveq12d 7450 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐵 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵))) | 
| 243 |  | ovex 7465 | . . . . . . . . . . . . . . 15
⊢ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵)) ∈ V | 
| 244 | 242, 237,
243 | fvmpt 7015 | . . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵))) | 
| 245 | 60, 244 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵))) | 
| 246 | 68, 69, 70, 106, 77, 78 | dvntaylp0 26415 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘(𝑁 − 1))‘𝐵) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) | 
| 247 | 246 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵))) | 
| 248 | 112, 60 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) ∈ ℂ) | 
| 249 | 248 | subidd 11609 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) = 0) | 
| 250 | 245, 247,
249 | 3eqtrd 2780 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = 0) | 
| 251 | 239, 250 | oveqan12rd 7452 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) − 0)) | 
| 252 | 112 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) ∈ ℂ) | 
| 253 | 130 | sselda 3982 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ) | 
| 254 | 155 | ffvelcdmda 7103 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((ℂ
D𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ) | 
| 255 | 253, 254 | syldan 591 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ) | 
| 256 | 252, 255 | subcld 11621 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) ∈ ℂ) | 
| 257 | 256 | subid1d 11610 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) − 0) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥))) | 
| 258 | 251, 257 | eqtr2d 2777 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵))) | 
| 259 | 233, 258 | sylan2 593 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵))) | 
| 260 | 130 | ssdifssd 4146 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ) | 
| 261 | 260 | sselda 3982 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ) | 
| 262 | 130, 60 | sseldd 3983 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 263 | 262 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ) | 
| 264 | 261, 263 | subcld 11621 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℂ) | 
| 265 | 264 | exp1d 14182 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑1) = (𝑥 − 𝐵)) | 
| 266 | 259, 265 | oveq12d 7450 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)) = ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) | 
| 267 | 266 | mpteq2dva 5241 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵)))) | 
| 268 | 267 | oveq1d 7447 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) limℂ 𝐵)) | 
| 269 | 232, 268 | eleqtrrd 2843 | . . . . 5
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵)) | 
| 270 | 269 | a1i 11 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵))) | 
| 271 |  | taylthlem1.i | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (1..^𝑁) ∧ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵))) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)) | 
| 272 | 271 | expr 456 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1..^𝑁)) → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵))) | 
| 273 | 272 | expcom 413 | . . . . 5
⊢ (𝑛 ∈ (1..^𝑁) → (𝜑 → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)))) | 
| 274 | 273 | a2d 29 | . . . 4
⊢ (𝑛 ∈ (1..^𝑁) → ((𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵)) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)))) | 
| 275 | 15, 35, 47, 59, 270, 274 | fzind2 13825 | . . 3
⊢ (𝑁 ∈ (1...𝑁) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵))) | 
| 276 | 3, 275 | mpcom 38 | . 2
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵)) | 
| 277 | 117 | subidd 11609 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 𝑁) = 0) | 
| 278 | 277 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁)) = ((𝑆 D𝑛 𝐹)‘0)) | 
| 279 |  | dvn0 25961 | . . . . . . . . . 10
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ ((𝑆
D𝑛 𝐹)‘0) = 𝐹) | 
| 280 | 122, 84, 279 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) | 
| 281 | 278, 280 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁)) = 𝐹) | 
| 282 | 281 | fveq1d 6907 | . . . . . . 7
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) = (𝐹‘𝑥)) | 
| 283 | 277 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑁)) = ((ℂ D𝑛 𝑇)‘0)) | 
| 284 |  | dvn0 25961 | . . . . . . . . . 10
⊢ ((ℂ
⊆ ℂ ∧ 𝑇
∈ (ℂ ↑pm ℂ)) → ((ℂ
D𝑛 𝑇)‘0) = 𝑇) | 
| 285 | 191, 197,
284 | sylancr 587 | . . . . . . . . 9
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘0) = 𝑇) | 
| 286 | 283, 285 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑁)) = 𝑇) | 
| 287 | 286 | fveq1d 6907 | . . . . . . 7
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥) = (𝑇‘𝑥)) | 
| 288 | 282, 287 | oveq12d 7450 | . . . . . 6
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) = ((𝐹‘𝑥) − (𝑇‘𝑥))) | 
| 289 | 288 | oveq1d 7447 | . . . . 5
⊢ (𝜑 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)) = (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) | 
| 290 | 289 | mpteq2dv 5243 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))) | 
| 291 |  | taylthlem1.r | . . . 4
⊢ 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) | 
| 292 | 290, 291 | eqtr4di 2794 | . . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = 𝑅) | 
| 293 | 292 | oveq1d 7447 | . 2
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵) = (𝑅 limℂ 𝐵)) | 
| 294 | 276, 293 | eleqtrd 2842 | 1
⊢ (𝜑 → 0 ∈ (𝑅 limℂ 𝐵)) |