Step | Hyp | Ref
| Expression |
1 | | oveq2 5883 |
. . . . . 6
โข (๐ = 1 โ (๐ ยท ๐) = (๐ ยท 1)) |
2 | 1 | oveq2d 5891 |
. . . . 5
โข (๐ = 1 โ (๐ gcd (๐ ยท ๐)) = (๐ gcd (๐ ยท 1))) |
3 | 2 | eqeq1d 2186 |
. . . 4
โข (๐ = 1 โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท 1)) = ๐)) |
4 | 3 | imbi2d 230 |
. . 3
โข (๐ = 1 โ ((๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐) โ (๐ โ โ โ (๐ gcd (๐ ยท 1)) = ๐))) |
5 | | oveq2 5883 |
. . . . . 6
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
6 | 5 | oveq2d 5891 |
. . . . 5
โข (๐ = ๐ โ (๐ gcd (๐ ยท ๐)) = (๐ gcd (๐ ยท ๐))) |
7 | 6 | eqeq1d 2186 |
. . . 4
โข (๐ = ๐ โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท ๐)) = ๐)) |
8 | 7 | imbi2d 230 |
. . 3
โข (๐ = ๐ โ ((๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐) โ (๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐))) |
9 | | oveq2 5883 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ ยท ๐) = (๐ ยท (๐ + 1))) |
10 | 9 | oveq2d 5891 |
. . . . 5
โข (๐ = (๐ + 1) โ (๐ gcd (๐ ยท ๐)) = (๐ gcd (๐ ยท (๐ + 1)))) |
11 | 10 | eqeq1d 2186 |
. . . 4
โข (๐ = (๐ + 1) โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท (๐ + 1))) = ๐)) |
12 | 11 | imbi2d 230 |
. . 3
โข (๐ = (๐ + 1) โ ((๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐) โ (๐ โ โ โ (๐ gcd (๐ ยท (๐ + 1))) = ๐))) |
13 | | oveq2 5883 |
. . . . . 6
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
14 | 13 | oveq2d 5891 |
. . . . 5
โข (๐ = ๐ โ (๐ gcd (๐ ยท ๐)) = (๐ gcd (๐ ยท ๐))) |
15 | 14 | eqeq1d 2186 |
. . . 4
โข (๐ = ๐ โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท ๐)) = ๐)) |
16 | 15 | imbi2d 230 |
. . 3
โข (๐ = ๐ โ ((๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐) โ (๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐))) |
17 | | nncn 8927 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
18 | 17 | mulridd 7974 |
. . . . 5
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
19 | 18 | oveq2d 5891 |
. . . 4
โข (๐ โ โ โ (๐ gcd (๐ ยท 1)) = (๐ gcd ๐)) |
20 | | nnz 9272 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
21 | | gcdid 11987 |
. . . . . 6
โข (๐ โ โค โ (๐ gcd ๐) = (absโ๐)) |
22 | 20, 21 | syl 14 |
. . . . 5
โข (๐ โ โ โ (๐ gcd ๐) = (absโ๐)) |
23 | | nnre 8926 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
24 | | nnnn0 9183 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ0) |
25 | 24 | nn0ge0d 9232 |
. . . . . 6
โข (๐ โ โ โ 0 โค
๐) |
26 | 23, 25 | absidd 11176 |
. . . . 5
โข (๐ โ โ โ
(absโ๐) = ๐) |
27 | 22, 26 | eqtrd 2210 |
. . . 4
โข (๐ โ โ โ (๐ gcd ๐) = ๐) |
28 | 19, 27 | eqtrd 2210 |
. . 3
โข (๐ โ โ โ (๐ gcd (๐ ยท 1)) = ๐) |
29 | 20 | adantr 276 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โค) |
30 | | nnz 9272 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
31 | | zmulcl 9306 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ ยท ๐) โ โค) |
32 | 20, 30, 31 | syl2an 289 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โค) |
33 | | 1z 9279 |
. . . . . . . . . 10
โข 1 โ
โค |
34 | | gcdaddm 11985 |
. . . . . . . . . 10
โข ((1
โ โค โง ๐
โ โค โง (๐
ยท ๐) โ โค)
โ (๐ gcd (๐ ยท ๐)) = (๐ gcd ((๐ ยท ๐) + (1 ยท ๐)))) |
35 | 33, 34 | mp3an1 1324 |
. . . . . . . . 9
โข ((๐ โ โค โง (๐ ยท ๐) โ โค) โ (๐ gcd (๐ ยท ๐)) = (๐ gcd ((๐ ยท ๐) + (1 ยท ๐)))) |
36 | 29, 32, 35 | syl2anc 411 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd (๐ ยท ๐)) = (๐ gcd ((๐ ยท ๐) + (1 ยท ๐)))) |
37 | | nncn 8927 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
38 | | ax-1cn 7904 |
. . . . . . . . . . . 12
โข 1 โ
โ |
39 | | adddi 7943 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ โง 1 โ
โ) โ (๐ ยท
(๐ + 1)) = ((๐ ยท ๐) + (๐ ยท 1))) |
40 | 38, 39 | mp3an3 1326 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + (๐ ยท 1))) |
41 | | mulcom 7940 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง 1 โ
โ) โ (๐ ยท
1) = (1 ยท ๐)) |
42 | 38, 41 | mpan2 425 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ ยท 1) = (1 ยท ๐)) |
43 | 42 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท 1) = (1 ยท ๐)) |
44 | 43 | oveq2d 5891 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) + (๐ ยท 1)) = ((๐ ยท ๐) + (1 ยท ๐))) |
45 | 40, 44 | eqtrd 2210 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + (1 ยท ๐))) |
46 | 17, 37, 45 | syl2an 289 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + (1 ยท ๐))) |
47 | 46 | oveq2d 5891 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd (๐ ยท (๐ + 1))) = (๐ gcd ((๐ ยท ๐) + (1 ยท ๐)))) |
48 | 36, 47 | eqtr4d 2213 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd (๐ ยท ๐)) = (๐ gcd (๐ ยท (๐ + 1)))) |
49 | 48 | eqeq1d 2186 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท (๐ + 1))) = ๐)) |
50 | 49 | biimpd 144 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท (๐ + 1))) = ๐)) |
51 | 50 | expcom 116 |
. . . 4
โข (๐ โ โ โ (๐ โ โ โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท (๐ + 1))) = ๐))) |
52 | 51 | a2d 26 |
. . 3
โข (๐ โ โ โ ((๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐) โ (๐ โ โ โ (๐ gcd (๐ ยท (๐ + 1))) = ๐))) |
53 | 4, 8, 12, 16, 28, 52 | nnind 8935 |
. 2
โข (๐ โ โ โ (๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐)) |
54 | 53 | impcom 125 |
1
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd (๐ ยท ๐)) = ๐) |