Therefore, there is a way to go from a proof of 0 = 1 to a proof of any basic arithmetic equality, and thus to a proof of any complex arithmetic proposition. Furthermore, to get this result it was not necessary to invoke the Peano axiom that states that 0 is "not" the successor of any natural number. This makes 0 = 1 suitable as formula_19 in Heyting arithmetic (and the Peano axiom is rewritten 0 = S"n" → 0 = S0). This use of 0 = 1 validates the principle of explosion.