Metamath Proof Explorer


Theorem eucalginv

Description: The invariant of the step function E for Euclid's Algorithm is the gcd operator applied to the state. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 29-May-2014)

Ref Expression
Hypothesis eucalgval.1 E = x 0 , y 0 if y = 0 x y y x mod y
Assertion eucalginv X 0 × 0 gcd E X = gcd X

Proof

Step Hyp Ref Expression
1 eucalgval.1 E = x 0 , y 0 if y = 0 x y y x mod y
2 1 eucalgval X 0 × 0 E X = if 2 nd X = 0 X 2 nd X mod X
3 2 fveq2d X 0 × 0 gcd E X = gcd if 2 nd X = 0 X 2 nd X mod X
4 1st2nd2 X 0 × 0 X = 1 st X 2 nd X
5 4 adantr X 0 × 0 2 nd X X = 1 st X 2 nd X
6 5 fveq2d X 0 × 0 2 nd X mod X = mod 1 st X 2 nd X
7 df-ov 1 st X mod 2 nd X = mod 1 st X 2 nd X
8 6 7 eqtr4di X 0 × 0 2 nd X mod X = 1 st X mod 2 nd X
9 8 oveq2d X 0 × 0 2 nd X 2 nd X gcd mod X = 2 nd X gcd 1 st X mod 2 nd X
10 nnz 2 nd X 2 nd X
11 xp1st X 0 × 0 1 st X 0
12 11 adantr X 0 × 0 2 nd X 1 st X 0
13 12 nn0zd X 0 × 0 2 nd X 1 st X
14 zmodcl 1 st X 2 nd X 1 st X mod 2 nd X 0
15 13 14 sylancom X 0 × 0 2 nd X 1 st X mod 2 nd X 0
16 15 nn0zd X 0 × 0 2 nd X 1 st X mod 2 nd X
17 gcdcom 2 nd X 1 st X mod 2 nd X 2 nd X gcd 1 st X mod 2 nd X = 1 st X mod 2 nd X gcd 2 nd X
18 10 16 17 syl2an2 X 0 × 0 2 nd X 2 nd X gcd 1 st X mod 2 nd X = 1 st X mod 2 nd X gcd 2 nd X
19 modgcd 1 st X 2 nd X 1 st X mod 2 nd X gcd 2 nd X = 1 st X gcd 2 nd X
20 13 19 sylancom X 0 × 0 2 nd X 1 st X mod 2 nd X gcd 2 nd X = 1 st X gcd 2 nd X
21 9 18 20 3eqtrd X 0 × 0 2 nd X 2 nd X gcd mod X = 1 st X gcd 2 nd X
22 nnne0 2 nd X 2 nd X 0
23 22 adantl X 0 × 0 2 nd X 2 nd X 0
24 23 neneqd X 0 × 0 2 nd X ¬ 2 nd X = 0
25 24 iffalsed X 0 × 0 2 nd X if 2 nd X = 0 X 2 nd X mod X = 2 nd X mod X
26 25 fveq2d X 0 × 0 2 nd X gcd if 2 nd X = 0 X 2 nd X mod X = gcd 2 nd X mod X
27 df-ov 2 nd X gcd mod X = gcd 2 nd X mod X
28 26 27 eqtr4di X 0 × 0 2 nd X gcd if 2 nd X = 0 X 2 nd X mod X = 2 nd X gcd mod X
29 5 fveq2d X 0 × 0 2 nd X gcd X = gcd 1 st X 2 nd X
30 df-ov 1 st X gcd 2 nd X = gcd 1 st X 2 nd X
31 29 30 eqtr4di X 0 × 0 2 nd X gcd X = 1 st X gcd 2 nd X
32 21 28 31 3eqtr4d X 0 × 0 2 nd X gcd if 2 nd X = 0 X 2 nd X mod X = gcd X
33 iftrue 2 nd X = 0 if 2 nd X = 0 X 2 nd X mod X = X
34 33 fveq2d 2 nd X = 0 gcd if 2 nd X = 0 X 2 nd X mod X = gcd X
35 34 adantl X 0 × 0 2 nd X = 0 gcd if 2 nd X = 0 X 2 nd X mod X = gcd X
36 xp2nd X 0 × 0 2 nd X 0
37 elnn0 2 nd X 0 2 nd X 2 nd X = 0
38 36 37 sylib X 0 × 0 2 nd X 2 nd X = 0
39 32 35 38 mpjaodan X 0 × 0 gcd if 2 nd X = 0 X 2 nd X mod X = gcd X
40 3 39 eqtrd X 0 × 0 gcd E X = gcd X