Distributive Property of Division over Addition
For this
exercise, we want to use natural deduction to show that:
For any
real numbers a, b, and c, if c <> 0 then (a + b) / c = (a / c)
+ (b / c).
I.e we want to show that: (x, y, z)((x ∈ R & y ∈ R & z ∈ R & z <> 0) => (x + y) / z = (x / z) + (y / z)).
Given that the number c does not equal 0, we can start our effort
to show that:
(a + b) / c = (a / c) + (b / c), by riting out a
sequence of connected equalities, and listing to the side a few rules
justifying the steps.
|
(a + b) / c |
= |
(a + b) * (1 / c) |
|
definition of division |
|
|
= |
(1 / c) * (a + b) |
|
commutative property |
|
|
= |
(1 / c) * a + (1 / c) * b |
|
distributive property |
|
|
= |
a * (1 / c) + (1 / c) * b |
|
commutative property |
|
|
= |
a * (1 / c) + b * (1 / c) |
|
commutative property |
|
|
= |
(a / c) + b * (1 / c) |
|
definition of division |
|
|
= |
(a / c) + (b / c) |
|
definition of division |
|
thus: |
|
|
|
|
|
(a + b) / c |
= |
(a / c) + (b / c) |
|
|
Win we construct our proof using natural deduction and the predicate calculus, we will make sure that our proof covers the expressions in this outline.
To construct our proof, we will employ the usual rules of natural deduction, which includes the rules of the propositional calculus, the predicate calculus, along with the substitution rule of equality.
This proof will be done as a hypothetical proof. We will make 2 hypotheses, an initial one and later a second one. In our initial hypothesis, we will include certin of the axioms of the real numbers and consider them as components of the initial hypothesis.
In our initial hypothesis, we will also hypothesize a certain set, and call it 'R'. Even tho its obvious that 'R' stands for the set of real numbers, in our initial hypothesis we will treat 'R' like a variable or a name letter. In our initial hypothesis the set we represent by 'R' will contain two elements, the first called '0' and the second called '1'. Agan '0' obviously reminds us of the real number 0, and '1' reminds us of the real number 1. In our initial hypothesis we will also include certain rules about these elements. These rules are some of the familiar properties of the real numbers 0 and 1.
Later in our derivation we will make a second hypothesis. From this second hypothesis, by application of the rules in our initial hypothesis, we will derive the conclusion that:
(x, y, z)((x ∈ R & y ∈ R & z ∈ R & z <> 0) => (x + y) / z = (x / z) + (y / z)).
Finally we will apply generalization, or universal instantiation, to quantify the variables R, 0, 1. So if S(R, 0, 1) represents the conjunction of propositions of our first hypothesis, we can state that.
(P, Q, I)[S(P, Q, I) => (x, y, z)((x ∈ P & y ∈ P & z ∈ P & z <> Q) => (x + y) / z = (x / z) + (y / z)) ].
Since the proof that we will make will turn out to be many steps long, it mite be hard to follow. One reason the proof is so very long is that we must devote many steps in the derivation to determining that certin expressions are members of the set R, so that we can apply the rules to those expressions. To give you an overall idea of what the proof is doing, I include here an approximate outline of the proof.
|
a ∈ R & b ∈ R & c ∈ R & c <> 0 |
hypothesis |
|
1 / c ∈ R |
set membership |
|
a + b ∈ R |
set membership |
|
(a + b) / c ∈ R |
set membership |
|
(a + b) / c = (a + b) * (1 / c) |
definition of division |
|
(a + b) * (1 / c) ∈ R |
set membership |
|
(1 / c) * a ∈ R |
set membership |
|
(1 / c) * b ∈ R |
set membership |
|
((1 / c) * a) + ((1 / c) * b) ∈ R |
set membership |
|
(1 / c) * (a + b) ∈ R |
set membership |
|
(a + b) * (1 / c) = (1 / c) * (a + b) |
commutative rule of multiplication |
|
(a + b) / c = (1 / c) * (a + b) |
substitution rule or transitive rule |
|
(1 / c) * (a + b) = (1 / c) * a + (1 / c) * b |
distributive rule |
|
(a + b) / c = (1 / c) * a + (1 / c) * b |
substitution rule or transitive rule |
|
(1 / c) * a = a * (1 / c) |
commutative rule |
|
(1 / c) * b = b * (1 / c) |
commutative rule |
|
(a + b) / c = a * (1 / c) + (1 / c) * b |
substitution rule |
|
(a + b) / c = a * (1 / c) + b * (1 / c) |
substitution rule |
|
a / c = a * (1 / c) |
definition of division |
|
b / c = b * (1 / c) |
definition of division |
|
(a + b) / c = a / c + b * (1 / c) |
substitution |
|
(a + b) / c = a / c + b / c |
substitution |
|
(a ∈ R & b ∈ R & c ∈ R & c <> 0) =>
|
conditional proof |
Having this as a gideline of where we want the proof to go, we now expand the proof and explicitly rite out many of its steps.
|
0H: R es set & |
Initial hypothesis, or Level 0 hypothesis |
|
(* To start off, we will use repeated application of conjunction elimination to take the several propositions of the initial hypothesis out of the long conjunction. *) |
|
|
R es set |
conjuction elimination i.e. |
|
0 ∈ R & |
cnj out |
|
0 ∈ R |
cnj out |
|
1 ∈ R & |
cnj out |
|
1 ∈ R |
cnj out |
|
(,x)((x ∈ R & x <> 0) => 1 / (x) ∈ R) & |
cnj out |
|
(,x)((x ∈ R & x <> 0) => 1 / (x) ∈ R) |
cnj out |
|
(x, y)((x ∈ R & y ∈ R) => (x) + (y) ∈ R) &
|
cnj out |
|
(x, y)((x ∈ R & y ∈ R) => (x) + (y) ∈ R) |
cnj out |
|
(x, y)((x ∈ R & y ∈ R) => (x) * (y) ∈ R) & |
|
|
(x, y)((x ∈ R & y ∈ R) => (x) * (y) ∈ R) |
cnj out |
|
(x, y)((x ∈ R & y ∈ R & y <> 0) => (x) /
(y) ∈ R) & |
|
|
(x, y)((x ∈ R & y ∈ R & y <> 0) => (x) / (y) ∈ R) |
cnj out |
|
(x, y)((x ∈ R & y ∈ R & y <> 0) => (x) /
(y) = (x) * (1 / (y)) ) & |
|
|
(x, y)((x ∈ R & y ∈ R & y <> 0) => (x) / (y) = (x) * (1 / (y)) ) (* definition of division *) |
cnj out |
|
(x, y)((x ∈ R & y ∈ R) => (x) * (y) = (y) * (x))
& |
|
|
(x, y)((x ∈ R & y ∈ R) => (x) * (y) = (y) * (x)) (* commutative rule for multiplication *) |
cnj out |
|
(x, y, z)((x ∈ R & y ∈ R & z ∈ R & x = y &
y = z) => x = z) & |
|
|
(x, y, z)((x ∈ R & y ∈ R & z ∈ R & x = y & y = z) => x = z) (* transitive rule *) |
cnj out |
|
(x, y, z)((x ∈ R & y ∈ R & z ∈ R) => (x) *
[(y) + (z)] = [(x) * (y)] + [(x) * (z)] ) |
cnj out |
|
(x, y, z)((x ∈ R & y ∈ R & z ∈ R & x = y & y = z) => x = z) |
cnj out |
|
(* Now we can use the hypothesized axioms in our derivation. *) |
|
|
1H: a ∈ R & b ∈ R & c ∈ R & c <> 0 |
Level 1 hypothesis |
|
a ∈ R |
cnj out |
|
b ∈ R & c ∈ R & c <> 0 |
cnj out |
|
b ∈ R |
cnj out |
|
c ∈ R & c <> 0 |
cnj out |
|
c <> 0 |
cnj out |
|
(,x)((x ∈ R & x <> 0) => 1 / (x) ∈ R) |
repeat. i.e. |
|
(c ∈ R & c <> 0) => 1 / (c) ∈ R |
specification spc |
|
c ∈ R & c <> 0 |
rp |
|
1 / (c) ∈ R |
modus ponens. i.e. |
|
1 / c ∈ R |
remove parenthesis clutter, i.e.: () out |
|
(x, y)((x ∈ R & y ∈ R) => (x) + (y) ∈ R) |
rp |
|
(,y)((a ∈ R & y ∈ R) => (a) + (y) ∈ R) |
specification i.e. |
|
(a ∈ R & b ∈ R) => (a) + (b) ∈ R |
spc |
|
a ∈ R & b ∈ R |
conjunction introduction i.e. |
|
(a) + (b) ∈ R |
mp |
|
a + b ∈ R |
() out |
|
(x, y)((x ∈ R & y ∈ R & y <> 0) => (x) / (y) ∈ R) |
rp |
|
(,y)((a + b ∈ R & y ∈ R & y <> 0) => (a + b) / (y) ∈ R) |
spc |
|
(a + b ∈ R & c ∈ R & c <> 0) => (a + b) / (c) ∈ R |
spc |
|
a + b ∈ R & c ∈ R & c <> 0 |
cnj |
|
(a + b) / (c) ∈ R |
mp |
|
(a + b) / c ∈ R |
() out |
|
(x, y)((x ∈ R & y ∈ R & y <> 0) => (x) / (y) = (x) * (1 / (y)) ) |
rp |
|
(,y)((a + b ∈ R & y ∈ R & y <> 0) => (a + b) / (y) = (a + b) * (1 / (y)) ) |
spc |
|
((a + b ∈ R & y ∈ R & c <> 0) => (a + b) / (c) = (a + b) * (1 / (c)) |
spc |
|
a + b ∈ R & c ∈ R & c <> 0 |
rp |
|
(a + b) / (c) = (a + b) * (1 / (c)) |
mp |
|
(a + b) / c = (a + b) * (1 / c) |
() out |
|
(x, y)((x ∈ R & y ∈ R) => (x) * (y) ∈ R) |
rp |
|
(,y)((a + b ∈ R & y ∈ R) => (a + b) * (y) ∈ R) |
spc |
|
(a + b ∈ R & (1 / c) ∈ R) => (a + b) * (1 / c) ∈ R |
spc |
|
a + b ∈ R & 1 / c ∈ R |
cnj |
|
(a + b) * (1 / c) ∈ R |
mp |
|
(x, y)((x ∈ R & y ∈ R) => (x) * (y) ∈ R) |
rp |
|
(,y)((1 / c ∈ R & y ∈ R) => (1 / c) * (y) ∈ R) |
spc |
|
(1 / c ∈ R & a ∈ R) => (1 / c) * (a) ∈ R |
spc |
|
1 / c ∈ R & a ∈ R |
cnj |
|
(1 / c) * (a) ∈ R |
mp |
|
(1 / c) * a ∈ R |
() out |
|
(,y)((1 / c ∈ R & y ∈ R) => (1 / c) * (y) ∈ R) |
rp |
|
(1 / c ∈ R & b ∈ R) => (1 / c) * (b) ∈ R |
spc |
|
1 / c ∈ R & b ∈ R |
cnj |
|
(1 / c) * (b) ∈ R |
mp |
|
(1 / c) * b ∈ R |
() out |
|
(x, y)((x ∈ R & y ∈ R) => (x) + (y) ∈ R) |
rp |
|
(,y)(((1 / c) * a ∈ R & y ∈ R) => ((1 / c) * a) + (y) ∈ R) |
spc |
|
((1 / c) * a ∈ R & (1 / c) * b ∈ R) => ((1 / c) * a) + ((1 / c) * b) ∈ R |
spc |
|
(1 / c) * a ∈ R & (1 / c) * b ∈ R |
cnj |
|
((1 / c) * a) + ((1 / c) * b) ∈ R |
mp |
|
(x, y)((x ∈ R & y ∈ R) => (x) * (y) ∈ R) |
rp |
|
(,y)((1 / c ∈ R & y ∈ R) => (1 / c) * (y) ∈ R) |
spc |
|
(1 / c ∈ R & a + b ∈ R) => (1 / c) * (a + b) ∈ R |
spc |
|
1 / c ∈ R & a + b ∈ R |
cnj |
|
(1 / c) * (a + b) ∈ R |
mp |
|
(x, y)((x ∈ R & y ∈ R) => (x) * (y) = (y) * (x) ) |
rp |
|
(,y)((a + b ∈ R & y ∈ R) => (a + b) * (y) = (y) * (a + b) ) |
spc |
|
(a + b ∈ R & 1 / c ∈ R) => (a + b) * (1 / c) = (1 / c) * (a + b) |
spc |
|
a + b ∈ R & 1 / c ∈ R |
rp |
|
(a + b) * (1 / c) = (1 / c) * (a + b) |
mp |
|
(x, y, z)((x ∈ R & y ∈ R & z ∈ R & x = y & y = z) => x = z) |
rp |
|
(y, z)(((a + b) / c ∈ R & y ∈ R & z ∈ R & (a + b) / c = y & y = z) => (a + b) / c = z) |
spc |
|
(,z)(((a + b) / c ∈ R & |
spc |
|
((a + b) / c ∈ R & |
|
|
(a + b) / c ∈ R & (a + b) * (1 / c) ∈ R |
cnj |
|
(a + b) / c ∈ R & |
|
|
(a + b) / c ∈ R & |
|
|
(a + b) / c ∈ R & |
|
|
(a + b) / c = (1 / c) * (a + b) |
mp |
|
(x, y, z)((x ∈ R & y ∈ R & z ∈ R) => (x) * [(y) + (z)] = [(x) * (y)] + [(x) * (z)] ) |
rp |
|
(y, z)(( 1 / c ∈ R & y ∈ R & z ∈ R) => (1 / c) * [(y) + (z)] = [(1 / c) * (y)] + [(1 / c) * (z)] ) |
spc |
|
(,z)(( 1 / c ∈ R & a ∈ R & z ∈ R) => (1 / c) * [(a) + (z)] = [(1 / c) * (a)] + [(1 / c) * (z)] ) |
spc |
|
( 1 / c ∈ R & a ∈ R & b ∈ R) => (1 / c) * [(a) + (b)] = [(1 / c) * (a)] + [(1 / c) * (b)] |
spc |
|
1 / c ∈ R & a ∈ R |
cnj |
|
1 / c ∈ R & a ∈ R & b ∈ R |
cnj |
|
(1 / c) * [(a) + (b)] = [(1 / c) * (a)] + [(1 / c) * (b)] |
mp |
|
(1 / c) * [a + b] = [(1 / c) * a] + [(1 / c) * b] |
() out |
|
(1 / c) * (a + b) = ((1 / c) * a) + ((1 / c) * b) |
change parenthesis to improve appearance |
|
(x, y, z)((x ∈ R & y ∈ R & z ∈ R & x = y & y = z) => x = z) |
rp |
|
(y, z)(((a + b) / c ∈ R & y ∈ R & z ∈ R & (a + b) / c = y & y = z) => (a + b) / c = z) |
spc |
|
(,z)(((a + b) / c ∈ R & |
|
|
((a + b) / c ∈ R & |
|
|
(a + b) / c ∈ R & (1 / c) * (a + b) ∈ R |
cnj |
|
(a + b) / c ∈ R & |
|
|
(a + b) / c ∈ R & |
|
|
(a + b) / c ∈ R & |
|
|
(a + b) / c = ((1 / c) * a) + ((1 / c) * b) |
mp |
|
(x, y)((x ∈ R & y ∈ R) => (x) * (y) = (y) * (x) ) |
rp |
|
(,y)(( 1 / c ∈ R & y ∈ R) => (1 / c) * (y) = (y) * (1 / c) ) |
spc |
|
( 1 / c ∈ R & a ∈ R) => (1 / c) * (a) = (a) * (1 / c) |
spc |
|
1 / c ∈ R & a ∈ R |
cnj |
|
(1 / c) * (a) = (a) * (1 / c) |
mp |
|
(1 / c) * a = a * (1 / c) |
() out |
|
(,y)(( 1 / c ∈ R & y ∈ R) => (1 / c) * (y) = (y) * (1 / c) ) |
rp |
|
( 1 / c ∈ R & b ∈ R) => (1 / c) * (b) = (b) * (1 / c) |
spc |
|
1 / c ∈ R & b ∈ R |
cnj |
|
(1 / c) * (b) = (b) * (1 / c) |
mp |
|
(1 / c) * b = b * (1 / c) |
() out |
|
(a + b) / c = ((1 / c) * a) + ((1 / c) * b) |
rp |
|
(a + b) / c = a * (1 / c) + ((1 / c) * b) |
substitution |
|
(a + b) / c = a * (1 / c) + b * (1 / c) |
substitution |
|
(x, y)((x ∈ R & y ∈ R & y <> 0) => (x) / (y) = (x) * (1 / (y)) ) (* definition of division *) |
rp |
|
(,y)((a ∈ R & y ∈ R & y <> 0) => (a) / (y) = (a) * (1 / (y)) ) |
spc |
|
(a ∈ R & c ∈ R & c <> 0) => (a) / (c) = (a) * (1 / (c)) |
spc |
|
a ∈ R & c ∈ R & c <> 0 |
cnj |
|
(a) / (c) = (a) * (1 / (c)) |
mp |
|
a / c = a * (1 / (c)) |
() out |
|
(x, y)((x ∈ R & y ∈ R & y <> 0) => (x) / (y) = (x) * (1 / (y)) ) (* definition of division *) |
rp |
|
(,y)((b ∈ R & y ∈ R & y <> 0) => (b) / (y) = (b) * (1 / (y)) ) |
spc |
|
(b ∈ R & c ∈ R & c <> 0) => (b) / (c) = (b) * (1 / (c)) |
spc |
|
b ∈ R & c ∈ R & c <> 0 |
cnj |
|
(b) / (c) = (b) * (1 / (c)) |
mp |
|
b / c = b * (1 / (c)) |
() out |
|
a / c = a * (1 / (c)) |
rp |
|
(a + b) / c = a * (1 / c) + b * (1 / c) |
rp |
|
(a + b) / c = a / c + b * (1 / c) |
substitution |
|
(a + b) / c = a / c + b / c |
substitution |
|
(* This is the conclusion we have bin seeking. We now discharge the second hypothesis *) |
|
|
-1H: (a ∈ R & b ∈ R & c ∈ R & c <> 0) => (a + b) / c = a / c + b / c |
conditional proof |
|
(,z)((a ∈ R & b ∈ R & z ∈ R & z <> 0) => (a + b) / z = a / z + b / z ) |
generaliza-tion |
|
(y,z)((a ∈ R & y ∈ R & z ∈ R & z <> 0) => (a + y) / z = a / z + y / z ) |
generaliza-tion |
|
(x,y,z)((x ∈ R & y ∈ R & z ∈ R & z <> 0) => (x + y) / z = x / z + y / z ) |
generaliza-tion |
|
(* We now discharge the initial hypothesis *) |
|
|
-0H: [R es set & |
|
|
(* We now apply generalization to quantify the name letters R, 0, 1. *) |
|
|
[[P es set & |
|
|
[[P es set & |
generaliza-tion 'Q' replaces '0' |
|
[[P es set & |
|
|
(* We are finally at the end of the proof *) |
|
Note: In this essay, I use the following notational conventions:
0H:, 1H:, 2H:, etc... start of hypothesis 0, start of hypothesis 1, start of hypothesis 2, etc.
-0H:, -1H:, -2H:, etc... end of hypothesis 0, end of hypothesis 1, end of hypothesis 2, etc.
(,x)(Fx => Gx). For all x, if x is F, then x is G.
x es Y: x is a Y, or x is Y.
x ∈ Y: x is an element of (the set) Y, i.e. x is in Y.
M => N: If M then N.
a <> b: a does not equal b