Metamath Proof Explorer

Theorem eucalgf

Description: Domain and codomain of the step function E for Euclid's Algorithm. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 28-May-2014)

Ref Expression
Hypothesis eucalgval.1 ⊢ 𝐸 = ( 𝑥 ∈ ℕ0 , 𝑦 ∈ ℕ0 ↦ if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) )
Assertion eucalgf 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ( ℕ0 × ℕ0 )

Proof

Step Hyp Ref Expression
1 eucalgval.1 ⊢ 𝐸 = ( 𝑥 ∈ ℕ0 , 𝑦 ∈ ℕ0 ↦ if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) )
2 nnne0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 )
3 2 adantl ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ ) → 𝑦 ≠ 0 )
4 3 neneqd ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ ) → ¬ 𝑦 = 0 )
5 4 iffalsed ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ ) → if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) = ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ )
6 nnnn0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℕ0 )
7 6 adantl ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℕ0 )
8 nn0z ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℤ )
9 zmodcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝑥 mod 𝑦 ) ∈ ℕ0 )
10 8 9 sylan ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ ) → ( 𝑥 mod 𝑦 ) ∈ ℕ0 )
11 7 10 opelxpd ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ ) → ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ∈ ( ℕ0 × ℕ0 ) )
12 5 11 eqeltrd ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ ) → if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) ∈ ( ℕ0 × ℕ0 ) )
13 12 adantlr ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑦 ∈ ℕ ) → if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) ∈ ( ℕ0 × ℕ0 ) )
14 iftrue ⊢ ( 𝑦 = 0 → if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) = ⟨ 𝑥 , 𝑦 ⟩ )
15 14 adantl ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑦 = 0 ) → if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) = ⟨ 𝑥 , 𝑦 ⟩ )
16 opelxpi ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ℕ0 × ℕ0 ) )
17 16 adantr ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑦 = 0 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ℕ0 × ℕ0 ) )
18 15 17 eqeltrd ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑦 = 0 ) → if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) ∈ ( ℕ0 × ℕ0 ) )
19 simpr ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → 𝑦 ∈ ℕ0 )
20 elnn0 ⊢ ( 𝑦 ∈ ℕ0 ↔ ( 𝑦 ∈ ℕ ∨ 𝑦 = 0 ) )
21 19 20 sylib ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑦 ∈ ℕ ∨ 𝑦 = 0 ) )
22 13 18 21 mpjaodan ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) ∈ ( ℕ0 × ℕ0 ) )
23 22 rgen2 ⊢ ∀ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) ∈ ( ℕ0 × ℕ0 )
24 1 fmpo ⊢ ( ∀ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 if ( 𝑦 = 0 , ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑦 , ( 𝑥 mod 𝑦 ) ⟩ ) ∈ ( ℕ0 × ℕ0 ) ↔ 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ( ℕ0 × ℕ0 ) )
25 23 24 mpbi ⊢ 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ( ℕ0 × ℕ0 )