P. 252 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25101-25200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ulmdvlem3 25101*	Lemma for ulmdv 25102. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋))    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻)    ⇒   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧(𝑆 D 𝐺)(𝐻‘𝑧))
Theorem	ulmdv 25102*	If 𝐹 is a sequence of differentiable functions on 𝑋 which converge pointwise to 𝐺, and the derivatives of 𝐹(𝑛) converge uniformly to 𝐻, then 𝐺 is differentiable with derivative 𝐻. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋))    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻)    ⇒   ⊢ (𝜑 → (𝑆 D 𝐺) = 𝐻)
Theorem	mtest 25103*	The Weierstrass M-test. If 𝐹 is a sequence of functions which are uniformly bounded by the convergent sequence 𝑀(𝑘), then the series generated by the sequence 𝐹 converges uniformly. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑀‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → (abs‘((𝐹‘𝑘)‘𝑧)) ≤ (𝑀‘𝑘))    &   ⊢ (𝜑 → seq𝑁( + , 𝑀) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → seq𝑁( ∘f + , 𝐹) ∈ dom (⇝𝑢‘𝑆))
Theorem	mtestbdd 25104*	Given the hypotheses of the Weierstrass M-test, the convergent function of the sequence is uniformly bounded. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑀‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → (abs‘((𝐹‘𝑘)‘𝑧)) ≤ (𝑀‘𝑘))    &   ⊢ (𝜑 → seq𝑁( + , 𝑀) ∈ dom ⇝ )    &   ⊢ (𝜑 → seq𝑁( ∘f + , 𝐹)(⇝𝑢‘𝑆)𝑇)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘(𝑇‘𝑧)) ≤ 𝑥)
Theorem	mbfulm 25105	A uniform limit of measurable functions is measurable. (This is just a corollary of the fact that a pointwise limit of measurable functions is measurable, see mbflim 24373.) (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶MblFn)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ MblFn)
Theorem	iblulm 25106	A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝐿1)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    &   ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝐿1)
Theorem	itgulm 25107*	A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝐿1)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    &   ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ ∫𝑆((𝐹‘𝑘)‘𝑥) d𝑥) ⇝ ∫𝑆(𝐺‘𝑥) d𝑥)
Theorem	itgulm2 25108*	A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐵) ∈ 𝐿1 ∧ (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥) ⇝ ∫𝑆𝐵 d𝑥))
14.2.3  Power series
Theorem	pserval 25109*	Value of the function 𝐺 that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    ⇒   ⊢ (𝑋 ∈ ℂ → (𝐺‘𝑋) = (𝑚 ∈ ℕ0 ↦ ((𝐴‘𝑚) · (𝑋↑𝑚))))
Theorem	pserval2 25110*	Value of the function 𝐺 that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    ⇒   ⊢ ((𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((𝐺‘𝑋)‘𝑁) = ((𝐴‘𝑁) · (𝑋↑𝑁)))
Theorem	psergf 25111*	The sequence of terms in the infinite sequence defining a power series for fixed 𝑋. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐺‘𝑋):ℕ0⟶ℂ)
Theorem	radcnvlem1 25112*	Lemma for radcnvlt1 25117, radcnvle 25119. If 𝑋 is a point closer to zero than 𝑌 and the power series converges at 𝑌, then it converges absolutely at 𝑋, even if the terms in the sequence are multiplied by 𝑛. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝑋) < (abs‘𝑌))    &   ⊢ (𝜑 → seq0( + , (𝐺‘𝑌)) ∈ dom ⇝ )    &   ⊢ 𝐻 = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))    ⇒   ⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ )
Theorem	radcnvlem2 25113*	Lemma for radcnvlt1 25117, radcnvle 25119. If 𝑋 is a point closer to zero than 𝑌 and the power series converges at 𝑌, then it converges absolutely at 𝑋. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝑋) < (abs‘𝑌))    &   ⊢ (𝜑 → seq0( + , (𝐺‘𝑌)) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → seq0( + , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ )
Theorem	radcnvlem3 25114*	Lemma for radcnvlt1 25117, radcnvle 25119. If 𝑋 is a point closer to zero than 𝑌 and the power series converges at 𝑌, then it converges at 𝑋. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝑋) < (abs‘𝑌))    &   ⊢ (𝜑 → seq0( + , (𝐺‘𝑌)) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ )
Theorem	radcnv0 25115*	Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    ⇒   ⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
Theorem	radcnvcl 25116*	The radius of convergence 𝑅 of an infinite series is a nonnegative extended real number. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    ⇒   ⊢ (𝜑 → 𝑅 ∈ (0[,]+∞))
Theorem	radcnvlt1 25117*	If 𝑋 is within the open disk of radius 𝑅 centered at zero, then the infinite series converges absolutely at 𝑋, and also converges when the series is multiplied by 𝑛. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝑋) < 𝑅)    &   ⊢ 𝐻 = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))    ⇒   ⊢ (𝜑 → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ ))
Theorem	radcnvlt2 25118*	If 𝑋 is within the open disk of radius 𝑅 centered at zero, then the infinite series converges at 𝑋. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝑋) < 𝑅)    ⇒   ⊢ (𝜑 → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ )
Theorem	radcnvle 25119*	If 𝑋 is a convergent point of the infinite series, then 𝑋 is within the closed disk of radius 𝑅 centered at zero. Or, by contraposition, the series diverges at any point strictly more than 𝑅 from the origin. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → (abs‘𝑋) ≤ 𝑅)
Theorem	dvradcnv 25120*	The radius of convergence of the (formal) derivative 𝐻 of the power series 𝐺 is at least as large as the radius of convergence of 𝐺. (In fact they are equal, but we don't have as much use for the negative side of this claim.) (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝑋) < 𝑅)    ⇒   ⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ )
Theorem	pserulm 25121*	If 𝑆 is a region contained in a circle of radius 𝑀 < 𝑅, then the sequence of partial sums of the infinite series converges uniformly on 𝑆. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 < 𝑅)    &   ⊢ (𝜑 → 𝑆 ⊆ (◡abs “ (0[,]𝑀)))    ⇒   ⊢ (𝜑 → 𝐻(⇝𝑢‘𝑆)𝐹)
Theorem	psercn2 25122*	Since by pserulm 25121 the series converges uniformly, it is also continuous by ulmcn 25098. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 < 𝑅)    &   ⊢ (𝜑 → 𝑆 ⊆ (◡abs “ (0[,]𝑀)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ))
Theorem	psercnlem2 25123*	Lemma for psercn 25125. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝑆 = (◡abs “ (0[,)𝑅))    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ − ))𝑀) ∧ (0(ball‘(abs ∘ − ))𝑀) ⊆ (◡abs “ (0[,]𝑀)) ∧ (◡abs “ (0[,]𝑀)) ⊆ 𝑆))
Theorem	psercnlem1 25124*	Lemma for psercn 25125. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝑆 = (◡abs “ (0[,)𝑅))    &   ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅))
Theorem	psercn 25125*	An infinite series converges to a continuous function on the open disk of radius 𝑅, where 𝑅 is the radius of convergence of the series. (Contributed by Mario Carneiro, 4-Mar-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝑆 = (◡abs “ (0[,)𝑅))    &   ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ))
Theorem	pserdvlem1 25126*	Lemma for pserdv 25128. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝑆 = (◡abs “ (0[,)𝑅))    &   ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+ ∧ (abs‘𝑎) < (((abs‘𝑎) + 𝑀) / 2) ∧ (((abs‘𝑎) + 𝑀) / 2) < 𝑅))
Theorem	pserdvlem2 25127*	Lemma for pserdv 25128. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝑆 = (◡abs “ (0[,)𝑅))    &   ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))    &   ⊢ 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (ℂ D (𝐹 ↾ 𝐵)) = (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))))
Theorem	pserdv 25128*	The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝑆 = (◡abs “ (0[,)𝑅))    &   ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))    &   ⊢ 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2))    ⇒   ⊢ (𝜑 → (ℂ D 𝐹) = (𝑦 ∈ 𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))))
Theorem	pserdv2 25129*	The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝑆 = (◡abs “ (0[,)𝑅))    &   ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))    &   ⊢ 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2))    ⇒   ⊢ (𝜑 → (ℂ D 𝐹) = (𝑦 ∈ 𝑆 ↦ Σ𝑘 ∈ ℕ ((𝑘 · (𝐴‘𝑘)) · (𝑦↑(𝑘 − 1)))))
Theorem	abelthlem1 25130*	Lemma for abelth 25140. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
Theorem	abelthlem2 25131*	Lemma for abelth 25140. The peculiar region 𝑆, known as a Stolz angle , is a teardrop-shaped subset of the closed unit ball containing 1. Indeed, except for 1 itself, the rest of the Stolz angle is enclosed in the open unit ball. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    ⇒   ⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
Theorem	abelthlem3 25132*	Lemma for abelth 25140. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ )
Theorem	abelthlem4 25133*	Lemma for abelth 25140. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    ⇒   ⊢ (𝜑 → 𝐹:𝑆⟶ℂ)
Theorem	abelthlem5 25134*	Lemma for abelth 25140. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ )
Theorem	abelthlem6 25135*	Lemma for abelth 25140. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1}))    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
Theorem	abelthlem7a 25136*	Lemma for abelth 25140. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1}))    ⇒   ⊢ (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))))
Theorem	abelthlem7 25137*	Lemma for abelth 25140. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1}))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅)    &   ⊢ (𝜑 → (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))    ⇒   ⊢ (𝜑 → (abs‘(𝐹‘𝑋)) < ((𝑀 + 1) · 𝑅))
Theorem	abelthlem8 25138*	Lemma for abelth 25140. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    ⇒   ⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅))
Theorem	abelthlem9 25139*	Lemma for abelth 25140. By adjusting the constant term, we can assume that the entire series converges to 0. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    ⇒   ⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅))
Theorem	abelth 25140*	Abel's theorem. If the power series Σ𝑛 ∈ ℕ0𝐴(𝑛)(𝑥↑𝑛) is convergent at 1, then it is equal to the limit from "below", along a Stolz angle 𝑆 (note that the 𝑀 = 1 case of a Stolz angle is the real line [0, 1]). (Continuity on 𝑆 ∖ {1} follows more generally from psercn 25125.) (Contributed by Mario Carneiro, 2-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ))
Theorem	abelth2 25141*	Abel's theorem, restricted to the [0, 1] interval. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ((0[,]1)–cn→ℂ))
14.3  Basic trigonometry
14.3.1  The exponential, sine, and cosine functions (cont.)
Theorem	efcn 25142	The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ exp ∈ (ℂ–cn→ℂ)
Theorem	sincn 25143	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ sin ∈ (ℂ–cn→ℂ)
Theorem	coscn 25144	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ cos ∈ (ℂ–cn→ℂ)
Theorem	reeff1olem 25145*	Lemma for reeff1o 25146. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈)
Theorem	reeff1o 25146	The real exponential function is one-to-one onto. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (exp ↾ ℝ):ℝ–1-1-onto→ℝ+
Theorem	reefiso 25147	The exponential function on the reals determines an isomorphism from reals onto positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) (Revised by Mario Carneiro, 11-Mar-2014.)
⊢ (exp ↾ ℝ) Isom < , < (ℝ, ℝ+)
Theorem	efcvx 25148	The exponential function on the reals is a strictly convex function. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (exp‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < ((𝑇 · (exp‘𝐴)) + ((1 − 𝑇) · (exp‘𝐵))))
Theorem	reefgim 25149	The exponential function is a group isomorphism from the group of reals under addition to the group of positive reals under multiplication. (Contributed by Mario Carneiro, 21-Jun-2015.) (Revised by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝑃 = ((mulGrp‘ℂfld) ↾s ℝ+)    ⇒   ⊢ (exp ↾ ℝ) ∈ (ℝfld GrpIso 𝑃)
14.3.2  Properties of pi = 3.14159...
Theorem	pilem1 25150	Lemma for pire 25155, pigt2lt4 25153 and sinpi 25154. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0))
Theorem	pilem2 25151	Lemma for pire 25155, pigt2lt4 25153 and sinpi 25154. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ (2(,)4))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → (sin‘𝐴) = 0)    &   ⊢ (𝜑 → (sin‘𝐵) = 0)    ⇒   ⊢ (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵)
Theorem	pilem3 25152	Lemma for pire 25155, pigt2lt4 25153 and sinpi 25154. Existence part. (Contributed by Paul Chapman, 23-Jan-2008.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) (Revised by AV, 14-Sep-2020.) (Proof shortened by BJ, 30-Jun-2022.)
⊢ (π ∈ (2(,)4) ∧ (sin‘π) = 0)
Theorem	pigt2lt4 25153	π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ (2 < π ∧ π < 4)
Theorem	sinpi 25154	The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘π) = 0
Theorem	pire 25155	π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ π ∈ ℝ
Theorem	picn 25156	π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ π ∈ ℂ
Theorem	pipos 25157	π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ 0 < π
Theorem	pirp 25158	π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ π ∈ ℝ+
Theorem	negpicn 25159	-π is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -π ∈ ℂ
Theorem	sinhalfpilem 25160	Lemma for sinhalfpi 25165 and coshalfpi 25166. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0)
Theorem	halfpire 25161	π / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
⊢ (π / 2) ∈ ℝ
Theorem	neghalfpire 25162	-π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ
Theorem	neghalfpirx 25163	-π / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ*
Theorem	pidiv2halves 25164	Adding π / 2 to itself gives π. See 2halves 11907. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ((π / 2) + (π / 2)) = π
Theorem	sinhalfpi 25165	The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘(π / 2)) = 1
Theorem	coshalfpi 25166	The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘(π / 2)) = 0
Theorem	cosneghalfpi 25167	The cosine of -π / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
⊢ (cos‘-(π / 2)) = 0
Theorem	efhalfpi 25168	The exponential of iπ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (exp‘(i · (π / 2))) = i
Theorem	cospi 25169	The cosine of π is -1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘π) = -1
Theorem	efipi 25170	The exponential of i · π is -1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ (exp‘(i · π)) = -1
Theorem	eulerid 25171	Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ ((exp‘(i · π)) + 1) = 0
Theorem	sin2pi 25172	The sine of 2π is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘(2 · π)) = 0
Theorem	cos2pi 25173	The cosine of 2π is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘(2 · π)) = 1
Theorem	ef2pi 25174	The exponential of 2πi is 1. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (exp‘(i · (2 · π))) = 1
Theorem	ef2kpi 25175	If 𝐾 is an integer, then the exponential of 2𝐾πi is 1. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (𝐾 ∈ ℤ → (exp‘((i · (2 · π)) · 𝐾)) = 1)
Theorem	efper 25176	The exponential function is periodic. (Contributed by Paul Chapman, 21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (exp‘(𝐴 + ((i · (2 · π)) · 𝐾))) = (exp‘𝐴))
Theorem	sinperlem 25177	Lemma for sinper 25178 and cosper 25179. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ (𝐴 ∈ ℂ → (𝐹‘𝐴) = (((exp‘(i · 𝐴))𝑂(exp‘(-i · 𝐴))) / 𝐷))    &   ⊢ ((𝐴 + (𝐾 · (2 · π))) ∈ ℂ → (𝐹‘(𝐴 + (𝐾 · (2 · π)))) = (((exp‘(i · (𝐴 + (𝐾 · (2 · π)))))𝑂(exp‘(-i · (𝐴 + (𝐾 · (2 · π)))))) / 𝐷))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (𝐹‘(𝐴 + (𝐾 · (2 · π)))) = (𝐹‘𝐴))
Theorem	sinper 25178	The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) = (sin‘𝐴))
Theorem	cosper 25179	The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) = (cos‘𝐴))
Theorem	sin2kpi 25180	If 𝐾 is an integer, then the sine of 2𝐾π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · (2 · π))) = 0)
Theorem	cos2kpi 25181	If 𝐾 is an integer, then the cosine of 2𝐾π is 1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · (2 · π))) = 1)
Theorem	sin2pim 25182	Sine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((2 · π) − 𝐴)) = -(sin‘𝐴))
Theorem	cos2pim 25183	Cosine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((2 · π) − 𝐴)) = (cos‘𝐴))
Theorem	sinmpi 25184	Sine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) = -(sin‘𝐴))
Theorem	cosmpi 25185	Cosine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) = -(cos‘𝐴))
Theorem	sinppi 25186	Sine of a number plus π. (Contributed by NM, 10-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴))
Theorem	cosppi 25187	Cosine of a number plus π. (Contributed by NM, 18-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴))
Theorem	efimpi 25188	The exponential function at i times a real number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (exp‘(i · (𝐴 − π))) = -(exp‘(i · 𝐴)))
Theorem	sinhalfpip 25189	The sine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) + 𝐴)) = (cos‘𝐴))
Theorem	sinhalfpim 25190	The sine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴))
Theorem	coshalfpip 25191	The cosine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) + 𝐴)) = -(sin‘𝐴))
Theorem	coshalfpim 25192	The cosine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) − 𝐴)) = (sin‘𝐴))
Theorem	ptolemy 25193	Ptolemy's Theorem. This theorem is named after the Greek astronomer and mathematician Ptolemy (Claudius Ptolemaeus). This particular version is expressed using the sine function. It is proved by expanding all the multiplication of sines to a product of cosines of differences using sinmul 15578, then using algebraic simplification to show that both sides are equal. This formalization is based on the proof in "Trigonometry" by Gelfand and Saul. This is Metamath 100 proof #95. (Contributed by David A. Wheeler, 31-May-2015.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = π) → (((sin‘𝐴) · (sin‘𝐵)) + ((sin‘𝐶) · (sin‘𝐷))) = ((sin‘(𝐵 + 𝐶)) · (sin‘(𝐴 + 𝐶))))
Theorem	sincosq1lem 25194	Lemma for sincosq1sgn 25195. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 < (sin‘𝐴))
Theorem	sincosq1sgn 25195	The signs of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ (0(,)(π / 2)) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
Theorem	sincosq2sgn 25196	The signs of the sine and cosine functions in the second quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ((π / 2)(,)π) → (0 < (sin‘𝐴) ∧ (cos‘𝐴) < 0))
Theorem	sincosq3sgn 25197	The signs of the sine and cosine functions in the third quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ (π(,)(3 · (π / 2))) → ((sin‘𝐴) < 0 ∧ (cos‘𝐴) < 0))
Theorem	sincosq4sgn 25198	The signs of the sine and cosine functions in the fourth quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ((3 · (π / 2))(,)(2 · π)) → ((sin‘𝐴) < 0 ∧ 0 < (cos‘𝐴)))
Theorem	coseq00topi 25199	Location of the zeroes of cosine in (0[,]π). (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2)))
Theorem	coseq0negpitopi 25200	Location of the zeroes of cosine in (-π(,]π). (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝐴 ∈ (-π(,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 ∈ {(π / 2), -(π / 2)}))