# Re: [isabelle] need help

```The following theorems may be of some use:
IntDiv.zmod_zmult1_eq
IntDiv.zmod_zmult1_eq'
IntDiv.zpower_zmod

In particular, you can use them to prove congruence rules for modular
arithmetic, such as:
[| x mod p = x' mod p; y mod p = y' mod p |]
==> (x + y) mod p = (x' + y') mod p

and similarly for subtraction, multiplication and exponentiation. I'm not sure
if this will give you everything you want, but at least this should allow you
to remove the inner mod operations from your subgoals.

- Brian

On Wednesday 06 December 2006 08:55, kuecuek at rbg.informatik.tu-darmstadt.de
wrote:
> hallo,
>
> i try to solve an equation but it is realy complex can anybody help me?
> if i try with numbers then i can show it with "auto" but if i use variables
> then i can not proof it.
>
>
> the equations below are given
>
> y1 ^2 = x1 ^3 + a*x1 + b
> y2 ^2 = x2 ^ 3 + a*x2 + b
>
> and
>
> x3 =  ((((y1 - y2) *  ((x1 - x2) ^ nat (p -2 ))) mod p) ^ 2 - x1 - x2) mod
> p y3 = ((((y1 - y2) *  ((x1 - x2) ^ nat (p -2 ))) mod p) * (x1 - x3) - y1)
> mod p
>
>
> and i must to show that y3^2 = x3^3 + a*x3 + b
>
> if you put the definitionof y3 and x3 in last equation you would see how
> complex it is :(
>
> can anybody give a trick to proof something like that?
>
> thanks a lot

```

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