Return to navigation page or list derivations

Review Euler equation: trig square root

step inference rule input feed output step validity (as per SymPy)
1
  • 111981: declare initial expression
  • number of inputs: 0; feeds: 0; outputs: 1
  • Eq.~\\ref{eq:#1} is an initial equation.
  1. 4938429483
    \(\exp(i x)=\cos(x)+i \sin(x)\)
no validation is available for declarations
2
  • 111886: change variable X to Y
  • number of inputs: 1; feeds: 2; outputs: 1
  • Change variable $#1$ to $#2$ in Eq.~\\ref{eq:#3}; yields Eq.~\\ref{eq:#4}.
  1. 4938429483
    \(\exp(i x)=\cos(x)+i \sin(x)\)
  1. 0004582412
    \(x\)
  1. 0004089571
    \(2 x\)
  1. 4838429483
    \(\exp(2 i x)=\cos(2 x)+i \sin(2 x)\)
valid
3
  • 111355: LHS of expr 1 equals LHS of expr 2
  • number of inputs: 2; feeds: 0; outputs: 1
  • LHS of Eq.~\\ref{eq:#1} is equal to LHS of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}.
  1. 4838429483
    \(\exp(2 i x)=\cos(2 x)+i \sin(2 x)\)
  1. 4598294821
    \(\exp(2 i x)=(\cos(x))^2+2i\cos(x)\sin(x)-(\sin(x))^2\)
  1. 9483928192
    \(\cos(2 x) + i\sin(2 x)=(\cos(x))^2 + 2 i \cos(x) \sin(x) - (\sin(x))^2\)
valid
4
  • 111253: multiply expr 1 by expr 2
  • number of inputs: 2; feeds: 0; outputs: 1
  • Multiply Eq.~\\ref{eq:#1} by Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}.
  1. 4938429483
    \(\exp(i x)=\cos(x)+i \sin(x)\)
  1. 4938429483
    \(\exp(i x)=\cos(x)+i \sin(x)\)
  1. 4638429483
    \(\exp(2 i x)=(\cos(x)+ i \sin(x))(\cos(x)+ i \sin(x))\)
valid
5
  • 111546: expand RHS
  • number of inputs: 1; feeds: 0; outputs: 1
  • Expand the RHS of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}.
  1. 4638429483
    \(\exp(2 i x)=(\cos(x)+ i \sin(x))(\cos(x)+ i \sin(x))\)
  1. 4598294821
    \(\exp(2 i x)=(\cos(x))^2+2i\cos(x)\sin(x)-(\sin(x))^2\)
LHS diff is 0 RHS diff is (pdg0004621**2 + 1)*sin(pdg0001464)**2
6
  • 111198: select real parts
  • number of inputs: 1; feeds: 0; outputs: 1
  • Select real parts of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}.
  1. 9483928192
    \(\cos(2 x) + i\sin(2 x)=(\cos(x))^2 + 2 i \cos(x) \sin(x) - (\sin(x))^2\)
  1. 9482928242
    \(\cos(2 x)=(\cos(x))^2 - (\sin(x))^2\)
LHS diff is -cos(2*pdg0001464) + cos(2*re(pdg0001464))*cosh(2*im(pdg0001464)) + re(pdg0004621*sin(2*pdg0001464)) RHS diff is -cos(2*pdg0001464) + 2*cos(2*re(pdg0001464))*sinh(im(pdg0001464))**2 + cos(2*re(pdg0001464)) + re(pdg0004621*sin(2*pdg0001464))
7
  • 111530: add X to both sides
  • number of inputs: 1; feeds: 1; outputs: 1
  • Add $#1$ to both sides of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}.
  1. 9482928242
    \(\cos(2 x)=(\cos(x))^2 - (\sin(x))^2\)
  1. 0007894942
    \((\sin(x))^2\)
  1. 9482928243
    \(\cos(2 x) + (\sin(x))^2=(\cos(x))^2\)
valid
8
  • 111299: declare identity
  • number of inputs: 0; feeds: 0; outputs: 1
  • Eq.~\\ref{eq:#1} is an identity.
  1. 5832984291
    \((\sin(x))^2 + (\cos(x))^2=1\)
no validation is available for declarations
9
  • 111282: subtract X from both sides
  • number of inputs: 1; feeds: 1; outputs: 1
  • Subtract $#1$ from both sides of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}.
  1. 5832984291
    \((\sin(x))^2 + (\cos(x))^2=1\)
  1. 0001111111
    \((\sin(x))^2\)
  1. 3285732911
    \((\cos(x))^2=1-(\sin(x))^2\)
valid
10
  • 111268: swap LHS with RHS
  • number of inputs: 1; feeds: 0; outputs: 1
  • Swap LHS of Eq.~\\ref{eq:#1} with RHS; yields Eq.~\\ref{eq:#2}.
  1. 9482928243
    \(\cos(2 x) + (\sin(x))^2=(\cos(x))^2\)
  1. 9482438243
    \((\cos(x))^2=\cos(2 x) + (\sin(x))^2\)
valid
11
  • 111355: LHS of expr 1 equals LHS of expr 2
  • number of inputs: 2; feeds: 0; outputs: 1
  • LHS of Eq.~\\ref{eq:#1} is equal to LHS of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}.
  1. 3285732911
    \((\cos(x))^2=1-(\sin(x))^2\)
  1. 9482438243
    \((\cos(x))^2=\cos(2 x) + (\sin(x))^2\)
  1. 4827492911
    \(\cos(2 x)+(\sin(x))^2=1 - (\sin(x))^2\)
valid
12
  • 111282: subtract X from both sides
  • number of inputs: 1; feeds: 1; outputs: 1
  • Subtract $#1$ from both sides of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}.
  1. 4827492911
    \(\cos(2 x)+(\sin(x))^2=1 - (\sin(x))^2\)
  1. 0006466214
    \((\sin(x))^2\)
  1. 1248277773
    \(\cos(2 x)=1 - 2 (\sin(x))^2\)
valid
13
  • 111530: add X to both sides
  • number of inputs: 1; feeds: 1; outputs: 1
  • Add $#1$ to both sides of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}.
  1. 1248277773
    \(\cos(2 x)=1 - 2 (\sin(x))^2\)
  1. 0007471778
    \(2(\sin(x))^2\)
  1. 7572664728
    \(\cos(2 x) + 2 (\sin(x))^2=1\)
valid
14
  • 111282: subtract X from both sides
  • number of inputs: 1; feeds: 1; outputs: 1
  • Subtract $#1$ from both sides of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}.
  1. 7572664728
    \(\cos(2 x) + 2 (\sin(x))^2=1\)
  1. 0008842811
    \(\cos(2 x)\)
  1. 9889984281
    \(2 (\sin(x))^2=1 - \cos(2 x)\)
valid
15
  • 111975: divide both sides by
  • number of inputs: 1; feeds: 1; outputs: 1
  • Divide both sides of Eq.~\\ref{eq:#2} by $#1$; yields Eq.~\\ref{eq:#3}.
  1. 9889984281
    \(2 (\sin(x))^2=1 - \cos(2 x)\)
  1. 0003838111
    \(2\)
  1. 9988949211
    \((\sin(x))^2=\frac{1 - \cos(2 x)}{2}\)
valid
16
  • 111341: declare final expression
  • number of inputs: 1; feeds: 0; outputs: 0
  • Eq.~\\ref{eq:#1} is one of the final equations.
  1. 9988949211
    \((\sin(x))^2=\frac{1 - \cos(2 x)}{2}\)
no validation is available for declarations


Hold the mouse over a node to highlight that node and its neighbors. You can zoom in/out. You can pan the image. You can move nodes by clicking and dragging.

Actions: Edit Derivation

Generate Tex file or PDF file

   xor   

Delete Derivation and all associated steps

This does not remove expressions, symbols, and operations.

timing of Neo4j queries: