Re: [isabelle] need help by mod

kuecuek at wrote:
Hallo everybody

i have some problems with modulo and power :(

i need following prooofs but i couldn't show these. 1) ((a::int) - b) mod p = (a mod p - b mod p) mod p there is a lemma called zmod_zadd1_eq in IntDiv. i have tried to use this lemma with the variable "-b" but it doesn't help.

[zmod_zsub_left_eq, zmod_zsub_right_eq] MRS trans RS sym

2)"(a::int) mod p = b mod p ==> a ^ k mod p = b ^ k mod p"
by this lemma i have problems too.

This would be proved by induction on k, I think for the induction step you would use the corresponding theorem for multiplication which would be
[zmod_zmult1_eq, zmod_zmult1_eq_rev] MRS trans RS sym ;



could anyone help me?

thanks for your helps

best regards

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.