Initial program 20.0
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
Initial simplification20.0
\[\leadsto \frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
- Using strategy
rm Applied flip--20.0
\[\leadsto \color{blue}{\frac{\frac{1}{\sqrt{x}} \cdot \frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}} \cdot \frac{1}{\sqrt{x + 1}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}}\]
- Using strategy
rm Applied frac-times25.0
\[\leadsto \frac{\frac{1}{\sqrt{x}} \cdot \frac{1}{\sqrt{x}} - \color{blue}{\frac{1 \cdot 1}{\sqrt{x + 1} \cdot \sqrt{x + 1}}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]
Applied frac-times20.1
\[\leadsto \frac{\color{blue}{\frac{1 \cdot 1}{\sqrt{x} \cdot \sqrt{x}}} - \frac{1 \cdot 1}{\sqrt{x + 1} \cdot \sqrt{x + 1}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]
Applied frac-sub19.9
\[\leadsto \frac{\color{blue}{\frac{\left(1 \cdot 1\right) \cdot \left(\sqrt{x + 1} \cdot \sqrt{x + 1}\right) - \left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \left(1 \cdot 1\right)}{\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \left(\sqrt{x + 1} \cdot \sqrt{x + 1}\right)}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]
Simplified5.9
\[\leadsto \frac{\frac{\color{blue}{1}}{\left(\sqrt{x} \cdot \sqrt{x}\right) \cdot \left(\sqrt{x + 1} \cdot \sqrt{x + 1}\right)}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]
Simplified5.7
\[\leadsto \frac{\frac{1}{\color{blue}{(x \cdot x + x)_*}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]
- Using strategy
rm Applied add-sqr-sqrt5.8
\[\leadsto \frac{\frac{1}{\color{blue}{\sqrt{(x \cdot x + x)_*} \cdot \sqrt{(x \cdot x + x)_*}}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]
Applied associate-/r*5.7
\[\leadsto \frac{\color{blue}{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]
- Using strategy
rm Applied div-inv5.7
\[\leadsto \frac{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}{\frac{1}{\sqrt{x}} + \color{blue}{1 \cdot \frac{1}{\sqrt{x + 1}}}}\]
Applied div-inv5.7
\[\leadsto \frac{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}{\color{blue}{1 \cdot \frac{1}{\sqrt{x}}} + 1 \cdot \frac{1}{\sqrt{x + 1}}}\]
Applied distribute-lft-out5.7
\[\leadsto \frac{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}{\color{blue}{1 \cdot \left(\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}\right)}}\]
Applied *-un-lft-identity5.7
\[\leadsto \frac{\color{blue}{1 \cdot \frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}}{1 \cdot \left(\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}\right)}\]
Applied times-frac5.7
\[\leadsto \color{blue}{\frac{1}{1} \cdot \frac{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}}\]
Simplified5.7
\[\leadsto \color{blue}{1} \cdot \frac{\frac{\frac{1}{\sqrt{(x \cdot x + x)_*}}}{\sqrt{(x \cdot x + x)_*}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]
Simplified5.7
\[\leadsto 1 \cdot \color{blue}{\frac{1}{\frac{(x \cdot x + x)_*}{\sqrt{x}} + \frac{(x \cdot x + x)_*}{\sqrt{x + 1}}}}\]
Final simplification5.7
\[\leadsto \frac{1}{\frac{(x \cdot x + x)_*}{\sqrt{x + 1}} + \frac{(x \cdot x + x)_*}{\sqrt{x}}}\]
