let i, n be Nat; ( i is_expressible_by n implies ADD_MOD (i,(NEG_MOD (i,n)),n) = 0 )
assume
i is_expressible_by n
; ADD_MOD (i,(NEG_MOD (i,n)),n) = 0
then i + (NEG_N (i,n)) =
i + ((2 to_power n) - i)
by Def5
.=
0 + (2 to_power n)
;
hence ADD_MOD (i,(NEG_MOD (i,n)),n) =
(2 to_power n) mod (2 to_power n)
by NAT_D:23
.=
0
by NAT_D:25
;
verum