Step | Hyp | Ref
| Expression |
1 | | oveq2 7417 |
. . . . . . . 8
โข (๐ = 1 โ (๐ดโ๐) = (๐ดโ1)) |
2 | 1 | oveq1d 7424 |
. . . . . . 7
โข (๐ = 1 โ ((๐ดโ๐) gcd ๐ต) = ((๐ดโ1) gcd ๐ต)) |
3 | 2 | eqeq1d 2735 |
. . . . . 6
โข (๐ = 1 โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ1) gcd ๐ต) = 1)) |
4 | 3 | imbi2d 341 |
. . . . 5
โข (๐ = 1 โ ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1) โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ1) gcd ๐ต) = 1))) |
5 | | oveq2 7417 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
6 | 5 | oveq1d 7424 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) gcd ๐ต) = ((๐ดโ๐) gcd ๐ต)) |
7 | 6 | eqeq1d 2735 |
. . . . . 6
โข (๐ = ๐ โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1)) |
8 | 7 | imbi2d 341 |
. . . . 5
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1) โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1))) |
9 | | oveq2 7417 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
10 | 9 | oveq1d 7424 |
. . . . . . 7
โข (๐ = (๐ + 1) โ ((๐ดโ๐) gcd ๐ต) = ((๐ดโ(๐ + 1)) gcd ๐ต)) |
11 | 10 | eqeq1d 2735 |
. . . . . 6
โข (๐ = (๐ + 1) โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1)) |
12 | 11 | imbi2d 341 |
. . . . 5
โข (๐ = (๐ + 1) โ ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1) โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1))) |
13 | | oveq2 7417 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
14 | 13 | oveq1d 7424 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) gcd ๐ต) = ((๐ดโ๐) gcd ๐ต)) |
15 | 14 | eqeq1d 2735 |
. . . . . 6
โข (๐ = ๐ โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1)) |
16 | 15 | imbi2d 341 |
. . . . 5
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1) โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1))) |
17 | | nncn 12220 |
. . . . . . . . . 10
โข (๐ด โ โ โ ๐ด โ
โ) |
18 | 17 | exp1d 14106 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐ดโ1) = ๐ด) |
19 | 18 | oveq1d 7424 |
. . . . . . . 8
โข (๐ด โ โ โ ((๐ดโ1) gcd ๐ต) = (๐ด gcd ๐ต)) |
20 | 19 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ1) gcd ๐ต) = (๐ด gcd ๐ต)) |
21 | 20 | eqeq1d 2735 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ1) gcd ๐ต) = 1 โ (๐ด gcd ๐ต) = 1)) |
22 | 21 | biimpar 479 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ1) gcd ๐ต) = 1) |
23 | | df-3an 1090 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ((๐ด โ โ โง ๐ต โ โ) โง ๐ โ
โ)) |
24 | | simpl1 1192 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ๐ด โ โ) |
25 | 24 | nncnd 12228 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ๐ด โ โ) |
26 | | simpl3 1194 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ๐ โ โ) |
27 | 26 | nnnn0d 12532 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ๐ โ โ0) |
28 | 25, 27 | expp1d 14112 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
29 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ๐ด โ
โ) |
30 | | nnnn0 12479 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ ๐ โ
โ0) |
31 | 30 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ๐ โ
โ0) |
32 | 29, 31 | nnexpcld 14208 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ (๐ดโ๐) โ โ) |
33 | 32 | nnzd 12585 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ (๐ดโ๐) โ โค) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ๐) โ โค) |
35 | 34 | zcnd 12667 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ๐) โ โ) |
36 | 35, 25 | mulcomd 11235 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) ยท ๐ด) = (๐ด ยท (๐ดโ๐))) |
37 | 28, 36 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ(๐ + 1)) = (๐ด ยท (๐ดโ๐))) |
38 | 37 | oveq2d 7425 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ต gcd (๐ดโ(๐ + 1))) = (๐ต gcd (๐ด ยท (๐ดโ๐)))) |
39 | | simpl2 1193 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ๐ต โ โ) |
40 | 32 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ๐) โ โ) |
41 | | nnz 12579 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ โ โ ๐ด โ
โค) |
42 | 41 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ๐ด โ
โค) |
43 | | nnz 12579 |
. . . . . . . . . . . . . . . . . 18
โข (๐ต โ โ โ ๐ต โ
โค) |
44 | 43 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ๐ต โ
โค) |
45 | 42, 44 | gcdcomd 16455 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ (๐ด gcd ๐ต) = (๐ต gcd ๐ด)) |
46 | 45 | eqeq1d 2735 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ((๐ด gcd ๐ต) = 1 โ (๐ต gcd ๐ด) = 1)) |
47 | 46 | biimpa 478 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ต gcd ๐ด) = 1) |
48 | | rpmulgcd 16498 |
. . . . . . . . . . . . . 14
โข (((๐ต โ โ โง ๐ด โ โ โง (๐ดโ๐) โ โ) โง (๐ต gcd ๐ด) = 1) โ (๐ต gcd (๐ด ยท (๐ดโ๐))) = (๐ต gcd (๐ดโ๐))) |
49 | 39, 24, 40, 47, 48 | syl31anc 1374 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ต gcd (๐ด ยท (๐ดโ๐))) = (๐ต gcd (๐ดโ๐))) |
50 | 38, 49 | eqtrd 2773 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ต gcd (๐ดโ(๐ + 1))) = (๐ต gcd (๐ดโ๐))) |
51 | | peano2nn 12224 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ (๐ + 1) โ
โ) |
52 | 51 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ (๐ + 1) โ
โ) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ + 1) โ โ) |
54 | 53 | nnnn0d 12532 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ + 1) โ
โ0) |
55 | 24, 54 | nnexpcld 14208 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ(๐ + 1)) โ โ) |
56 | 55 | nnzd 12585 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ(๐ + 1)) โ โค) |
57 | 44 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ๐ต โ โค) |
58 | 56, 57 | gcdcomd 16455 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ(๐ + 1)) gcd ๐ต) = (๐ต gcd (๐ดโ(๐ + 1)))) |
59 | 34, 57 | gcdcomd 16455 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = (๐ต gcd (๐ดโ๐))) |
60 | 50, 58, 59 | 3eqtr4d 2783 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ(๐ + 1)) gcd ๐ต) = ((๐ดโ๐) gcd ๐ต)) |
61 | 60 | eqeq1d 2735 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (((๐ดโ(๐ + 1)) gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1)) |
62 | 61 | biimprd 247 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1)) |
63 | 23, 62 | sylanbr 583 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ) โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1)) |
64 | 63 | an32s 651 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โง ๐ โ โ) โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1)) |
65 | 64 | expcom 415 |
. . . . . 6
โข (๐ โ โ โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1))) |
66 | 65 | a2d 29 |
. . . . 5
โข (๐ โ โ โ ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1) โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1))) |
67 | 4, 8, 12, 16, 22, 66 | nnind 12230 |
. . . 4
โข (๐ โ โ โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1)) |
68 | 67 | expd 417 |
. . 3
โข (๐ โ โ โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1))) |
69 | 68 | com12 32 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ โ โ โ ((๐ด gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1))) |
70 | 69 | 3impia 1118 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ((๐ด gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1)) |