Step | Hyp | Ref
| Expression |
1 | | nnmulcl 12184 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
2 | 1 | nnred 12175 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
3 | | nnz 12527 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โค) |
4 | 3 | adantr 482 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โค) |
5 | 4 | zred 12614 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
6 | | nnz 12527 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โค) |
7 | 6 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โค) |
8 | 7 | zred 12614 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
9 | | 0red 11165 |
. . . . . . 7
โข (๐ โ โ โ 0 โ
โ) |
10 | | nnre 12167 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
11 | | nngt0 12191 |
. . . . . . 7
โข (๐ โ โ โ 0 <
๐) |
12 | 9, 10, 11 | ltled 11310 |
. . . . . 6
โข (๐ โ โ โ 0 โค
๐) |
13 | 12 | adantr 482 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ 0 โค
๐) |
14 | | 0red 11165 |
. . . . . . 7
โข (๐ โ โ โ 0 โ
โ) |
15 | | nnre 12167 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
16 | | nngt0 12191 |
. . . . . . 7
โข (๐ โ โ โ 0 <
๐) |
17 | 14, 15, 16 | ltled 11310 |
. . . . . 6
โข (๐ โ โ โ 0 โค
๐) |
18 | 17 | adantl 483 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ 0 โค
๐) |
19 | 5, 8, 13, 18 | mulge0d 11739 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ 0 โค
(๐ ยท ๐)) |
20 | 2, 19 | absidd 15314 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ
(absโ(๐ ยท
๐)) = (๐ ยท ๐)) |
21 | 3, 6 | anim12i 614 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โ โค โง ๐ โ
โค)) |
22 | | nnne0 12194 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ 0) |
23 | 22 | neneqd 2949 |
. . . . . . . 8
โข (๐ โ โ โ ยฌ
๐ = 0) |
24 | | nnne0 12194 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ 0) |
25 | 24 | neneqd 2949 |
. . . . . . . 8
โข (๐ โ โ โ ยฌ
๐ = 0) |
26 | 23, 25 | anim12i 614 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (ยฌ
๐ = 0 โง ยฌ ๐ = 0)) |
27 | | ioran 983 |
. . . . . . 7
โข (ยฌ
(๐ = 0 โจ ๐ = 0) โ (ยฌ ๐ = 0 โง ยฌ ๐ = 0)) |
28 | 26, 27 | sylibr 233 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ยฌ
(๐ = 0 โจ ๐ = 0)) |
29 | | lcmn0val 16478 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (๐ lcm ๐) = inf({๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}, โ, < )) |
30 | 21, 28, 29 | syl2anc 585 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ lcm ๐) = inf({๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}, โ, < )) |
31 | | ltso 11242 |
. . . . . . 7
โข < Or
โ |
32 | 31 | a1i 11 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ < Or
โ) |
33 | | gcddvds 16390 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โง (๐ gcd ๐) โฅ ๐)) |
34 | 33 | simpld 496 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โฅ ๐) |
35 | | gcdcl 16393 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โ
โ0) |
36 | 35 | nn0zd 12532 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โ โค) |
37 | | dvdsmultr1 16185 |
. . . . . . . . . . . 12
โข (((๐ gcd ๐) โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โ (๐ gcd ๐) โฅ (๐ ยท ๐))) |
38 | 37 | 3expb 1121 |
. . . . . . . . . . 11
โข (((๐ gcd ๐) โ โค โง (๐ โ โค โง ๐ โ โค)) โ ((๐ gcd ๐) โฅ ๐ โ (๐ gcd ๐) โฅ (๐ ยท ๐))) |
39 | 36, 38 | mpancom 687 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โ (๐ gcd ๐) โฅ (๐ ยท ๐))) |
40 | 34, 39 | mpd 15 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โฅ (๐ ยท ๐)) |
41 | 21, 40 | syl 17 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โฅ (๐ ยท ๐)) |
42 | | gcdnncl 16394 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ โ) |
43 | | nndivdvds 16152 |
. . . . . . . . 9
โข (((๐ ยท ๐) โ โ โง (๐ gcd ๐) โ โ) โ ((๐ gcd ๐) โฅ (๐ ยท ๐) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โ)) |
44 | 1, 42, 43 | syl2anc 585 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) โฅ (๐ ยท ๐) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โ)) |
45 | 41, 44 | mpbid 231 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โ) |
46 | 45 | nnred 12175 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โ) |
47 | | breq2 5114 |
. . . . . . . 8
โข (๐ฅ = ((๐ ยท ๐) / (๐ gcd ๐)) โ (๐ โฅ ๐ฅ โ ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐)))) |
48 | | breq2 5114 |
. . . . . . . 8
โข (๐ฅ = ((๐ ยท ๐) / (๐ gcd ๐)) โ (๐ โฅ ๐ฅ โ ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐)))) |
49 | 47, 48 | anbi12d 632 |
. . . . . . 7
โข (๐ฅ = ((๐ ยท ๐) / (๐ gcd ๐)) โ ((๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ) โ (๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐)) โง ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐))))) |
50 | 33 | simprd 497 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โฅ ๐) |
51 | 21, 50 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โฅ ๐) |
52 | 21, 36 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ โค) |
53 | 42 | nnne0d 12210 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ 0) |
54 | | dvdsval2 16146 |
. . . . . . . . . . . 12
โข (((๐ gcd ๐) โ โค โง (๐ gcd ๐) โ 0 โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โ (๐ / (๐ gcd ๐)) โ โค)) |
55 | 52, 53, 7, 54 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) โฅ ๐ โ (๐ / (๐ gcd ๐)) โ โค)) |
56 | 51, 55 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ / (๐ gcd ๐)) โ โค) |
57 | | dvdsmul1 16167 |
. . . . . . . . . 10
โข ((๐ โ โค โง (๐ / (๐ gcd ๐)) โ โค) โ ๐ โฅ (๐ ยท (๐ / (๐ gcd ๐)))) |
58 | 4, 56, 57 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โฅ (๐ ยท (๐ / (๐ gcd ๐)))) |
59 | | nncn 12168 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
60 | 59 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
61 | | nncn 12168 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
62 | 61 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
63 | 42 | nncnd 12176 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ โ) |
64 | 60, 62, 63, 53 | divassd 11973 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) = (๐ ยท (๐ / (๐ gcd ๐)))) |
65 | 58, 64 | breqtrrd 5138 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐))) |
66 | 21, 34 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โฅ ๐) |
67 | | dvdsval2 16146 |
. . . . . . . . . . . 12
โข (((๐ gcd ๐) โ โค โง (๐ gcd ๐) โ 0 โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โ (๐ / (๐ gcd ๐)) โ โค)) |
68 | 52, 53, 4, 67 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) โฅ ๐ โ (๐ / (๐ gcd ๐)) โ โค)) |
69 | 66, 68 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ / (๐ gcd ๐)) โ โค) |
70 | | dvdsmul1 16167 |
. . . . . . . . . 10
โข ((๐ โ โค โง (๐ / (๐ gcd ๐)) โ โค) โ ๐ โฅ (๐ ยท (๐ / (๐ gcd ๐)))) |
71 | 7, 69, 70 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โฅ (๐ ยท (๐ / (๐ gcd ๐)))) |
72 | 60, 62 | mulcomd 11183 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) = (๐ ยท ๐)) |
73 | 72 | oveq1d 7377 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) = ((๐ ยท ๐) / (๐ gcd ๐))) |
74 | 62, 60, 63, 53 | divassd 11973 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) = (๐ ยท (๐ / (๐ gcd ๐)))) |
75 | 73, 74 | eqtrd 2777 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) = (๐ ยท (๐ / (๐ gcd ๐)))) |
76 | 71, 75 | breqtrrd 5138 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐))) |
77 | 65, 76 | jca 513 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐)) โง ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐)))) |
78 | 49, 45, 77 | elrabd 3652 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}) |
79 | 46 | adantr 482 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โ) |
80 | | elrabi 3644 |
. . . . . . . . 9
โข (๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)} โ ๐ โ โ) |
81 | 80 | nnred 12175 |
. . . . . . . 8
โข (๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)} โ ๐ โ โ) |
82 | 81 | adantl 483 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}) โ ๐ โ โ) |
83 | | breq2 5114 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐)) |
84 | | breq2 5114 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐)) |
85 | 83, 84 | anbi12d 632 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ((๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ) โ (๐ โฅ ๐ โง ๐ โฅ ๐))) |
86 | 85 | elrab 3650 |
. . . . . . . 8
โข (๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)} โ (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) |
87 | | bezout 16431 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ
โ๐ฅ โ โค
โ๐ฆ โ โค
(๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
88 | 21, 87 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ
โ๐ฅ โ โค
โ๐ฆ โ โค
(๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
89 | 88 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ โ๐ฅ โ โค โ๐ฆ โ โค (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
90 | | nncn 12168 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ ๐ โ
โ) |
91 | 90 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โ) |
92 | 1 | nncnd 12176 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
93 | 92 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐) โ โ) |
94 | 63 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ gcd ๐) โ โ) |
95 | 60 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โ) |
96 | 61 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โ) |
97 | 22 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ 0) |
98 | 24 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ 0) |
99 | 95, 96, 97, 98 | mulne0d 11814 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐) โ 0) |
100 | 53 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ gcd ๐) โ 0) |
101 | 91, 93, 94, 99, 100 | divdiv2d 11970 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) = ((๐ ยท (๐ gcd ๐)) / (๐ ยท ๐))) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ โ
โ โง ๐ โ
โ) โง ๐ โ
โ) โง (๐ฅ โ
โค โง ๐ฆ โ
โค)) โง (๐ gcd
๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) = ((๐ ยท (๐ gcd ๐)) / (๐ ยท ๐))) |
103 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ (๐ ยท (๐ gcd ๐)) = (๐ ยท ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)))) |
104 | 103 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ((๐ ยท (๐ gcd ๐)) / (๐ ยท ๐)) = ((๐ ยท ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) / (๐ ยท ๐))) |
105 | | zcn 12511 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
106 | 105 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฅ โ
โ) |
107 | 95, 106 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐ฅ) โ โ) |
108 | | zcn 12511 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
109 | 108 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฆ โ
โ) |
110 | 96, 109 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐ฆ) โ โ) |
111 | 91, 107, 110 | adddid 11186 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) = ((๐ ยท (๐ ยท ๐ฅ)) + (๐ ยท (๐ ยท ๐ฆ)))) |
112 | 111 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) / (๐ ยท ๐)) = (((๐ ยท (๐ ยท ๐ฅ)) + (๐ ยท (๐ ยท ๐ฆ))) / (๐ ยท ๐))) |
113 | 91, 107 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท (๐ ยท ๐ฅ)) โ โ) |
114 | 91, 110 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท (๐ ยท ๐ฆ)) โ โ) |
115 | 113, 114,
93, 99 | divdird 11976 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ ยท (๐ ยท ๐ฅ)) + (๐ ยท (๐ ยท ๐ฆ))) / (๐ ยท ๐)) = (((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) + ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)))) |
116 | 112, 115 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) / (๐ ยท ๐)) = (((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) + ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)))) |
117 | 104, 116 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ โ
โ โง ๐ โ
โ) โง ๐ โ
โ) โง (๐ฅ โ
โค โง ๐ฆ โ
โค)) โง (๐ gcd
๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ ((๐ ยท (๐ gcd ๐)) / (๐ ยท ๐)) = (((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) + ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)))) |
118 | 91, 95, 106 | mul12d 11371 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท (๐ ยท ๐ฅ)) = (๐ ยท (๐ ยท ๐ฅ))) |
119 | 118 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐))) |
120 | 91, 106 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐ฅ) โ โ) |
121 | 120, 96, 95, 98, 97 | divcan5d 11964 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) = ((๐ ยท ๐ฅ) / ๐)) |
122 | 119, 121 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) = ((๐ ยท ๐ฅ) / ๐)) |
123 | 91, 96, 109 | mul12d 11371 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท (๐ ยท ๐ฆ)) = (๐ ยท (๐ ยท ๐ฆ))) |
124 | 123 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐))) |
125 | 72 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐) = (๐ ยท ๐)) |
126 | 125 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐))) |
127 | 91, 109 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐ฆ) โ โ) |
128 | 127, 95, 96, 97, 98 | divcan5d 11964 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)) = ((๐ ยท ๐ฆ) / ๐)) |
129 | 124, 126,
128 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)) = ((๐ ยท ๐ฆ) / ๐)) |
130 | 122, 129 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) + ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐))) = (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐))) |
131 | 130 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ โ
โ โง ๐ โ
โ) โง ๐ โ
โ) โง (๐ฅ โ
โค โง ๐ฆ โ
โค)) โง (๐ gcd
๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) + ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐))) = (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐))) |
132 | 102, 117,
131 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โ
โ โง ๐ โ
โ) โง ๐ โ
โ) โง (๐ฅ โ
โค โง ๐ฆ โ
โค)) โง (๐ gcd
๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) = (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐))) |
133 | 132 | ex 414 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) = (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)))) |
134 | 133 | adantlrr 720 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) = (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)))) |
135 | 134 | imp 408 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โ
โ โง ๐ โ
โ) โง (๐ โ
โ โง (๐ โฅ
๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) = (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐))) |
136 | 6 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โค) |
137 | | nnz 12527 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ ๐ โ
โค) |
138 | 137 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โค) |
139 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฅ โ
โค) |
140 | | dvdsmultr1 16185 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โ โค โง ๐ โ โค โง ๐ฅ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (๐ ยท ๐ฅ))) |
141 | 136, 138,
139, 140 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ ๐ โ ๐ โฅ (๐ ยท ๐ฅ))) |
142 | 138, 139 | zmulcld 12620 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐ฅ) โ โค) |
143 | | dvdsval2 16146 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โ โค โง ๐ โ 0 โง (๐ ยท ๐ฅ) โ โค) โ (๐ โฅ (๐ ยท ๐ฅ) โ ((๐ ยท ๐ฅ) / ๐) โ โค)) |
144 | 136, 98, 142, 143 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ (๐ ยท ๐ฅ) โ ((๐ ยท ๐ฅ) / ๐) โ โค)) |
145 | 141, 144 | sylibd 238 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ ๐ โ ((๐ ยท ๐ฅ) / ๐) โ โค)) |
146 | 145 | adantld 492 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ ((๐ ยท ๐ฅ) / ๐) โ โค)) |
147 | 146 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ((๐ ยท ๐ฅ) / ๐) โ โค) |
148 | 3 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โค) |
149 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฆ โ
โค) |
150 | | dvdsmultr1 16185 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โ โค โง ๐ โ โค โง ๐ฆ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (๐ ยท ๐ฆ))) |
151 | 148, 138,
149, 150 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ ๐ โ ๐ โฅ (๐ ยท ๐ฆ))) |
152 | 138, 149 | zmulcld 12620 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐ฆ) โ โค) |
153 | | dvdsval2 16146 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โ โค โง ๐ โ 0 โง (๐ ยท ๐ฆ) โ โค) โ (๐ โฅ (๐ ยท ๐ฆ) โ ((๐ ยท ๐ฆ) / ๐) โ โค)) |
154 | 148, 97, 152, 153 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ (๐ ยท ๐ฆ) โ ((๐ ยท ๐ฆ) / ๐) โ โค)) |
155 | 151, 154 | sylibd 238 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ ๐ โ ((๐ ยท ๐ฆ) / ๐) โ โค)) |
156 | 155 | adantrd 493 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ ((๐ ยท ๐ฆ) / ๐) โ โค)) |
157 | 156 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ((๐ ยท ๐ฆ) / ๐) โ โค) |
158 | 147, 157 | zaddcld 12618 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)) โ โค) |
159 | 158 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)) โ โค)) |
160 | 159 | an32s 651 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ โ โ) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)) โ โค)) |
161 | 160 | impr 456 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)) โ โค) |
162 | 161 | an32s 651 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)) โ โค) |
163 | 162 | adantr 482 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โ
โ โง ๐ โ
โ) โง (๐ โ
โ โง (๐ โฅ
๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)) โ โค) |
164 | 135, 163 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ
โ โง ๐ โ
โ) โง (๐ โ
โ โง (๐ โฅ
๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) โ โค) |
165 | 45 | nnzd 12533 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โค) |
166 | 165 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โค) |
167 | 1 | nnne0d 12210 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ 0) |
168 | 92, 63, 167, 53 | divne0d 11954 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ 0) |
169 | 168 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ 0) |
170 | 138 | adantlrr 720 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ โค) |
171 | | dvdsval2 16146 |
. . . . . . . . . . . . . . . 16
โข ((((๐ ยท ๐) / (๐ gcd ๐)) โ โค โง ((๐ ยท ๐) / (๐ gcd ๐)) โ 0 โง ๐ โ โค) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) โ โค)) |
172 | 166, 169,
170, 171 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) โ โค)) |
173 | 172 | adantr 482 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ
โ โง ๐ โ
โ) โง (๐ โ
โ โง (๐ โฅ
๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) โ โค)) |
174 | 164, 173 | mpbird 257 |
. . . . . . . . . . . . 13
โข
(((((๐ โ
โ โง ๐ โ
โ) โง (๐ โ
โ โง (๐ โฅ
๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐) |
175 | 174 | ex 414 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐)) |
176 | 175 | reximdvva 3203 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ (โ๐ฅ โ โค โ๐ฆ โ โค (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐)) |
177 | 89, 176 | mpd 15 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐) |
178 | | 1z 12540 |
. . . . . . . . . . . 12
โข 1 โ
โค |
179 | | ne0i 4299 |
. . . . . . . . . . . 12
โข (1 โ
โค โ โค โ โ
) |
180 | | r19.9rzv 4462 |
. . . . . . . . . . . 12
โข (โค
โ โ
โ (((๐
ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐)) |
181 | 178, 179,
180 | mp2b 10 |
. . . . . . . . . . 11
โข (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐) |
182 | | r19.9rzv 4462 |
. . . . . . . . . . . 12
โข (โค
โ โ
โ (โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐)) |
183 | 178, 179,
182 | mp2b 10 |
. . . . . . . . . . 11
โข
(โ๐ฆ โ
โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐) |
184 | 181, 183 | bitri 275 |
. . . . . . . . . 10
โข (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐) |
185 | 177, 184 | sylibr 233 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐) |
186 | 165 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โค) |
187 | | simprl 770 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ ๐ โ โ) |
188 | | dvdsle 16199 |
. . . . . . . . . 10
โข ((((๐ ยท ๐) / (๐ gcd ๐)) โ โค โง ๐ โ โ) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ ((๐ ยท ๐) / (๐ gcd ๐)) โค ๐)) |
189 | 186, 187,
188 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ ((๐ ยท ๐) / (๐ gcd ๐)) โค ๐)) |
190 | 185, 189 | mpd 15 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ ((๐ ยท ๐) / (๐ gcd ๐)) โค ๐) |
191 | 86, 190 | sylan2b 595 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}) โ ((๐ ยท ๐) / (๐ gcd ๐)) โค ๐) |
192 | 79, 82, 191 | lensymd 11313 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}) โ ยฌ ๐ < ((๐ ยท ๐) / (๐ gcd ๐))) |
193 | 32, 46, 78, 192 | infmin 9437 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ
inf({๐ฅ โ โ
โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}, โ, < ) = ((๐ ยท ๐) / (๐ gcd ๐))) |
194 | 30, 193 | eqtr2d 2778 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) = (๐ lcm ๐)) |
195 | 194, 45 | eqeltrrd 2839 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ lcm ๐) โ โ) |
196 | 195 | nncnd 12176 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ lcm ๐) โ โ) |
197 | 92, 196, 63, 53 | divmul3d 11972 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ ยท ๐) / (๐ gcd ๐)) = (๐ lcm ๐) โ (๐ ยท ๐) = ((๐ lcm ๐) ยท (๐ gcd ๐)))) |
198 | 194, 197 | mpbid 231 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) = ((๐ lcm ๐) ยท (๐ gcd ๐))) |
199 | 20, 198 | eqtr2d 2778 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐))) |
200 | | simprl 770 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง (๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ))) โ ๐พ โ โ) |
201 | | eleq1 2826 |
. . . . . . . 8
โข (๐ = ๐พ โ (๐ โ โ โ ๐พ โ โ)) |
202 | | breq2 5114 |
. . . . . . . . 9
โข (๐ = ๐พ โ (๐ โฅ ๐ โ ๐ โฅ ๐พ)) |
203 | | breq2 5114 |
. . . . . . . . 9
โข (๐ = ๐พ โ (๐ โฅ ๐ โ ๐ โฅ ๐พ)) |
204 | 202, 203 | anbi12d 632 |
. . . . . . . 8
โข (๐ = ๐พ โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ (๐ โฅ ๐พ โง ๐ โฅ ๐พ))) |
205 | 201, 204 | anbi12d 632 |
. . . . . . 7
โข (๐ = ๐พ โ ((๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ)))) |
206 | 205 | anbi2d 630 |
. . . . . 6
โข (๐ = ๐พ โ (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ ((๐ โ โ โง ๐ โ โ) โง (๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ))))) |
207 | | breq2 5114 |
. . . . . 6
โข (๐ = ๐พ โ ((๐ lcm ๐) โฅ ๐ โ (๐ lcm ๐) โฅ ๐พ)) |
208 | 206, 207 | imbi12d 345 |
. . . . 5
โข (๐ = ๐พ โ ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ (๐ lcm ๐) โฅ ๐) โ (((๐ โ โ โง ๐ โ โ) โง (๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ))) โ (๐ lcm ๐) โฅ ๐พ))) |
209 | 194 | breq1d 5120 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ (๐ lcm ๐) โฅ ๐)) |
210 | 209 | adantr 482 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ (๐ lcm ๐) โฅ ๐)) |
211 | 185, 210 | mpbid 231 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ (๐ lcm ๐) โฅ ๐) |
212 | 208, 211 | vtoclg 3528 |
. . . 4
โข (๐พ โ โ โ (((๐ โ โ โง ๐ โ โ) โง (๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ))) โ (๐ lcm ๐) โฅ ๐พ)) |
213 | 200, 212 | mpcom 38 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง (๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ))) โ (๐ lcm ๐) โฅ ๐พ) |
214 | 213 | ex 414 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ ((๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ)) โ (๐ lcm ๐) โฅ ๐พ)) |
215 | 199, 214 | jca 513 |
1
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐)) โง ((๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ)) โ (๐ lcm ๐) โฅ ๐พ))) |