P. 439 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43801-43900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	etransclem19 43801*	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 43802*	𝐻 is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁):𝑋⟶ℂ)
Theorem	etransclem21 43803*	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 43804*	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 43805*	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 43806*	𝑃 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 43807*	𝑃 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 43808*	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 43809*	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 43810*	(𝑃 − 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 43811*	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 43812*	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 43813*	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 43814*	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 43815*	𝐹 is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):𝑋⟶ℂ)
Theorem	etransclem34 43816*	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 43817*	𝑃 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 43818*	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 43819*	(𝑃 − 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 43820*	𝑃 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 43821*	𝐺 is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))    ⇒   ⊢ (𝜑 → 𝐺:ℝ⟶ℂ)
Theorem	etransclem40 43822*	The 𝑁-th derivative of 𝐹 is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (𝑋–cn→ℂ))
Theorem	etransclem41 43823*	𝑃 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 43824*	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 43825*	𝐺 is a continuous function. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋 ↦ Σ𝑖 ∈ (0...𝑅)(((𝑆 D𝑛 𝐹)‘𝑖)‘𝑥))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ))
Theorem	etransclem44 43826*	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 43827*	𝐾 is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℤ)    &   ⊢ 𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st ‘𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st ‘𝑘))) / (!‘(𝑃 − 1)))    ⇒   ⊢ (𝜑 → 𝐾 ∈ ℤ)
Theorem	etransclem46 43828*	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 43829*	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 43830*	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 43831	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 ∈ (ℂ ∖ 𝔸)
20.37.18  n-dimensional Euclidean space
Theorem	rrxtopn 43832*	The topology of the generalized real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐼 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))))))
Theorem	rrxngp 43833	Generalized Euclidean real spaces are normed groups. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝐼 ∈ 𝑉 → (ℝ^‘𝐼) ∈ NrmGrp)
Theorem	rrxtps 43834	Generalized Euclidean real spaces are topological spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝐼 ∈ 𝑉 → (ℝ^‘𝐼) ∈ TopSp)
Theorem	rrxtopnfi 43835*	The topology of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐼 ∈ Fin)    ⇒   ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))))
Theorem	rrxtopon 43836	The topology on generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐽 ∈ (TopOn‘(Base‘(ℝ^‘𝐼))))
Theorem	rrxtop 43837	The topology on generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐽 ∈ Top)
Theorem	rrndistlt 43838*	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 43839	The topology on n-dimensional Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ Fin → 𝐽 ∈ (TopOn‘(ℝ ↑m 𝐼)))
Theorem	rrxunitopnfi 43840	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 43841	The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (TopOpen‘(ℝ^‘∅)) = 𝒫 {∅}
Theorem	qndenserrnbllem 43842*	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 43843*	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 43844	The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (TopOpen‘(ℝ^‘∅)) = {∅, {∅}}
Theorem	qndenserrnopnlem 43845*	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 43846*	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 43847	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 43848*	A multidimensional singleton expressed as a multidimensional closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m 𝑋))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) = {𝐴})
Theorem	rrnprjdstle 43849	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 43850*	𝐷 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 43851*	𝐷 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 43852*	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 43853*	The indexed product of open intervals is an open set in (ℝ^‘𝑋). (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)    ⇒   ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ (TopOpen‘(ℝ^‘𝑋)))
Theorem	ioorrnopnxrlem 43854*	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 43855*	The indexed product of open intervals is an open set in (ℝ^‘𝑋). Similar to ioorrnopn 43853 but here unbounded intervals are allowed. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴:𝑋⟶ℝ*)    &   ⊢ (𝜑 → 𝐵:𝑋⟶ℝ*)    ⇒   ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ (TopOpen‘(ℝ^‘𝑋)))
20.37.19  Basic measure theory
20.37.19.1  σ-Algebras Proofs for most of the theorems in section 111 of [Fremlin1]
Syntax	csalg 43856	Extend class notation with the class of all sigma-algebras.
class SAlg
Definition	df-salg 43857*	Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥))}
Syntax	csalon 43858	Extend class notation with the class of sigma-algebras on a set.
class SalOn
Definition	df-salon 43859*	Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥})
Syntax	csalgen 43860	Extend class notation with the class of sigma-algebra generator.
class SalGen
Definition	df-salgen 43861*	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 43887. 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 43889. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Glauco Siliprandi, 1-Jan-2021.)
⊢ SalGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)})
Theorem	issal 43862*	Express the predicate "𝑆 is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ SAlg ↔ (∅ ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (∪ 𝑆 ∖ 𝑦) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝒫 𝑆(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆))))
Theorem	pwsal 43863	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 43864	SAlg sigma-algebra is closed under countable union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝑆)    &   ⊢ (𝜑 → 𝑇 ≼ ω)    ⇒   ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑆)
Theorem	saluncl 43865	The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∪ 𝐹) ∈ 𝑆)
Theorem	prsal 43866	The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ SAlg)
Theorem	saldifcl 43867	The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆) → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆)
Theorem	0sal 43868	The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑆 ∈ SAlg → ∅ ∈ 𝑆)
Theorem	salgenval 43869*	The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)})
Theorem	saliuncl 43870*	SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐾 ≼ ω)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆)
Theorem	salincl 43871	The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∩ 𝐹) ∈ 𝑆)
Theorem	saluni 43872	A set is an element of any sigma-algebra on it . (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑆 ∈ SAlg → ∪ 𝑆 ∈ 𝑆)
Theorem	saliincl 43873*	SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐾 ≼ ω)    &   ⊢ (𝜑 → 𝐾 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆)
Theorem	saldifcl2 43874	The difference of two elements of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∖ 𝐹) ∈ 𝑆)
Theorem	intsaluni 43875*	The union of an arbitrary intersection of sigma-algebras on the same set 𝑋, is 𝑋. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐺 ⊆ SAlg)    &   ⊢ (𝜑 → 𝐺 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋)    ⇒   ⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋)
Theorem	intsal 43876*	The arbitrary intersection of sigma-algebra (on the same set 𝑋) is a sigma-algebra ( on the same set 𝑋, see intsaluni 43875). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐺 ⊆ SAlg)    &   ⊢ (𝜑 → 𝐺 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋)    ⇒   ⊢ (𝜑 → ∩ 𝐺 ∈ SAlg)
Theorem	salgenn0 43877*	The set used in the definition of the generated sigma-algebra, is not empty. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝑋 ∈ 𝑉 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅)
Theorem	salgencl 43878	SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) ∈ SAlg)
Theorem	issald 43879*	Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → ∅ ∈ 𝑆)    &   ⊢ 𝑋 = ∪ 𝑆    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	salexct 43880*	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 43881	A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝑆 = (SalGen‘𝑋)    ⇒   ⊢ (𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝑆)
Theorem	salgenss 43882	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 43890, 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)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → ∪ 𝑆 = ∪ 𝑋)    ⇒   ⊢ (𝜑 → 𝐺 ⊆ 𝑆)
Theorem	salgenuni 43883	The base set of the sigma-algebra generated by a set is the union of the set itself. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ 𝑆 = (SalGen‘𝑋)    &   ⊢ 𝑈 = ∪ 𝑋    ⇒   ⊢ (𝜑 → ∪ 𝑆 = 𝑈)
Theorem	issalgend 43884*	One side of dfsalgen2 43887. If a sigma-algebra on ∪ 𝑋 includes 𝑋 and it is included in all the sigma-algebras with such two properties, then it is the sigma-algebra generated by 𝑋. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → ∪ 𝑆 = ∪ 𝑋)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ SAlg ∧ ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦)) → 𝑆 ⊆ 𝑦)    ⇒   ⊢ (𝜑 → (SalGen‘𝑋) = 𝑆)
Theorem	salexct2 43885*	An example of a subset that does not belong to a nontrivial sigma-algebra, see salexct 43880. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝐴 = (0[,]2)    &   ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)}    &   ⊢ 𝐵 = (0[,]1)    ⇒   ⊢ ¬ 𝐵 ∈ 𝑆
Theorem	unisalgen 43886	The union of a set belongs to the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ 𝑆 = (SalGen‘𝑋)    &   ⊢ 𝑈 = ∪ 𝑋    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑆)
Theorem	dfsalgen2 43887*	Alternate characterization of the sigma-algebra generated by a set. It is the smallest sigma-algebra, on the same base set, that includes the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((SalGen‘𝑋) = 𝑆 ↔ ((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))))
Theorem	salexct3 43888*	An example of a sigma-algebra that's not closed under uncountable union. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝐴 = (0[,]2)    &   ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)}    &   ⊢ 𝑋 = ran (𝑦 ∈ (0[,]1) ↦ {𝑦})    ⇒   ⊢ (𝑆 ∈ SAlg ∧ 𝑋 ⊆ 𝑆 ∧ ¬ ∪ 𝑋 ∈ 𝑆)
Theorem	salgencntex 43889*	This counterexample shows that df-salgen 43861 needs to require that all containing sigma-algebra have the same base set. Otherwise, the intersection could lead to a set that is not a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝐴 = (0[,]2)    &   ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)}    &   ⊢ 𝐵 = (0[,]1)    &   ⊢ 𝑇 = 𝒫 𝐵    &   ⊢ 𝐶 = (𝑆 ∩ 𝑇)    &   ⊢ 𝑍 = ∩ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠}    ⇒   ⊢ ¬ 𝑍 ∈ SAlg
Theorem	salgensscntex 43890*	This counterexample shows that the sigma-algebra generated by a set is not the smallest sigma-algebra containing the set, if we consider also sigma-algebras with a larger base set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝐴 = (0[,]2)    &   ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)}    &   ⊢ 𝑋 = ran (𝑦 ∈ (0[,]1) ↦ {𝑦})    &   ⊢ 𝐺 = (SalGen‘𝑋)    ⇒   ⊢ (𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ SAlg ∧ ¬ 𝐺 ⊆ 𝑆)
Theorem	issalnnd 43891*	Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → ∅ ∈ 𝑆)    &   ⊢ 𝑋 = ∪ 𝑆    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆) → ∪ 𝑛 ∈ ℕ (𝑒‘𝑛) ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	dmvolsal 43892	Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ dom vol ∈ SAlg
Theorem	saldifcld 43893	The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆)
Theorem	saluncld 43894	The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ 𝑆)
Theorem	salgencld 43895	SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ 𝑆 = (SalGen‘𝑋)    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	0sald 43896	The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝑆)
Theorem	iooborel 43897	An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ (𝐴(,)𝐶) ∈ 𝐵
Theorem	salincld 43898	The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐸 ∩ 𝐹) ∈ 𝑆)
Theorem	salunid 43899	A set is an element of any sigma-algebra on it . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    ⇒   ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆)
Theorem	unisalgen2 43900	The union of a set belongs is equal to the union of the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ 𝑆 = (SalGen‘𝐴)    ⇒   ⊢ (𝜑 → ∪ 𝑆 = ∪ 𝐴)