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	⊢ 𝐸 = ( 𝑥 ∈ ℕ₀ , 𝑦 ∈ ℕ₀ ↦ if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) )
	Assertion	eucalglt	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 → ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) < ( 2^nd ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eucalgval.1	⊢ 𝐸 = ( 𝑥 ∈ ℕ₀ , 𝑦 ∈ ℕ₀ ↦ if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) )
2	1	eucalgval	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( 𝐸 ‘ 𝑋 ) = if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) )
3	2	adantr	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( 𝐸 ‘ 𝑋 ) = if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) )
4		simpr	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 )
5		iftrue	⊢ ( ( 2^nd ‘ 𝑋 ) = 0 → if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) = 𝑋 )
6	5	eqeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 0 → ( ( 𝐸 ‘ 𝑋 ) = if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) ↔ ( 𝐸 ‘ 𝑋 ) = 𝑋 ) )
7		fveq2	⊢ ( ( 𝐸 ‘ 𝑋 ) = 𝑋 → ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) = ( 2^nd ‘ 𝑋 ) )
8	6 7	syl6bi	⊢ ( ( 2^nd ‘ 𝑋 ) = 0 → ( ( 𝐸 ‘ 𝑋 ) = if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) → ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) = ( 2^nd ‘ 𝑋 ) ) )
9		eqeq2	⊢ ( ( 2^nd ‘ 𝑋 ) = 0 → ( ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) = ( 2^nd ‘ 𝑋 ) ↔ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) = 0 ) )
10	8 9	sylibd	⊢ ( ( 2^nd ‘ 𝑋 ) = 0 → ( ( 𝐸 ‘ 𝑋 ) = if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) → ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) = 0 ) )
11	3 10	syl5com	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( ( 2^nd ‘ 𝑋 ) = 0 → ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) = 0 ) )
12	11	necon3ad	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 → ¬ ( 2^nd ‘ 𝑋 ) = 0 ) )
13	4 12	mpd	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ¬ ( 2^nd ‘ 𝑋 ) = 0 )
14	13	iffalsed	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → if ( ( 2^nd ‘ 𝑋 ) = 0 , 𝑋 , ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) = ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ )
15	3 14	eqtrd	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( 𝐸 ‘ 𝑋 ) = ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ )
16	15	fveq2d	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) = ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) )
17		fvex	⊢ ( 2^nd ‘ 𝑋 ) ∈ V
18		fvex	⊢ ( mod ‘ 𝑋 ) ∈ V
19	17 18	op2nd	⊢ ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑋 ) , ( mod ‘ 𝑋 ) ⟩ ) = ( mod ‘ 𝑋 )
20	16 19	eqtrdi	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) = ( mod ‘ 𝑋 ) )
21		1st2nd2	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
22	21	adantr	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
23	22	fveq2d	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( mod ‘ 𝑋 ) = ( mod ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ) )
24		df-ov	⊢ ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) = ( mod ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
25	23 24	eqtr4di	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( mod ‘ 𝑋 ) = ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) )
26	20 25	eqtrd	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) = ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) )
27		xp1st	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( 1^st ‘ 𝑋 ) ∈ ℕ₀ )
28	27	adantr	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( 1^st ‘ 𝑋 ) ∈ ℕ₀ )
29	28	nn0red	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( 1^st ‘ 𝑋 ) ∈ ℝ )
30		xp2nd	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( 2^nd ‘ 𝑋 ) ∈ ℕ₀ )
31	30	adantr	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( 2^nd ‘ 𝑋 ) ∈ ℕ₀ )
32		elnn0	⊢ ( ( 2^nd ‘ 𝑋 ) ∈ ℕ₀ ↔ ( ( 2^nd ‘ 𝑋 ) ∈ ℕ ∨ ( 2^nd ‘ 𝑋 ) = 0 ) )
33	31 32	sylib	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( ( 2^nd ‘ 𝑋 ) ∈ ℕ ∨ ( 2^nd ‘ 𝑋 ) = 0 ) )
34	33	ord	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( ¬ ( 2^nd ‘ 𝑋 ) ∈ ℕ → ( 2^nd ‘ 𝑋 ) = 0 ) )
35	13 34	mt3d	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( 2^nd ‘ 𝑋 ) ∈ ℕ )
36	35	nnrpd	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( 2^nd ‘ 𝑋 ) ∈ ℝ⁺ )
37		modlt	⊢ ( ( ( 1^st ‘ 𝑋 ) ∈ ℝ ∧ ( 2^nd ‘ 𝑋 ) ∈ ℝ⁺ ) → ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) < ( 2^nd ‘ 𝑋 ) )
38	29 36 37	syl2anc	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( ( 1^st ‘ 𝑋 ) mod ( 2^nd ‘ 𝑋 ) ) < ( 2^nd ‘ 𝑋 ) )
39	26 38	eqbrtrd	⊢ ( ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) ∧ ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 ) → ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) < ( 2^nd ‘ 𝑋 ) )
40	39	ex	⊢ ( 𝑋 ∈ ( ℕ₀ × ℕ₀ ) → ( ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) ≠ 0 → ( 2^nd ‘ ( 𝐸 ‘ 𝑋 ) ) < ( 2^nd ‘ 𝑋 ) ) )

Metamath Proof Explorer

Theorem eucalglt

Proof