| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | etransclem22.s | . . 3
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) | 
| 2 |  | etransclem22.x | . . 3
⊢ (𝜑 → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) | 
| 3 |  | etransclem22.p | . . 3
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 4 |  | etransclem22.h | . . 3
⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) | 
| 5 |  | etransclem22.J | . . 3
⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) | 
| 6 |  | etransclem22.n | . . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 7 | 1, 2, 3, 4, 5, 6 | etransclem17 46266 | . 2
⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) = (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))))) | 
| 8 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) | 
| 9 | 8 | iftrued 4533 | . . . . 5
⊢ ((𝜑 ∧ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))) = 0) | 
| 10 | 9 | mpteq2dv 5244 | . . . 4
⊢ ((𝜑 ∧ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))))) = (𝑥 ∈ 𝑋 ↦ 0)) | 
| 11 | 1, 2 | dvdmsscn 45951 | . . . . . 6
⊢ (𝜑 → 𝑋 ⊆ ℂ) | 
| 12 |  | 0cnd 11254 | . . . . . 6
⊢ (𝜑 → 0 ∈
ℂ) | 
| 13 |  | ssid 4006 | . . . . . . 7
⊢ ℂ
⊆ ℂ | 
| 14 | 13 | a1i 11 | . . . . . 6
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 15 | 11, 12, 14 | constcncfg 45887 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 0) ∈ (𝑋–cn→ℂ)) | 
| 16 | 15 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (𝑥 ∈ 𝑋 ↦ 0) ∈ (𝑋–cn→ℂ)) | 
| 17 | 10, 16 | eqeltrd 2841 | . . 3
⊢ ((𝜑 ∧ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))))) ∈ (𝑋–cn→ℂ)) | 
| 18 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) | 
| 19 | 18 | iffalsed 4536 | . . . . 5
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))) = (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))) | 
| 20 | 19 | mpteq2dv 5244 | . . . 4
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))))) = (𝑥 ∈ 𝑋 ↦ (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))))) | 
| 21 |  | nfv 1914 | . . . . 5
⊢
Ⅎ𝑥(𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) | 
| 22 | 11, 14 | idcncfg 45888 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (𝑋–cn→ℂ)) | 
| 23 | 5 | elfzelzd 13565 | . . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 24 | 23 | zcnd 12723 | . . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ ℂ) | 
| 25 | 11, 24, 14 | constcncfg 45887 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐽) ∈ (𝑋–cn→ℂ)) | 
| 26 | 22, 25 | subcncf 25479 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑥 − 𝐽)) ∈ (𝑋–cn→ℂ)) | 
| 27 | 26 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (𝑥 ∈ 𝑋 ↦ (𝑥 − 𝐽)) ∈ (𝑋–cn→ℂ)) | 
| 28 | 13 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → ℂ ⊆
ℂ) | 
| 29 |  | nnm1nn0 12567 | . . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) | 
| 30 | 3, 29 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) | 
| 31 | 3 | nnnn0d 12587 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈
ℕ0) | 
| 32 | 30, 31 | ifcld 4572 | . . . . . . . . . . 11
⊢ (𝜑 → if(𝐽 = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) | 
| 33 | 32 | faccld 14323 | . . . . . . . . . 10
⊢ (𝜑 → (!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) ∈ ℕ) | 
| 34 | 33 | nncnd 12282 | . . . . . . . . 9
⊢ (𝜑 → (!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ) | 
| 35 | 34 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ) | 
| 36 | 32 | nn0zd 12639 | . . . . . . . . . . . . 13
⊢ (𝜑 → if(𝐽 = 0, (𝑃 − 1), 𝑃) ∈ ℤ) | 
| 37 | 6 | nn0zd 12639 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 38 | 36, 37 | zsubcld 12727 | . . . . . . . . . . . 12
⊢ (𝜑 → (if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ∈ ℤ) | 
| 39 | 38 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ∈ ℤ) | 
| 40 | 6 | nn0red 12588 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 41 | 40 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → 𝑁 ∈ ℝ) | 
| 42 | 32 | nn0red 12588 | . . . . . . . . . . . . . 14
⊢ (𝜑 → if(𝐽 = 0, (𝑃 − 1), 𝑃) ∈ ℝ) | 
| 43 | 42 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → if(𝐽 = 0, (𝑃 − 1), 𝑃) ∈ ℝ) | 
| 44 | 41, 43, 18 | nltled 11411 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → 𝑁 ≤ if(𝐽 = 0, (𝑃 − 1), 𝑃)) | 
| 45 | 43, 41 | subge0d 11853 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (0 ≤ (if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ↔ 𝑁 ≤ if(𝐽 = 0, (𝑃 − 1), 𝑃))) | 
| 46 | 44, 45 | mpbird 257 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → 0 ≤ (if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)) | 
| 47 |  | elnn0z 12626 | . . . . . . . . . . 11
⊢
((if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ∈ ℕ0 ↔
((if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ∈ ℤ ∧ 0 ≤ (if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) | 
| 48 | 39, 46, 47 | sylanbrc 583 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ∈
ℕ0) | 
| 49 | 48 | faccld 14323 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)) ∈ ℕ) | 
| 50 | 49 | nncnd 12282 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)) ∈ ℂ) | 
| 51 | 49 | nnne0d 12316 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)) ≠ 0) | 
| 52 | 35, 50, 51 | divcld 12043 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → ((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) ∈ ℂ) | 
| 53 | 28, 52, 28 | constcncfg 45887 | . . . . . 6
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (𝑦 ∈ ℂ ↦ ((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))) ∈ (ℂ–cn→ℂ)) | 
| 54 |  | expcncf 24953 | . . . . . . 7
⊢
((if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ∈ ℕ0 → (𝑦 ∈ ℂ ↦ (𝑦↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) ∈ (ℂ–cn→ℂ)) | 
| 55 | 48, 54 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (𝑦 ∈ ℂ ↦ (𝑦↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) ∈ (ℂ–cn→ℂ)) | 
| 56 | 53, 55 | mulcncf 25480 | . . . . 5
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (𝑦 ∈ ℂ ↦ (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · (𝑦↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))) ∈ (ℂ–cn→ℂ)) | 
| 57 |  | oveq1 7438 | . . . . . 6
⊢ (𝑦 = (𝑥 − 𝐽) → (𝑦↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)) = ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) | 
| 58 | 57 | oveq2d 7447 | . . . . 5
⊢ (𝑦 = (𝑥 − 𝐽) → (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · (𝑦↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) = (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))) | 
| 59 | 21, 27, 56, 28, 58 | cncfcompt2 24934 | . . . 4
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (𝑥 ∈ 𝑋 ↦ (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))) ∈ (𝑋–cn→ℂ)) | 
| 60 | 20, 59 | eqeltrd 2841 | . . 3
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))))) ∈ (𝑋–cn→ℂ)) | 
| 61 | 17, 60 | pm2.61dan 813 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))))) ∈ (𝑋–cn→ℂ)) | 
| 62 | 7, 61 | eqeltrd 2841 | 1
⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) ∈ (𝑋–cn→ℂ)) |