Metamath Proof Explorer


Theorem eucalglt

Description: The second member of the state decreases with each iteration of the step function E for Euclid's Algorithm. (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 eucalglt X 0 × 0 2 nd E X 0 2 nd E X < 2 nd 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 adantr X 0 × 0 2 nd E X 0 E X = if 2 nd X = 0 X 2 nd X mod X
4 simpr X 0 × 0 2 nd E X 0 2 nd E X 0
5 iftrue 2 nd X = 0 if 2 nd X = 0 X 2 nd X mod X = X
6 5 eqeq2d 2 nd X = 0 E X = if 2 nd X = 0 X 2 nd X mod X E X = X
7 fveq2 E X = X 2 nd E X = 2 nd X
8 6 7 syl6bi 2 nd X = 0 E X = if 2 nd X = 0 X 2 nd X mod X 2 nd E X = 2 nd X
9 eqeq2 2 nd X = 0 2 nd E X = 2 nd X 2 nd E X = 0
10 8 9 sylibd 2 nd X = 0 E X = if 2 nd X = 0 X 2 nd X mod X 2 nd E X = 0
11 3 10 syl5com X 0 × 0 2 nd E X 0 2 nd X = 0 2 nd E X = 0
12 11 necon3ad X 0 × 0 2 nd E X 0 2 nd E X 0 ¬ 2 nd X = 0
13 4 12 mpd X 0 × 0 2 nd E X 0 ¬ 2 nd X = 0
14 13 iffalsed X 0 × 0 2 nd E X 0 if 2 nd X = 0 X 2 nd X mod X = 2 nd X mod X
15 3 14 eqtrd X 0 × 0 2 nd E X 0 E X = 2 nd X mod X
16 15 fveq2d X 0 × 0 2 nd E X 0 2 nd E X = 2 nd 2 nd X mod X
17 fvex 2 nd X V
18 fvex mod X V
19 17 18 op2nd 2 nd 2 nd X mod X = mod X
20 16 19 eqtrdi X 0 × 0 2 nd E X 0 2 nd E X = mod X
21 1st2nd2 X 0 × 0 X = 1 st X 2 nd X
22 21 adantr X 0 × 0 2 nd E X 0 X = 1 st X 2 nd X
23 22 fveq2d X 0 × 0 2 nd E X 0 mod X = mod 1 st X 2 nd X
24 df-ov 1 st X mod 2 nd X = mod 1 st X 2 nd X
25 23 24 eqtr4di X 0 × 0 2 nd E X 0 mod X = 1 st X mod 2 nd X
26 20 25 eqtrd X 0 × 0 2 nd E X 0 2 nd E X = 1 st X mod 2 nd X
27 xp1st X 0 × 0 1 st X 0
28 27 adantr X 0 × 0 2 nd E X 0 1 st X 0
29 28 nn0red X 0 × 0 2 nd E X 0 1 st X
30 xp2nd X 0 × 0 2 nd X 0
31 30 adantr X 0 × 0 2 nd E X 0 2 nd X 0
32 elnn0 2 nd X 0 2 nd X 2 nd X = 0
33 31 32 sylib X 0 × 0 2 nd E X 0 2 nd X 2 nd X = 0
34 33 ord X 0 × 0 2 nd E X 0 ¬ 2 nd X 2 nd X = 0
35 13 34 mt3d X 0 × 0 2 nd E X 0 2 nd X
36 35 nnrpd X 0 × 0 2 nd E X 0 2 nd X +
37 modlt 1 st X 2 nd X + 1 st X mod 2 nd X < 2 nd X
38 29 36 37 syl2anc X 0 × 0 2 nd E X 0 1 st X mod 2 nd X < 2 nd X
39 26 38 eqbrtrd X 0 × 0 2 nd E X 0 2 nd E X < 2 nd X
40 39 ex X 0 × 0 2 nd E X 0 2 nd E X < 2 nd X