Initial program 30.5
\[\frac{1 - \cos x}{x \cdot x}\]
Initial simplification30.5
\[\leadsto \frac{1 - \cos x}{x \cdot x}\]
- Using strategy
rm Applied flip--30.6
\[\leadsto \frac{\color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}}{x \cdot x}\]
Applied associate-/l/30.6
\[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(x \cdot x\right) \cdot \left(1 + \cos x\right)}}\]
Simplified15.0
\[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(x \cdot x\right) \cdot \left(1 + \cos x\right)}\]
- Using strategy
rm Applied associate-*l*15.1
\[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{x \cdot \left(x \cdot \left(1 + \cos x\right)\right)}}\]
- Using strategy
rm Applied times-frac0.3
\[\leadsto \color{blue}{\frac{\sin x}{x} \cdot \frac{\sin x}{x \cdot \left(1 + \cos x\right)}}\]
Simplified0.3
\[\leadsto \frac{\sin x}{x} \cdot \color{blue}{\frac{\sin x}{(\left(\cos x\right) \cdot x + x)_*}}\]
- Using strategy
rm Applied *-un-lft-identity0.3
\[\leadsto \frac{\sin x}{x} \cdot \frac{\sin x}{\color{blue}{1 \cdot (\left(\cos x\right) \cdot x + x)_*}}\]
Applied *-un-lft-identity0.3
\[\leadsto \frac{\sin x}{x} \cdot \frac{\color{blue}{1 \cdot \sin x}}{1 \cdot (\left(\cos x\right) \cdot x + x)_*}\]
Applied times-frac0.3
\[\leadsto \frac{\sin x}{x} \cdot \color{blue}{\left(\frac{1}{1} \cdot \frac{\sin x}{(\left(\cos x\right) \cdot x + x)_*}\right)}\]
Simplified0.3
\[\leadsto \frac{\sin x}{x} \cdot \left(\color{blue}{1} \cdot \frac{\sin x}{(\left(\cos x\right) \cdot x + x)_*}\right)\]
Simplified0.1
\[\leadsto \frac{\sin x}{x} \cdot \left(1 \cdot \color{blue}{\frac{\tan \left(\frac{x}{2}\right)}{x}}\right)\]
Final simplification0.1
\[\leadsto \frac{\sin x}{x} \cdot \frac{\tan \left(\frac{x}{2}\right)}{x}\]