Home Metamath Proof ExplorerTheorem List (p. 413 of 437) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-28351) Hilbert Space Explorer (28352-29876) Users' Mathboxes (29877-43667)

Theorem List for Metamath Proof Explorer - 41201-41300   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremstoweidlem47 41201* Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
𝑡𝐹    &   𝑡𝑆    &   𝑡𝜑    &   𝑇 = 𝐽    &   𝐺 = (𝑇 × {-𝑆})    &   𝐾 = (topGen‘ran (,))    &   (𝜑𝐽 ∈ Top)    &   𝐶 = (𝐽 Cn 𝐾)    &   (𝜑𝐹𝐶)    &   (𝜑𝑆 ∈ ℝ)       (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡) − 𝑆)) ∈ 𝐶)

Theoremstoweidlem48 41202* 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)    &   ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)    &   ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)    &   (𝜑𝐸 ∈ ℝ+)       (𝜑 → ∀𝑡𝐷 (𝑋𝑡) < 𝐸)

Theoremstoweidlem49 41203* 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 − 𝐸) < (𝑦𝑡) ∧ ∀𝑡 ∈ (𝑇𝑈)(𝑦𝑡) < 𝐸))

Theoremstoweidlem50 41204* 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 ∧ 𝑢𝑊 ∧ (𝑇𝑈) ⊆ 𝑢))

Theoremstoweidlem51 41205* 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 − 𝐸) < (𝑥𝑡))))

Theoremstoweidlem52 41206* There exists a neighborood 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 − 𝑒) < (𝑥𝑡))))

Theoremstoweidlem53 41207* 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(t_0) = 0, and p > 0 on T - U. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
𝑡𝑈    &   𝑡𝜑    &   𝐾 = (topGen‘ran (,))    &   𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}    &   𝑊 = {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}    &   𝑇 = 𝐽    &   𝐶 = (𝐽 Cn 𝐾)    &   (𝜑𝐽 ∈ Comp)    &   (𝜑𝐴𝐶)    &   ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)    &   ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)    &   ((𝜑𝑥 ∈ ℝ) → (𝑡𝑇𝑥) ∈ 𝐴)    &   ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))    &   (𝜑𝑈𝐽)    &   (𝜑 → (𝑇𝑈) ≠ ∅)    &   (𝜑𝑍𝑈)       (𝜑 → ∃𝑝𝐴 (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)))

Theoremstoweidlem54 41208* 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 − 𝐸) < (𝑥𝑡)))

Theoremstoweidlem55 41209* 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(t_0) = 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 < (𝑝𝑡)))

Theoremstoweidlem56 41210* 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 − 𝑒) < (𝑥𝑡))))

Theoremstoweidlem57 41211* 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 − 𝐸) < (𝑥𝑡)))

Theoremstoweidlem58 41212* 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 − 𝐸) < (𝑥𝑡)))

Theoremstoweidlem59 41213* 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 - \epslon / 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 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))))

Theoremstoweidlem60 41214* 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)) · 𝐸) < (𝑔𝑡))))

Theoremstoweidlem61 41215* 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 · 𝐸))

Theoremstoweidlem62 41216* 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‘((𝑓𝑡) − (𝐹𝑡))) < 𝐸)

Theoremstoweid 41217* 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‘((𝑓𝑡) − (𝐹𝑡))) < 𝐸)

Theoremstowei 41218* 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 41217: often times it will be better to use stoweid 41217 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‘((𝑓𝑡) − (𝐹𝑡))) < 𝐸

20.33.13  Wallis' product for π

Theoremwallispilem1 41219* 𝐼 is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → (𝐼‘(𝑁 + 1)) ≤ (𝐼𝑁))

Theoremwallispilem2 41220* 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)))))

Theoremwallispilem3 41221* I maps to real values. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)       (𝑁 ∈ ℕ0 → (𝐼𝑁) ∈ ℝ+)

Theoremwallispilem4 41222* 𝐹 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( · , 𝐹)‘𝑛))))       𝐺 = 𝐻

Theoremwallispilem5 41223* 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

Theoremwallispi 41224* Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))    &   𝑊 = (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛))       𝑊 ⇝ (π / 2)

Theoremwallispi2lem1 41225 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))))‘𝑁)))

Theoremwallispi2lem2 41226 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)))

Theoremwallispi2 41227 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)

20.33.14  Stirling's approximation formula for ` n ` factorial

Theoremstirlinglem1 41228 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)

Theoremstirlinglem2 41229 𝐴 maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))       (𝑁 ∈ ℕ → (𝐴𝑁) ∈ ℝ+)

Theoremstirlinglem3 41230 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)))))

Theoremstirlinglem4 41231* 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))) = (𝐽𝑁))

Theoremstirlinglem5 41232* 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 − 𝑇))))

Theoremstirlinglem6 41233* A series that converges to log (N+1)/N. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
𝐻 = (𝑗 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))       (𝑁 ∈ ℕ → seq0( + , 𝐻) ⇝ (log‘((𝑁 + 1) / 𝑁)))

Theoremstirlinglem7 41234* 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( + , 𝐾) ⇝ (𝐽𝑁))

Theoremstirlinglem8 41235 If 𝐴 converges to 𝐶, then 𝐹 converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
𝑛𝜑    &   𝑛𝐴    &   𝑛𝐷    &   𝐷 = (𝑛 ∈ ℕ ↦ (𝐴‘(2 · 𝑛)))    &   (𝜑𝐴:ℕ⟶ℝ+)    &   𝐹 = (𝑛 ∈ ℕ ↦ (((𝐴𝑛)↑4) / ((𝐷𝑛)↑2)))    &   𝐿 = (𝑛 ∈ ℕ ↦ ((𝐴𝑛)↑4))    &   𝑀 = (𝑛 ∈ ℕ ↦ ((𝐷𝑛)↑2))    &   ((𝜑𝑛 ∈ ℕ) → (𝐷𝑛) ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐴𝐶)       (𝜑𝐹 ⇝ (𝐶↑2))

Theoremstirlinglem9 41236* ((𝐵𝑁) − (𝐵‘(𝑁 + 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))))

Theoremstirlinglem10 41237* 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)))))

Theoremstirlinglem11 41238* 𝐵 is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴𝑛)))    &   𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))))       (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) < (𝐵𝑁))

Theoremstirlinglem12 41239* The sequence 𝐵 is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴𝑛)))    &   𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1))))       (𝑁 ∈ ℕ → ((𝐵‘1) − (1 / 4)) ≤ (𝐵𝑁))

Theoremstirlinglem13 41240* 𝐵 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‘(𝐴𝑛)))       𝑑 ∈ ℝ 𝐵𝑑

Theoremstirlinglem14 41241* 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‘(𝐴𝑛)))       𝑐 ∈ ℝ+ 𝐴𝑐

Theoremstirlinglem15 41242* The Stirling's formula is proven using a number of local definitions. The main theorem stirling 41243 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)

Theoremstirling 41243 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

Theoremstirlingr 41244 Stirling's approximation formula for 𝑛 factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling 41243 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

20.33.15  Dirichlet kernel

Theoremdirkerval 41245* 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)))))))

Theoremdirker2re 41246 The Dirchlet 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)))) ∈ ℝ)

Theoremdirkerdenne0 41247 The Dirchlet Kernel denominator is never 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
((𝑆 ∈ ℝ ∧ ¬ (𝑆 mod (2 · π)) = 0) → ((2 · π) · (sin‘(𝑆 / 2))) ≠ 0)

Theoremdirkerval2 41248* 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))))))

Theoremdirkerre 41249* 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)))))))       ((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ) → ((𝐷𝑁)‘𝑆) ∈ ℝ)

Theoremdirkerper 41250* the Dirichlet Kernel has period . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    &   𝑇 = (2 · π)       ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ) → ((𝐷𝑁)‘(𝑥 + 𝑇)) = ((𝐷𝑁)‘𝑥))

Theoremdirkerf 41251* 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)))))))       (𝑁 ∈ ℕ → (𝐷𝑁):ℝ⟶ℝ)

