Home | Metamath
Proof Explorer Theorem List (p. 425 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | etransclem1 42401* | 𝐻 is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑋 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) ⇒ ⊢ (𝜑 → (𝐻‘𝐽):𝑋⟶ℂ) | ||
Theorem | etransclem2 42402* | Derivative of 𝐺. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) ⇒ ⊢ (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) | ||
Theorem | etransclem3 42403 | The given if term is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝐾 ∈ ℤ) ⇒ ⊢ (𝜑 → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · ((𝐾 − 𝐽)↑(𝑃 − (𝐶‘𝐽))))) ∈ ℤ) | ||
Theorem | etransclem4 42404* | 𝐹 expressed as a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐸 = (𝑥 ∈ 𝐴 ↦ ∏𝑗 ∈ (0...𝑀)((𝐻‘𝑗)‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐸) | ||
Theorem | etransclem5 42405* | A change of bound variable, often used in proofs for etransc 42449. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) = (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ 𝑋 ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) | ||
Theorem | etransclem6 42406* | A change of bound variable, often used in proofs for etransc 42449. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃))) | ||
Theorem | etransclem7 42407* | The given product is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) ⇒ ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) | ||
Theorem | etransclem8 42408* | 𝐹 is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑋 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) | ||
Theorem | etransclem9 42409 | If 𝐾 divides 𝑁 but 𝐾 does not divide 𝑀 then 𝑀 + 𝑁 cannot be zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ≠ 0) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → ¬ 𝐾 ∥ 𝑀) & ⊢ (𝜑 → 𝐾 ∥ 𝑁) ⇒ ⊢ (𝜑 → (𝑀 + 𝑁) ≠ 0) | ||
Theorem | etransclem10 42410 | The given if term is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) ∈ ℤ) | ||
Theorem | etransclem11 42411* | A change of bound variable, often used in proofs for etransc 42449. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚}) | ||
Theorem | etransclem12 42412* | 𝐶 applied to 𝑁. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶‘𝑁) = {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) | ||
Theorem | etransclem13 42413* | 𝐹 applied to 𝑌. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑋 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹‘𝑌) = ∏𝑗 ∈ (0...𝑀)((𝑌 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) | ||
Theorem | etransclem14 42414* | Value of the term 𝑇, when 𝐽 = 0 and (𝐶‘0) = 𝑃 − 1 (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) & ⊢ (𝜑 → 𝐽 = 0) & ⊢ (𝜑 → (𝐶‘0) = (𝑃 − 1)) ⇒ ⊢ (𝜑 → 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · (-𝑗↑(𝑃 − (𝐶‘𝑗)))))))) | ||
Theorem | etransclem15 42415* | Value of the term 𝑇, when 𝐽 = 0 and (𝐶‘0) = 𝑃 − 1 (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) & ⊢ (𝜑 → 𝐽 = 0) & ⊢ (𝜑 → (𝐶‘0) ≠ (𝑃 − 1)) ⇒ ⊢ (𝜑 → 𝑇 = 0) | ||
Theorem | etransclem16 42416* | Every element in the range of 𝐶 is a finite set. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶‘𝑁) ∈ Fin) | ||
Theorem | etransclem17 42417* | The 𝑁-th derivative of 𝐻. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) = (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))))) | ||
Theorem | etransclem18 42418* | The given function is integrable. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → ℝ ∈ {ℝ, ℂ}) & ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈ 𝐿1) | ||
Theorem | etransclem19 42419* | The 𝑁-th derivative of 𝐻 is 0 if 𝑁 is large enough. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) = (𝑥 ∈ 𝑋 ↦ 0)) | ||
Theorem | etransclem20 42420* | 𝐻 is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁):𝑋⟶ℂ) | ||
Theorem | etransclem21 42421* | The 𝑁-th derivative of 𝐻 applied to 𝑌. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁)‘𝑌) = if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑌 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))))) | ||
Theorem | etransclem22 42422* | The 𝑁-th derivative of 𝐻 is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) ∈ (𝑋–cn→ℂ)) | ||
Theorem | etransclem23 42423* | This is the claim proof in [Juillerat] p. 14 (but in our proof, Stirling's approximation is not used). (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℤ) & ⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) & ⊢ 𝐾 = (𝐿 / (!‘(𝑃 − 1))) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) < 1) ⇒ ⊢ (𝜑 → (abs‘𝐾) < 1) | ||
Theorem | etransclem24 42424* | 𝑃 divides the I -th derivative of 𝐹 applied to 𝐽. when 𝐽 = 0 and 𝐼 is not equal to 𝑃 − 1. This is the second part of case 2 proven in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝐼 ∈ ℕ0) & ⊢ (𝜑 → 𝐼 ≠ (𝑃 − 1)) & ⊢ (𝜑 → 𝐽 = 0) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝐷 ∈ (𝐶‘𝐼)) ⇒ ⊢ (𝜑 → 𝑃 ∥ ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (𝐽↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) / (!‘(𝑃 − 1)))) | ||
Theorem | etransclem25 42425* | 𝑃 factorial divides the 𝑁-th derivative of 𝐹 applied to 𝐽. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗) = 𝑁) & ⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (!‘𝑃) ∥ 𝑇) | ||
Theorem | etransclem26 42426* | Every term in the sum of the 𝑁-th derivative of 𝐹 applied to 𝐽 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝐷 ∈ (𝐶‘𝑁)) ⇒ ⊢ (𝜑 → (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (𝐽↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) ∈ ℤ) | ||
Theorem | etransclem27 42427* | The 𝑁-th derivative of 𝐹 applied to 𝐽 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐶 ∈ Fin) & ⊢ (𝜑 → 𝐶:dom 𝐶⟶(ℕ0 ↑m (0...𝑀))) & ⊢ 𝐺 = (𝑥 ∈ 𝑋 ↦ Σ𝑙 ∈ dom 𝐶∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘((𝐶‘𝑙)‘𝑗))‘𝑥)) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐺‘𝐽) ∈ ℤ) | ||
Theorem | etransclem28 42428* | (𝑃 − 1) factorial divides the 𝑁-th derivative of 𝐹 applied to 𝐽. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝐷 ∈ (𝐶‘𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (𝐽↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) ⇒ ⊢ (𝜑 → (!‘(𝑃 − 1)) ∥ 𝑇) | ||
Theorem | etransclem29 42429* | The 𝑁-th derivative of 𝐹. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ 𝐸 = (𝑥 ∈ 𝑋 ↦ ∏𝑗 ∈ (0...𝑀)((𝐻‘𝑗)‘𝑥)) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥)))) | ||
Theorem | etransclem30 42430* | The 𝑁-th derivative of 𝐹. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥)))) | ||
Theorem | etransclem31 42431* | The 𝑁-th derivative of 𝐻 applied to 𝑌. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑌) = Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝑌↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝑌 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))))) | ||
Theorem | etransclem32 42432* | This is the proof for the last equation in the proof of the derivative calculated in [Juillerat] p. 12, just after equation *(6) . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < 𝑁) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ 0)) | ||
Theorem | etransclem33 42433* | 𝐹 is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):𝑋⟶ℂ) | ||
Theorem | etransclem34 42434* | The 𝑁-th derivative of 𝐹 is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐻 = (𝑘 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘) = 𝑛}) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (𝑋–cn→ℂ)) | ||
Theorem | etransclem35 42435* | 𝑃 does not divide the P-1 -th derivative of 𝐹 applied to 0. This is case 2 of the proof in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ 𝐷 = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0)) ⇒ ⊢ (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃))) | ||
Theorem | etransclem36 42436* | The 𝑁-th derivative of 𝐹 applied to 𝐽 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) ⇒ ⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐽) ∈ ℤ) | ||
Theorem | etransclem37 42437* | (𝑃 − 1) factorial divides the 𝑁-th derivative of 𝐹 applied to 𝐽. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) ⇒ ⊢ (𝜑 → (!‘(𝑃 − 1)) ∥ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐽)) | ||
Theorem | etransclem38 42438* | 𝑃 divides the I -th derivative of 𝐹 applied to 𝐽. if it is not the case that 𝐼 = 𝑃 − 1 and 𝐽 = 0. This is case 1 and the second part of case 2 proven in in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝐼 ∈ ℕ0) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → ¬ (𝐼 = (𝑃 − 1) ∧ 𝐽 = 0)) & ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) ⇒ ⊢ (𝜑 → 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘𝐼)‘𝐽) / (!‘(𝑃 − 1)))) | ||
Theorem | etransclem39 42439* | 𝐺 is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) ⇒ ⊢ (𝜑 → 𝐺:ℝ⟶ℂ) | ||
Theorem | etransclem40 42440* | The 𝑁-th derivative of 𝐹 is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (𝑋–cn→ℂ)) | ||
Theorem | etransclem41 42441* | 𝑃 does not divide the P-1 -th derivative of 𝐹 applied to 0. This is the first part of case 2: proven in in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → (!‘𝑀) < 𝑃) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) ⇒ ⊢ (𝜑 → ¬ 𝑃 ∥ ((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) | ||
Theorem | etransclem42 42442* | The 𝑁-th derivative of 𝐹 applied to 𝐽 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐽) ∈ ℤ) | ||
Theorem | etransclem43 42443* | 𝐺 is a continuous function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐺 = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (0...𝑅)(((𝑆 D𝑛 𝐹)‘𝑖)‘𝑥)) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ)) | ||
Theorem | etransclem44 42444* | The given finite sum is nonzero. This is the claim proved after equation (7) in [Juillerat] p. 12 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℤ) & ⊢ (𝜑 → (𝐴‘0) ≠ 0) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → (abs‘(𝐴‘0)) < 𝑃) & ⊢ (𝜑 → (!‘𝑀) < 𝑃) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st ‘𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st ‘𝑘))) / (!‘(𝑃 − 1))) ⇒ ⊢ (𝜑 → 𝐾 ≠ 0) | ||
Theorem | etransclem45 42445* | 𝐾 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℤ) & ⊢ 𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st ‘𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st ‘𝑘))) / (!‘(𝑃 − 1))) ⇒ ⊢ (𝜑 → 𝐾 ∈ ℤ) | ||
Theorem | etransclem46 42446* | This is the proof for equation *(7) in [Juillerat] p. 12. The proven equality will lead to a contradiction, because the left-hand side goes to 0 for large 𝑃, but the right-hand side is a nonzero integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝})) & ⊢ (𝜑 → (𝑄‘e) = 0) & ⊢ 𝐴 = (coeff‘𝑄) & ⊢ 𝑀 = (deg‘𝑄) & ⊢ (𝜑 → ℝ ⊆ ℝ) & ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ}) & ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ)) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) & ⊢ 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1)) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) & ⊢ 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺‘𝑥))) ⇒ ⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st ‘𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st ‘𝑘))) / (!‘(𝑃 − 1)))) | ||
Theorem | etransclem47 42447* | e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝})) & ⊢ (𝜑 → (𝑄‘e) = 0) & ⊢ 𝐴 = (coeff‘𝑄) & ⊢ (𝜑 → (𝐴‘0) ≠ 0) & ⊢ 𝑀 = (deg‘𝑄) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → (abs‘(𝐴‘0)) < 𝑃) & ⊢ (𝜑 → (!‘𝑀) < 𝑃) & ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) < 1) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) & ⊢ 𝐾 = (𝐿 / (!‘(𝑃 − 1))) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1)) | ||
Theorem | etransclem48 42448* | e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. In this lemma, a large enough prime 𝑝 is chosen: it will be used by subsequent lemmas. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 28-Sep-2020.) |
⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝})) & ⊢ (𝜑 → (𝑄‘e) = 0) & ⊢ 𝐴 = (coeff‘𝑄) & ⊢ (𝜑 → (𝐴‘0) ≠ 0) & ⊢ 𝑀 = (deg‘𝑄) & ⊢ 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) & ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))) & ⊢ 𝐼 = inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < ) & ⊢ 𝑇 = sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1)) | ||
Theorem | etransc 42449 | e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Proof shortened by AV, 28-Sep-2020.) |
⊢ e ∈ (ℂ ∖ 𝔸) | ||
Theorem | rrxtopn 42450* | The topology of the generalized real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ 𝑉) ⇒ ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))))) | ||
Theorem | rrxngp 42451 | Generalized Euclidean real spaces are normed groups. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝐼 ∈ 𝑉 → (ℝ^‘𝐼) ∈ NrmGrp) | ||
Theorem | rrxtps 42452 | Generalized Euclidean real spaces are topological spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝐼 ∈ 𝑉 → (ℝ^‘𝐼) ∈ TopSp) | ||
Theorem | rrxtopnfi 42453* | The topology of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) ⇒ ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))) | ||
Theorem | rrxtopon 42454 | The topology on generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐽 ∈ (TopOn‘(Base‘(ℝ^‘𝐼)))) | ||
Theorem | rrxtop 42455 | The topology on generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐽 ∈ Top) | ||
Theorem | rrndistlt 42456* | Given two points in the space of n-dimensional real numbers, if every component is closer than 𝐸 then the distance between the two points is less then ((√‘𝑛) · 𝐸) (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐼 ≠ ∅) & ⊢ 𝑁 = (♯‘𝐼) & ⊢ (𝜑 → 𝑋 ∈ (ℝ ↑m 𝐼)) & ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m 𝐼)) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (abs‘((𝑋‘𝑖) − (𝑌‘𝑖))) < 𝐸) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝜑 → (𝑋𝐷𝑌) < ((√‘𝑁) · 𝐸)) | ||
Theorem | rrxtoponfi 42457 | The topology on n-dimensional Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ Fin → 𝐽 ∈ (TopOn‘(ℝ ↑m 𝐼))) | ||
Theorem | rrxunitopnfi 42458 | The base set of the standard topology on the space of n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝑋 ∈ Fin → ∪ (TopOpen‘(ℝ^‘𝑋)) = (ℝ ↑m 𝑋)) | ||
Theorem | rrxtopn0 42459 | The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (TopOpen‘(ℝ^‘∅)) = 𝒫 {∅} | ||
Theorem | qndenserrnbllem 42460* | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐼 ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ (ℝ ↑m 𝐼)) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑m 𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸)) | ||
Theorem | qndenserrnbl 42461* | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (ℝ ↑m 𝐼)) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑m 𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸)) | ||
Theorem | rrxtopn0b 42462 | The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (TopOpen‘(ℝ^‘∅)) = {∅, {∅}} | ||
Theorem | qndenserrnopnlem 42463* | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝑉 ∈ 𝐽) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑m 𝐼)𝑦 ∈ 𝑉) | ||
Theorem | qndenserrnopn 42464* | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝑉 ∈ 𝐽) & ⊢ (𝜑 → 𝑉 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑m 𝐼)𝑦 ∈ 𝑉) | ||
Theorem | qndenserrn 42465 | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) ⇒ ⊢ (𝜑 → ((cls‘𝐽)‘(ℚ ↑m 𝐼)) = (ℝ ↑m 𝐼)) | ||
Theorem | rrxsnicc 42466* | A multidimensional singleton expressed as a multidimensional closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) = {𝐴}) | ||
Theorem | rrnprjdstle 42467 | The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐺:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ 𝐷 = (dist‘(ℝ^‘𝑋)) ⇒ ⊢ (𝜑 → (abs‘((𝐹‘𝐼) − (𝐺‘𝐼))) ≤ (𝐹𝐷𝐺)) | ||
Theorem | rrndsmet 42468* | 𝐷 is a metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝐷 = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘 ∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (Met‘(ℝ ↑m 𝑋))) | ||
Theorem | rrndsxmet 42469* | 𝐷 is an extended metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝐷 = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘 ∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘(ℝ ↑m 𝑋))) | ||
Theorem | ioorrnopnlem 42470* | The a point in an indexed product of open intervals is contained in an open ball that is contained in the indexed product of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) & ⊢ 𝐻 = ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) & ⊢ 𝐸 = inf(𝐻, ℝ, < ) & ⊢ 𝑉 = (𝐹(ball‘𝐷)𝐸) & ⊢ 𝐷 = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘 ∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) | ||
Theorem | ioorrnopn 42471* | The indexed product of open intervals is an open set in (ℝ^‘𝑋). (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ (TopOpen‘(ℝ^‘𝑋))) | ||
Theorem | ioorrnopnxrlem 42472* | Given a point 𝐹 that belongs to an indexed product of (possibly unbounded) open intervals, then 𝐹 belongs to an open product of bounded open intervals that's a subset of the original indexed product. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ*) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ*) & ⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) & ⊢ 𝐿 = (𝑖 ∈ 𝑋 ↦ if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖))) & ⊢ 𝑅 = (𝑖 ∈ 𝑋 ↦ if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖))) & ⊢ 𝑉 = X𝑖 ∈ 𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) | ||
Theorem | ioorrnopnxr 42473* | The indexed product of open intervals is an open set in (ℝ^‘𝑋). Similar to ioorrnopn 42471 but here unbounded intervals are allowed. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ*) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ*) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ (TopOpen‘(ℝ^‘𝑋))) | ||
Proofs for most of the theorems in section 111 of [Fremlin1] | ||
Syntax | csalg 42474 | Extend class notation with the class of all sigma-algebras. |
class SAlg | ||
Definition | df-salg 42475* | Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥))} | ||
Syntax | csalon 42476 | Extend class notation with the class of sigma-algebras on a set. |
class SalOn | ||
Definition | df-salon 42477* | Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥}) | ||
Syntax | csalgen 42478 | Extend class notation with the class of sigma-algebra generator. |
class SalGen | ||
Definition | df-salgen 42479* | Define the sigma-algebra generated by a given set. Definition 111G (b) of [Fremlin1] p. 13. The sigma-algebra generated by a set is the smallest sigma-algebra, on the same base set, that includes the set, see dfsalgen2 42505. The base set of the sigma-algebras used for the intersection needs to be the same, otherwise the resulting set is not guaranteed to be a sigma-algebra, as shown in the counterexample salgencntex 42507. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Glauco Siliprandi, 1-Jan-2021.) |
⊢ SalGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)}) | ||
Theorem | issal 42480* | Express the predicate "𝑆 is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ SAlg ↔ (∅ ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (∪ 𝑆 ∖ 𝑦) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝒫 𝑆(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆)))) | ||
Theorem | pwsal 42481 | The power set of a given set is a sigma-algebra (the so called discrete sigma-algebra). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ SAlg) | ||
Theorem | salunicl 42482 | SAlg sigma-algebra is closed under countable union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝑆) & ⊢ (𝜑 → 𝑇 ≼ ω) ⇒ ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑆) | ||
Theorem | saluncl 42483 | The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∪ 𝐹) ∈ 𝑆) | ||
Theorem | prsal 42484 | The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ SAlg) | ||
Theorem | saldifcl 42485 | The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆) → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆) | ||
Theorem | 0sal 42486 | The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑆 ∈ SAlg → ∅ ∈ 𝑆) | ||
Theorem | salgenval 42487* | The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) | ||
Theorem | saliuncl 42488* | SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐾 ≼ ω) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆) | ||
Theorem | salincl 42489 | The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∩ 𝐹) ∈ 𝑆) | ||
Theorem | saluni 42490 | A set is an element of any sigma-algebra on it . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑆 ∈ SAlg → ∪ 𝑆 ∈ 𝑆) | ||
Theorem | saliincl 42491* | SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐾 ≼ ω) & ⊢ (𝜑 → 𝐾 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆) | ||
Theorem | saldifcl2 42492 | The difference of two elements of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∖ 𝐹) ∈ 𝑆) | ||
Theorem | intsaluni 42493* | The union of an arbitrary intersection of sigma-algebras on the same set 𝑋, is 𝑋. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐺 ⊆ SAlg) & ⊢ (𝜑 → 𝐺 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋) ⇒ ⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋) | ||
Theorem | intsal 42494* | The arbitrary intersection of sigma-algebra (on the same set 𝑋) is a sigma-algebra ( on the same set 𝑋, see intsaluni 42493). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐺 ⊆ SAlg) & ⊢ (𝜑 → 𝐺 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋) ⇒ ⊢ (𝜑 → ∩ 𝐺 ∈ SAlg) | ||
Theorem | salgenn0 42495* | The set used in the definition of the generated sigma-algebra, is not empty. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝑋 ∈ 𝑉 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅) | ||
Theorem | salgencl 42496 | SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) ∈ SAlg) | ||
Theorem | issald 42497* | Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → ∅ ∈ 𝑆) & ⊢ 𝑋 = ∪ 𝑆 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | salexct 42498* | An example of nontrivial sigma-algebra: the collection of all subsets which either are countable or have countable complement. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | sssalgen 42499 | A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ 𝑆 = (SalGen‘𝑋) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝑆) | ||
Theorem | salgenss 42500 | The sigma-algebra generated by a set is the smallest sigma-algebra, on the same base set, that includes the set. Proposition 111G (b) of [Fremlin1] p. 13. Notice that the condition "on the same base set" is needed, see the counterexample salgensscntex 42508, where a sigma-algebra is shown that includes a set, but does not include the sigma-algebra generated (the key is that its base set is larger than the base set of the generating set). (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝐺 = (SalGen‘𝑋) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → ∪ 𝑆 = ∪ 𝑋) ⇒ ⊢ (𝜑 → 𝐺 ⊆ 𝑆) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |