Step | Hyp | Ref
| Expression |
1 | | odadd1.2 |
. . . . . . . . 9
โข ๐ = (Baseโ๐บ) |
2 | | odadd1.1 |
. . . . . . . . 9
โข ๐ = (odโ๐บ) |
3 | 1, 2 | odcl 19319 |
. . . . . . . 8
โข (๐ด โ ๐ โ (๐โ๐ด) โ
โ0) |
4 | 3 | 3ad2ant2 1135 |
. . . . . . 7
โข ((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐โ๐ด) โ
โ0) |
5 | 4 | nn0zd 12526 |
. . . . . 6
โข ((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐โ๐ด) โ โค) |
6 | 1, 2 | odcl 19319 |
. . . . . . . 8
โข (๐ต โ ๐ โ (๐โ๐ต) โ
โ0) |
7 | 6 | 3ad2ant3 1136 |
. . . . . . 7
โข ((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐โ๐ต) โ
โ0) |
8 | 7 | nn0zd 12526 |
. . . . . 6
โข ((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐โ๐ต) โ โค) |
9 | 5, 8 | zmulcld 12614 |
. . . . 5
โข ((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โ ((๐โ๐ด) ยท (๐โ๐ต)) โ โค) |
10 | 9 | adantr 482 |
. . . 4
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) = 0) โ ((๐โ๐ด) ยท (๐โ๐ต)) โ โค) |
11 | | dvds0 16155 |
. . . 4
โข (((๐โ๐ด) ยท (๐โ๐ต)) โ โค โ ((๐โ๐ด) ยท (๐โ๐ต)) โฅ 0) |
12 | 10, 11 | syl 17 |
. . 3
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) = 0) โ ((๐โ๐ด) ยท (๐โ๐ต)) โฅ 0) |
13 | | simpr 486 |
. . . . . 6
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) = 0) โ ((๐โ๐ด) gcd (๐โ๐ต)) = 0) |
14 | 13 | sq0id 14099 |
. . . . 5
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) = 0) โ (((๐โ๐ด) gcd (๐โ๐ต))โ2) = 0) |
15 | 14 | oveq2d 7374 |
. . . 4
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) = 0) โ ((๐โ(๐ด + ๐ต)) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2)) = ((๐โ(๐ด + ๐ต)) ยท 0)) |
16 | | ablgrp 19568 |
. . . . . . . . . 10
โข (๐บ โ Abel โ ๐บ โ Grp) |
17 | | odadd1.3 |
. . . . . . . . . . 11
โข + =
(+gโ๐บ) |
18 | 1, 17 | grpcl 18757 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐ด + ๐ต) โ ๐) |
19 | 16, 18 | syl3an1 1164 |
. . . . . . . . 9
โข ((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐ด + ๐ต) โ ๐) |
20 | 1, 2 | odcl 19319 |
. . . . . . . . 9
โข ((๐ด + ๐ต) โ ๐ โ (๐โ(๐ด + ๐ต)) โ
โ0) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
โข ((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐โ(๐ด + ๐ต)) โ
โ0) |
22 | 21 | nn0zd 12526 |
. . . . . . 7
โข ((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐โ(๐ด + ๐ต)) โ โค) |
23 | 22 | adantr 482 |
. . . . . 6
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) = 0) โ (๐โ(๐ด + ๐ต)) โ โค) |
24 | 23 | zcnd 12609 |
. . . . 5
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) = 0) โ (๐โ(๐ด + ๐ต)) โ โ) |
25 | 24 | mul01d 11355 |
. . . 4
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) = 0) โ ((๐โ(๐ด + ๐ต)) ยท 0) = 0) |
26 | 15, 25 | eqtrd 2777 |
. . 3
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) = 0) โ ((๐โ(๐ด + ๐ต)) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2)) = 0) |
27 | 12, 26 | breqtrrd 5134 |
. 2
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) = 0) โ ((๐โ๐ด) ยท (๐โ๐ต)) โฅ ((๐โ(๐ด + ๐ต)) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2))) |
28 | 5 | adantr 482 |
. . . . . . . 8
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ๐ด) โ โค) |
29 | 8 | adantr 482 |
. . . . . . . 8
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ๐ต) โ โค) |
30 | 28, 29 | gcdcld 16389 |
. . . . . . 7
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ด) gcd (๐โ๐ต)) โ
โ0) |
31 | 30 | nn0cnd 12476 |
. . . . . 6
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ด) gcd (๐โ๐ต)) โ โ) |
32 | 31 | sqvald 14049 |
. . . . 5
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) gcd (๐โ๐ต))โ2) = (((๐โ๐ด) gcd (๐โ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) |
33 | 32 | oveq2d 7374 |
. . . 4
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2)) = ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) ยท (((๐โ๐ด) gcd (๐โ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต))))) |
34 | | gcddvds 16384 |
. . . . . . . . 9
โข (((๐โ๐ด) โ โค โง (๐โ๐ต) โ โค) โ (((๐โ๐ด) gcd (๐โ๐ต)) โฅ (๐โ๐ด) โง ((๐โ๐ด) gcd (๐โ๐ต)) โฅ (๐โ๐ต))) |
35 | 28, 29, 34 | syl2anc 585 |
. . . . . . . 8
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) gcd (๐โ๐ต)) โฅ (๐โ๐ด) โง ((๐โ๐ด) gcd (๐โ๐ต)) โฅ (๐โ๐ต))) |
36 | 35 | simpld 496 |
. . . . . . 7
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ด) gcd (๐โ๐ต)) โฅ (๐โ๐ด)) |
37 | 30 | nn0zd 12526 |
. . . . . . . 8
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ด) gcd (๐โ๐ต)) โ โค) |
38 | | simpr 486 |
. . . . . . . 8
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) |
39 | | dvdsval2 16140 |
. . . . . . . 8
โข ((((๐โ๐ด) gcd (๐โ๐ต)) โ โค โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0 โง (๐โ๐ด) โ โค) โ (((๐โ๐ด) gcd (๐โ๐ต)) โฅ (๐โ๐ด) โ ((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โค)) |
40 | 37, 38, 28, 39 | syl3anc 1372 |
. . . . . . 7
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) gcd (๐โ๐ต)) โฅ (๐โ๐ด) โ ((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โค)) |
41 | 36, 40 | mpbid 231 |
. . . . . 6
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โค) |
42 | 41 | zcnd 12609 |
. . . . 5
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โ) |
43 | 35 | simprd 497 |
. . . . . . 7
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ด) gcd (๐โ๐ต)) โฅ (๐โ๐ต)) |
44 | | dvdsval2 16140 |
. . . . . . . 8
โข ((((๐โ๐ด) gcd (๐โ๐ต)) โ โค โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0 โง (๐โ๐ต) โ โค) โ (((๐โ๐ด) gcd (๐โ๐ต)) โฅ (๐โ๐ต) โ ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โค)) |
45 | 37, 38, 29, 44 | syl3anc 1372 |
. . . . . . 7
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) gcd (๐โ๐ต)) โฅ (๐โ๐ต) โ ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โค)) |
46 | 43, 45 | mpbid 231 |
. . . . . 6
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โค) |
47 | 46 | zcnd 12609 |
. . . . 5
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โ) |
48 | 42, 31, 47, 31 | mul4d 11368 |
. . . 4
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) ยท (((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) = ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) ยท (((๐โ๐ด) gcd (๐โ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต))))) |
49 | 28 | zcnd 12609 |
. . . . . 6
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ๐ด) โ โ) |
50 | 49, 31, 38 | divcan1d 11933 |
. . . . 5
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) = (๐โ๐ด)) |
51 | 29 | zcnd 12609 |
. . . . . 6
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ๐ต) โ โ) |
52 | 51, 31, 38 | divcan1d 11933 |
. . . . 5
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) = (๐โ๐ต)) |
53 | 50, 52 | oveq12d 7376 |
. . . 4
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) ยท (((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) = ((๐โ๐ด) ยท (๐โ๐ต))) |
54 | 33, 48, 53 | 3eqtr2d 2783 |
. . 3
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2)) = ((๐โ๐ด) ยท (๐โ๐ต))) |
55 | 22 | adantr 482 |
. . . . . . . . . 10
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ(๐ด + ๐ต)) โ โค) |
56 | | dvdsmul2 16162 |
. . . . . . . . . 10
โข (((๐โ(๐ด + ๐ต)) โ โค โง (๐โ๐ด) โ โค) โ (๐โ๐ด) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))) |
57 | 55, 28, 56 | syl2anc 585 |
. . . . . . . . 9
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ๐ด) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))) |
58 | | simpl1 1192 |
. . . . . . . . . . . . 13
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ๐บ โ Abel) |
59 | 55, 29 | zmulcld 12614 |
. . . . . . . . . . . . 13
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ โค) |
60 | | simpl2 1193 |
. . . . . . . . . . . . 13
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ๐ด โ ๐) |
61 | | simpl3 1194 |
. . . . . . . . . . . . 13
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ๐ต โ ๐) |
62 | | eqid 2737 |
. . . . . . . . . . . . . 14
โข
(.gโ๐บ) = (.gโ๐บ) |
63 | 1, 62, 17 | mulgdi 19606 |
. . . . . . . . . . . . 13
โข ((๐บ โ Abel โง (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ โค โง ๐ด โ ๐ โง ๐ต โ ๐)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)(๐ด + ๐ต)) = ((((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) + (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ต))) |
64 | 58, 59, 60, 61, 63 | syl13anc 1373 |
. . . . . . . . . . . 12
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)(๐ด + ๐ต)) = ((((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) + (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ต))) |
65 | | dvdsmul2 16162 |
. . . . . . . . . . . . . . 15
โข (((๐โ(๐ด + ๐ต)) โ โค โง (๐โ๐ต) โ โค) โ (๐โ๐ต) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))) |
66 | 55, 29, 65 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ๐ต) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))) |
67 | 58, 16 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ๐บ โ Grp) |
68 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
โข
(0gโ๐บ) = (0gโ๐บ) |
69 | 1, 2, 62, 68 | oddvds 19330 |
. . . . . . . . . . . . . . 15
โข ((๐บ โ Grp โง ๐ต โ ๐ โง ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ โค) โ ((๐โ๐ต) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ต) = (0gโ๐บ))) |
70 | 67, 61, 59, 69 | syl3anc 1372 |
. . . . . . . . . . . . . 14
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ต) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ต) = (0gโ๐บ))) |
71 | 66, 70 | mpbid 231 |
. . . . . . . . . . . . 13
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ต) = (0gโ๐บ)) |
72 | 71 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) + (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ต)) = ((((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) + (0gโ๐บ))) |
73 | 64, 72 | eqtrd 2777 |
. . . . . . . . . . 11
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)(๐ด + ๐ต)) = ((((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) + (0gโ๐บ))) |
74 | | dvdsmul1 16161 |
. . . . . . . . . . . . 13
โข (((๐โ(๐ด + ๐ต)) โ โค โง (๐โ๐ต) โ โค) โ (๐โ(๐ด + ๐ต)) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))) |
75 | 55, 29, 74 | syl2anc 585 |
. . . . . . . . . . . 12
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ(๐ด + ๐ต)) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))) |
76 | 19 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐ด + ๐ต) โ ๐) |
77 | 1, 2, 62, 68 | oddvds 19330 |
. . . . . . . . . . . . 13
โข ((๐บ โ Grp โง (๐ด + ๐ต) โ ๐ โง ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ โค) โ ((๐โ(๐ด + ๐ต)) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)(๐ด + ๐ต)) = (0gโ๐บ))) |
78 | 67, 76, 59, 77 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ(๐ด + ๐ต)) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)(๐ด + ๐ต)) = (0gโ๐บ))) |
79 | 75, 78 | mpbid 231 |
. . . . . . . . . . 11
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)(๐ด + ๐ต)) = (0gโ๐บ)) |
80 | 1, 62 | mulgcl 18894 |
. . . . . . . . . . . . 13
โข ((๐บ โ Grp โง ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ โค โง ๐ด โ ๐) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) โ ๐) |
81 | 67, 59, 60, 80 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) โ ๐) |
82 | 1, 17, 68 | grprid 18782 |
. . . . . . . . . . . 12
โข ((๐บ โ Grp โง (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) โ ๐) โ ((((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) + (0gโ๐บ)) = (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด)) |
83 | 67, 81, 82 | syl2anc 585 |
. . . . . . . . . . 11
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) + (0gโ๐บ)) = (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด)) |
84 | 73, 79, 83 | 3eqtr3rd 2786 |
. . . . . . . . . 10
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) = (0gโ๐บ)) |
85 | 1, 2, 62, 68 | oddvds 19330 |
. . . . . . . . . . 11
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ โค) โ ((๐โ๐ด) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) = (0gโ๐บ))) |
86 | 67, 60, 59, 85 | syl3anc 1372 |
. . . . . . . . . 10
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ด) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))(.gโ๐บ)๐ด) = (0gโ๐บ))) |
87 | 84, 86 | mpbird 257 |
. . . . . . . . 9
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ๐ด) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))) |
88 | 55, 28 | zmulcld 12614 |
. . . . . . . . . 10
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ โค) |
89 | | dvdsgcd 16426 |
. . . . . . . . . 10
โข (((๐โ๐ด) โ โค โง ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ โค โง ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ โค) โ (((๐โ๐ด) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โง (๐โ๐ด) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))) โ (๐โ๐ด) โฅ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) gcd ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))))) |
90 | 28, 88, 59, 89 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โง (๐โ๐ด) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))) โ (๐โ๐ด) โฅ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) gcd ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))))) |
91 | 57, 87, 90 | mp2and 698 |
. . . . . . . 8
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ๐ด) โฅ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) gcd ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)))) |
92 | 21 | adantr 482 |
. . . . . . . . 9
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ(๐ด + ๐ต)) โ
โ0) |
93 | | mulgcd 16430 |
. . . . . . . . 9
โข (((๐โ(๐ด + ๐ต)) โ โ0 โง (๐โ๐ด) โ โค โง (๐โ๐ต) โ โค) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) gcd ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))) = ((๐โ(๐ด + ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) |
94 | 92, 28, 29, 93 | syl3anc 1372 |
. . . . . . . 8
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) gcd ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))) = ((๐โ(๐ด + ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) |
95 | 91, 94 | breqtrd 5132 |
. . . . . . 7
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ๐ด) โฅ ((๐โ(๐ด + ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) |
96 | 50, 95 | eqbrtrd 5128 |
. . . . . 6
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) โฅ ((๐โ(๐ด + ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) |
97 | | dvdsmulcr 16169 |
. . . . . . 7
โข ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โค โง (๐โ(๐ด + ๐ต)) โ โค โง (((๐โ๐ด) gcd (๐โ๐ต)) โ โค โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0)) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) โฅ ((๐โ(๐ด + ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต))) โ ((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) โฅ (๐โ(๐ด + ๐ต)))) |
98 | 41, 55, 37, 38, 97 | syl112anc 1375 |
. . . . . 6
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) โฅ ((๐โ(๐ด + ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต))) โ ((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) โฅ (๐โ(๐ด + ๐ต)))) |
99 | 96, 98 | mpbid 231 |
. . . . 5
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) โฅ (๐โ(๐ด + ๐ต))) |
100 | 1, 62, 17 | mulgdi 19606 |
. . . . . . . . . . . . 13
โข ((๐บ โ Abel โง (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ โค โง ๐ด โ ๐ โง ๐ต โ ๐)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)(๐ด + ๐ต)) = ((((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ด) + (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต))) |
101 | 58, 88, 60, 61, 100 | syl13anc 1373 |
. . . . . . . . . . . 12
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)(๐ด + ๐ต)) = ((((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ด) + (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต))) |
102 | 1, 2, 62, 68 | oddvds 19330 |
. . . . . . . . . . . . . . 15
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ โค) โ ((๐โ๐ด) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ด) = (0gโ๐บ))) |
103 | 67, 60, 88, 102 | syl3anc 1372 |
. . . . . . . . . . . . . 14
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ด) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ด) = (0gโ๐บ))) |
104 | 57, 103 | mpbid 231 |
. . . . . . . . . . . . 13
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ด) = (0gโ๐บ)) |
105 | 104 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ด) + (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต)) = ((0gโ๐บ) + (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต))) |
106 | 101, 105 | eqtrd 2777 |
. . . . . . . . . . 11
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)(๐ด + ๐ต)) = ((0gโ๐บ) + (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต))) |
107 | | dvdsmul1 16161 |
. . . . . . . . . . . . 13
โข (((๐โ(๐ด + ๐ต)) โ โค โง (๐โ๐ด) โ โค) โ (๐โ(๐ด + ๐ต)) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))) |
108 | 55, 28, 107 | syl2anc 585 |
. . . . . . . . . . . 12
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ(๐ด + ๐ต)) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))) |
109 | 1, 2, 62, 68 | oddvds 19330 |
. . . . . . . . . . . . 13
โข ((๐บ โ Grp โง (๐ด + ๐ต) โ ๐ โง ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ โค) โ ((๐โ(๐ด + ๐ต)) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)(๐ด + ๐ต)) = (0gโ๐บ))) |
110 | 67, 76, 88, 109 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ(๐ด + ๐ต)) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)(๐ด + ๐ต)) = (0gโ๐บ))) |
111 | 108, 110 | mpbid 231 |
. . . . . . . . . . 11
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)(๐ด + ๐ต)) = (0gโ๐บ)) |
112 | 1, 62 | mulgcl 18894 |
. . . . . . . . . . . . 13
โข ((๐บ โ Grp โง ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ โค โง ๐ต โ ๐) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต) โ ๐) |
113 | 67, 88, 61, 112 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต) โ ๐) |
114 | 1, 17, 68 | grplid 18781 |
. . . . . . . . . . . 12
โข ((๐บ โ Grp โง (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต) โ ๐) โ ((0gโ๐บ) + (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต)) = (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต)) |
115 | 67, 113, 114 | syl2anc 585 |
. . . . . . . . . . 11
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ
((0gโ๐บ)
+
(((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต)) = (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต)) |
116 | 106, 111,
115 | 3eqtr3rd 2786 |
. . . . . . . . . 10
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต) = (0gโ๐บ)) |
117 | 1, 2, 62, 68 | oddvds 19330 |
. . . . . . . . . . 11
โข ((๐บ โ Grp โง ๐ต โ ๐ โง ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ โค) โ ((๐โ๐ต) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต) = (0gโ๐บ))) |
118 | 67, 61, 88, 117 | syl3anc 1372 |
. . . . . . . . . 10
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ต) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))(.gโ๐บ)๐ต) = (0gโ๐บ))) |
119 | 116, 118 | mpbird 257 |
. . . . . . . . 9
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ๐ต) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด))) |
120 | | dvdsgcd 16426 |
. . . . . . . . . 10
โข (((๐โ๐ต) โ โค โง ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โ โค โง ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)) โ โค) โ (((๐โ๐ต) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โง (๐โ๐ต) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))) โ (๐โ๐ต) โฅ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) gcd ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))))) |
121 | 29, 88, 59, 120 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ต) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) โง (๐โ๐ต) โฅ ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))) โ (๐โ๐ต) โฅ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) gcd ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต))))) |
122 | 119, 66, 121 | mp2and 698 |
. . . . . . . 8
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ๐ต) โฅ (((๐โ(๐ด + ๐ต)) ยท (๐โ๐ด)) gcd ((๐โ(๐ด + ๐ต)) ยท (๐โ๐ต)))) |
123 | 122, 94 | breqtrd 5132 |
. . . . . . 7
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (๐โ๐ต) โฅ ((๐โ(๐ด + ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) |
124 | 52, 123 | eqbrtrd 5128 |
. . . . . 6
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) โฅ ((๐โ(๐ด + ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) |
125 | | dvdsmulcr 16169 |
. . . . . . 7
โข ((((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โค โง (๐โ(๐ด + ๐ต)) โ โค โง (((๐โ๐ด) gcd (๐โ๐ต)) โ โค โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0)) โ ((((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) โฅ ((๐โ(๐ด + ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต))) โ ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) โฅ (๐โ(๐ด + ๐ต)))) |
126 | 46, 55, 37, 38, 125 | syl112anc 1375 |
. . . . . 6
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) โฅ ((๐โ(๐ด + ๐ต)) ยท ((๐โ๐ด) gcd (๐โ๐ต))) โ ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) โฅ (๐โ(๐ด + ๐ต)))) |
127 | 124, 126 | mpbid 231 |
. . . . 5
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) โฅ (๐โ(๐ด + ๐ต))) |
128 | 41, 46 | gcdcld 16389 |
. . . . . . . 8
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) gcd ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) โ
โ0) |
129 | 128 | nn0cnd 12476 |
. . . . . . 7
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) gcd ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) โ โ) |
130 | | 1cnd 11151 |
. . . . . . 7
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ 1 โ
โ) |
131 | 31 | mulid2d 11174 |
. . . . . . . 8
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (1 ยท ((๐โ๐ด) gcd (๐โ๐ต))) = ((๐โ๐ด) gcd (๐โ๐ต))) |
132 | 50, 52 | oveq12d 7376 |
. . . . . . . 8
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) gcd (((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) = ((๐โ๐ด) gcd (๐โ๐ต))) |
133 | | mulgcdr 16432 |
. . . . . . . . 9
โข ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โค โง ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โค โง ((๐โ๐ด) gcd (๐โ๐ต)) โ โ0) โ
((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) gcd (((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) = ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) gcd ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) |
134 | 41, 46, 30, 133 | syl3anc 1372 |
. . . . . . . 8
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) gcd (((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) = ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) gcd ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) ยท ((๐โ๐ด) gcd (๐โ๐ต)))) |
135 | 131, 132,
134 | 3eqtr2rd 2784 |
. . . . . . 7
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) gcd ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) ยท ((๐โ๐ด) gcd (๐โ๐ต))) = (1 ยท ((๐โ๐ด) gcd (๐โ๐ต)))) |
136 | 129, 130,
31, 38, 135 | mulcan2ad 11792 |
. . . . . 6
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) gcd ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) = 1) |
137 | | coprmdvds2 16531 |
. . . . . 6
โข
(((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โค โง ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) โ โค โง (๐โ(๐ด + ๐ต)) โ โค) โง (((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) gcd ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) = 1) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) โฅ (๐โ(๐ด + ๐ต)) โง ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) โฅ (๐โ(๐ด + ๐ต))) โ (((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) โฅ (๐โ(๐ด + ๐ต)))) |
138 | 41, 46, 55, 136, 137 | syl31anc 1374 |
. . . . 5
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) โฅ (๐โ(๐ด + ๐ต)) โง ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต))) โฅ (๐โ(๐ด + ๐ต))) โ (((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) โฅ (๐โ(๐ด + ๐ต)))) |
139 | 99, 127, 138 | mp2and 698 |
. . . 4
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) โฅ (๐โ(๐ด + ๐ต))) |
140 | 41, 46 | zmulcld 12614 |
. . . . 5
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) โ โค) |
141 | | zsqcl 14035 |
. . . . . 6
โข (((๐โ๐ด) gcd (๐โ๐ต)) โ โค โ (((๐โ๐ด) gcd (๐โ๐ต))โ2) โ โค) |
142 | 37, 141 | syl 17 |
. . . . 5
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ (((๐โ๐ด) gcd (๐โ๐ต))โ2) โ โค) |
143 | | dvdsmulc 16167 |
. . . . 5
โข
(((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) โ โค โง (๐โ(๐ด + ๐ต)) โ โค โง (((๐โ๐ด) gcd (๐โ๐ต))โ2) โ โค) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) โฅ (๐โ(๐ด + ๐ต)) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2)) โฅ ((๐โ(๐ด + ๐ต)) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2)))) |
144 | 140, 55, 142, 143 | syl3anc 1372 |
. . . 4
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) โฅ (๐โ(๐ด + ๐ต)) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2)) โฅ ((๐โ(๐ด + ๐ต)) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2)))) |
145 | 139, 144 | mpd 15 |
. . 3
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((((๐โ๐ด) / ((๐โ๐ด) gcd (๐โ๐ต))) ยท ((๐โ๐ต) / ((๐โ๐ด) gcd (๐โ๐ต)))) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2)) โฅ ((๐โ(๐ด + ๐ต)) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2))) |
146 | 54, 145 | eqbrtrrd 5130 |
. 2
โข (((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โง ((๐โ๐ด) gcd (๐โ๐ต)) โ 0) โ ((๐โ๐ด) ยท (๐โ๐ต)) โฅ ((๐โ(๐ด + ๐ต)) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2))) |
147 | 27, 146 | pm2.61dane 3033 |
1
โข ((๐บ โ Abel โง ๐ด โ ๐ โง ๐ต โ ๐) โ ((๐โ๐ด) ยท (๐โ๐ต)) โฅ ((๐โ(๐ด + ๐ต)) ยท (((๐โ๐ด) gcd (๐โ๐ต))โ2))) |