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 \in ℕ_{0}, y \in ℕ_{0} ⟼ if (y = 0, ⟨x, y⟩, ⟨y, x \mod y⟩))$
	Assertion	eucalglt	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to (2^{nd} (E (X)) \neq 0 \to 2^{nd} (E (X)) < 2^{nd} (X))$

Proof

Step	Hyp	Ref	Expression
1		eucalgval.1	$⊢ E = (x \in ℕ_{0}, y \in ℕ_{0} ⟼ if (y = 0, ⟨x, y⟩, ⟨y, x \mod y⟩))$
2	1	eucalgval	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to E (X) = if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩)$
3	2	adantr	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to E (X) = if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩)$
4		simpr	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to 2^{nd} (E (X)) \neq 0$
5		iftrue	$⊢ 2^{nd} (X) = 0 \to if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩) = X$
6	5	eqeq2d	$⊢ 2^{nd} (X) = 0 \to (E (X) = if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩) \leftrightarrow E (X) = X)$
7		fveq2	$⊢ E (X) = X \to 2^{nd} (E (X)) = 2^{nd} (X)$
8	6 7	syl6bi	$⊢ 2^{nd} (X) = 0 \to (E (X) = if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩) \to 2^{nd} (E (X)) = 2^{nd} (X))$
9		eqeq2	$⊢ 2^{nd} (X) = 0 \to (2^{nd} (E (X)) = 2^{nd} (X) \leftrightarrow 2^{nd} (E (X)) = 0)$
10	8 9	sylibd	$⊢ 2^{nd} (X) = 0 \to (E (X) = if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩) \to 2^{nd} (E (X)) = 0)$
11	3 10	syl5com	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to (2^{nd} (X) = 0 \to 2^{nd} (E (X)) = 0)$
12	11	necon3ad	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to (2^{nd} (E (X)) \neq 0 \to \neg 2^{nd} (X) = 0)$
13	4 12	mpd	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to \neg 2^{nd} (X) = 0$
14	13	iffalsed	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to if (2^{nd} (X) = 0, X, ⟨2^{nd} (X), \mod (X)⟩) = ⟨2^{nd} (X), \mod (X)⟩$
15	3 14	eqtrd	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to E (X) = ⟨2^{nd} (X), \mod (X)⟩$
16	15	fveq2d	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to 2^{nd} (E (X)) = 2^{nd} (⟨2^{nd} (X), \mod (X)⟩)$
17		fvex	$⊢ 2^{nd} (X) \in V$
18		fvex	$⊢ \mod (X) \in V$
19	17 18	op2nd	$⊢ 2^{nd} (⟨2^{nd} (X), \mod (X)⟩) = \mod (X)$
20	16 19	syl6eq	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to 2^{nd} (E (X)) = \mod (X)$
21		1st2nd2	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
22	21	adantr	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
23	22	fveq2d	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to \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	syl6eqr	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to \mod (X) = 1^{st} (X) \mod 2^{nd} (X)$
26	20 25	eqtrd	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to 2^{nd} (E (X)) = 1^{st} (X) \mod 2^{nd} (X)$
27		xp1st	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to 1^{st} (X) \in ℕ_{0}$
28	27	adantr	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to 1^{st} (X) \in ℕ_{0}$
29	28	nn0red	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to 1^{st} (X) \in ℝ$
30		xp2nd	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to 2^{nd} (X) \in ℕ_{0}$
31	30	adantr	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to 2^{nd} (X) \in ℕ_{0}$
32		elnn0	$⊢ 2^{nd} (X) \in ℕ_{0} \leftrightarrow (2^{nd} (X) \in ℕ \lor 2^{nd} (X) = 0)$
33	31 32	sylib	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to (2^{nd} (X) \in ℕ \lor 2^{nd} (X) = 0)$
34	33	ord	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to (\neg 2^{nd} (X) \in ℕ \to 2^{nd} (X) = 0)$
35	13 34	mt3d	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to 2^{nd} (X) \in ℕ$
36	35	nnrpd	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to 2^{nd} (X) \in ℝ^{+}$
37		modlt	$⊢ (1^{st} (X) \in ℝ \land 2^{nd} (X) \in ℝ^{+}) \to 1^{st} (X) \mod 2^{nd} (X) < 2^{nd} (X)$
38	29 36 37	syl2anc	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to 1^{st} (X) \mod 2^{nd} (X) < 2^{nd} (X)$
39	26 38	eqbrtrd	$⊢ (X \in (ℕ_{0} \times ℕ_{0}) \land 2^{nd} (E (X)) \neq 0) \to 2^{nd} (E (X)) < 2^{nd} (X)$
40	39	ex	$⊢ X \in (ℕ_{0} \times ℕ_{0}) \to (2^{nd} (E (X)) \neq 0 \to 2^{nd} (E (X)) < 2^{nd} (X))$

Metamath Proof Explorer

Theorem eucalglt

Proof