---

Step * of Lemma cos-sin-equation-nc

∀f,g:ℝ ⟶ ℝ.
  ((∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y))))
  ⇒ (∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y))))
  ⇒ (∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y)))))
  ⇒ (∃a:ℝ. f(a) ≠ f(r0))
  ⇒ (∃b:ℝ. g(-(b)) ≠ g(b))
  ⇒ ((∀x,y:ℝ.  (f(x - y) = f(y - x)))
     ∧ (∀y:ℝ. (f(-(y)) = f(y)))
     ∧ (∀y:ℝ. (g(-(y)) = -(g(y))))
     ∧ (g(r0) = r0)
     ∧ (∃d:ℝ. f(d) ≠ r0)
     ∧ (f(r0) = r1)
     ∧ (∀x:ℝ. ((f(x)^2 + g(x)^2) = r1))
     ∧ (∀x:ℝ. (|f(x)| ≤ r1))
     ∧ (∀x,y:ℝ.  ((f(x - -(y)) + f(x - y)) = (r(2) * f(x) * f(y))))
     ∧ (∀x,y:ℝ.  ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y))))))
BY
{ Auto }

1
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. ∃a:ℝ. f(a) ≠ f(r0)
7. ∃b:ℝ. g(-(b)) ≠ g(b)
8. x : ℝ
9. y : ℝ
⊢ f(x - y) = f(y - x)

2
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. ∃a:ℝ. f(a) ≠ f(r0)
7. ∃b:ℝ. g(-(b)) ≠ g(b)
8. ∀x,y:ℝ.  (f(x - y) = f(y - x))
9. y : ℝ
⊢ f(-(y)) = f(y)

3
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. ∃a:ℝ. f(a) ≠ f(r0)
7. ∃b:ℝ. g(-(b)) ≠ g(b)
8. ∀x,y:ℝ.  (f(x - y) = f(y - x))
9. ∀y:ℝ. (f(-(y)) = f(y))
10. y : ℝ
⊢ g(-(y)) = -(g(y))

4
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. ∃a:ℝ. f(a) ≠ f(r0)
7. ∃b:ℝ. g(-(b)) ≠ g(b)
8. ∀x,y:ℝ.  (f(x - y) = f(y - x))
9. ∀y:ℝ. (f(-(y)) = f(y))
10. ∀y:ℝ. (g(-(y)) = -(g(y)))
⊢ g(r0) = r0

5
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. ∃a:ℝ. f(a) ≠ f(r0)
7. ∃b:ℝ. g(-(b)) ≠ g(b)
8. ∀x,y:ℝ.  (f(x - y) = f(y - x))
9. ∀y:ℝ. (f(-(y)) = f(y))
10. ∀y:ℝ. (g(-(y)) = -(g(y)))
11. g(r0) = r0
⊢ ∃d:ℝ. f(d) ≠ r0

6
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. ∃a:ℝ. f(a) ≠ f(r0)
7. ∃b:ℝ. g(-(b)) ≠ g(b)
8. ∀x,y:ℝ.  (f(x - y) = f(y - x))
9. ∀y:ℝ. (f(-(y)) = f(y))
10. ∀y:ℝ. (g(-(y)) = -(g(y)))
11. g(r0) = r0
12. ∃d:ℝ. f(d) ≠ r0
⊢ f(r0) = r1

7
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. ∃a:ℝ. f(a) ≠ f(r0)
7. ∃b:ℝ. g(-(b)) ≠ g(b)
8. ∀x,y:ℝ.  (f(x - y) = f(y - x))
9. ∀y:ℝ. (f(-(y)) = f(y))
10. ∀y:ℝ. (g(-(y)) = -(g(y)))
11. g(r0) = r0
12. ∃d:ℝ. f(d) ≠ r0
13. f(r0) = r1
14. x : ℝ
⊢ (f(x)^2 + g(x)^2) = r1

