---

Step * 1 2 of Lemma cos-sin-equation-non-constant3


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:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x)))))
7. ∀x,y:ℝ.  ((x = y) ⇒ ((g x) = (g y)))
8. b : ℝ
9. r0_∫-b -(g(x)) dx ≠ r0
10. f(b) ≠ r1
11. f(b) - r1 ≠ r0
12. ∀a:ℝ. (a ≠ r0 ⇒ (∀x:ℝ. (g(x) = rsin(a * x))) ⇒ (f(r0) = r1) ⇒ (a = (f(b) - f(r0)/r0_∫-b -(g(x)) dx)))
⊢ ∃a:ℝ. ((∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))
BY
{ ((D 0 With ⌜(f(b) - f(r0)/r0_∫-b -(g(x)) dx)⌝  THENW Auto)
   THEN (StableCases ⌜∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))⌝⋅
         THENA (Auto THEN (BLemma `stable__and` THEN Auto) THEN BLemma `stable__all` THEN Auto)
         )
   THEN Try (Trivial)) }

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:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x)))))
7. ∀x,y:ℝ.  ((x = y) ⇒ ((g x) = (g y)))
8. b : ℝ
9. r0_∫-b -(g(x)) dx ≠ r0
10. f(b) ≠ r1
11. f(b) - r1 ≠ r0
12. ∀a:ℝ. (a ≠ r0 ⇒ (∀x:ℝ. (g(x) = rsin(a * x))) ⇒ (f(r0) = r1) ⇒ (a = (f(b) - f(r0)/r0_∫-b -(g(x)) dx)))
13. ∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))
⊢ (∀x:ℝ. (f(x) = rcos((f(b) - f(r0)/r0_∫-b -(g(x)) dx) * x)))
∧ (∀x:ℝ. (g(x) = rsin((f(b) - f(r0)/r0_∫-b -(g(x)) dx) * x)))

---

Latex:

---

Latex:

1.  f  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
2.  g  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
3.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y)))
4.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (g(x)  =  g(y)))
5.  \mforall{}x,y:\mBbbR{}.    (f(x  -  y)  =  ((f(x)  *  f(y))  +  (g(x)  *  g(y))))
6.  \mneg{}\mneg{}(\mexists{}a:\mBbbR{}.  (a  \mneq{}  r0  \mwedge{}  (\mforall{}x:\mBbbR{}.  (f(x)  =  rcos(a  *  x)))  \mwedge{}  (\mforall{}x:\mBbbR{}.  (g(x)  =  rsin(a  *  x)))))
7.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  ((g  x)  =  (g  y)))
8.  b  :  \mBbbR{}
9.  r0\_\mint{}\msupminus{}b  -(g(x))  dx  \mneq{}  r0
10.  f(b)  \mneq{}  r1
11.  f(b)  -  r1  \mneq{}  r0
12.  \mforall{}a:\mBbbR{}
            (a  \mneq{}  r0
            {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  (g(x)  =  rsin(a  *  x)))
            {}\mRightarrow{}  (f(r0)  =  r1)
            {}\mRightarrow{}  (a  =  (f(b)  -  f(r0)/r0\_\mint{}\msupminus{}b  -(g(x))  dx)))
\mvdash{}  \mexists{}a:\mBbbR{}.  ((\mforall{}x:\mBbbR{}.  (f(x)  =  rcos(a  *  x)))  \mwedge{}  (\mforall{}x:\mBbbR{}.  (g(x)  =  rsin(a  *  x))))


By

---

Latex:
((D  0  With  \mkleeneopen{}(f(b)  -  f(r0)/r0\_\mint{}\msupminus{}b  -(g(x))  dx)\mkleeneclose{}    THENW  Auto)
  THEN  (StableCases  \mkleeneopen{}\mexists{}a:\mBbbR{}.  (a  \mneq{}  r0  \mwedge{}  (\mforall{}x:\mBbbR{}.  (f(x)  =  rcos(a  *  x)))  \mwedge{}  (\mforall{}x:\mBbbR{}.  (g(x)  =  rsin(a  *  x))))\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  (BLemma  `stable\_\_and`  THEN  Auto)  THEN  BLemma  `stable\_\_all`  THEN  Auto)
              )
  THEN  Try  (Trivial))

---

Home Index