Theoremdirkertrigeqlem1 41252* Sum of an even number of alternating cos values. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝐾 ∈ ℕ → Σ𝑛 ∈ (1...(2 · 𝐾))(cos‘(𝑛 · π)) = 0)

Theoremdirkertrigeqlem2 41253* 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)))))

Theoremdirkertrigeqlem3 41254* 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)))))

Theoremdirkertrigeq 41255* 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‘(𝑘 · 𝑠))) / π))       (𝜑𝐹 = 𝐻)

Theoremdirkeritg 41256* 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𝑥 = ((𝐺𝐵) − (𝐺𝐴)))

Theoremdirkercncflem1 41257* 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)))

Theoremdirkercncflem2 41258* 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 𝑌))

Theoremdirkercncflem3 41259* 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 𝑌))

Theoremdirkercncflem4 41260* 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 (,)))‘𝑌))

Theoremdirkercncf 41261* 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→ℝ))

20.33.16  Fourier Series

Theoremfourierdlem1 41262 A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))    &   (𝜑𝐼 ∈ (0..^𝑀))    &   (𝜑𝑋 ∈ ((𝑄𝐼)[,](𝑄‘(𝐼 + 1))))       (𝜑𝑋 ∈ (𝐴[,]𝐵))

Theoremfourierdlem2 41263* Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})       (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))

Theoremfourierdlem3 41264* Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ ((-π[,]π) ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})       (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ ((-π[,]π) ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))

Theoremfourierdlem4 41265* 𝐸 is a function that maps any point to a periodic corresponding point in (𝐴, 𝐵]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   𝑇 = (𝐵𝐴)    &   𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))       (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))

Theoremfourierdlem5 41266* 𝑆 is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
𝑆 = (𝑥 ∈ (-π[,]π) ↦ (sin‘((𝑋 + (1 / 2)) · 𝑥)))       (𝑋 ∈ ℝ → 𝑆:(-π[,]π)⟶ℝ)

Theoremfourierdlem6 41267 𝑋 is in the periodic partition, when the considered interval is centered at 𝑋. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   𝑇 = (𝐵𝐴)    &   (𝜑𝑋 ∈ ℝ)    &   (𝜑𝐼 ∈ ℤ)    &   (𝜑𝐽 ∈ ℤ)    &   (𝜑𝐼 < 𝐽)    &   (𝜑 → (𝑋 + (𝐼 · 𝑇)) ∈ (𝐴[,]𝐵))    &   (𝜑 → (𝑋 + (𝐽 · 𝑇)) ∈ (𝐴[,]𝐵))       (𝜑𝐽 = (𝐼 + 1))

Theoremfourierdlem7 41268* The difference between the periodic sawtooth function and the identity function is decreasing. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   𝑇 = (𝐵𝐴)    &   𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))    &   (𝜑𝑋 ∈ ℝ)    &   (𝜑𝑌 ∈ ℝ)    &   (𝜑𝑋𝑌)       (𝜑 → ((𝐸𝑌) − 𝑌) ≤ ((𝐸𝑋) − 𝑋))

Theoremfourierdlem8 41269 A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))    &   (𝜑𝐼 ∈ (0..^𝑀))       (𝜑 → ((𝑄𝐼)[,](𝑄‘(𝐼 + 1))) ⊆ (𝐴[,]𝐵))

Theoremfourierdlem9 41270* 𝐻 is a complex function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐹:ℝ⟶ℝ)    &   (𝜑𝑋 ∈ ℝ)    &   (𝜑𝑌 ∈ ℝ)    &   (𝜑𝑊 ∈ ℝ)    &   𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))       (𝜑𝐻:(-π[,]π)⟶ℝ)

Theoremfourierdlem10 41271 Condition on the bounds of a nonempty subinterval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐷 ∈ ℝ)    &   (𝜑𝐶 < 𝐷)    &   (𝜑 → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵))       (𝜑 → (𝐴𝐶𝐷𝐵))

Theoremfourierdlem11 41272* If there is a partition, than the lower bound is strictly less than the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑄 ∈ (𝑃𝑀))       (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))

Theoremfourierdlem12 41273* A point of a partition is not an element of any open interval determined by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑄 ∈ (𝑃𝑀))    &   (𝜑𝑋 ∈ ran 𝑄)       ((𝜑𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))