8
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. ∃a:ℝ. f(a) ≠ f(r0)
7. ∃b:ℝ. g(-(b)) ≠ g(b)
8. ∀x,y:ℝ.  (f(x - y) = f(y - x))
9. ∀y:ℝ. (f(-(y)) = f(y))
10. ∀y:ℝ. (g(-(y)) = -(g(y)))
11. g(r0) = r0
12. ∃d:ℝ. f(d) ≠ r0
13. f(r0) = r1
14. ∀x:ℝ. ((f(x)^2 + g(x)^2) = r1)
15. x : ℝ
⊢ |f(x)| ≤ r1

9
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. ∃a:ℝ. f(a) ≠ f(r0)
7. ∃b:ℝ. g(-(b)) ≠ g(b)
8. ∀x,y:ℝ.  (f(x - y) = f(y - x))
9. ∀y:ℝ. (f(-(y)) = f(y))
10. ∀y:ℝ. (g(-(y)) = -(g(y)))
11. g(r0) = r0
12. ∃d:ℝ. f(d) ≠ r0
13. f(r0) = r1
14. ∀x:ℝ. ((f(x)^2 + g(x)^2) = r1)
15. ∀x:ℝ. (|f(x)| ≤ r1)
16. x : ℝ
17. y : ℝ
⊢ (f(x - -(y)) + f(x - y)) = (r(2) * f(x) * f(y))

10
1. f : ℝ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x,y:ℝ.  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:ℝ.  ((x = y) ⇒ (g(x) = g(y)))
5. ∀x,y:ℝ.  (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y))))
6. ∃a:ℝ. f(a) ≠ f(r0)
7. ∃b:ℝ. g(-(b)) ≠ g(b)
8. ∀x,y:ℝ.  (f(x - y) = f(y - x))
9. ∀y:ℝ. (f(-(y)) = f(y))
10. ∀y:ℝ. (g(-(y)) = -(g(y)))
11. g(r0) = r0
12. ∃d:ℝ. f(d) ≠ r0
13. f(r0) = r1
14. ∀x:ℝ. ((f(x)^2 + g(x)^2) = r1)
15. ∀x:ℝ. (|f(x)| ≤ r1)
16. ∀x,y:ℝ.  ((f(x - -(y)) + f(x - y)) = (r(2) * f(x) * f(y)))
17. x : ℝ
18. y : ℝ
⊢ (f(x + y) + f(x - y)) = (r(2) * f(x) * f(y))

---

Latex:

---

Latex:
\mforall{}f,g:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y))))
    {}\mRightarrow{}  (\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (g(x)  =  g(y))))
    {}\mRightarrow{}  (\mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  ((f(x)  *  f(y))  +  (g(x)  *  g(y)))))
    {}\mRightarrow{}  (\mexists{}a:\mBbbR{}.  f(a)  \mneq{}  f(r0))
    {}\mRightarrow{}  (\mexists{}b:\mBbbR{}.  g(-(b))  \mneq{}  g(b))
    {}\mRightarrow{}  ((\mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  f(y  -  x)))
          \mwedge{}  (\mforall{}y:\mBbbR{}.  (f(-(y))  =  f(y)))
          \mwedge{}  (\mforall{}y:\mBbbR{}.  (g(-(y))  =  -(g(y))))
          \mwedge{}  (g(r0)  =  r0)
          \mwedge{}  (\mexists{}d:\mBbbR{}.  f(d)  \mneq{}  r0)
          \mwedge{}  (f(r0)  =  r1)
          \mwedge{}  (\mforall{}x:\mBbbR{}.  ((f(x)\^{}2  +  g(x)\^{}2)  =  r1))
          \mwedge{}  (\mforall{}x:\mBbbR{}.  (|f(x)|  \mleq{}  r1))
          \mwedge{}  (\mforall{}x,y:\mBbbR{}.    ((f(x  -  -(y))  +  f(x  -  y))  =  (r(2)  *  f(x)  *  f(y))))
          \mwedge{}  (\mforall{}x,y:\mBbbR{}.    ((f(x  +  y)  +  f(x  -  y))  =  (r(2)  *  f(x)  *  f(y))))))


By

---

Latex:
Auto

---

Home Index