let i, n be Nat; :: thesis: ( i is_expressible_by n implies ADD_MOD (i,(NEG_MOD (i,n)),n) = 0 )
assume i is_expressible_by n ; :: thesis: 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 ;
:: thesis: verum