Theoremfourierdlem13 41274* Value of 𝑉 in terms of value of 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑋 ∈ ℝ)    &   𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑋) ∧ (𝑝𝑚) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑉 ∈ (𝑃𝑀))    &   (𝜑𝐼 ∈ (0...𝑀))    &   𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))       (𝜑 → ((𝑄𝐼) = ((𝑉𝐼) − 𝑋) ∧ (𝑉𝐼) = (𝑋 + (𝑄𝐼))))

Theoremfourierdlem14 41275* Given the partition 𝑉, 𝑄 is the partition shifted to the left by 𝑋. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑋 ∈ ℝ)    &   𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑋) ∧ (𝑝𝑚) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})    &   𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑉 ∈ (𝑃𝑀))    &   𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))       (𝜑𝑄 ∈ (𝑂𝑀))

Theoremfourierdlem15 41276* The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑄 ∈ (𝑃𝑀))       (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))

Theoremfourierdlem16 41277* 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𝑥 ∈ ℝ))

Theoremfourierdlem17 41278* The defined 𝐿 is actually a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   𝐿 = (𝑥 ∈ (𝐴(,]𝐵) ↦ if(𝑥 = 𝐵, 𝐴, 𝑥))       (𝜑𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))

Theoremfourierdlem18 41279* The function 𝑆 is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝑁 ∈ ℝ)    &   𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠)))       (𝜑𝑆 ∈ ((-π[,]π)–cn→ℝ))

Theoremfourierdlem19 41280* If two elements of 𝐷 have the same periodic image in (𝐴(,]𝐵) then they are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑𝑋 ∈ ℝ)    &   𝐷 = {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}    &   𝑇 = (𝐵𝐴)    &   𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))    &   (𝜑𝑊𝐷)    &   (𝜑𝑍𝐷)    &   (𝜑 → (𝐸𝑍) = (𝐸𝑊))       (𝜑 → ¬ 𝑊 < 𝑍)

Theoremfourierdlem20 41281* Every interval in the partition 𝑆 is included in an interval of the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴𝐵)    &   (𝜑𝑄:(0...𝑀)⟶ℝ)    &   (𝜑 → (𝑄‘0) ≤ 𝐴)    &   (𝜑𝐵 ≤ (𝑄𝑀))    &   (𝜑𝐽 ∈ (0..^𝑁))    &   𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))    &   (𝜑𝑆 Isom < , < ((0...𝑁), 𝑇))    &   𝐼 = sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) ≤ (𝑆𝐽)}, ℝ, < )       (𝜑 → ∃𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))

Theoremfourierdlem21 41282* The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐹:ℝ⟶ℝ)    &   𝐶 = (-π(,)π)    &   (𝜑 → (𝐹𝐶) ∈ 𝐿1)    &   𝐵 = (𝑛 ∈ ℕ ↦ (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))    &   (𝜑𝑁 ∈ ℕ)       (𝜑 → (((𝐵𝑁) ∈ ℝ ∧ (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 ∈ ℝ))

Theoremfourierdlem22 41283* The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐹:ℝ⟶ℝ)    &   𝐶 = (-π(,)π)    &   (𝜑 → (𝐹𝐶) ∈ 𝐿1)    &   𝐴 = (𝑛 ∈ ℕ0 ↦ (∫𝐶((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))    &   𝐵 = (𝑛 ∈ ℕ ↦ (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))       (𝜑 → ((𝑛 ∈ ℕ0 → (𝐴𝑛) ∈ ℝ) ∧ (𝑛 ∈ ℕ → (𝐵𝑛) ∈ ℝ)))

Theoremfourierdlem23 41284* If 𝐹 is continuous and 𝑋 is constant, then (𝐹‘(𝑋 + 𝑠)) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ⊆ ℂ)    &   (𝜑𝐹 ∈ (𝐴cn→ℂ))    &   (𝜑𝐵 ⊆ ℂ)    &   (𝜑𝑋 ∈ ℂ)    &   ((𝜑𝑠𝐵) → (𝑋 + 𝑠) ∈ 𝐴)       (𝜑 → (𝑠𝐵 ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (𝐵cn→ℂ))

Theoremfourierdlem24 41285 A sufficient condition for module being nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝐴 ∈ ((-π[,]π) ∖ {0}) → (𝐴 mod (2 · π)) ≠ 0)

Theoremfourierdlem25 41286* If 𝐶 is not in the range of the partition, then it is in an open interval induced by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝑄:(0...𝑀)⟶ℝ)    &   (𝜑𝐶 ∈ ((𝑄‘0)[,](𝑄𝑀)))    &   (𝜑 → ¬ 𝐶 ∈ ran 𝑄)    &   𝐼 = sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}, ℝ, < )       (𝜑 → ∃𝑗 ∈ (0..^𝑀)𝐶 ∈ ((𝑄𝑗)(,)(𝑄‘(𝑗 + 1))))

