Step | Hyp | Ref
| Expression |
1 | | gcdnncl 16448 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ โ) |
2 | 1 | nnsqcld 14207 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐)โ2) โ โ) |
3 | 2 | nncnd 12228 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐)โ2) โ โ) |
4 | 3 | mulridd 11231 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ gcd ๐)โ2) ยท 1) = ((๐ gcd ๐)โ2)) |
5 | | nnsqcl 14093 |
. . . . . . 7
โข (๐ โ โ โ (๐โ2) โ
โ) |
6 | 5 | nnzd 12585 |
. . . . . 6
โข (๐ โ โ โ (๐โ2) โ
โค) |
7 | 6 | adantr 482 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐โ2) โ
โค) |
8 | | nnsqcl 14093 |
. . . . . . 7
โข (๐ โ โ โ (๐โ2) โ
โ) |
9 | 8 | nnzd 12585 |
. . . . . 6
โข (๐ โ โ โ (๐โ2) โ
โค) |
10 | 9 | adantl 483 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐โ2) โ
โค) |
11 | | nnz 12579 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โค) |
12 | | nnz 12579 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โค) |
13 | | gcddvds 16444 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โง (๐ gcd ๐) โฅ ๐)) |
14 | 11, 12, 13 | syl2an 597 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) โฅ ๐ โง (๐ gcd ๐) โฅ ๐)) |
15 | 14 | simpld 496 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โฅ ๐) |
16 | 1 | nnzd 12585 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ โค) |
17 | 11 | adantr 482 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โค) |
18 | | dvdssqim 16496 |
. . . . . . 7
โข (((๐ gcd ๐) โ โค โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โ ((๐ gcd ๐)โ2) โฅ (๐โ2))) |
19 | 16, 17, 18 | syl2anc 585 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) โฅ ๐ โ ((๐ gcd ๐)โ2) โฅ (๐โ2))) |
20 | 15, 19 | mpd 15 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐)โ2) โฅ (๐โ2)) |
21 | 14 | simprd 497 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โฅ ๐) |
22 | 12 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โค) |
23 | | dvdssqim 16496 |
. . . . . . 7
โข (((๐ gcd ๐) โ โค โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โ ((๐ gcd ๐)โ2) โฅ (๐โ2))) |
24 | 16, 22, 23 | syl2anc 585 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) โฅ ๐ โ ((๐ gcd ๐)โ2) โฅ (๐โ2))) |
25 | 21, 24 | mpd 15 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐)โ2) โฅ (๐โ2)) |
26 | | gcddiv 16493 |
. . . . 5
โข ((((๐โ2) โ โค โง
(๐โ2) โ โค
โง ((๐ gcd ๐)โ2) โ โ) โง
(((๐ gcd ๐)โ2) โฅ (๐โ2) โง ((๐ gcd ๐)โ2) โฅ (๐โ2))) โ (((๐โ2) gcd (๐โ2)) / ((๐ gcd ๐)โ2)) = (((๐โ2) / ((๐ gcd ๐)โ2)) gcd ((๐โ2) / ((๐ gcd ๐)โ2)))) |
27 | 7, 10, 2, 20, 25, 26 | syl32anc 1379 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (((๐โ2) gcd (๐โ2)) / ((๐ gcd ๐)โ2)) = (((๐โ2) / ((๐ gcd ๐)โ2)) gcd ((๐โ2) / ((๐ gcd ๐)โ2)))) |
28 | | nncn 12220 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
29 | 28 | adantr 482 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
30 | 1 | nncnd 12228 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ โ) |
31 | 1 | nnne0d 12262 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ 0) |
32 | 29, 30, 31 | sqdivd 14124 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ / (๐ gcd ๐))โ2) = ((๐โ2) / ((๐ gcd ๐)โ2))) |
33 | | nncn 12220 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
34 | 33 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
35 | 34, 30, 31 | sqdivd 14124 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ / (๐ gcd ๐))โ2) = ((๐โ2) / ((๐ gcd ๐)โ2))) |
36 | 32, 35 | oveq12d 7427 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ / (๐ gcd ๐))โ2) gcd ((๐ / (๐ gcd ๐))โ2)) = (((๐โ2) / ((๐ gcd ๐)โ2)) gcd ((๐โ2) / ((๐ gcd ๐)โ2)))) |
37 | | gcddiv 16493 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค โง (๐ gcd ๐) โ โ) โง ((๐ gcd ๐) โฅ ๐ โง (๐ gcd ๐) โฅ ๐)) โ ((๐ gcd ๐) / (๐ gcd ๐)) = ((๐ / (๐ gcd ๐)) gcd (๐ / (๐ gcd ๐)))) |
38 | 17, 22, 1, 14, 37 | syl31anc 1374 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) / (๐ gcd ๐)) = ((๐ / (๐ gcd ๐)) gcd (๐ / (๐ gcd ๐)))) |
39 | 30, 31 | dividd 11988 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) / (๐ gcd ๐)) = 1) |
40 | 38, 39 | eqtr3d 2775 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ / (๐ gcd ๐)) gcd (๐ / (๐ gcd ๐))) = 1) |
41 | | dvdsval2 16200 |
. . . . . . . . 9
โข (((๐ gcd ๐) โ โค โง (๐ gcd ๐) โ 0 โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โ (๐ / (๐ gcd ๐)) โ โค)) |
42 | 16, 31, 17, 41 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) โฅ ๐ โ (๐ / (๐ gcd ๐)) โ โค)) |
43 | 15, 42 | mpbid 231 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ / (๐ gcd ๐)) โ โค) |
44 | | nnre 12219 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
45 | 44 | adantr 482 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
46 | 1 | nnred 12227 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ โ) |
47 | | nngt0 12243 |
. . . . . . . . 9
โข (๐ โ โ โ 0 <
๐) |
48 | 47 | adantr 482 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ 0 <
๐) |
49 | 1 | nngt0d 12261 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ 0 <
(๐ gcd ๐)) |
50 | 45, 46, 48, 49 | divgt0d 12149 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ 0 <
(๐ / (๐ gcd ๐))) |
51 | | elnnz 12568 |
. . . . . . 7
โข ((๐ / (๐ gcd ๐)) โ โ โ ((๐ / (๐ gcd ๐)) โ โค โง 0 < (๐ / (๐ gcd ๐)))) |
52 | 43, 50, 51 | sylanbrc 584 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ / (๐ gcd ๐)) โ โ) |
53 | | dvdsval2 16200 |
. . . . . . . . 9
โข (((๐ gcd ๐) โ โค โง (๐ gcd ๐) โ 0 โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โ (๐ / (๐ gcd ๐)) โ โค)) |
54 | 16, 31, 22, 53 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) โฅ ๐ โ (๐ / (๐ gcd ๐)) โ โค)) |
55 | 21, 54 | mpbid 231 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ / (๐ gcd ๐)) โ โค) |
56 | | nnre 12219 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
57 | 56 | adantl 483 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
58 | | nngt0 12243 |
. . . . . . . . 9
โข (๐ โ โ โ 0 <
๐) |
59 | 58 | adantl 483 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ 0 <
๐) |
60 | 57, 46, 59, 49 | divgt0d 12149 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ 0 <
(๐ / (๐ gcd ๐))) |
61 | | elnnz 12568 |
. . . . . . 7
โข ((๐ / (๐ gcd ๐)) โ โ โ ((๐ / (๐ gcd ๐)) โ โค โง 0 < (๐ / (๐ gcd ๐)))) |
62 | 55, 60, 61 | sylanbrc 584 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ / (๐ gcd ๐)) โ โ) |
63 | | 2nn 12285 |
. . . . . . 7
โข 2 โ
โ |
64 | | rppwr 16501 |
. . . . . . 7
โข (((๐ / (๐ gcd ๐)) โ โ โง (๐ / (๐ gcd ๐)) โ โ โง 2 โ โ)
โ (((๐ / (๐ gcd ๐)) gcd (๐ / (๐ gcd ๐))) = 1 โ (((๐ / (๐ gcd ๐))โ2) gcd ((๐ / (๐ gcd ๐))โ2)) = 1)) |
65 | 63, 64 | mp3an3 1451 |
. . . . . 6
โข (((๐ / (๐ gcd ๐)) โ โ โง (๐ / (๐ gcd ๐)) โ โ) โ (((๐ / (๐ gcd ๐)) gcd (๐ / (๐ gcd ๐))) = 1 โ (((๐ / (๐ gcd ๐))โ2) gcd ((๐ / (๐ gcd ๐))โ2)) = 1)) |
66 | 52, 62, 65 | syl2anc 585 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ / (๐ gcd ๐)) gcd (๐ / (๐ gcd ๐))) = 1 โ (((๐ / (๐ gcd ๐))โ2) gcd ((๐ / (๐ gcd ๐))โ2)) = 1)) |
67 | 40, 66 | mpd 15 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ / (๐ gcd ๐))โ2) gcd ((๐ / (๐ gcd ๐))โ2)) = 1) |
68 | 27, 36, 67 | 3eqtr2d 2779 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (((๐โ2) gcd (๐โ2)) / ((๐ gcd ๐)โ2)) = 1) |
69 | 6, 9 | anim12i 614 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐โ2) โ โค โง
(๐โ2) โ
โค)) |
70 | 5 | nnne0d 12262 |
. . . . . . . . 9
โข (๐ โ โ โ (๐โ2) โ
0) |
71 | 70 | neneqd 2946 |
. . . . . . . 8
โข (๐ โ โ โ ยฌ
(๐โ2) =
0) |
72 | 71 | intnanrd 491 |
. . . . . . 7
โข (๐ โ โ โ ยฌ
((๐โ2) = 0 โง
(๐โ2) =
0)) |
73 | 72 | adantr 482 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ยฌ
((๐โ2) = 0 โง
(๐โ2) =
0)) |
74 | | gcdn0cl 16443 |
. . . . . 6
โข ((((๐โ2) โ โค โง
(๐โ2) โ โค)
โง ยฌ ((๐โ2) = 0
โง (๐โ2) = 0))
โ ((๐โ2) gcd
(๐โ2)) โ
โ) |
75 | 69, 73, 74 | syl2anc 585 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ((๐โ2) gcd (๐โ2)) โ โ) |
76 | 75 | nncnd 12228 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ ((๐โ2) gcd (๐โ2)) โ โ) |
77 | 2 | nnne0d 12262 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐)โ2) โ 0) |
78 | | ax-1cn 11168 |
. . . . 5
โข 1 โ
โ |
79 | | divmul 11875 |
. . . . 5
โข ((((๐โ2) gcd (๐โ2)) โ โ โง 1 โ
โ โง (((๐ gcd
๐)โ2) โ โ
โง ((๐ gcd ๐)โ2) โ 0)) โ
((((๐โ2) gcd (๐โ2)) / ((๐ gcd ๐)โ2)) = 1 โ (((๐ gcd ๐)โ2) ยท 1) = ((๐โ2) gcd (๐โ2)))) |
80 | 78, 79 | mp3an2 1450 |
. . . 4
โข ((((๐โ2) gcd (๐โ2)) โ โ โง (((๐ gcd ๐)โ2) โ โ โง ((๐ gcd ๐)โ2) โ 0)) โ ((((๐โ2) gcd (๐โ2)) / ((๐ gcd ๐)โ2)) = 1 โ (((๐ gcd ๐)โ2) ยท 1) = ((๐โ2) gcd (๐โ2)))) |
81 | 76, 3, 77, 80 | syl12anc 836 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ
((((๐โ2) gcd (๐โ2)) / ((๐ gcd ๐)โ2)) = 1 โ (((๐ gcd ๐)โ2) ยท 1) = ((๐โ2) gcd (๐โ2)))) |
82 | 68, 81 | mpbid 231 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ gcd ๐)โ2) ยท 1) = ((๐โ2) gcd (๐โ2))) |
83 | 4, 82 | eqtr3d 2775 |
1
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐)โ2) = ((๐โ2) gcd (๐โ2))) |