Proof of Theorem eucalginv
Step | Hyp | Ref
| Expression |
1 | | eucalgval.1 |
. . . 4
⊢ 𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0
↦ if(𝑦 = 0,
〈𝑥, 𝑦〉, 〈𝑦, (𝑥 mod 𝑦)〉)) |
2 | 1 | eucalgval 12008 |
. . 3
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → (𝐸‘𝑋) = if((2nd ‘𝑋) = 0, 𝑋, 〈(2nd ‘𝑋), ( mod ‘𝑋)〉)) |
3 | 2 | fveq2d 5500 |
. 2
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → ( gcd ‘(𝐸‘𝑋)) = ( gcd ‘if((2nd
‘𝑋) = 0, 𝑋, 〈(2nd
‘𝑋), ( mod
‘𝑋)〉))) |
4 | | 1st2nd2 6154 |
. . . . . . . . 9
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → 𝑋 = 〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
5 | 4 | adantr 274 |
. . . . . . . 8
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → 𝑋 = 〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
6 | 5 | fveq2d 5500 |
. . . . . . 7
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( mod ‘𝑋) = ( mod
‘〈(1st ‘𝑋), (2nd ‘𝑋)〉)) |
7 | | df-ov 5856 |
. . . . . . 7
⊢
((1st ‘𝑋) mod (2nd ‘𝑋)) = ( mod
‘〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
8 | 6, 7 | eqtr4di 2221 |
. . . . . 6
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( mod ‘𝑋) = ((1st
‘𝑋) mod
(2nd ‘𝑋))) |
9 | 8 | oveq2d 5869 |
. . . . 5
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ((2nd
‘𝑋) gcd ( mod
‘𝑋)) =
((2nd ‘𝑋)
gcd ((1st ‘𝑋) mod (2nd ‘𝑋)))) |
10 | | nnz 9231 |
. . . . . . 7
⊢
((2nd ‘𝑋) ∈ ℕ → (2nd
‘𝑋) ∈
ℤ) |
11 | 10 | adantl 275 |
. . . . . 6
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → (2nd
‘𝑋) ∈
ℤ) |
12 | | xp1st 6144 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → (1st ‘𝑋) ∈
ℕ0) |
13 | 12 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → (1st
‘𝑋) ∈
ℕ0) |
14 | 13 | nn0zd 9332 |
. . . . . . . 8
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → (1st
‘𝑋) ∈
ℤ) |
15 | | zmodcl 10300 |
. . . . . . . 8
⊢
(((1st ‘𝑋) ∈ ℤ ∧ (2nd
‘𝑋) ∈ ℕ)
→ ((1st ‘𝑋) mod (2nd ‘𝑋)) ∈
ℕ0) |
16 | 14, 15 | sylancom 418 |
. . . . . . 7
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ((1st
‘𝑋) mod
(2nd ‘𝑋))
∈ ℕ0) |
17 | 16 | nn0zd 9332 |
. . . . . 6
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ((1st
‘𝑋) mod
(2nd ‘𝑋))
∈ ℤ) |
18 | | gcdcom 11928 |
. . . . . 6
⊢
(((2nd ‘𝑋) ∈ ℤ ∧ ((1st
‘𝑋) mod
(2nd ‘𝑋))
∈ ℤ) → ((2nd ‘𝑋) gcd ((1st ‘𝑋) mod (2nd
‘𝑋))) =
(((1st ‘𝑋)
mod (2nd ‘𝑋)) gcd (2nd ‘𝑋))) |
19 | 11, 17, 18 | syl2anc 409 |
. . . . 5
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ((2nd
‘𝑋) gcd
((1st ‘𝑋)
mod (2nd ‘𝑋))) = (((1st ‘𝑋) mod (2nd
‘𝑋)) gcd
(2nd ‘𝑋))) |
20 | | modgcd 11946 |
. . . . . 6
⊢
(((1st ‘𝑋) ∈ ℤ ∧ (2nd
‘𝑋) ∈ ℕ)
→ (((1st ‘𝑋) mod (2nd ‘𝑋)) gcd (2nd
‘𝑋)) =
((1st ‘𝑋)
gcd (2nd ‘𝑋))) |
21 | 14, 20 | sylancom 418 |
. . . . 5
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → (((1st
‘𝑋) mod
(2nd ‘𝑋))
gcd (2nd ‘𝑋)) = ((1st ‘𝑋) gcd (2nd
‘𝑋))) |
22 | 9, 19, 21 | 3eqtrd 2207 |
. . . 4
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ((2nd
‘𝑋) gcd ( mod
‘𝑋)) =
((1st ‘𝑋)
gcd (2nd ‘𝑋))) |
23 | | nnne0 8906 |
. . . . . . . . 9
⊢
((2nd ‘𝑋) ∈ ℕ → (2nd
‘𝑋) ≠
0) |
24 | 23 | adantl 275 |
. . . . . . . 8
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → (2nd
‘𝑋) ≠
0) |
25 | 24 | neneqd 2361 |
. . . . . . 7
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ¬
(2nd ‘𝑋) =
0) |
26 | 25 | iffalsed 3536 |
. . . . . 6
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → if((2nd
‘𝑋) = 0, 𝑋, 〈(2nd
‘𝑋), ( mod
‘𝑋)〉) =
〈(2nd ‘𝑋), ( mod ‘𝑋)〉) |
27 | 26 | fveq2d 5500 |
. . . . 5
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( gcd
‘if((2nd ‘𝑋) = 0, 𝑋, 〈(2nd ‘𝑋), ( mod ‘𝑋)〉)) = ( gcd
‘〈(2nd ‘𝑋), ( mod ‘𝑋)〉)) |
28 | | df-ov 5856 |
. . . . 5
⊢
((2nd ‘𝑋) gcd ( mod ‘𝑋)) = ( gcd ‘〈(2nd
‘𝑋), ( mod
‘𝑋)〉) |
29 | 27, 28 | eqtr4di 2221 |
. . . 4
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( gcd
‘if((2nd ‘𝑋) = 0, 𝑋, 〈(2nd ‘𝑋), ( mod ‘𝑋)〉)) = ((2nd
‘𝑋) gcd ( mod
‘𝑋))) |
30 | 5 | fveq2d 5500 |
. . . . 5
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( gcd ‘𝑋) = ( gcd
‘〈(1st ‘𝑋), (2nd ‘𝑋)〉)) |
31 | | df-ov 5856 |
. . . . 5
⊢
((1st ‘𝑋) gcd (2nd ‘𝑋)) = ( gcd
‘〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
32 | 30, 31 | eqtr4di 2221 |
. . . 4
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( gcd ‘𝑋) = ((1st
‘𝑋) gcd
(2nd ‘𝑋))) |
33 | 22, 29, 32 | 3eqtr4d 2213 |
. . 3
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) ∈ ℕ) → ( gcd
‘if((2nd ‘𝑋) = 0, 𝑋, 〈(2nd ‘𝑋), ( mod ‘𝑋)〉)) = ( gcd ‘𝑋)) |
34 | | iftrue 3531 |
. . . . 5
⊢
((2nd ‘𝑋) = 0 → if((2nd ‘𝑋) = 0, 𝑋, 〈(2nd ‘𝑋), ( mod ‘𝑋)〉) = 𝑋) |
35 | 34 | fveq2d 5500 |
. . . 4
⊢
((2nd ‘𝑋) = 0 → ( gcd ‘if((2nd
‘𝑋) = 0, 𝑋, 〈(2nd
‘𝑋), ( mod
‘𝑋)〉)) = ( gcd
‘𝑋)) |
36 | 35 | adantl 275 |
. . 3
⊢ ((𝑋 ∈ (ℕ0
× ℕ0) ∧ (2nd ‘𝑋) = 0) → ( gcd
‘if((2nd ‘𝑋) = 0, 𝑋, 〈(2nd ‘𝑋), ( mod ‘𝑋)〉)) = ( gcd ‘𝑋)) |
37 | | xp2nd 6145 |
. . . 4
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → (2nd ‘𝑋) ∈
ℕ0) |
38 | | elnn0 9137 |
. . . 4
⊢
((2nd ‘𝑋) ∈ ℕ0 ↔
((2nd ‘𝑋)
∈ ℕ ∨ (2nd ‘𝑋) = 0)) |
39 | 37, 38 | sylib 121 |
. . 3
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → ((2nd ‘𝑋) ∈ ℕ ∨ (2nd
‘𝑋) =
0)) |
40 | 33, 36, 39 | mpjaodan 793 |
. 2
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → ( gcd ‘if((2nd
‘𝑋) = 0, 𝑋, 〈(2nd
‘𝑋), ( mod
‘𝑋)〉)) = ( gcd
‘𝑋)) |
41 | 3, 40 | eqtrd 2203 |
1
⊢ (𝑋 ∈ (ℕ0
× ℕ0) → ( gcd ‘(𝐸‘𝑋)) = ( gcd ‘𝑋)) |