Step | Hyp | Ref
| Expression |
1 | | nnmulcl 8939 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
2 | 1 | nnred 8931 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
3 | | nnz 9271 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โค) |
4 | 3 | adantr 276 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โค) |
5 | 4 | zred 9374 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
6 | | nnz 9271 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โค) |
7 | 6 | adantl 277 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โค) |
8 | 7 | zred 9374 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
9 | | 0red 7957 |
. . . . . . 7
โข (๐ โ โ โ 0 โ
โ) |
10 | | nnre 8925 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
11 | | nngt0 8943 |
. . . . . . 7
โข (๐ โ โ โ 0 <
๐) |
12 | 9, 10, 11 | ltled 8075 |
. . . . . 6
โข (๐ โ โ โ 0 โค
๐) |
13 | 12 | adantr 276 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ 0 โค
๐) |
14 | | 0red 7957 |
. . . . . . 7
โข (๐ โ โ โ 0 โ
โ) |
15 | | nnre 8925 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
16 | | nngt0 8943 |
. . . . . . 7
โข (๐ โ โ โ 0 <
๐) |
17 | 14, 15, 16 | ltled 8075 |
. . . . . 6
โข (๐ โ โ โ 0 โค
๐) |
18 | 17 | adantl 277 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ 0 โค
๐) |
19 | 5, 8, 13, 18 | mulge0d 8577 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ 0 โค
(๐ ยท ๐)) |
20 | 2, 19 | absidd 11175 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ
(absโ(๐ ยท
๐)) = (๐ ยท ๐)) |
21 | 3, 6 | anim12i 338 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โ โค โง ๐ โ
โค)) |
22 | | nnne0 8946 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ 0) |
23 | 22 | neneqd 2368 |
. . . . . . . 8
โข (๐ โ โ โ ยฌ
๐ = 0) |
24 | | nnne0 8946 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ 0) |
25 | 24 | neneqd 2368 |
. . . . . . . 8
โข (๐ โ โ โ ยฌ
๐ = 0) |
26 | 23, 25 | anim12i 338 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (ยฌ
๐ = 0 โง ยฌ ๐ = 0)) |
27 | | ioran 752 |
. . . . . . 7
โข (ยฌ
(๐ = 0 โจ ๐ = 0) โ (ยฌ ๐ = 0 โง ยฌ ๐ = 0)) |
28 | 26, 27 | sylibr 134 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ยฌ
(๐ = 0 โจ ๐ = 0)) |
29 | | lcmn0val 12065 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (๐ lcm ๐) = inf({๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}, โ, < )) |
30 | 21, 28, 29 | syl2anc 411 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ lcm ๐) = inf({๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}, โ, < )) |
31 | | lttri3 8036 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ = ๐ โ (ยฌ ๐ < ๐ โง ยฌ ๐ < ๐))) |
32 | 31 | adantl 277 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ = ๐ โ (ยฌ ๐ < ๐ โง ยฌ ๐ < ๐))) |
33 | | gcddvds 11963 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โง (๐ gcd ๐) โฅ ๐)) |
34 | 33 | simpld 112 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โฅ ๐) |
35 | | gcdcl 11966 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โ
โ0) |
36 | 35 | nn0zd 9372 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โ โค) |
37 | | dvdsmultr1 11837 |
. . . . . . . . . . . 12
โข (((๐ gcd ๐) โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โ (๐ gcd ๐) โฅ (๐ ยท ๐))) |
38 | 37 | 3expb 1204 |
. . . . . . . . . . 11
โข (((๐ gcd ๐) โ โค โง (๐ โ โค โง ๐ โ โค)) โ ((๐ gcd ๐) โฅ ๐ โ (๐ gcd ๐) โฅ (๐ ยท ๐))) |
39 | 36, 38 | mpancom 422 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โ (๐ gcd ๐) โฅ (๐ ยท ๐))) |
40 | 34, 39 | mpd 13 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โฅ (๐ ยท ๐)) |
41 | 21, 40 | syl 14 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โฅ (๐ ยท ๐)) |
42 | | gcdnncl 11967 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ โ) |
43 | | nndivdvds 11802 |
. . . . . . . . 9
โข (((๐ ยท ๐) โ โ โง (๐ gcd ๐) โ โ) โ ((๐ gcd ๐) โฅ (๐ ยท ๐) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โ)) |
44 | 1, 42, 43 | syl2anc 411 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) โฅ (๐ ยท ๐) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โ)) |
45 | 41, 44 | mpbid 147 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โ) |
46 | 45 | nnred 8931 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โ) |
47 | 33 | simprd 114 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โฅ ๐) |
48 | 21, 47 | syl 14 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โฅ ๐) |
49 | 21, 36 | syl 14 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ โค) |
50 | 42 | nnne0d 8963 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ 0) |
51 | | dvdsval2 11796 |
. . . . . . . . . . . 12
โข (((๐ gcd ๐) โ โค โง (๐ gcd ๐) โ 0 โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โ (๐ / (๐ gcd ๐)) โ โค)) |
52 | 49, 50, 7, 51 | syl3anc 1238 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) โฅ ๐ โ (๐ / (๐ gcd ๐)) โ โค)) |
53 | 48, 52 | mpbid 147 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ / (๐ gcd ๐)) โ โค) |
54 | | dvdsmul1 11819 |
. . . . . . . . . 10
โข ((๐ โ โค โง (๐ / (๐ gcd ๐)) โ โค) โ ๐ โฅ (๐ ยท (๐ / (๐ gcd ๐)))) |
55 | 4, 53, 54 | syl2anc 411 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โฅ (๐ ยท (๐ / (๐ gcd ๐)))) |
56 | | nncn 8926 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
57 | 56 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
58 | | nncn 8926 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
59 | 58 | adantl 277 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
60 | 42 | nncnd 8932 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โ โ) |
61 | 42 | nnap0d 8964 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) # 0) |
62 | 57, 59, 60, 61 | divassapd 8782 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) = (๐ ยท (๐ / (๐ gcd ๐)))) |
63 | 55, 62 | breqtrrd 4031 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐))) |
64 | 21, 34 | syl 14 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd ๐) โฅ ๐) |
65 | | dvdsval2 11796 |
. . . . . . . . . . . 12
โข (((๐ gcd ๐) โ โค โง (๐ gcd ๐) โ 0 โง ๐ โ โค) โ ((๐ gcd ๐) โฅ ๐ โ (๐ / (๐ gcd ๐)) โ โค)) |
66 | 49, 50, 4, 65 | syl3anc 1238 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) โฅ ๐ โ (๐ / (๐ gcd ๐)) โ โค)) |
67 | 64, 66 | mpbid 147 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ / (๐ gcd ๐)) โ โค) |
68 | | dvdsmul1 11819 |
. . . . . . . . . 10
โข ((๐ โ โค โง (๐ / (๐ gcd ๐)) โ โค) โ ๐ โฅ (๐ ยท (๐ / (๐ gcd ๐)))) |
69 | 7, 67, 68 | syl2anc 411 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โฅ (๐ ยท (๐ / (๐ gcd ๐)))) |
70 | 57, 59 | mulcomd 7978 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) = (๐ ยท ๐)) |
71 | 70 | oveq1d 5889 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) = ((๐ ยท ๐) / (๐ gcd ๐))) |
72 | 59, 57, 60, 61 | divassapd 8782 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) = (๐ ยท (๐ / (๐ gcd ๐)))) |
73 | 71, 72 | eqtrd 2210 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) = (๐ ยท (๐ / (๐ gcd ๐)))) |
74 | 69, 73 | breqtrrd 4031 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐))) |
75 | 63, 74 | jca 306 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐)) โง ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐)))) |
76 | | breq2 4007 |
. . . . . . . . 9
โข (๐ฅ = ((๐ ยท ๐) / (๐ gcd ๐)) โ (๐ โฅ ๐ฅ โ ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐)))) |
77 | | breq2 4007 |
. . . . . . . . 9
โข (๐ฅ = ((๐ ยท ๐) / (๐ gcd ๐)) โ (๐ โฅ ๐ฅ โ ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐)))) |
78 | 76, 77 | anbi12d 473 |
. . . . . . . 8
โข (๐ฅ = ((๐ ยท ๐) / (๐ gcd ๐)) โ ((๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ) โ (๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐)) โง ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐))))) |
79 | 78 | elrab 2893 |
. . . . . . 7
โข (((๐ ยท ๐) / (๐ gcd ๐)) โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)} โ (((๐ ยท ๐) / (๐ gcd ๐)) โ โ โง (๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐)) โง ๐ โฅ ((๐ ยท ๐) / (๐ gcd ๐))))) |
80 | 45, 75, 79 | sylanbrc 417 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}) |
81 | 46 | adantr 276 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โ) |
82 | | elrabi 2890 |
. . . . . . . . 9
โข (๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)} โ ๐ โ โ) |
83 | 82 | nnred 8931 |
. . . . . . . 8
โข (๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)} โ ๐ โ โ) |
84 | 83 | adantl 277 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}) โ ๐ โ โ) |
85 | | breq2 4007 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐)) |
86 | | breq2 4007 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐)) |
87 | 85, 86 | anbi12d 473 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ((๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ) โ (๐ โฅ ๐ โง ๐ โฅ ๐))) |
88 | 87 | elrab 2893 |
. . . . . . . 8
โข (๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)} โ (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) |
89 | | bezout 12011 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ
โ๐ฅ โ โค
โ๐ฆ โ โค
(๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
90 | 21, 89 | syl 14 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ
โ๐ฅ โ โค
โ๐ฆ โ โค
(๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
91 | 90 | adantr 276 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ โ๐ฅ โ โค โ๐ฆ โ โค (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
92 | | nncn 8926 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ ๐ โ
โ) |
93 | 92 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โ) |
94 | 1 | nncnd 8932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
95 | 94 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐) โ โ) |
96 | 60 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ gcd ๐) โ โ) |
97 | 57 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โ) |
98 | 58 | ad3antlr 493 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โ) |
99 | | simplll 533 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โ) |
100 | 99 | nnap0d 8964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ # 0) |
101 | | simpllr 534 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โ) |
102 | 101 | nnap0d 8964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ # 0) |
103 | 97, 98, 100, 102 | mulap0d 8614 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐) # 0) |
104 | 61 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ gcd ๐) # 0) |
105 | 93, 95, 96, 103, 104 | divdivap2d 8779 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) = ((๐ ยท (๐ gcd ๐)) / (๐ ยท ๐))) |
106 | 105 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ โ
โ โง ๐ โ
โ) โง ๐ โ
โ) โง (๐ฅ โ
โค โง ๐ฆ โ
โค)) โง (๐ gcd
๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) = ((๐ ยท (๐ gcd ๐)) / (๐ ยท ๐))) |
107 | | oveq2 5882 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ (๐ ยท (๐ gcd ๐)) = (๐ ยท ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)))) |
108 | 107 | oveq1d 5889 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ((๐ ยท (๐ gcd ๐)) / (๐ ยท ๐)) = ((๐ ยท ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) / (๐ ยท ๐))) |
109 | | zcn 9257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
110 | 109 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฅ โ
โ) |
111 | 97, 110 | mulcld 7977 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐ฅ) โ โ) |
112 | | zcn 9257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
113 | 112 | ad2antll 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฆ โ
โ) |
114 | 98, 113 | mulcld 7977 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐ฆ) โ โ) |
115 | 93, 111, 114 | adddid 7981 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) = ((๐ ยท (๐ ยท ๐ฅ)) + (๐ ยท (๐ ยท ๐ฆ)))) |
116 | 115 | oveq1d 5889 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) / (๐ ยท ๐)) = (((๐ ยท (๐ ยท ๐ฅ)) + (๐ ยท (๐ ยท ๐ฆ))) / (๐ ยท ๐))) |
117 | 93, 111 | mulcld 7977 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท (๐ ยท ๐ฅ)) โ โ) |
118 | 93, 114 | mulcld 7977 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท (๐ ยท ๐ฆ)) โ โ) |
119 | 117, 118,
95, 103 | divdirapd 8785 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ ยท (๐ ยท ๐ฅ)) + (๐ ยท (๐ ยท ๐ฆ))) / (๐ ยท ๐)) = (((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) + ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)))) |
120 | 116, 119 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) / (๐ ยท ๐)) = (((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) + ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)))) |
121 | 108, 120 | sylan9eqr 2232 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ โ
โ โง ๐ โ
โ) โง ๐ โ
โ) โง (๐ฅ โ
โค โง ๐ฆ โ
โค)) โง (๐ gcd
๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ ((๐ ยท (๐ gcd ๐)) / (๐ ยท ๐)) = (((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) + ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)))) |
122 | 93, 97, 110 | mul12d 8108 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท (๐ ยท ๐ฅ)) = (๐ ยท (๐ ยท ๐ฅ))) |
123 | 122 | oveq1d 5889 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐))) |
124 | 93, 110 | mulcld 7977 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐ฅ) โ โ) |
125 | 124, 98, 97, 102, 100 | divcanap5d 8773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) = ((๐ ยท ๐ฅ) / ๐)) |
126 | 123, 125 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) = ((๐ ยท ๐ฅ) / ๐)) |
127 | 93, 98, 113 | mul12d 8108 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท (๐ ยท ๐ฆ)) = (๐ ยท (๐ ยท ๐ฆ))) |
128 | 127 | oveq1d 5889 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐))) |
129 | 70 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐) = (๐ ยท ๐)) |
130 | 129 | oveq2d 5890 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐))) |
131 | 93, 113 | mulcld 7977 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐ฆ) โ โ) |
132 | 131, 97, 98, 100, 102 | divcanap5d 8773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)) = ((๐ ยท ๐ฆ) / ๐)) |
133 | 128, 130,
132 | 3eqtrd 2214 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐)) = ((๐ ยท ๐ฆ) / ๐)) |
134 | 126, 133 | oveq12d 5892 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) + ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐))) = (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐))) |
135 | 134 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ โ
โ โง ๐ โ
โ) โง ๐ โ
โ) โง (๐ฅ โ
โค โง ๐ฆ โ
โค)) โง (๐ gcd
๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (((๐ ยท (๐ ยท ๐ฅ)) / (๐ ยท ๐)) + ((๐ ยท (๐ ยท ๐ฆ)) / (๐ ยท ๐))) = (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐))) |
136 | 106, 121,
135 | 3eqtrd 2214 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((((๐ โ
โ โง ๐ โ
โ) โง ๐ โ
โ) โง (๐ฅ โ
โค โง ๐ฆ โ
โค)) โง (๐ gcd
๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) = (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐))) |
137 | 136 | ex 115 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) = (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)))) |
138 | 137 | adantlrr 483 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) = (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)))) |
139 | 138 | imp 124 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โ
โ โง ๐ โ
โ) โง (๐ โ
โ โง (๐ โฅ
๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) = (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐))) |
140 | 6 | ad3antlr 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โค) |
141 | | nnz 9271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ โ โ ๐ โ
โค) |
142 | 141 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โค) |
143 | | simprl 529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฅ โ
โค) |
144 | | dvdsmultr1 11837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ โค โง ๐ โ โค โง ๐ฅ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (๐ ยท ๐ฅ))) |
145 | 140, 142,
143, 144 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ ๐ โ ๐ โฅ (๐ ยท ๐ฅ))) |
146 | 24 | ad3antlr 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ 0) |
147 | 142, 143 | zmulcld 9380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐ฅ) โ โค) |
148 | | dvdsval2 11796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ โค โง ๐ โ 0 โง (๐ ยท ๐ฅ) โ โค) โ (๐ โฅ (๐ ยท ๐ฅ) โ ((๐ ยท ๐ฅ) / ๐) โ โค)) |
149 | 140, 146,
147, 148 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ (๐ ยท ๐ฅ) โ ((๐ ยท ๐ฅ) / ๐) โ โค)) |
150 | 145, 149 | sylibd 149 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ ๐ โ ((๐ ยท ๐ฅ) / ๐) โ โค)) |
151 | 150 | adantld 278 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ ((๐ ยท ๐ฅ) / ๐) โ โค)) |
152 | 151 | 3impia 1200 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ((๐ ยท ๐ฅ) / ๐) โ โค) |
153 | 3 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ
โค) |
154 | | simprr 531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฆ โ
โค) |
155 | | dvdsmultr1 11837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ โค โง ๐ โ โค โง ๐ฆ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (๐ ยท ๐ฆ))) |
156 | 153, 142,
154, 155 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ ๐ โ ๐ โฅ (๐ ยท ๐ฆ))) |
157 | 22 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ 0) |
158 | 142, 154 | zmulcld 9380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ ยท ๐ฆ) โ โค) |
159 | | dvdsval2 11796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ โค โง ๐ โ 0 โง (๐ ยท ๐ฆ) โ โค) โ (๐ โฅ (๐ ยท ๐ฆ) โ ((๐ ยท ๐ฆ) / ๐) โ โค)) |
160 | 153, 157,
158, 159 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ (๐ ยท ๐ฆ) โ ((๐ ยท ๐ฆ) / ๐) โ โค)) |
161 | 156, 160 | sylibd 149 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ ๐ โ ((๐ ยท ๐ฆ) / ๐) โ โค)) |
162 | 161 | adantrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ ((๐ ยท ๐ฆ) / ๐) โ โค)) |
163 | 162 | 3impia 1200 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ((๐ ยท ๐ฆ) / ๐) โ โค) |
164 | 152, 163 | zaddcld 9378 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)) โ โค) |
165 | 164 | 3expia 1205 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ โ โง ๐ โ โ) โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)) โ โค)) |
166 | 165 | an32s 568 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ โ โ) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)) โ โค)) |
167 | 166 | impr 379 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)) โ โค) |
168 | 167 | an32s 568 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)) โ โค) |
169 | 168 | adantr 276 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โ
โ โง ๐ โ
โ) โง (๐ โ
โ โง (๐ โฅ
๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (((๐ ยท ๐ฅ) / ๐) + ((๐ ยท ๐ฆ) / ๐)) โ โค) |
170 | 139, 169 | eqeltrd 2254 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ โ
โ โง ๐ โ
โ) โง (๐ โ
โ โง (๐ โฅ
๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) โ โค) |
171 | 45 | nnzd 9373 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โค) |
172 | 171 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โค) |
173 | 45 | nnne0d 8963 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ 0) |
174 | 173 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ 0) |
175 | 142 | adantlrr 483 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ โค) |
176 | | dvdsval2 11796 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ ยท ๐) / (๐ gcd ๐)) โ โค โง ((๐ ยท ๐) / (๐ gcd ๐)) โ 0 โง ๐ โ โค) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) โ โค)) |
177 | 172, 174,
175, 176 | syl3anc 1238 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) โ โค)) |
178 | 177 | adantr 276 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ โ
โ โง ๐ โ
โ) โง (๐ โ
โ โง (๐ โฅ
๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ (๐ / ((๐ ยท ๐) / (๐ gcd ๐))) โ โค)) |
179 | 170, 178 | mpbird 167 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โ
โ โง ๐ โ
โ) โง (๐ โ
โ โง (๐ โฅ
๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) โ ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐) |
180 | 179 | ex 115 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐)) |
181 | 180 | anassrs 400 |
. . . . . . . . . . . . 13
โข
(((((๐ โ
โ โง ๐ โ
โ) โง (๐ โ
โ โง (๐ โฅ
๐ โง ๐ โฅ ๐))) โง ๐ฅ โ โค) โง ๐ฆ โ โค) โ ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐)) |
182 | 181 | reximdva 2579 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โง ๐ฅ โ โค) โ (โ๐ฆ โ โค (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐)) |
183 | 182 | reximdva 2579 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ (โ๐ฅ โ โค โ๐ฆ โ โค (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐)) |
184 | 91, 183 | mpd 13 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐) |
185 | | 1z 9278 |
. . . . . . . . . . . 12
โข 1 โ
โค |
186 | | elex2 2753 |
. . . . . . . . . . . 12
โข (1 โ
โค โ โ๐ค
๐ค โ
โค) |
187 | | r19.9rmv 3514 |
. . . . . . . . . . . 12
โข
(โ๐ค ๐ค โ โค โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐)) |
188 | 185, 186,
187 | mp2b 8 |
. . . . . . . . . . 11
โข (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐) |
189 | | r19.9rmv 3514 |
. . . . . . . . . . . 12
โข
(โ๐ค ๐ค โ โค โ
(โ๐ฆ โ โค
((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐)) |
190 | 185, 186,
189 | mp2b 8 |
. . . . . . . . . . 11
โข
(โ๐ฆ โ
โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐) |
191 | 188, 190 | bitri 184 |
. . . . . . . . . 10
โข (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐) |
192 | 184, 191 | sylibr 134 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ ((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐) |
193 | 171 | adantr 276 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ ((๐ ยท ๐) / (๐ gcd ๐)) โ โค) |
194 | | simprl 529 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ ๐ โ โ) |
195 | | dvdsle 11849 |
. . . . . . . . . 10
โข ((((๐ ยท ๐) / (๐ gcd ๐)) โ โค โง ๐ โ โ) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ ((๐ ยท ๐) / (๐ gcd ๐)) โค ๐)) |
196 | 193, 194,
195 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ ((๐ ยท ๐) / (๐ gcd ๐)) โค ๐)) |
197 | 192, 196 | mpd 13 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ ((๐ ยท ๐) / (๐ gcd ๐)) โค ๐) |
198 | 88, 197 | sylan2b 287 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}) โ ((๐ ยท ๐) / (๐ gcd ๐)) โค ๐) |
199 | 81, 84, 198 | lensymd 8078 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ {๐ฅ โ โ โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}) โ ยฌ ๐ < ((๐ ยท ๐) / (๐ gcd ๐))) |
200 | 32, 46, 80, 199 | infminti 7025 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ
inf({๐ฅ โ โ
โฃ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฅ)}, โ, < ) = ((๐ ยท ๐) / (๐ gcd ๐))) |
201 | 30, 200 | eqtr2d 2211 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) / (๐ gcd ๐)) = (๐ lcm ๐)) |
202 | 201, 45 | eqeltrrd 2255 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ lcm ๐) โ โ) |
203 | 202 | nncnd 8932 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ lcm ๐) โ โ) |
204 | 94, 203, 60, 61 | divmulap3d 8781 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ ยท ๐) / (๐ gcd ๐)) = (๐ lcm ๐) โ (๐ ยท ๐) = ((๐ lcm ๐) ยท (๐ gcd ๐)))) |
205 | 201, 204 | mpbid 147 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) = ((๐ lcm ๐) ยท (๐ gcd ๐))) |
206 | 20, 205 | eqtr2d 2211 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐))) |
207 | | simprl 529 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง (๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ))) โ ๐พ โ โ) |
208 | | eleq1 2240 |
. . . . . . . 8
โข (๐ = ๐พ โ (๐ โ โ โ ๐พ โ โ)) |
209 | | breq2 4007 |
. . . . . . . . 9
โข (๐ = ๐พ โ (๐ โฅ ๐ โ ๐ โฅ ๐พ)) |
210 | | breq2 4007 |
. . . . . . . . 9
โข (๐ = ๐พ โ (๐ โฅ ๐ โ ๐ โฅ ๐พ)) |
211 | 209, 210 | anbi12d 473 |
. . . . . . . 8
โข (๐ = ๐พ โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ (๐ โฅ ๐พ โง ๐ โฅ ๐พ))) |
212 | 208, 211 | anbi12d 473 |
. . . . . . 7
โข (๐ = ๐พ โ ((๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ)))) |
213 | 212 | anbi2d 464 |
. . . . . 6
โข (๐ = ๐พ โ (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ ((๐ โ โ โง ๐ โ โ) โง (๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ))))) |
214 | | breq2 4007 |
. . . . . 6
โข (๐ = ๐พ โ ((๐ lcm ๐) โฅ ๐ โ (๐ lcm ๐) โฅ ๐พ)) |
215 | 213, 214 | imbi12d 234 |
. . . . 5
โข (๐ = ๐พ โ ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ (๐ lcm ๐) โฅ ๐) โ (((๐ โ โ โง ๐ โ โ) โง (๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ))) โ (๐ lcm ๐) โฅ ๐พ))) |
216 | 201 | breq1d 4013 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ (๐ lcm ๐) โฅ ๐)) |
217 | 216 | adantr 276 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ (((๐ ยท ๐) / (๐ gcd ๐)) โฅ ๐ โ (๐ lcm ๐) โฅ ๐)) |
218 | 192, 217 | mpbid 147 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ โฅ ๐ โง ๐ โฅ ๐))) โ (๐ lcm ๐) โฅ ๐) |
219 | 215, 218 | vtoclg 2797 |
. . . 4
โข (๐พ โ โ โ (((๐ โ โ โง ๐ โ โ) โง (๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ))) โ (๐ lcm ๐) โฅ ๐พ)) |
220 | 207, 219 | mpcom 36 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง (๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ))) โ (๐ lcm ๐) โฅ ๐พ) |
221 | 220 | ex 115 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ ((๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ)) โ (๐ lcm ๐) โฅ ๐พ)) |
222 | 206, 221 | jca 306 |
1
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐)) โง ((๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ)) โ (๐ lcm ๐) โฅ ๐พ))) |