Step | Hyp | Ref
| Expression |
1 | | oveq2 7311 |
. . . . . 6
โข (๐ = 1 โ (๐ ยท ๐) = (๐ ยท 1)) |
2 | 1 | oveq2d 7319 |
. . . . 5
โข (๐ = 1 โ (๐ gcd (๐ ยท ๐)) = (๐ gcd (๐ ยท 1))) |
3 | 2 | eqeq1d 2738 |
. . . 4
โข (๐ = 1 โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท 1)) = ๐)) |
4 | 3 | imbi2d 342 |
. . 3
โข (๐ = 1 โ ((๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐) โ (๐ โ โ โ (๐ gcd (๐ ยท 1)) = ๐))) |
5 | | oveq2 7311 |
. . . . . 6
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
6 | 5 | oveq2d 7319 |
. . . . 5
โข (๐ = ๐ โ (๐ gcd (๐ ยท ๐)) = (๐ gcd (๐ ยท ๐))) |
7 | 6 | eqeq1d 2738 |
. . . 4
โข (๐ = ๐ โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท ๐)) = ๐)) |
8 | 7 | imbi2d 342 |
. . 3
โข (๐ = ๐ โ ((๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐) โ (๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐))) |
9 | | oveq2 7311 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ ยท ๐) = (๐ ยท (๐ + 1))) |
10 | 9 | oveq2d 7319 |
. . . . 5
โข (๐ = (๐ + 1) โ (๐ gcd (๐ ยท ๐)) = (๐ gcd (๐ ยท (๐ + 1)))) |
11 | 10 | eqeq1d 2738 |
. . . 4
โข (๐ = (๐ + 1) โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท (๐ + 1))) = ๐)) |
12 | 11 | imbi2d 342 |
. . 3
โข (๐ = (๐ + 1) โ ((๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐) โ (๐ โ โ โ (๐ gcd (๐ ยท (๐ + 1))) = ๐))) |
13 | | oveq2 7311 |
. . . . . 6
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
14 | 13 | oveq2d 7319 |
. . . . 5
โข (๐ = ๐ โ (๐ gcd (๐ ยท ๐)) = (๐ gcd (๐ ยท ๐))) |
15 | 14 | eqeq1d 2738 |
. . . 4
โข (๐ = ๐ โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท ๐)) = ๐)) |
16 | 15 | imbi2d 342 |
. . 3
โข (๐ = ๐ โ ((๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐) โ (๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐))) |
17 | | nncn 12023 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
18 | 17 | mulid1d 11034 |
. . . . 5
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
19 | 18 | oveq2d 7319 |
. . . 4
โข (๐ โ โ โ (๐ gcd (๐ ยท 1)) = (๐ gcd ๐)) |
20 | | nnz 12384 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
21 | | gcdid 16275 |
. . . . . 6
โข (๐ โ โค โ (๐ gcd ๐) = (absโ๐)) |
22 | 20, 21 | syl 17 |
. . . . 5
โข (๐ โ โ โ (๐ gcd ๐) = (absโ๐)) |
23 | | nnre 12022 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
24 | | nnnn0 12282 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ0) |
25 | 24 | nn0ge0d 12338 |
. . . . . 6
โข (๐ โ โ โ 0 โค
๐) |
26 | 23, 25 | absidd 15175 |
. . . . 5
โข (๐ โ โ โ
(absโ๐) = ๐) |
27 | 22, 26 | eqtrd 2776 |
. . . 4
โข (๐ โ โ โ (๐ gcd ๐) = ๐) |
28 | 19, 27 | eqtrd 2776 |
. . 3
โข (๐ โ โ โ (๐ gcd (๐ ยท 1)) = ๐) |
29 | | 1z 12392 |
. . . . . . . . 9
โข 1 โ
โค |
30 | | nnz 12384 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
31 | | zmulcl 12411 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ ยท ๐) โ โค) |
32 | 20, 30, 31 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โค) |
33 | | gcdaddm 16273 |
. . . . . . . . 9
โข ((1
โ โค โง ๐
โ โค โง (๐
ยท ๐) โ โค)
โ (๐ gcd (๐ ยท ๐)) = (๐ gcd ((๐ ยท ๐) + (1 ยท ๐)))) |
34 | 29, 20, 32, 33 | mp3an2ani 1468 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd (๐ ยท ๐)) = (๐ gcd ((๐ ยท ๐) + (1 ยท ๐)))) |
35 | | nncn 12023 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
36 | | ax-1cn 10971 |
. . . . . . . . . . . 12
โข 1 โ
โ |
37 | | adddi 11002 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ โง 1 โ
โ) โ (๐ ยท
(๐ + 1)) = ((๐ ยท ๐) + (๐ ยท 1))) |
38 | 36, 37 | mp3an3 1450 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + (๐ ยท 1))) |
39 | | mulcom 10999 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง 1 โ
โ) โ (๐ ยท
1) = (1 ยท ๐)) |
40 | 36, 39 | mpan2 689 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ ยท 1) = (1 ยท ๐)) |
41 | 40 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท 1) = (1 ยท ๐)) |
42 | 41 | oveq2d 7319 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) + (๐ ยท 1)) = ((๐ ยท ๐) + (1 ยท ๐))) |
43 | 38, 42 | eqtrd 2776 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + (1 ยท ๐))) |
44 | 17, 35, 43 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + (1 ยท ๐))) |
45 | 44 | oveq2d 7319 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd (๐ ยท (๐ + 1))) = (๐ gcd ((๐ ยท ๐) + (1 ยท ๐)))) |
46 | 34, 45 | eqtr4d 2779 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd (๐ ยท ๐)) = (๐ gcd (๐ ยท (๐ + 1)))) |
47 | 46 | eqeq1d 2738 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท (๐ + 1))) = ๐)) |
48 | 47 | biimpd 228 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท (๐ + 1))) = ๐)) |
49 | 48 | expcom 415 |
. . . 4
โข (๐ โ โ โ (๐ โ โ โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท (๐ + 1))) = ๐))) |
50 | 49 | a2d 29 |
. . 3
โข (๐ โ โ โ ((๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐) โ (๐ โ โ โ (๐ gcd (๐ ยท (๐ + 1))) = ๐))) |
51 | 4, 8, 12, 16, 28, 50 | nnind 12033 |
. 2
โข (๐ โ โ โ (๐ โ โ โ (๐ gcd (๐ ยท ๐)) = ๐)) |
52 | 51 | impcom 409 |
1
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd (๐ ยท ๐)) = ๐) |