Metamath Proof Explorer

Theorem etransclem20

Description: H is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem20.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
etransclem20.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
etransclem20.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
etransclem20.h ⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
etransclem20.J ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
etransclem20.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion etransclem20 ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝐽 ) ) ‘ 𝑁 ) : 𝑋 ⟶ ℂ )

Proof

Step Hyp Ref Expression
1 etransclem20.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 etransclem20.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3 etransclem20.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
4 etransclem20.h ⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
5 etransclem20.J ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
6 etransclem20.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7 iftrue ⊢ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 → if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) = 0 )
8 0cnd ⊢ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 → 0 ∈ ℂ )
9 7 8 eqeltrd ⊢ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 → if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ∈ ℂ )
10 9 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ∈ ℂ )
11 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 )
12 11 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ 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 ) , 𝑃 ) − 𝑁 ) ) ) )
13 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
14 3 13 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
15 3 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
16 14 15 ifcld ⊢ ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
17 16 faccld ⊢ ( 𝜑 → ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℕ )
18 17 nncnd ⊢ ( 𝜑 → ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℂ )
19 18 adantr ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℂ )
20 16 nn0zd ⊢ ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℤ )
21 6 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
22 20 21 zsubcld ⊢ ( 𝜑 → ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℤ )
23 22 adantr ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℤ )
24 6 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
25 24 adantr ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → 𝑁 ∈ ℝ )
26 16 nn0red ⊢ ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
27 26 adantr ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
28 simpr ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 )
29 25 27 28 nltled ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → 𝑁 ≤ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
30 27 25 subge0d ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 0 ≤ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ↔ 𝑁 ≤ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
31 29 30 mpbird ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → 0 ≤ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) )
32 elnn0z ⊢ ( ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℕ0 ↔ ( ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℤ ∧ 0 ≤ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) )
33 23 31 32 sylanbrc ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℕ0 )
34 33 faccld ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ∈ ℕ )
35 34 nncnd ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ∈ ℂ )
36 34 nnne0d ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ≠ 0 )
37 19 35 36 divcld ⊢ ( ( 𝜑 ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ∈ ℂ )
38 37 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ∈ ℂ )
39 1 2 dvdmsscn ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
40 39 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ℂ )
41 elfzelz ⊢ ( 𝐽 ∈ ( 0 ... 𝑀 ) → 𝐽 ∈ ℤ )
42 41 zcnd ⊢ ( 𝐽 ∈ ( 0 ... 𝑀 ) → 𝐽 ∈ ℂ )
43 5 42 syl ⊢ ( 𝜑 → 𝐽 ∈ ℂ )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐽 ∈ ℂ )
45 40 44 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 − 𝐽 ) ∈ ℂ )
46 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( 𝑥 − 𝐽 ) ∈ ℂ )
47 33 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ∈ ℕ0 )
48 46 47 expcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ∈ ℂ )
49 38 48 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ∈ ℂ )
50 12 49 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 ) → if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ∈ ℂ )
51 10 50 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ∈ ℂ )
52 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) )
53 51 52 fmptd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) : 𝑋 ⟶ ℂ )
54 1 2 3 4 5 6 etransclem17 ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝐽 ) ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) )
55 54 feq1d ⊢ ( 𝜑 → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝐽 ) ) ‘ 𝑁 ) : 𝑋 ⟶ ℂ ↔ ( 𝑥 ∈ 𝑋 ↦ if ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < 𝑁 , 0 , ( ( ( ! ‘ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) · ( ( 𝑥 − 𝐽 ) ↑ ( if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 𝑁 ) ) ) ) ) : 𝑋 ⟶ ℂ ) )
56 53 55 mpbird ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝐽 ) ) ‘ 𝑁 ) : 𝑋 ⟶ ℂ )