Step | Hyp | Ref
| Expression |
1 | | nn0uz 11598 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
2 | | eucalg.2 |
. . . . . . . 8
⊢ 𝑅 = seq0((𝐸 ∘ 1st ),
(ℕ0 × {𝐴})) |
3 | | 0zd 11266 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 0 ∈ ℤ) |
4 | | eucalg.3 |
. . . . . . . . 9
⊢ 𝐴 = 〈𝑀, 𝑁〉 |
5 | | opelxpi 5072 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 〈𝑀, 𝑁〉 ∈ (ℕ0 ×
ℕ0)) |
6 | 4, 5 | syl5eqel 2692 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝐴 ∈ (ℕ0 ×
ℕ0)) |
7 | | eucalgval.1 |
. . . . . . . . . 10
⊢ 𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0
↦ if(𝑦 = 0,
〈𝑥, 𝑦〉, 〈𝑦, (𝑥 mod 𝑦)〉)) |
8 | 7 | eucalgf 15134 |
. . . . . . . . 9
⊢ 𝐸:(ℕ0 ×
ℕ0)⟶(ℕ0 ×
ℕ0) |
9 | 8 | a1i 11 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝐸:(ℕ0 ×
ℕ0)⟶(ℕ0 ×
ℕ0)) |
10 | 1, 2, 3, 6, 9 | algrf 15124 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑅:ℕ0⟶(ℕ0
× ℕ0)) |
11 | | ffvelrn 6265 |
. . . . . . 7
⊢ ((𝑅:ℕ0⟶(ℕ0
× ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝑅‘𝑁) ∈ (ℕ0 ×
ℕ0)) |
12 | 10, 11 | sylancom 698 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑅‘𝑁) ∈ (ℕ0 ×
ℕ0)) |
13 | | 1st2nd2 7096 |
. . . . . 6
⊢ ((𝑅‘𝑁) ∈ (ℕ0 ×
ℕ0) → (𝑅‘𝑁) = 〈(1st ‘(𝑅‘𝑁)), (2nd ‘(𝑅‘𝑁))〉) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑅‘𝑁) = 〈(1st ‘(𝑅‘𝑁)), (2nd ‘(𝑅‘𝑁))〉) |
15 | 14 | fveq2d 6107 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ( gcd ‘(𝑅‘𝑁)) = ( gcd ‘〈(1st
‘(𝑅‘𝑁)), (2nd
‘(𝑅‘𝑁))〉)) |
16 | | df-ov 6552 |
. . . 4
⊢
((1st ‘(𝑅‘𝑁)) gcd (2nd ‘(𝑅‘𝑁))) = ( gcd ‘〈(1st
‘(𝑅‘𝑁)), (2nd
‘(𝑅‘𝑁))〉) |
17 | 15, 16 | syl6eqr 2662 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ( gcd ‘(𝑅‘𝑁)) = ((1st ‘(𝑅‘𝑁)) gcd (2nd ‘(𝑅‘𝑁)))) |
18 | 4 | fveq2i 6106 |
. . . . . . . 8
⊢
(2nd ‘𝐴) = (2nd ‘〈𝑀, 𝑁〉) |
19 | | op2ndg 7072 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (2nd ‘〈𝑀, 𝑁〉) = 𝑁) |
20 | 18, 19 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (2nd ‘𝐴) = 𝑁) |
21 | 20 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑅‘(2nd ‘𝐴)) = (𝑅‘𝑁)) |
22 | 21 | fveq2d 6107 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (2nd ‘(𝑅‘(2nd ‘𝐴))) = (2nd
‘(𝑅‘𝑁))) |
23 | | xp2nd 7090 |
. . . . . . . . 9
⊢ (𝐴 ∈ (ℕ0
× ℕ0) → (2nd ‘𝐴) ∈
ℕ0) |
24 | 23 | nn0zd 11356 |
. . . . . . . 8
⊢ (𝐴 ∈ (ℕ0
× ℕ0) → (2nd ‘𝐴) ∈ ℤ) |
25 | | uzid 11578 |
. . . . . . . 8
⊢
((2nd ‘𝐴) ∈ ℤ → (2nd
‘𝐴) ∈
(ℤ≥‘(2nd ‘𝐴))) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ (ℕ0
× ℕ0) → (2nd ‘𝐴) ∈
(ℤ≥‘(2nd ‘𝐴))) |
27 | | eqid 2610 |
. . . . . . . 8
⊢
(2nd ‘𝐴) = (2nd ‘𝐴) |
28 | 7, 2, 27 | eucalgcvga 15137 |
. . . . . . 7
⊢ (𝐴 ∈ (ℕ0
× ℕ0) → ((2nd ‘𝐴) ∈
(ℤ≥‘(2nd ‘𝐴)) → (2nd ‘(𝑅‘(2nd
‘𝐴))) =
0)) |
29 | 26, 28 | mpd 15 |
. . . . . 6
⊢ (𝐴 ∈ (ℕ0
× ℕ0) → (2nd ‘(𝑅‘(2nd ‘𝐴))) = 0) |
30 | 6, 29 | syl 17 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (2nd ‘(𝑅‘(2nd ‘𝐴))) = 0) |
31 | 22, 30 | eqtr3d 2646 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (2nd ‘(𝑅‘𝑁)) = 0) |
32 | 31 | oveq2d 6565 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((1st ‘(𝑅‘𝑁)) gcd (2nd ‘(𝑅‘𝑁))) = ((1st ‘(𝑅‘𝑁)) gcd 0)) |
33 | | xp1st 7089 |
. . . 4
⊢ ((𝑅‘𝑁) ∈ (ℕ0 ×
ℕ0) → (1st ‘(𝑅‘𝑁)) ∈
ℕ0) |
34 | | nn0gcdid0 15080 |
. . . 4
⊢
((1st ‘(𝑅‘𝑁)) ∈ ℕ0 →
((1st ‘(𝑅‘𝑁)) gcd 0) = (1st ‘(𝑅‘𝑁))) |
35 | 12, 33, 34 | 3syl 18 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((1st ‘(𝑅‘𝑁)) gcd 0) = (1st ‘(𝑅‘𝑁))) |
36 | 17, 32, 35 | 3eqtrrd 2649 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (1st ‘(𝑅‘𝑁)) = ( gcd ‘(𝑅‘𝑁))) |
37 | | gcdf 15072 |
. . . . . . 7
⊢ gcd
:(ℤ × ℤ)⟶ℕ0 |
38 | | ffn 5958 |
. . . . . . 7
⊢ ( gcd
:(ℤ × ℤ)⟶ℕ0 → gcd Fn (ℤ
× ℤ)) |
39 | 37, 38 | ax-mp 5 |
. . . . . 6
⊢ gcd Fn
(ℤ × ℤ) |
40 | | nn0ssz 11275 |
. . . . . . 7
⊢
ℕ0 ⊆ ℤ |
41 | | xpss12 5148 |
. . . . . . 7
⊢
((ℕ0 ⊆ ℤ ∧ ℕ0 ⊆
ℤ) → (ℕ0 × ℕ0) ⊆
(ℤ × ℤ)) |
42 | 40, 40, 41 | mp2an 704 |
. . . . . 6
⊢
(ℕ0 × ℕ0) ⊆ (ℤ
× ℤ) |
43 | | fnssres 5918 |
. . . . . 6
⊢ (( gcd Fn
(ℤ × ℤ) ∧ (ℕ0 ×
ℕ0) ⊆ (ℤ × ℤ)) → ( gcd ↾
(ℕ0 × ℕ0)) Fn (ℕ0
× ℕ0)) |
44 | 39, 42, 43 | mp2an 704 |
. . . . 5
⊢ ( gcd
↾ (ℕ0 × ℕ0)) Fn
(ℕ0 × ℕ0) |
45 | 7 | eucalginv 15135 |
. . . . . 6
⊢ (𝑧 ∈ (ℕ0
× ℕ0) → ( gcd ‘(𝐸‘𝑧)) = ( gcd ‘𝑧)) |
46 | 8 | ffvelrni 6266 |
. . . . . . 7
⊢ (𝑧 ∈ (ℕ0
× ℕ0) → (𝐸‘𝑧) ∈ (ℕ0 ×
ℕ0)) |
47 | | fvres 6117 |
. . . . . . 7
⊢ ((𝐸‘𝑧) ∈ (ℕ0 ×
ℕ0) → (( gcd ↾ (ℕ0 ×
ℕ0))‘(𝐸‘𝑧)) = ( gcd ‘(𝐸‘𝑧))) |
48 | 46, 47 | syl 17 |
. . . . . 6
⊢ (𝑧 ∈ (ℕ0
× ℕ0) → (( gcd ↾ (ℕ0 ×
ℕ0))‘(𝐸‘𝑧)) = ( gcd ‘(𝐸‘𝑧))) |
49 | | fvres 6117 |
. . . . . 6
⊢ (𝑧 ∈ (ℕ0
× ℕ0) → (( gcd ↾ (ℕ0 ×
ℕ0))‘𝑧) = ( gcd ‘𝑧)) |
50 | 45, 48, 49 | 3eqtr4d 2654 |
. . . . 5
⊢ (𝑧 ∈ (ℕ0
× ℕ0) → (( gcd ↾ (ℕ0 ×
ℕ0))‘(𝐸‘𝑧)) = (( gcd ↾ (ℕ0
× ℕ0))‘𝑧)) |
51 | 2, 8, 44, 50 | alginv 15126 |
. . . 4
⊢ ((𝐴 ∈ (ℕ0
× ℕ0) ∧ 𝑁 ∈ ℕ0) → (( gcd
↾ (ℕ0 × ℕ0))‘(𝑅‘𝑁)) = (( gcd ↾ (ℕ0
× ℕ0))‘(𝑅‘0))) |
52 | 6, 51 | sylancom 698 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (( gcd ↾ (ℕ0 ×
ℕ0))‘(𝑅‘𝑁)) = (( gcd ↾ (ℕ0
× ℕ0))‘(𝑅‘0))) |
53 | | fvres 6117 |
. . . 4
⊢ ((𝑅‘𝑁) ∈ (ℕ0 ×
ℕ0) → (( gcd ↾ (ℕ0 ×
ℕ0))‘(𝑅‘𝑁)) = ( gcd ‘(𝑅‘𝑁))) |
54 | 12, 53 | syl 17 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (( gcd ↾ (ℕ0 ×
ℕ0))‘(𝑅‘𝑁)) = ( gcd ‘(𝑅‘𝑁))) |
55 | | 0nn0 11184 |
. . . . 5
⊢ 0 ∈
ℕ0 |
56 | | ffvelrn 6265 |
. . . . 5
⊢ ((𝑅:ℕ0⟶(ℕ0
× ℕ0) ∧ 0 ∈ ℕ0) → (𝑅‘0) ∈
(ℕ0 × ℕ0)) |
57 | 10, 55, 56 | sylancl 693 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑅‘0) ∈ (ℕ0
× ℕ0)) |
58 | | fvres 6117 |
. . . 4
⊢ ((𝑅‘0) ∈
(ℕ0 × ℕ0) → (( gcd ↾
(ℕ0 × ℕ0))‘(𝑅‘0)) = ( gcd ‘(𝑅‘0))) |
59 | 57, 58 | syl 17 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (( gcd ↾ (ℕ0 ×
ℕ0))‘(𝑅‘0)) = ( gcd ‘(𝑅‘0))) |
60 | 52, 54, 59 | 3eqtr3d 2652 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ( gcd ‘(𝑅‘𝑁)) = ( gcd ‘(𝑅‘0))) |
61 | 1, 2, 3, 6 | algr0 15123 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑅‘0) = 𝐴) |
62 | 61, 4 | syl6eq 2660 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑅‘0) = 〈𝑀, 𝑁〉) |
63 | 62 | fveq2d 6107 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ( gcd ‘(𝑅‘0)) = ( gcd ‘〈𝑀, 𝑁〉)) |
64 | | df-ov 6552 |
. . 3
⊢ (𝑀 gcd 𝑁) = ( gcd ‘〈𝑀, 𝑁〉) |
65 | 63, 64 | syl6eqr 2662 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ( gcd ‘(𝑅‘0)) = (𝑀 gcd 𝑁)) |
66 | 36, 60, 65 | 3eqtrd 2648 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (1st ‘(𝑅‘𝑁)) = (𝑀 gcd 𝑁)) |