Step | Hyp | Ref
| Expression |
1 | | oveq2 5873 |
. . . . . . . 8
โข (๐ = 1 โ (๐ดโ๐) = (๐ดโ1)) |
2 | 1 | oveq1d 5880 |
. . . . . . 7
โข (๐ = 1 โ ((๐ดโ๐) gcd ๐ต) = ((๐ดโ1) gcd ๐ต)) |
3 | 2 | eqeq1d 2184 |
. . . . . 6
โข (๐ = 1 โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ1) gcd ๐ต) = 1)) |
4 | 3 | imbi2d 230 |
. . . . 5
โข (๐ = 1 โ ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1) โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ1) gcd ๐ต) = 1))) |
5 | | oveq2 5873 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
6 | 5 | oveq1d 5880 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) gcd ๐ต) = ((๐ดโ๐) gcd ๐ต)) |
7 | 6 | eqeq1d 2184 |
. . . . . 6
โข (๐ = ๐ โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1)) |
8 | 7 | imbi2d 230 |
. . . . 5
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1) โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1))) |
9 | | oveq2 5873 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
10 | 9 | oveq1d 5880 |
. . . . . . 7
โข (๐ = (๐ + 1) โ ((๐ดโ๐) gcd ๐ต) = ((๐ดโ(๐ + 1)) gcd ๐ต)) |
11 | 10 | eqeq1d 2184 |
. . . . . 6
โข (๐ = (๐ + 1) โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1)) |
12 | 11 | imbi2d 230 |
. . . . 5
โข (๐ = (๐ + 1) โ ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1) โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1))) |
13 | | oveq2 5873 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
14 | 13 | oveq1d 5880 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ดโ๐) gcd ๐ต) = ((๐ดโ๐) gcd ๐ต)) |
15 | 14 | eqeq1d 2184 |
. . . . . 6
โข (๐ = ๐ โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1)) |
16 | 15 | imbi2d 230 |
. . . . 5
โข (๐ = ๐ โ ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1) โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1))) |
17 | | nncn 8898 |
. . . . . . . . . 10
โข (๐ด โ โ โ ๐ด โ
โ) |
18 | 17 | exp1d 10616 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐ดโ1) = ๐ด) |
19 | 18 | oveq1d 5880 |
. . . . . . . 8
โข (๐ด โ โ โ ((๐ดโ1) gcd ๐ต) = (๐ด gcd ๐ต)) |
20 | 19 | adantr 276 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ1) gcd ๐ต) = (๐ด gcd ๐ต)) |
21 | 20 | eqeq1d 2184 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ1) gcd ๐ต) = 1 โ (๐ด gcd ๐ต) = 1)) |
22 | 21 | biimpar 297 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ1) gcd ๐ต) = 1) |
23 | | df-3an 980 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ((๐ด โ โ โง ๐ต โ โ) โง ๐ โ
โ)) |
24 | | simpl1 1000 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ๐ด โ โ) |
25 | 24 | nncnd 8904 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ๐ด โ โ) |
26 | | simpl3 1002 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ๐ โ โ) |
27 | 26 | nnnn0d 9200 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ๐ โ โ0) |
28 | 25, 27 | expp1d 10622 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
29 | | simp1 997 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ๐ด โ
โ) |
30 | | nnnn0 9154 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ ๐ โ
โ0) |
31 | 30 | 3ad2ant3 1020 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ๐ โ
โ0) |
32 | 29, 31 | nnexpcld 10643 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ (๐ดโ๐) โ โ) |
33 | 32 | nnzd 9345 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ (๐ดโ๐) โ โค) |
34 | 33 | adantr 276 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ๐) โ โค) |
35 | 34 | zcnd 9347 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ๐) โ โ) |
36 | 35, 25 | mulcomd 7953 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) ยท ๐ด) = (๐ด ยท (๐ดโ๐))) |
37 | 28, 36 | eqtrd 2208 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ(๐ + 1)) = (๐ด ยท (๐ดโ๐))) |
38 | 37 | oveq2d 5881 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ต gcd (๐ดโ(๐ + 1))) = (๐ต gcd (๐ด ยท (๐ดโ๐)))) |
39 | | simpl2 1001 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ๐ต โ โ) |
40 | 32 | adantr 276 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ๐) โ โ) |
41 | | nnz 9243 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ โ โ ๐ด โ
โค) |
42 | 41 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ๐ด โ
โค) |
43 | | nnz 9243 |
. . . . . . . . . . . . . . . . . 18
โข (๐ต โ โ โ ๐ต โ
โค) |
44 | 43 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ๐ต โ
โค) |
45 | | gcdcom 11940 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด gcd ๐ต) = (๐ต gcd ๐ด)) |
46 | 42, 44, 45 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ (๐ด gcd ๐ต) = (๐ต gcd ๐ด)) |
47 | 46 | eqeq1d 2184 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ((๐ด gcd ๐ต) = 1 โ (๐ต gcd ๐ด) = 1)) |
48 | 47 | biimpa 296 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ต gcd ๐ด) = 1) |
49 | | rpmulgcd 11993 |
. . . . . . . . . . . . . 14
โข (((๐ต โ โ โง ๐ด โ โ โง (๐ดโ๐) โ โ) โง (๐ต gcd ๐ด) = 1) โ (๐ต gcd (๐ด ยท (๐ดโ๐))) = (๐ต gcd (๐ดโ๐))) |
50 | 39, 24, 40, 48, 49 | syl31anc 1241 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ต gcd (๐ด ยท (๐ดโ๐))) = (๐ต gcd (๐ดโ๐))) |
51 | 38, 50 | eqtrd 2208 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ต gcd (๐ดโ(๐ + 1))) = (๐ต gcd (๐ดโ๐))) |
52 | | peano2nn 8902 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ (๐ + 1) โ
โ) |
53 | 52 | 3ad2ant3 1020 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ (๐ + 1) โ
โ) |
54 | 53 | adantr 276 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ + 1) โ โ) |
55 | 54 | nnnn0d 9200 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ + 1) โ
โ0) |
56 | 24, 55 | nnexpcld 10643 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ(๐ + 1)) โ โ) |
57 | 56 | nnzd 9345 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (๐ดโ(๐ + 1)) โ โค) |
58 | 44 | adantr 276 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ๐ต โ โค) |
59 | | gcdcom 11940 |
. . . . . . . . . . . . 13
โข (((๐ดโ(๐ + 1)) โ โค โง ๐ต โ โค) โ ((๐ดโ(๐ + 1)) gcd ๐ต) = (๐ต gcd (๐ดโ(๐ + 1)))) |
60 | 57, 58, 59 | syl2anc 411 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ(๐ + 1)) gcd ๐ต) = (๐ต gcd (๐ดโ(๐ + 1)))) |
61 | | gcdcom 11940 |
. . . . . . . . . . . . 13
โข (((๐ดโ๐) โ โค โง ๐ต โ โค) โ ((๐ดโ๐) gcd ๐ต) = (๐ต gcd (๐ดโ๐))) |
62 | 34, 58, 61 | syl2anc 411 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = (๐ต gcd (๐ดโ๐))) |
63 | 51, 60, 62 | 3eqtr4d 2218 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ(๐ + 1)) gcd ๐ต) = ((๐ดโ๐) gcd ๐ต)) |
64 | 63 | eqeq1d 2184 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (((๐ดโ(๐ + 1)) gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1)) |
65 | 64 | biimprd 158 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1)) |
66 | 23, 65 | sylanbr 285 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ) โง ๐ โ โ) โง (๐ด gcd ๐ต) = 1) โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1)) |
67 | 66 | an32s 568 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โง ๐ โ โ) โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1)) |
68 | 67 | expcom 116 |
. . . . . 6
โข (๐ โ โ โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ (((๐ดโ๐) gcd ๐ต) = 1 โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1))) |
69 | 68 | a2d 26 |
. . . . 5
โข (๐ โ โ โ ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1) โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ(๐ + 1)) gcd ๐ต) = 1))) |
70 | 4, 8, 12, 16, 22, 69 | nnind 8906 |
. . . 4
โข (๐ โ โ โ (((๐ด โ โ โง ๐ต โ โ) โง (๐ด gcd ๐ต) = 1) โ ((๐ดโ๐) gcd ๐ต) = 1)) |
71 | 70 | expd 258 |
. . 3
โข (๐ โ โ โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1))) |
72 | 71 | com12 30 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ โ โ โ ((๐ด gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1))) |
73 | 72 | 3impia 1200 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ((๐ด gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1)) |