Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eucalginv Structured version   Unicode version

Theorem eucalginv 13080
 Description: The invariant of the step function for Euclid's Algorithm is the operator applied to the state. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 29-May-2014.)
Hypothesis
Ref Expression
eucalgval.1
Assertion
Ref Expression
eucalginv
Distinct variable group:   ,,
Allowed substitution hints:   (,)

Proof of Theorem eucalginv
StepHypRef Expression
1 eucalgval.1 . . . 4
21eucalgval 13078 . . 3
32fveq2d 5735 . 2
4 1st2nd2 6389 . . . . . . . . 9
54adantr 453 . . . . . . . 8
65fveq2d 5735 . . . . . . 7
7 df-ov 6087 . . . . . . 7
86, 7syl6eqr 2488 . . . . . 6
98oveq2d 6100 . . . . 5
10 nnz 10308 . . . . . . 7
1110adantl 454 . . . . . 6
12 xp1st 6379 . . . . . . . . . 10
1312adantr 453 . . . . . . . . 9
1413nn0zd 10378 . . . . . . . 8
15 zmodcl 11271 . . . . . . . 8
1614, 15sylancom 650 . . . . . . 7
1716nn0zd 10378 . . . . . 6
18 gcdcom 13025 . . . . . 6
1911, 17, 18syl2anc 644 . . . . 5
20 modgcd 13041 . . . . . 6
2114, 20sylancom 650 . . . . 5
229, 19, 213eqtrd 2474 . . . 4
23 nnne0 10037 . . . . . . . . 9
2423adantl 454 . . . . . . . 8
2524neneqd 2619 . . . . . . 7
26 iffalse 3748 . . . . . . 7
2725, 26syl 16 . . . . . 6
2827fveq2d 5735 . . . . 5
29 df-ov 6087 . . . . 5
3028, 29syl6eqr 2488 . . . 4
315fveq2d 5735 . . . . 5
32 df-ov 6087 . . . . 5
3331, 32syl6eqr 2488 . . . 4
3422, 30, 333eqtr4d 2480 . . 3
35 iftrue 3747 . . . . 5
3635fveq2d 5735 . . . 4