Theoremfourierdlem26 41287* Periodic image of a point 𝑌 that's in the period that begins with the point 𝑋. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   𝑇 = (𝐵𝐴)    &   𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))    &   (𝜑𝑋 ∈ ℝ)    &   (𝜑 → (𝐸𝑋) = 𝐵)    &   (𝜑𝑌 ∈ (𝑋(,](𝑋 + 𝑇)))       (𝜑 → (𝐸𝑌) = (𝐴 + (𝑌𝑋)))

Theoremfourierdlem27 41288 A partition open interval is a subset of the partitioned open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))    &   (𝜑𝐼 ∈ (0..^𝑀))       (𝜑 → ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (𝐴(,)𝐵))

Theoremfourierdlem28 41289* Derivative of (𝐹‘(𝑋 + 𝑠)). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐹:ℝ⟶ℝ)    &   (𝜑𝑋 ∈ ℝ)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   𝐷 = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))    &   (𝜑𝐷:((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)       (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐷‘(𝑋 + 𝑠))))

Theoremfourierdlem29 41290* Explicit function value for 𝐾 applied to 𝐴. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))       (𝐴 ∈ (-π[,]π) → (𝐾𝐴) = if(𝐴 = 0, 1, (𝐴 / (2 · (sin‘(𝐴 / 2))))))

Theoremfourierdlem30 41291* Sum of three small pieces is less than ε. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑 → (𝑥𝐼 ↦ (𝐹 · -𝐺)) ∈ 𝐿1)    &   ((𝜑𝑥𝐼) → 𝐹 ∈ ℂ)    &   ((𝜑𝑥𝐼) → 𝐺 ∈ ℂ)    &   (𝜑𝐴 ∈ ℂ)    &   𝑋 = (abs‘𝐴)    &   (𝜑𝐶 ∈ ℂ)    &   𝑌 = (abs‘𝐶)    &   𝑍 = (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)    &   (𝜑𝐸 ∈ ℝ+)    &   (𝜑𝑅 ∈ ℝ)    &   (𝜑 → ((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1) ≤ 𝑅)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑 → (abs‘𝐵) ≤ 1)    &   (𝜑𝐷 ∈ ℂ)    &   (𝜑 → (abs‘𝐷) ≤ 1)       (𝜑 → (abs‘(((𝐴 · -(𝐵 / 𝑅)) − (𝐶 · -(𝐷 / 𝑅))) − ∫𝐼(𝐹 · -(𝐺 / 𝑅)) d𝑥)) < 𝐸)

Theoremfourierdlem31 41292* If 𝐴 is finite and for any element in 𝐴 there is a number 𝑚 such that a property holds for all numbers larger than 𝑚, then there is a number 𝑛 such that the property holds for all numbers larger than 𝑛 and for all elements in 𝐴. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.)
𝑖𝜑    &   𝑟𝜑    &   𝑖𝑉    &   (𝜑𝐴 ∈ Fin)    &   (𝜑 → ∀𝑖𝐴𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)    &   𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}    &   𝑉 = (𝑖𝐴 ↦ inf(𝑀, ℝ, < ))    &   𝑁 = sup(ran 𝑉, ℝ, < )       (𝜑 → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)

