[Sussex] Challenge

[Mark Harrison]

> The proof is simple, it must in base 2 prove
> that the following base 10 equation is correct:
> 10 * 0.1 = 1.0

Notes on typography:

1: Due to the limitation of plain text, I cannot realistically use subscript
numbers to indicate base. I will, therefore adopt the convention of including
the base in curly brackets {}. For the avoidance of doubt, I will attempt to
include the base on all numbers (except for the expression of the base itself,
which will always be expressed in decimal.)

2: I have furthermore adopted the conventional use of the binding power of
operators - namely that ^ has higher priority than * and /, which in turn have
higher priority than + and -. I've done this to stop there being too many
superfluous brackets.

-------------------------------------

The challenge is, therefore:

Prove that 10 {10} * 0.1 {10} = 1.0 {10}

Let us start by converting our numbers to binary EXPRESSIONS.

Conversion 0:        1 {10} = 1 {2}
--- Proved by the definition of position arithmetic

Conversion 1:     1{10} = 1.0 {10}
---- 1.0 {10} = 1{10} * 1{10} ^ 0 {10}
                     + 0 * 1 {10} ^ -1 {10}
----- by the definition of position arithmetic
--- 1.0 {10} = 1 {10} * 1{10} ^ 0{10}
----- by the rule 0 * anything = 0
--- 1 {10} = 1 {10} * 1{10} ^ 0{10}
----- by the defintion of position arithmetic
--- Therefore 1.0 {10} = 1 {10}
----- by transitivity of the equality operator

Conversion 1b: 1{2} = 1.0 {2}
----- trivial from Conversion 1, substituting {2} for {10}

Conversion 2:         10 {10} = 1010 {2}

--- Proof that 10 {10} = 1010 {2}
--- 1010 {2} = 1 {10} *     (2{10} ^ 3{10})
                     + 0 {10} *     (2{10} ^ 2{10})
                     + 1 {10} *     (2{10} ^ 1{10})
                     + 0 {10} *     (2{10} ^ 0{10})
----- by the definition of position arithmetic
--- 1010 {2} = 1 {10} * (2{10} ^ 3{10})  + 1 {10} * (2{10} ^ 1{0})
----- by the rule 0 * anything = 0
--- 1010 {2} = 1 * 8 + 1 * 2
----- by evaluation of the powers of 2 in decimal
--- 1010 {2} = 10 {10}
----- by addition in decimal

Conversion 3        .1 {10} = 1 {2} * 1010 {2} ^ -1 {2}

--- Proof that .1 {10} = 1 {2} / 1010 {2}
--- .1 {10} = 1 {10} * 10 {10} ^ -1 {10}
----- by the defintion of position arithmetic
--- We know that 1 {10} = 1 {2}
----- by the defintion of unity
----- hence we can substitute
--- .1 {10} = 1 {2} * 10 {10} ^ -1 {10}
--- We know that 10 {10} = 1010 {2}
----- from Conversion 2 above
----- hence we can substitute
--- .1 {10} = 1 {2} * 1010 {2} ^ -1 {10}
----- Again, we know that 1 {10} = 1 {2}
----- from Conversion 0 above
----- so again we can substitute
--- .1 {10} = 1 {2} * 1010 {2} ^ - 1{2}

To restate the requirement, we are asked to prove the following in binary:

Prove that 10 {10} * 0.1 {10} = 1.0 {10}

By substitution of the two conversions above, the requirement is to prove that:

1010 {2} *  1 {2} * 1010 {2} ^ - 1{2}= 1.0 (2)

We can substitute by conversion 1b to read:

1010 {2} *  1 {2} * 1010 {2} ^ - 1{2}= 1 (2)

We can rearrange the left hand side to read:

(1010 {2} * 1{2}) * (1010 {2} ^ -1 {2})

= 1010 {2} / 1010 {2}
---- by the definition of expressing anything to the power of minus 1

= 1 {2}
---- by the rule that any non-zero number divided by itself equals 1

Job done....

... believe me, a hell of a lot easier in paper and pen, when I can write
equations out :-)

Regards,

Mark