Following is the proof that *Cast9*(*a*) = mod_{9} (*a*-1) + 1. Let's start with a few definitions that the proof will use:

- Let
*a*= source number. - Let's refer to the rightmost digit of
*a*as*a*_{0}and to the leftmost digit of*a*as*a*._{n} - Let
*a'*= ∑^{n}i=0_{a}^{i},*a.* - Let
*a"*= recursive sum of digits of*a*until one digit is left—i.e., Cast9(*a*).

Let's prove that *a" *= mod_{9} (*a*-1) + 1. You can represent the number *a* as the sum of its digits multiplied by 10 to the power of the digit's position: *a *= 10* ^{n}a_{n }*+ 10

^{n}^{-1}

*a*

_{n}_{-1}+...+10

^{1}

*a*

_{1}+10

^{0}

*a*

_{0}. For example, you can represent the number 947 as 10

^{2 }* 9 + 10

^{1 }* 4 +10

^{0 }* 7.

You can represent the number as a number composed of *i* instances of 9 plus 1 (999... + 1) or as 9 multiplied by *i* digits of 1 plus 1 (9 x 111... + 1). For example, you can represent 10^{3} as 999

+ 1 or as 9 * 111 + 1. Let's refer to a number composed of *i* digits of 1 as *x _{i}.* Applying this rule to the previous equation, you can write:

*a *= (9*x _{n }*+ 1)

*a*+ (9

_{n }*x*

_{n}_{-1 }+ 1)

*a*

_{n}_{-1 }+...+ (9

*x*

_{1 }+ 1)

*a*

_{1 }+ (9

*x*

_{0 }+ 1)

*a*

_{0 }=

9

*x*+

_{n}a_{n }*a*+ 9

_{n }*x*

_{n}_{-1}

*a*

_{n}_{-1 }+...+ 9

*x*

_{1}

*a*

_{1 }+ 9

*x*

_{0}

*a*

_{0}

You can separate the parts that are multiplied by *x _{i}* (where

*i*ranges from 0 to

*n*) from the

parts that aren't, then rewrite the equation in the summarized notation

*a*= 9∑

*+ ∑*

^{ni=0}x_{i}a_{i}*. Performing a modulo 9 operation on both sides of the equation, you get mod*

^{ni=0}a_{i}_{9}(

*a*) = mod

_{9 }(9∑

*+ ∑*

^{ni=0}x_{i}a_{i}*). From the rules of modulo, it follows that mod*

^{ni=0}a_{i}*(*

_{b }*bc + d*) = mod

*(*

_{b }*d*). Applying this rule to the previous equation gives you mod

_{9}(

*a*) = mod

_{9 }(∑

*). Notice that the sigma inside the parentheses on the right side of the equation is the sum of all the digits of*

^{ni=0}a_{i}*a*. You can rewrite the equation as mod

_{9}(

*a*) = mod

_{9}(

*a'*).

Thus, modulo 9 of a number is equal to modulo 9 of the sum of that number's digits. Applying that conclusion to the sum of the source number's digits, you can say that modulo 9 of the sum of a number's digits is equal to modulo 9 of the sum of the digits of the result number. You can continue in this manner until one digit remains, but let's simply conclude that the equation is recursive. You can, therefore, write mod_{9} (*a*) = mod_{9} (*a'*) = ... = mod_{9} (*a"*).

Remember that we defined *a"* as the recursive sum of the digits of the number *a*. From the rules of modulo, it follows that if mod* _{b }*(

*c*) = mod

*(*

_{b }*d*), then mod

*(*

_{b }*c + e*) = mod

*(*

_{b }*d+ e*). Applying this rule to the previous equation, you get mod

_{9}(

*a* 1) = mod

_{9}(

*a"* 1).

For any *a* > 0, *a"* is a digit in the range of 1 to 9, so (*a"* 1) is in the range of 0 to 8. Modulo 9 of any number in the range of 0 to 8 is the number itself; hence, mod_{9} (*a" * 1) = *a" * 1. Applying this rule to the previous equation, you get mod_{9} (*a* 1) = *a" * 1. And by adding 1 to both sides of the equation to simplify it, you get mod_{9} (*a* 1) + 1 = *a"*