Metamath Proof Explorer

Theorem fourierdlem29

Description: Explicit function value for K applied to A . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis fourierdlem29.1 ⊢ K = s ∈ − π π ⟼ if s = 0 1 s 2 ⁢ sin ⁡ s 2
Assertion fourierdlem29 ⊢ A ∈ − π π → K ⁡ A = if A = 0 1 A 2 ⁢ sin ⁡ A 2

Proof

Step Hyp Ref Expression
1 fourierdlem29.1 ⊢ K = s ∈ − π π ⟼ if s = 0 1 s 2 ⁢ sin ⁡ s 2
2 eqeq1 ⊢ s = A → s = 0 ↔ A = 0
3 id ⊢ s = A → s = A
4 fvoveq1 ⊢ s = A → sin ⁡ s 2 = sin ⁡ A 2
5 4 oveq2d ⊢ s = A → 2 ⁢ sin ⁡ s 2 = 2 ⁢ sin ⁡ A 2
6 3 5 oveq12d ⊢ s = A → s 2 ⁢ sin ⁡ s 2 = A 2 ⁢ sin ⁡ A 2
7 2 6 ifbieq2d ⊢ s = A → if s = 0 1 s 2 ⁢ sin ⁡ s 2 = if A = 0 1 A 2 ⁢ sin ⁡ A 2
8 1ex ⊢ 1 ∈ V
9 ovex ⊢ A 2 ⁢ sin ⁡ A 2 ∈ V
10 8 9 ifex ⊢ if A = 0 1 A 2 ⁢ sin ⁡ A 2 ∈ V
11 7 1 10 fvmpt ⊢ A ∈ − π π → K ⁡ A = if A = 0 1 A 2 ⁢ sin ⁡ A 2