P. 461 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46001-46100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	stoweidlem24 46001*	This lemma proves that for 𝑛 sufficiently large, qn( t ) > ( 1 - epsilon ), for all 𝑡 in 𝑉: see Lemma 1 [BrosowskiDeutsh] p. 90, (at the bottom of page 90). 𝑄 is used to represent qn in the paper, 𝑁 to represent 𝑛 in the paper, 𝐾 to represent 𝑘, 𝐷 to represent δ, and 𝐸 to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑉 = {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)}    &   ⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁)))    &   ⊢ (𝜑 → 𝑃:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (1 − 𝐸) < (1 − (((𝐾 · 𝐷) / 2)↑𝑁)))    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))    ⇒   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) < (𝑄‘𝑡))
Theorem	stoweidlem25 46002*	This lemma proves that for n sufficiently large, qn( t ) < ε, for all 𝑡 in 𝑇 ∖ 𝑈: see Lemma 1 [BrosowskiDeutsh] p. 91 (at the top of page 91). 𝑄 is used to represent qn in the paper, 𝑁 to represent n in the paper, 𝐾 to represent k, 𝐷 to represent δ, 𝑃 to represent p, and 𝐸 to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃:𝑇⟶ℝ)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)𝐷 ≤ (𝑃‘𝑡))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (1 / ((𝐾 · 𝐷)↑𝑁)) < 𝐸)    ⇒   ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (𝑄‘𝑡) < 𝐸)
Theorem	stoweidlem26 46003*	This lemma is used to prove that there is a function 𝑔 as in the proof of [BrosowskiDeutsh] p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * ε. Here 𝐿 is used to represent j in the paper, 𝐷 is used to represent A in the paper, 𝑆 is used to represent t, and 𝐸 is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})    &   ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇 ∈ V)    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))))    &   ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡))    ⇒   ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆))
Theorem	stoweidlem27 46004*	This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Here (𝑞‘𝑖) is used to represent p_(ti) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})    &   ⊢ (𝜑 → 𝑄 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑌 Fn ran 𝐺)    &   ⊢ (𝜑 → ran 𝐺 ∈ V)    &   ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙)    &   ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→ran 𝐺)    &   ⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋)    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎℎ𝑄    ⇒   ⊢ (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))))
Theorem	stoweidlem28 46005*	There exists a δ as in Lemma 1 [BrosowskiDeutsh] p. 90: 0 < delta < 1 and p >= delta on 𝑇 ∖ 𝑈. Here 𝑑 is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑈    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    ⇒   ⊢ (𝜑 → ∃𝑑(𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)𝑑 ≤ (𝑃‘𝑡)))
Theorem	stoweidlem29 46006*	When the hypothesis for the extreme value theorem hold, then the inf of the range of the function belongs to the range, it is real and it a lower bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017.) (Revised by AV, 13-Sep-2020.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑇 ≠ ∅)    ⇒   ⊢ (𝜑 → (inf(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ∧ inf(ran 𝐹, ℝ, < ) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑡)))
Theorem	stoweidlem30 46007*	This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, (𝐺‘𝑖) is used for p_(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝑄)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (𝑃‘𝑆) = ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆)))
Theorem	stoweidlem31 46008*	This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that 𝑅 is a finite subset of 𝑉, 𝑥 indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all 𝑖 ranging in the finite indexing set, 0 ≤ xi ≤ 1, xi < ε / m on V(ti), and xi > 1 - ε / m on 𝐵. Here M is used to represent m in the paper, 𝐸 is used to represent ε in the paper, vi is used to represent V(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎℎ𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}    &   ⊢ 𝑉 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}    &   ⊢ 𝐺 = (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})    &   ⊢ (𝜑 → 𝑅 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑣:(1...𝑀)–1-1-onto→𝑅)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ⊆ (𝑇 ∖ 𝑈))    &   ⊢ (𝜑 → 𝑉 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → ran 𝐺 ∈ Fin)    ⇒   ⊢ (𝜑 → ∃𝑥(𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))))
Theorem	stoweidlem32 46009*	If a set A of real functions from a common domain T is a subalgebra and it contains constants, then it is closed under the sum of a finite number of functions, indexed by G and finally scaled by a real Y. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)))    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))    &   ⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ 𝑌)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    ⇒   ⊢ (𝜑 → 𝑃 ∈ 𝐴)
Theorem	stoweidlem33 46010*	If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝐺    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − (𝐺‘𝑡))) ∈ 𝐴)
Theorem	stoweidlem34 46011*	This lemma proves that for all 𝑡 in 𝑇 there is a 𝑗 as in the proof of [BrosowskiDeutsh] p. 91 (at the bottom of page 91 and at the top of page 92): (j-4/3) * ε < f(t) <= (j-1/3) * ε , g(t) < (j+1/3) * ε, and g(t) > (j-4/3) * ε. Here 𝐸 is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})    &   ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})    &   ⊢ 𝐽 = (𝑡 ∈ 𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)})    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇 ∈ V)    &   ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 ≤ (𝐹‘𝑡))    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) < ((𝑁 − 1) · 𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑋‘𝑗):𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑗)‘𝑡))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → ((𝑋‘𝑗)‘𝑡) ≤ 1)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑗)) → ((𝑋‘𝑗)‘𝑡) < (𝐸 / 𝑁))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑗)‘𝑡))    ⇒   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))))
Theorem	stoweidlem35 46012*	This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Here (𝑞‘𝑖) is used to represent p_(ti) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎℎ𝜑    &   ⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}    &   ⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑊)    &   ⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋)    &   ⊢ (𝜑 → (𝑇 ∖ 𝑈) ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑚∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))
Theorem	stoweidlem36 46013*	This lemma is used to prove the existence of a function pt as in Lemma 1 of [BrosowskiDeutsh] p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function p in the subalgebra, such that pt ( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. Z is used for t0 , S is used for t e. T - U , h is used for pt . G is used for (ht)^2 and the final h is a normalized version of G ( divided by its norm, see the variable N ). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎℎ𝑄    &   ⊢ Ⅎ𝑡𝐻    &   ⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝐺    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐺 = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐹‘𝑡)))    &   ⊢ 𝑁 = sup(ran 𝐺, ℝ, < )    &   ⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ ((𝐺‘𝑡) / 𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝑆) ≠ (𝐹‘𝑍))    &   ⊢ (𝜑 → (𝐹‘𝑍) = 0)    ⇒   ⊢ (𝜑 → ∃ℎ(ℎ ∈ 𝑄 ∧ 0 < (ℎ‘𝑆)))
Theorem	stoweidlem37 46014*	This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, (𝐺‘𝑖) is used for p_(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝑄)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑇)    ⇒   ⊢ (𝜑 → (𝑃‘𝑍) = 0)
Theorem	stoweidlem38 46015*	This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, (𝐺‘𝑖) is used for p_(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝑄)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (0 ≤ (𝑃‘𝑆) ∧ (𝑃‘𝑆) ≤ 1))
Theorem	stoweidlem39 46016*	This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that 𝑟 is a finite subset of 𝑊, 𝑥 indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ xi ≤ 1, xi < ε / m on V(ti), and xi > 1 - ε / m on 𝐵. Here 𝐷 is used to represent A in the paper's Lemma 2 (because 𝐴 is used for the subalgebra), 𝑀 is used to represent m in the paper, 𝐸 is used to represent ε, and vi is used to represent V(ti). 𝑊 is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎℎ𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ 𝑈 = (𝑇 ∖ 𝐵)    &   ⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}    &   ⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}    &   ⊢ (𝜑 → 𝑟 ∈ (𝒫 𝑊 ∩ Fin))    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑟)    &   ⊢ (𝜑 → 𝐷 ≠ ∅)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑇)    &   ⊢ (𝜑 → 𝑊 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))))
Theorem	stoweidlem40 46017*	This lemma proves that qn is in the subalgebra, as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90. Q is used to represent qn in the paper, N is used to represent n in the paper, and M is used to represent k^n in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑃    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑𝑀))    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (1 − ((𝑃‘𝑡)↑𝑁)))    &   ⊢ 𝐺 = (𝑡 ∈ 𝑇 ↦ 1)    &   ⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ ((𝑃‘𝑡)↑𝑁))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑃:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝑄 ∈ 𝐴)
Theorem	stoweidlem41 46018*	This lemma is used to prove that there exists x as in Lemma 1 of [BrosowskiDeutsh] p. 90: 0 <= x(t) <= 1 for all t in T, x(t) < epsilon for all t in V, x(t) > 1 - epsilon for all t in T \ U. Here we prove the very last step of the proof of Lemma 1: "The result follows from taking x = 1 - qn";. Here 𝐸 is used to represent ε in the paper, and 𝑦 to represent qn in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑋 = (𝑡 ∈ 𝑇 ↦ (1 − (𝑦‘𝑡)))    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ 1)    &   ⊢ 𝑉 ⊆ 𝑇    &   ⊢ (𝜑 → 𝑦 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑦:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑤) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1))    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑉 (1 − 𝐸) < (𝑦‘𝑡))    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝐸)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝐸) < (𝑥‘𝑡)))
Theorem	stoweidlem42 46019*	This lemma is used to prove that 𝑥 built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x > 1 - ε on B. Here 𝑋 is used to represent 𝑥 in the paper, and E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑡𝑌    &   ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))    &   ⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))    &   ⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑈‘𝑖)‘𝑡))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)    &   ⊢ (𝜑 → 𝑇 ∈ V)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑇)    ⇒   ⊢ (𝜑 → ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑋‘𝑡))
Theorem	stoweidlem43 46020*	This lemma is used to prove the existence of a function pt as in Lemma 1 of [BrosowskiDeutsh] p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function pt in the subalgebra, such that pt( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. Hera Z is used for t0 , S is used for t e. T - U , h is used for pt. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑔𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎℎ𝑄    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑙‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑙‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑔 ∈ 𝐴 (𝑔‘𝑟) ≠ (𝑔‘𝑡))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑆 ∈ (𝑇 ∖ 𝑈))    ⇒   ⊢ (𝜑 → ∃ℎ(ℎ ∈ 𝑄 ∧ 0 < (ℎ‘𝑆)))
Theorem	stoweidlem44 46021*	This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Z is used to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝑄)    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑗 ∈ (1...𝑀)0 < ((𝐺‘𝑗)‘𝑡))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑇)    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡)))
Theorem	stoweidlem45 46022*	This lemma proves that, given an appropriate 𝐾 (in another theorem we prove such a 𝐾 exists), there exists a function qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 ( at the top of page 91): 0 <= qn <= 1 , qn < ε on T \ U, and qn > 1 - ε on 𝑉. We use y to represent the final qn in the paper (the one with n large enough), 𝑁 to represent 𝑛 in the paper, 𝐾 to represent 𝑘, 𝐷 to represent δ, 𝐸 to represent ε, and 𝑃 to represent 𝑝. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑃    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑉 = {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)}    &   ⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 < 1)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑃:𝑇⟶ℝ)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)𝐷 ≤ (𝑃‘𝑡))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (1 − 𝐸) < (1 − (((𝐾 · 𝐷) / 2)↑𝑁)))    &   ⊢ (𝜑 → (1 / ((𝐾 · 𝐷)↑𝑁)) < 𝐸)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝐸) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝐸))
Theorem	stoweidlem46 46023*	This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, are a cover of T \ U. Using this lemma, in a later theorem we will prove that a finite subcover exists. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑈    &   ⊢ Ⅎℎ𝑄    &   ⊢ Ⅎ𝑞𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ V)    ⇒   ⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊)
Theorem	stoweidlem47 46024*	Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝑆    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐺 = (𝑇 × {-𝑆})    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑆 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − 𝑆)) ∈ 𝐶)
Theorem	stoweidlem48 46025*	This lemma is used to prove that 𝑥 built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x < ε on 𝐴. Here 𝑋 is used to represent 𝑥 in the paper, 𝐸 is used to represent ε in the paper, and 𝐷 is used to represent 𝐴 in the paper (because 𝐴 is always used to represent the subalgebra). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}    &   ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))    &   ⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))    &   ⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊:(1...𝑀)⟶𝑉)    &   ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ ran 𝑊)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑊‘𝑖)((𝑈‘𝑖)‘𝑡) < 𝐸)    &   ⊢ (𝜑 → 𝑇 ∈ V)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∀𝑡 ∈ 𝐷 (𝑋‘𝑡) < 𝐸)
Theorem	stoweidlem49 46026*	There exists a function qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 (at the top of page 91): 0 <= qn <= 1 , qn < ε on 𝑇 ∖ 𝑈, and qn > 1 - ε on 𝑉. Here y is used to represent the final qn in the paper (the one with n large enough), 𝑁 represents 𝑛 in the paper, 𝐾 represents 𝑘, 𝐷 represents δ, 𝐸 represents ε, and 𝑃 represents 𝑝. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑃    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑉 = {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)}    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 < 1)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑃:𝑇⟶ℝ)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)𝐷 ≤ (𝑃‘𝑡))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝐸) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝐸))
Theorem	stoweidlem50 46027*	This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, contain a finite subcover of T \ U. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑈    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑢(𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢))
Theorem	stoweidlem51 46028*	There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here 𝐷 is used to represent 𝐴 in the paper, because here 𝐴 is used for the subalgebra of functions. 𝐸 is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑤𝑉    &   ⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}    &   ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))    &   ⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))    &   ⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊:(1...𝑀)⟶𝑉)    &   ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)    &   ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉) → 𝑤 ⊆ 𝑇)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ ran 𝑊)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝑇)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑊‘𝑖)((𝑈‘𝑖)‘𝑡) < (𝐸 / 𝑀))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑈‘𝑖)‘𝑡))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝑇 ∈ V)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    ⇒   ⊢ (𝜑 → ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡))))
Theorem	stoweidlem52 46029*	There exists a neighborhood V as in Lemma 1 of [BrosowskiDeutsh] p. 90. Here Z is used to represent t0 in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑈    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑡𝑃    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑉 = {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)}    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑎) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 < 1)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))    &   ⊢ (𝜑 → (𝑃‘𝑍) = 0)    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)𝐷 ≤ (𝑃‘𝑡))    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ 𝐽 ((𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑣 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡))))
Theorem	stoweidlem53 46030*	This lemma is used to prove the existence of a function 𝑝 as in Lemma 1 of [BrosowskiDeutsh] p. 90: 𝑝 is in the subalgebra, such that 0 ≤ 𝑝 ≤ 1, p_(t0) = 0, and 0 < 𝑝 on 𝑇 ∖ 𝑈. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑈    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → (𝑇 ∖ 𝑈) ≠ ∅)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡)))
Theorem	stoweidlem54 46031*	There exists a function 𝑥 as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here 𝐷 is used to represent 𝐴 in the paper, because here 𝐴 is used for the subalgebra of functions. 𝐸 is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}    &   ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑦‘𝑖)‘𝑡)))    &   ⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀))    &   ⊢ 𝑉 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊:(1...𝑀)⟶𝑉)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑇)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ ran 𝑊)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝑇)    &   ⊢ (𝜑 → ∃𝑦(𝑦:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑊‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑦‘𝑖)‘𝑡))))    &   ⊢ (𝜑 → 𝑇 ∈ V)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡)))
Theorem	stoweidlem55 46032*	This lemma proves the existence of a function p as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Here Z is used to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑈    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡)))
Theorem	stoweidlem56 46033*	This theorem proves Lemma 1 in [BrosowskiDeutsh] p. 90. Here 𝑍 is used to represent t0 in the paper, 𝑣 is used to represent 𝑉 in the paper, and 𝑒 is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑈    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ 𝐽 ((𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑣 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡))))
Theorem	stoweidlem57 46034*	There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. In this theorem, it is proven the non-trivial case (the closed set D is nonempty). Here D is used to represent A in the paper, because the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐷    &   ⊢ Ⅎ𝑡𝑈    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}    &   ⊢ 𝑉 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ 𝑈 = (𝑇 ∖ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑎) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))    &   ⊢ (𝜑 → 𝐵 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → 𝐷 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → (𝐵 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐷 ≠ ∅)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡)))
Theorem	stoweidlem58 46035*	This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐷    &   ⊢ Ⅎ𝑡𝑈    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑎) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))    &   ⊢ (𝜑 → 𝐵 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → 𝐷 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → (𝐵 ∩ 𝐷) = ∅)    &   ⊢ 𝑈 = (𝑇 ∖ 𝐵)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡)))
Theorem	stoweidlem59 46036*	This lemma proves that there exists a function 𝑥 as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: xj is in the subalgebra, 0 <= xj <= 1, xj < ε / n on Aj (meaning A in the paper), xj > 1 - \epsilon / n on Bj. Here 𝐷 is used to represent A in the paper (because A is used for the subalgebra of functions), 𝐸 is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})    &   ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})    &   ⊢ 𝑌 = {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)}    &   ⊢ 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))))
Theorem	stoweidlem60 46037*	This lemma proves that there exists a function g as in the proof in [BrosowskiDeutsh] p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all 𝑡 in 𝑇, there is a 𝑗 such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here 𝐹 is used to represent f in the paper, and 𝐸 is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ 𝐷 = (𝑗 ∈ (0...𝑛) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})    &   ⊢ 𝐵 = (𝑗 ∈ (0...𝑛) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑇 ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 0 ≤ (𝐹‘𝑡))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝐴 ∀𝑡 ∈ 𝑇 ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔‘𝑡))))
Theorem	stoweidlem61 46038*	This lemma proves that there exists a function 𝑔 as in the proof in [BrosowskiDeutsh] p. 92: 𝑔 is in the subalgebra, and for all 𝑡 in 𝑇, abs( f(t) - g(t) ) < 2*ε. Here 𝐹 is used to represent f in the paper, and 𝐸 is used to represent ε. For this lemma there's the further assumption that the function 𝐹 to be approximated is nonnegative (this assumption is removed in a later theorem). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ (𝜑 → 𝑇 ≠ ∅)    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 0 ≤ (𝐹‘𝑡))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑔‘𝑡) − (𝐹‘𝑡))) < (2 · 𝐸))
Theorem	stoweidlem62 46039*	This theorem proves the Stone Weierstrass theorem for the non-trivial case in which T is nonempty. The proof follows [BrosowskiDeutsh] p. 89 (through page 92). (Contributed by Glauco Siliprandi, 20-Apr-2017.) (Revised by AV, 13-Sep-2020.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑓𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − inf(ran 𝐹, ℝ, < )))    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑇 ≠ ∅)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸)
Theorem	stoweid 46040*	This theorem proves the Stone-Weierstrass theorem for real-valued functions: let 𝐽 be a compact topology on 𝑇, and 𝐶 be the set of real continuous functions on 𝑇. Assume that 𝐴 is a subalgebra of 𝐶 (closed under addition and multiplication of functions) containing constant functions and discriminating points (if 𝑟 and 𝑡 are distinct points in 𝑇, then there exists a function ℎ in 𝐴 such that h(r) is distinct from h(t) ). Then, for any continuous function 𝐹 and for any positive real 𝐸, there exists a function 𝑓 in the subalgebra 𝐴, such that 𝑓 approximates 𝐹 up to 𝐸 (𝐸 represents the usual ε value). As a classical example, given any a, b reals, the closed interval 𝑇 = [𝑎, 𝑏] could be taken, along with the subalgebra 𝐴 of real polynomials on 𝑇, and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on [𝑎, 𝑏]. The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃ℎ ∈ 𝐴 (ℎ‘𝑟) ≠ (ℎ‘𝑡))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸)
Theorem	stowei 46041*	This theorem proves the Stone-Weierstrass theorem for real-valued functions: let 𝐽 be a compact topology on 𝑇, and 𝐶 be the set of real continuous functions on 𝑇. Assume that 𝐴 is a subalgebra of 𝐶 (closed under addition and multiplication of functions) containing constant functions and discriminating points (if 𝑟 and 𝑡 are distinct points in 𝑇, then there exists a function ℎ in 𝐴 such that h(r) is distinct from h(t) ). Then, for any continuous function 𝐹 and for any positive real 𝐸, there exists a function 𝑓 in the subalgebra 𝐴, such that 𝑓 approximates 𝐹 up to 𝐸 (𝐸 represents the usual ε value). As a classical example, given any a, b reals, the closed interval 𝑇 = [𝑎, 𝑏] could be taken, along with the subalgebra 𝐴 of real polynomials on 𝑇, and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on [𝑎, 𝑏]. The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. The deduction version of this theorem is stoweid 46040: often times it will be better to use stoweid 46040 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝐽 ∈ Comp    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ 𝐴 ⊆ 𝐶    &   ⊢ ((𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ (𝑥 ∈ ℝ → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡) → ∃ℎ ∈ 𝐴 (ℎ‘𝑟) ≠ (ℎ‘𝑡))    &   ⊢ 𝐹 ∈ 𝐶    &   ⊢ 𝐸 ∈ ℝ+    ⇒   ⊢ ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸
21.43.13  Wallis' product for π
Theorem	wallispilem1 46042*	𝐼 is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐼‘(𝑁 + 1)) ≤ (𝐼‘𝑁))
Theorem	wallispilem2 46043*	A first set of properties for the sequence 𝐼 that will be used in the proof of the Wallis product formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)    ⇒   ⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (𝑁 ∈ (ℤ≥‘2) → (𝐼‘𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2)))))
Theorem	wallispilem3 46044*	I maps to real values. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐼‘𝑁) ∈ ℝ+)
Theorem	wallispilem4 46045*	𝐹 maps to explicit expression for the ratio of two consecutive values of 𝐼. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))    &   ⊢ 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))    ⇒   ⊢ 𝐺 = 𝐻
Theorem	wallispilem5 46046*	The sequence 𝐻 converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))    &   ⊢ 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))    &   ⊢ 𝐿 = (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛)))    ⇒   ⊢ 𝐻 ⇝ 1
Theorem	wallispi 46047*	Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))    &   ⊢ 𝑊 = (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛))    ⇒   ⊢ 𝑊 ⇝ (π / 2)
Theorem	wallispi2lem1 46048	An intermediate step between the first version of the Wallis' formula for π and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
⊢ (𝑁 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑁) = ((1 / ((2 · 𝑁) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁)))
Theorem	wallispi2lem2 46049	Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for π . (Contributed by Glauco Siliprandi, 30-Jun-2017.)
⊢ (𝑁 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁) = (((2↑(4 · 𝑁)) · ((!‘𝑁)↑4)) / ((!‘(2 · 𝑁))↑2)))
Theorem	wallispi2 46050	An alternative version of Wallis' formula for π ; this second formula uses factorials and it is later used to prove Stirling's approximation formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑉 = (𝑛 ∈ ℕ ↦ ((((2↑(4 · 𝑛)) · ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1)))    ⇒   ⊢ 𝑉 ⇝ (π / 2)
21.43.14  Stirling's approximation formula for ` n ` factorial
Theorem	stirlinglem1 46051	A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1))))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))    &   ⊢ 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))    ⇒   ⊢ 𝐻 ⇝ (1 / 2)
Theorem	stirlinglem2 46052	𝐴 maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝐴‘𝑁) ∈ ℝ+)
Theorem	stirlinglem3 46053	Long but simple algebraic transformations are applied to show that 𝑉, the Wallis formula for π , can be expressed in terms of 𝐴, the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the 𝐴, in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝐴‘(2 · 𝑛)))    &   ⊢ 𝐸 = (𝑛 ∈ ℕ ↦ ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))    &   ⊢ 𝑉 = (𝑛 ∈ ℕ ↦ ((((2↑(4 · 𝑛)) · ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1)))    ⇒   ⊢ 𝑉 = (𝑛 ∈ ℕ ↦ ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))))
Theorem	stirlinglem4 46054*	Algebraic manipulation of ((𝐵 n ) - ( B (𝑛 + 1))). It will be used in other theorems to show that 𝐵 is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))    &   ⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1))    ⇒   ⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) = (𝐽‘𝑁))
Theorem	stirlinglem5 46055*	If 𝑇 is between 0 and 1, then a series (without alternating negative and positive terms) is given that converges to log((1+T)/(1-T)). (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)))    &   ⊢ 𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇↑𝑗) / 𝑗))    &   ⊢ 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)))    &   ⊢ 𝐻 = (𝑗 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1)))))    &   ⊢ 𝐺 = (𝑗 ∈ ℕ0 ↦ ((2 · 𝑗) + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ+)    &   ⊢ (𝜑 → (abs‘𝑇) < 1)    ⇒   ⊢ (𝜑 → seq0( + , 𝐻) ⇝ (log‘((1 + 𝑇) / (1 − 𝑇))))
Theorem	stirlinglem6 46056*	A series that converges to log((𝑁 + 1) / 𝑁). (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐻 = (𝑗 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))    ⇒   ⊢ (𝑁 ∈ ℕ → seq0( + , 𝐻) ⇝ (log‘((𝑁 + 1) / 𝑁)))
Theorem	stirlinglem7 46057*	Algebraic manipulation of the formula for J(n). (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1))    &   ⊢ 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))))    &   ⊢ 𝐻 = (𝑘 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))))    ⇒   ⊢ (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ (𝐽‘𝑁))
Theorem	stirlinglem8 46058	If 𝐴 converges to 𝐶, then 𝐹 converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑛𝐴    &   ⊢ Ⅎ𝑛𝐷    &   ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝐴‘(2 · 𝑛)))    &   ⊢ (𝜑 → 𝐴:ℕ⟶ℝ+)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)))    &   ⊢ 𝐿 = (𝑛 ∈ ℕ ↦ ((𝐴‘𝑛)↑4))    &   ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ((𝐷‘𝑛)↑2))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ⇝ 𝐶)    ⇒   ⊢ (𝜑 → 𝐹 ⇝ (𝐶↑2))
Theorem	stirlinglem9 46059*	((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) is expressed as a limit of a series. This result will be used both to prove that 𝐵 is decreasing and to prove that 𝐵 is bounded (below). It will follow that 𝐵 converges in the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))    &   ⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1))    &   ⊢ 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))))    ⇒   ⊢ (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))))
Theorem	stirlinglem10 46060*	A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole 𝐵 sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))    &   ⊢ 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))))    &   ⊢ 𝐿 = (𝑘 ∈ ℕ ↦ ((1 / (((2 · 𝑁) + 1)↑2))↑𝑘))    ⇒   ⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) ≤ ((1 / 4) · (1 / (𝑁 · (𝑁 + 1)))))
Theorem	stirlinglem11 46061*	𝐵 is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))    &   ⊢ 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) < (𝐵‘𝑁))
Theorem	stirlinglem12 46062*	The sequence 𝐵 is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1))))    ⇒   ⊢ (𝑁 ∈ ℕ → ((𝐵‘1) − (1 / 4)) ≤ (𝐵‘𝑁))
Theorem	stirlinglem13 46063*	𝐵 is decreasing and has a lower bound, then it converges. Since 𝐵 is log𝐴, in another theorem it is proven that 𝐴 converges as well. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))    ⇒   ⊢ ∃𝑑 ∈ ℝ 𝐵 ⇝ 𝑑
Theorem	stirlinglem14 46064*	The sequence 𝐴 converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for π& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))    ⇒   ⊢ ∃𝑐 ∈ ℝ+ 𝐴 ⇝ 𝑐
Theorem	stirlinglem15 46065*	The Stirling's formula is proven using a number of local definitions. The main theorem stirling 46066 will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑛𝜑    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ ((√‘((2 · π) · 𝑛)) · ((𝑛 / e)↑𝑛)))    &   ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝐴‘(2 · 𝑛)))    &   ⊢ 𝐸 = (𝑛 ∈ ℕ ↦ ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))    &   ⊢ 𝑉 = (𝑛 ∈ ℕ ↦ ((((2↑(4 · 𝑛)) · ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ⇝ 𝐶)    ⇒   ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((!‘𝑛) / (𝑆‘𝑛))) ⇝ 1)
Theorem	stirling 46066	Stirling's approximation formula for 𝑛 factorial. The proof follows two major steps: first it is proven that 𝑆 and 𝑛 factorial are asymptotically equivalent, up to an unknown constant. Then, using Wallis' formula for π it is proven that the unknown constant is the square root of π and then the exact Stirling's formula is established. This is Metamath 100 proof #90. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ ((√‘((2 · π) · 𝑛)) · ((𝑛 / e)↑𝑛)))    ⇒   ⊢ (𝑛 ∈ ℕ ↦ ((!‘𝑛) / (𝑆‘𝑛))) ⇝ 1
Theorem	stirlingr 46067	Stirling's approximation formula for 𝑛 factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling 46066 is proven for convergence in the topology of complex numbers. The variable 𝑅 is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ ((√‘((2 · π) · 𝑛)) · ((𝑛 / e)↑𝑛)))    &   ⊢ 𝑅 = (⇝𝑡‘(topGen‘ran (,)))    ⇒   ⊢ (𝑛 ∈ ℕ ↦ ((!‘𝑛) / (𝑆‘𝑛)))𝑅1
21.43.15  Dirichlet kernel
Theorem	dirkerval 46068*	The Nth Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) = (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))
Theorem	dirker2re 46069	The Dirichlet Kernel value is a real if the argument is not a multiple of π . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ) ∧ ¬ (𝑆 mod (2 · π)) = 0) → ((sin‘((𝑁 + (1 / 2)) · 𝑆)) / ((2 · π) · (sin‘(𝑆 / 2)))) ∈ ℝ)
Theorem	dirkerdenne0 46070	The Dirichlet Kernel denominator is never 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝑆 ∈ ℝ ∧ ¬ (𝑆 mod (2 · π)) = 0) → ((2 · π) · (sin‘(𝑆 / 2))) ≠ 0)
Theorem	dirkerval2 46071*	The Nth Dirichlet Kernel evaluated at a specific point 𝑆. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ) → ((𝐷‘𝑁)‘𝑆) = if((𝑆 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑆)) / ((2 · π) · (sin‘(𝑆 / 2))))))
Theorem	dirkerre 46072*	The Dirichlet Kernel at any point evaluates to a real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ) → ((𝐷‘𝑁)‘𝑆) ∈ ℝ)
Theorem	dirkerper 46073*	the Dirichlet Kernel has period 2π. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    &   ⊢ 𝑇 = (2 · π)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ) → ((𝐷‘𝑁)‘(𝑥 + 𝑇)) = ((𝐷‘𝑁)‘𝑥))
Theorem	dirkerf 46074*	For any natural number 𝑁, the Dirichlet Kernel (𝐷‘𝑁) is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ)
Theorem	dirkertrigeqlem1 46075*	Sum of an even number of alternating cos values. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐾 ∈ ℕ → Σ𝑛 ∈ (1...(2 · 𝐾))(cos‘(𝑛 · π)) = 0)
Theorem	dirkertrigeqlem2 46076*	Trigonomic equality lemma for the Dirichlet Kernel trigonomic equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (sin‘𝐴) ≠ 0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
Theorem	dirkertrigeqlem3 46077*	Trigonometric equality lemma for the Dirichlet Kernel trigonometric equality. Here we handle the case for an angle that's an odd multiple of π. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ 𝐴 = (((2 · 𝐾) + 1) · π)    ⇒   ⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
Theorem	dirkertrigeq 46078*	Trigonometric equality for the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐹 = (𝐷‘𝑁)    &   ⊢ 𝐻 = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑘 ∈ (1...𝑁)(cos‘(𝑘 · 𝑠))) / π))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐻)
Theorem	dirkeritg 46079*	The definite integral of the Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝑥 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑥)) / ((2 · π) · (sin‘(𝑥 / 2)))))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐹 = (𝐷‘𝑁)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 / 2) + Σ𝑘 ∈ (1...𝑁)((sin‘(𝑘 · 𝑥)) / 𝑘)) / π))    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐹‘𝑥) d𝑥 = ((𝐺‘𝐵) − (𝐺‘𝐴)))
Theorem	dirkercncflem1 46080*	If 𝑌 is a multiple of π then it belongs to an open inerval (𝐴(,)𝐵) such that for any other point 𝑦 in the interval, cos y/2 and sin y/2 are nonzero. Such an interval is needed to apply De L'Hopital theorem. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐴 = (𝑌 − π)    &   ⊢ 𝐵 = (𝑌 + π)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)    ⇒   ⊢ (𝜑 → (𝑌 ∈ (𝐴(,)𝐵) ∧ ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0)))
Theorem	dirkercncflem2 46081*	Lemma used to prove that the Dirichlet Kernel is continuous at 𝑌 points that are multiples of (2 · π). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    &   ⊢ 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))    &   ⊢ 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0)    &   ⊢ 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))    &   ⊢ 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))    &   ⊢ 𝐿 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) limℂ 𝑌))
Theorem	dirkercncflem3 46082*	The Dirichlet Kernel is continuous at 𝑌 points that are multiples of (2 · π). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    &   ⊢ 𝐴 = (𝑌 − π)    &   ⊢ 𝐵 = (𝑌 + π)    &   ⊢ 𝐹 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))    &   ⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑦 / 2))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)    ⇒   ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ ((𝐷‘𝑁) limℂ 𝑌))
Theorem	dirkercncflem4 46083*	The Dirichlet Kernel is continuos at points that are not multiple of 2 π . This is the easier condition, for the proof of the continuity of the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → (𝑌 mod (2 · π)) ≠ 0)    &   ⊢ 𝐴 = (⌊‘(𝑌 / (2 · π)))    &   ⊢ 𝐵 = (𝐴 + 1)    &   ⊢ 𝐶 = (𝐴 · (2 · π))    &   ⊢ 𝐸 = (𝐵 · (2 · π))    ⇒   ⊢ (𝜑 → (𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP (topGen‘ran (,)))‘𝑌))
Theorem	dirkercncf 46084*	For any natural number 𝑁, the Dirichlet Kernel (𝐷‘𝑁) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ))
21.43.16  Fourier Series
Theorem	fourierdlem1 46085	A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))    &   ⊢ (𝜑 → 𝑋 ∈ ((𝑄‘𝐼)[,](𝑄‘(𝐼 + 1))))    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))
Theorem	fourierdlem2 46086*	Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    ⇒   ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
Theorem	fourierdlem3 46087*	Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ ((-π[,]π) ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    ⇒   ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ ((-π[,]π) ↑m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
Theorem	fourierdlem4 46088*	𝐸 is a function that maps any point to a periodic corresponding point in (𝐴, 𝐵]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))    ⇒   ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
Theorem	fourierdlem5 46089*	𝑆 is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑆 = (𝑥 ∈ (-π[,]π) ↦ (sin‘((𝑋 + (1 / 2)) · 𝑥)))    ⇒   ⊢ (𝑋 ∈ ℝ → 𝑆:(-π[,]π)⟶ℝ)
Theorem	fourierdlem6 46090	𝑋 is in the periodic partition, when the considered interval is centered at 𝑋. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝐼 ∈ ℤ)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → 𝐼 < 𝐽)    &   ⊢ (𝜑 → (𝑋 + (𝐼 · 𝑇)) ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (𝑋 + (𝐽 · 𝑇)) ∈ (𝐴[,]𝐵))    ⇒   ⊢ (𝜑 → 𝐽 = (𝐼 + 1))
Theorem	fourierdlem7 46091*	The difference between the periodic sawtooth function and the identity function is decreasing. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ≤ ((𝐸‘𝑋) − 𝑋))
Theorem	fourierdlem8 46092	A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐼)[,](𝑄‘(𝐼 + 1))) ⊆ (𝐴[,]𝐵))
Theorem	fourierdlem9 46093*	𝐻 is a complex function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ)    &   ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))    ⇒   ⊢ (𝜑 → 𝐻:(-π[,]π)⟶ℝ)
Theorem	fourierdlem10 46094	Condition on the bounds of a nonempty subinterval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    &   ⊢ (𝜑 → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵))
Theorem	fourierdlem11 46095*	If there is a partition, than the lower bound is strictly less than the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    ⇒   ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
Theorem	fourierdlem12 46096*	A point of a partition is not an element of any open interval determined by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑄)    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
Theorem	fourierdlem13 46097*	Value of 𝑉 in terms of value of 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑋) ∧ (𝑝‘𝑚) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))    &   ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐼) = ((𝑉‘𝐼) − 𝑋) ∧ (𝑉‘𝐼) = (𝑋 + (𝑄‘𝐼))))
Theorem	fourierdlem14 46098*	Given the partition 𝑉, 𝑄 is the partition shifted to the left by 𝑋. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑋) ∧ (𝑝‘𝑚) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))    &   ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))    ⇒   ⊢ (𝜑 → 𝑄 ∈ (𝑂‘𝑀))
Theorem	fourierdlem15 46099*	The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    ⇒   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
Theorem	fourierdlem16 46100*	The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ 𝐶 = (-π(,)π)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐶) ∈ 𝐿1)    &   ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (((𝐴‘𝑁) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿1) ∧ ∫𝐶((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 ∈ ℝ))