Theoremfourierdlem32 41293 Limit of a continuous function on an open subinterval. Lower bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   (𝜑𝑅 ∈ (𝐹 lim 𝐴))    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐷 ∈ ℝ)    &   (𝜑𝐶 < 𝐷)    &   (𝜑 → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵))    &   𝑌 = if(𝐶 = 𝐴, 𝑅, (𝐹𝐶))    &   𝐽 = ((TopOpen‘ℂfld) ↾t (𝐴[,)𝐵))       (𝜑𝑌 ∈ ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐶))

Theoremfourierdlem33 41294 Limit of a continuous function on an open subinterval. Upper bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   (𝜑𝐿 ∈ (𝐹 lim 𝐵))    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐷 ∈ ℝ)    &   (𝜑𝐶 < 𝐷)    &   (𝜑 → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵))    &   𝑌 = if(𝐷 = 𝐵, 𝐿, (𝐹𝐷))    &   𝐽 = ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵}))       (𝜑𝑌 ∈ ((𝐹 ↾ (𝐶(,)𝐷)) lim 𝐷))

Theoremfourierdlem34 41295* A partition is one to one. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑄 ∈ (𝑃𝑀))       (𝜑𝑄:(0...𝑀)–1-1→ℝ)

Theoremfourierdlem35 41296 There is a single point in (𝐴(,]𝐵) that's distant from 𝑋 a multiple integer of 𝑇. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)    &   𝑇 = (𝐵𝐴)    &   (𝜑𝑋 ∈ ℝ)    &   (𝜑𝐼 ∈ ℤ)    &   (𝜑𝐽 ∈ ℤ)    &   (𝜑 → (𝑋 + (𝐼 · 𝑇)) ∈ (𝐴(,]𝐵))    &   (𝜑 → (𝑋 + (𝐽 · 𝑇)) ∈ (𝐴(,]𝐵))       (𝜑𝐼 = 𝐽)

Theoremfourierdlem36 41297* 𝐹 is an isomorphism. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ Fin)    &   (𝜑𝐴 ⊆ ℝ)    &   𝐹 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐴))    &   𝑁 = ((♯‘𝐴) − 1)       (𝜑𝐹 Isom < , < ((0...𝑁), 𝐴))

Theoremfourierdlem37 41298* 𝐼 is a function that maps any real point to the point that in the partition that immediately precedes the corresponding periodic point in the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑄 ∈ (𝑃𝑀))    &   𝑇 = (𝐵𝐴)    &   𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))    &   𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))    &   𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ))       (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))})))

Theoremfourierdlem38 41299* The function 𝐹 is continuous on every interval induced by the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐹 ∈ (dom 𝐹cn→ℂ))    &   𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑄 ∈ (𝑃𝑀))    &   𝐻 = (𝐴 ∪ ((-π[,]π) ∖ dom 𝐹))    &   (𝜑 → ran 𝑄 = 𝐻)       ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))

