Proof of Theorem eucalginv
| Step | Hyp | Ref
| Expression |
| 1 | | eucalgval.1 |
. . . 4
⊢ 𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0
↦ if(𝑦 = 0,
〈𝑥, 𝑦〉, 〈𝑦, (𝑥 mod 𝑦)〉)) |
| 2 | 1 | eucalgval 16619 |
. . 3
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → (𝐸‘𝑋) = if((2nd ‘𝑋) = 0, 𝑋, 〈(2nd ‘𝑋), ( mod ‘𝑋)〉)) |
| 3 | 2 | fveq2d 6910 |
. 2
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → ( gcd ‘(𝐸‘𝑋)) = ( gcd ‘if((2nd
‘𝑋) = 0, 𝑋, 〈(2nd
‘𝑋), ( mod
‘𝑋)〉))) |
| 4 | | 1st2nd2 8053 |
. . . . . . . . 9
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → 𝑋 = 〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
| 5 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → 𝑋 = 〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
| 6 | 5 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( mod ‘𝑋) = ( mod
‘〈(1st ‘𝑋), (2nd ‘𝑋)〉)) |
| 7 | | df-ov 7434 |
. . . . . . 7
⊢
((1st ‘𝑋) mod (2nd ‘𝑋)) = ( mod
‘〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( mod ‘𝑋) = ((1st
‘𝑋) mod
(2nd ‘𝑋))) |
| 9 | 8 | oveq2d 7447 |
. . . . 5
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ((2nd
‘𝑋) gcd ( mod
‘𝑋)) =
((2nd ‘𝑋)
gcd ((1st ‘𝑋) mod (2nd ‘𝑋)))) |
| 10 | | nnz 12634 |
. . . . . 6
⊢
((2nd ‘𝑋) ∈ ℕ → (2nd
‘𝑋) ∈
ℤ) |
| 11 | | xp1st 8046 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → (1st ‘𝑋) ∈
ℕ0) |
| 12 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → (1st
‘𝑋) ∈
ℕ0) |
| 13 | 12 | nn0zd 12639 |
. . . . . . . 8
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → (1st
‘𝑋) ∈
ℤ) |
| 14 | | zmodcl 13931 |
. . . . . . . 8
⊢
(((1st ‘𝑋) ∈ ℤ ∧ (2nd
‘𝑋) ∈ ℕ)
→ ((1st ‘𝑋) mod (2nd ‘𝑋)) ∈
ℕ0) |
| 15 | 13, 14 | sylancom 588 |
. . . . . . 7
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ((1st
‘𝑋) mod
(2nd ‘𝑋))
∈ ℕ0) |
| 16 | 15 | nn0zd 12639 |
. . . . . 6
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ((1st
‘𝑋) mod
(2nd ‘𝑋))
∈ ℤ) |
| 17 | | gcdcom 16550 |
. . . . . 6
⊢
(((2nd ‘𝑋) ∈ ℤ ∧ ((1st
‘𝑋) mod
(2nd ‘𝑋))
∈ ℤ) → ((2nd ‘𝑋) gcd ((1st ‘𝑋) mod (2nd
‘𝑋))) =
(((1st ‘𝑋)
mod (2nd ‘𝑋)) gcd (2nd ‘𝑋))) |
| 18 | 10, 16, 17 | syl2an2 686 |
. . . . 5
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ((2nd
‘𝑋) gcd
((1st ‘𝑋)
mod (2nd ‘𝑋))) = (((1st ‘𝑋) mod (2nd
‘𝑋)) gcd
(2nd ‘𝑋))) |
| 19 | | modgcd 16569 |
. . . . . 6
⊢
(((1st ‘𝑋) ∈ ℤ ∧ (2nd
‘𝑋) ∈ ℕ)
→ (((1st ‘𝑋) mod (2nd ‘𝑋)) gcd (2nd
‘𝑋)) =
((1st ‘𝑋)
gcd (2nd ‘𝑋))) |
| 20 | 13, 19 | sylancom 588 |
. . . . 5
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → (((1st
‘𝑋) mod
(2nd ‘𝑋))
gcd (2nd ‘𝑋)) = ((1st ‘𝑋) gcd (2nd
‘𝑋))) |
| 21 | 9, 18, 20 | 3eqtrd 2781 |
. . . 4
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ((2nd
‘𝑋) gcd ( mod
‘𝑋)) =
((1st ‘𝑋)
gcd (2nd ‘𝑋))) |
| 22 | | nnne0 12300 |
. . . . . . . . 9
⊢
((2nd ‘𝑋) ∈ ℕ → (2nd
‘𝑋) ≠
0) |
| 23 | 22 | adantl 481 |
. . . . . . . 8
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → (2nd
‘𝑋) ≠
0) |
| 24 | 23 | neneqd 2945 |
. . . . . . 7
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ¬
(2nd ‘𝑋) =
0) |
| 25 | 24 | iffalsed 4536 |
. . . . . 6
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → if((2nd
‘𝑋) = 0, 𝑋, 〈(2nd
‘𝑋), ( mod
‘𝑋)〉) =
〈(2nd ‘𝑋), ( mod ‘𝑋)〉) |
| 26 | 25 | fveq2d 6910 |
. . . . 5
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( gcd
‘if((2nd ‘𝑋) = 0, 𝑋, 〈(2nd ‘𝑋), ( mod ‘𝑋)〉)) = ( gcd
‘〈(2nd ‘𝑋), ( mod ‘𝑋)〉)) |
| 27 | | df-ov 7434 |
. . . . 5
⊢
((2nd ‘𝑋) gcd ( mod ‘𝑋)) = ( gcd ‘〈(2nd
‘𝑋), ( mod
‘𝑋)〉) |
| 28 | 26, 27 | eqtr4di 2795 |
. . . 4
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( gcd
‘if((2nd ‘𝑋) = 0, 𝑋, 〈(2nd ‘𝑋), ( mod ‘𝑋)〉)) = ((2nd
‘𝑋) gcd ( mod
‘𝑋))) |
| 29 | 5 | fveq2d 6910 |
. . . . 5
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( gcd ‘𝑋) = ( gcd
‘〈(1st ‘𝑋), (2nd ‘𝑋)〉)) |
| 30 | | df-ov 7434 |
. . . . 5
⊢
((1st ‘𝑋) gcd (2nd ‘𝑋)) = ( gcd
‘〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
| 31 | 29, 30 | eqtr4di 2795 |
. . . 4
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( gcd ‘𝑋) = ((1st
‘𝑋) gcd
(2nd ‘𝑋))) |
| 32 | 21, 28, 31 | 3eqtr4d 2787 |
. . 3
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( gcd
‘if((2nd ‘𝑋) = 0, 𝑋, 〈(2nd ‘𝑋), ( mod ‘𝑋)〉)) = ( gcd ‘𝑋)) |
| 33 | | iftrue 4531 |
. . . . 5
⊢
((2nd ‘𝑋) = 0 → if((2nd ‘𝑋) = 0, 𝑋, 〈(2nd ‘𝑋), ( mod ‘𝑋)〉) = 𝑋) |
| 34 | 33 | fveq2d 6910 |
. . . 4
⊢
((2nd ‘𝑋) = 0 → ( gcd ‘if((2nd
‘𝑋) = 0, 𝑋, 〈(2nd
‘𝑋), ( mod
‘𝑋)〉)) = ( gcd
‘𝑋)) |
| 35 | 34 | adantl 481 |
. . 3
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) = 0) → ( gcd
‘if((2nd ‘𝑋) = 0, 𝑋, 〈(2nd ‘𝑋), ( mod ‘𝑋)〉)) = ( gcd ‘𝑋)) |
| 36 | | xp2nd 8047 |
. . . 4
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → (2nd ‘𝑋) ∈
ℕ0) |
| 37 | | elnn0 12528 |
. . . 4
⊢
((2nd ‘𝑋) ∈ ℕ0 ↔
((2nd ‘𝑋)
∈ ℕ ∨ (2nd ‘𝑋) = 0)) |
| 38 | 36, 37 | sylib 218 |
. . 3
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → ((2nd ‘𝑋) ∈ ℕ ∨ (2nd
‘𝑋) =
0)) |
| 39 | 32, 35, 38 | mpjaodan 961 |
. 2
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → ( gcd ‘if((2nd
‘𝑋) = 0, 𝑋, 〈(2nd
‘𝑋), ( mod
‘𝑋)〉)) = ( gcd
‘𝑋)) |
| 40 | 3, 39 | eqtrd 2777 |
1
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → ( gcd ‘(𝐸‘𝑋)) = ( gcd ‘𝑋)) |