Proof: Divide Simplify

Let's prove the following theorem:

if not (b = 0), then (b ⋅ d) ⋅ (a / b) = d ⋅ a

Proof:

View as a tree | View dependent proofs | Try proving it

Given
1 not (b = 0)
Proof Table
# Claim Reason
1 (b ⋅ d) ⋅ a = (d ⋅ a) ⋅ b (b ⋅ d) ⋅ a = (d ⋅ a) ⋅ b
2 ((b ⋅ d) ⋅ a) / b = ((d ⋅ a) ⋅ b) / b if (b ⋅ d) ⋅ a = (d ⋅ a) ⋅ b, then ((b ⋅ d) ⋅ a) / b = ((d ⋅ a) ⋅ b) / b
3 b / b = 1 if not (b = 0), then b / b = 1
4 ((d ⋅ a) ⋅ b) / b = (d ⋅ a) ⋅ (b / b) ((d ⋅ a) ⋅ b) / b = (d ⋅ a) ⋅ (b / b)
5 ((d ⋅ a) ⋅ b) / b = (d ⋅ a) ⋅ 1 if b / b = 1 and ((d ⋅ a) ⋅ b) / b = (d ⋅ a) ⋅ (b / b), then ((d ⋅ a) ⋅ b) / b = (d ⋅ a) ⋅ 1
6 (d ⋅ a) ⋅ 1 = d ⋅ a (d ⋅ a) ⋅ 1 = d ⋅ a
7 ((d ⋅ a) ⋅ b) / b = d ⋅ a if (d ⋅ a) ⋅ 1 = d ⋅ a and ((d ⋅ a) ⋅ b) / b = (d ⋅ a) ⋅ 1, then ((d ⋅ a) ⋅ b) / b = d ⋅ a
8 ((b ⋅ d) ⋅ a) / b = d ⋅ a if ((d ⋅ a) ⋅ b) / b = d ⋅ a and ((b ⋅ d) ⋅ a) / b = ((d ⋅ a) ⋅ b) / b, then ((b ⋅ d) ⋅ a) / b = d ⋅ a
9 ((b ⋅ d) ⋅ a) / b = (b ⋅ d) ⋅ (a / b) ((b ⋅ d) ⋅ a) / b = (b ⋅ d) ⋅ (a / b)
10 (b ⋅ d) ⋅ (a / b) = d ⋅ a if ((b ⋅ d) ⋅ a) / b = d ⋅ a and ((b ⋅ d) ⋅ a) / b = (b ⋅ d) ⋅ (a / b), then (b ⋅ d) ⋅ (a / b) = d ⋅ a

Comments

Please log in to add comments