Theoremfourierdlem39 41300* Integration by parts of ∫(𝐴(,)𝐵)((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) d𝑥 (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴𝐵)    &   (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))    &   𝐺 = (ℝ D 𝐹)    &   (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦)    &   (𝜑𝑅 ∈ ℝ+)       (𝜑 → ∫(𝐴(,)𝐵)((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) d𝑥 = ((((𝐹𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅)) − ((𝐹𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅))) − ∫(𝐴(,)𝐵)((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) d𝑥))

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19500 196 19501-19600 197 19601-19700 198 19701-19800 199 19801-19900 200 19901-20000 201 20001-20100 202 20101-20200 203 20201-20300 204 20301-20400 205 20401-20500 206 20501-20600 207 20601-20700 208 20701-20800 209 20801-20900 210 20901-21000 211 21001-21100 212 21101-21200 213 21201-21300 214 21301-21400 215 21401-21500 216 21501-21600 217 21601-21700 218 21701-21800 219 21801-21900 220 21901-22000 221 22001-22100 222 22101-22200 223 22201-22300 224 22301-22400 225 22401-22500 226 22501-22600 227 22601-22700 228 22701-22800 229 22801-22900 230 22901-23000 231 23001-23100 232 23101-23200 233 23201-23300 234 23301-23400 235 23401-23500 236 23501-23600 237 23601-23700 238 23701-23800 239 23801-23900 240 23901-24000 241 24001-24100 242 24101-24200 243 24201-24300 244 24301-24400 245 24401-24500 246 24501-24600 247 24601-24700 248 24701-24800 249 24801-24900 250 24901-25000 251 25001-25100 252 25101-25200 253 25201-25300 254 25301-25400 255 25401-25500 256 25501-25600 257 25601-25700 258 25701-25800 259 25801-25900 260 25901-26000 261 26001-26100 262 26101-26200 263 26201-26300 264 26301-26400 265 26401-26500 266 26501-26600 267 26601-26700 268 26701-26800 269 26801-26900 270 26901-27000 271 27001-27100 272 27101-27200 273 27201-27300 274 27301-27400 275 27401-27500 276 27501-27600 277 27601-27700 278 27701-27800 279 27801-27900 280 27901-28000 281 28001-28100 282 28101-28200 283 28201-28300 284 28301-28400 285 28401-28500 286 28501-28600 287 28601-28700 288 28701-28800 289 28801-28900 290 28901-29000 291 29001-29100 292 29101-29200 293 29201-29300 294 29301-29400 295 29401-29500 296 29501-29600 297 29601-29700 298 29701-29800 299 29801-29900 300 29901-30000 301 30001-30100 302 30101-30200 303 30201-30300 304 30301-30400 305 30401-30500 306 30501-30600 307 30601-30700 308 30701-30800 309 30801-30900 310 30901-31000 311 31001-31100 312 31101-31200 313 31201-31300 314 31301-31400 315 31401-31500 316 31501-31600 317 31601-31700 318 31701-31800 319 31801-31900 320 31901-32000 321 32001-32100 322 32101-32200 323 32201-32300 324 32301-32400 325 32401-32500 326 32501-32600 327 32601-32700 328 32701-32800 329 32801-32900 330 32901-33000 331 33001-33100 332 33101-33200 333 33201-33300 334 33301-33400 335 33401-33500 336 33501-33600 337 33601-33700 338 33701-33800 339 33801-33900 340 33901-34000 341 34001-34100 342 34101-34200 343 34201-34300 344 34301-34400 345 34401-34500 346 34501-34600 347 34601-34700 348 34701-34800 349 34801-34900 350 34901-35000 351 35001-35100 352 35101-35200 353 35201-35300 354 35301-35400 355 35401-35500 356 35501-35600 357 35601-35700 358 35701-35800 359 35801-35900 360 35901-36000 361 36001-36100 362 36101-36200 363 36201-36300 364 36301-36400 365 36401-36500 366 36501-36600 367 36601-36700 368 36701-36800 369 36801-36900 370 36901-37000 371 37001-37100 372 37101-37200 373 37201-37300 374 37301-37400 375 37401-37500 376 37501-37600 377 37601-37700 378 37701-37800 379 37801-37900 380 37901-38000 381 38001-38100 382 38101-38200 383 38201-38300 384 38301-38400 385 38401-38500 386 38501-38600 387 38601-38700 388 38701-38800 389 38801-38900 390 38901-39000 391 39001-39100 392 39101-39200 393 39201-39300 394 39301-39400 395 39401-39500 396 39501-39600 397 39601-39700 398 39701-39800 399 39801-39900 400 39901-40000 401 40001-40100 402 40101-40200 403 40201-40300 404 40301-40400 405 40401-40500 406 40501-40600 407 40601-40700 408 40701-40800 409 40801-40900 410 40901-41000 411 41001-41100 412 41101-41200 413 41201-41300 414 41301-41400 415 41401-41500 416 41501-41600 417 41601-41700 418 41701-41800 419 41801-41900 420 41901-42000 421 42001-42100 422 42101-42200 423 42201-42300 424 42301-42400 425 42401-42500 426 42501-42600 427 42601-42700 428 42701-42800 429 42801-42900 430 42901-43000 431 43001-43100 432 43101-43200 433 43201-43300 434 43301-43400 435 43401-43500 436 43501-43600 437 43601-43667
 Copyright terms: Public domain < Previous  Next >