Step | Hyp | Ref
| Expression |
1 | | pcdvdstr 12325 |
. . . . 5
โข ((๐ โ โ โง (๐ด โ โค โง ๐ต โ โค โง ๐ด โฅ ๐ต)) โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต)) |
2 | 1 | ancoms 268 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ด โฅ ๐ต) โง ๐ โ โ) โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต)) |
3 | 2 | ralrimiva 2550 |
. . 3
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ด โฅ ๐ต) โ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต)) |
4 | 3 | 3expia 1205 |
. 2
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด โฅ ๐ต โ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต))) |
5 | | 2prm 12126 |
. . . . . . . 8
โข 2 โ
โ |
6 | | elex2 2753 |
. . . . . . . 8
โข (2 โ
โ โ โ๐ค
๐ค โ
โ) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
โข
โ๐ค ๐ค โ โ |
8 | | r19.2m 3509 |
. . . . . . 7
โข
((โ๐ค ๐ค โ โ โง
โ๐ โ โ
(๐ pCnt 0) โค (๐ pCnt ๐ต)) โ โ๐ โ โ (๐ pCnt 0) โค (๐ pCnt ๐ต)) |
9 | 7, 8 | mpan 424 |
. . . . . 6
โข
(โ๐ โ
โ (๐ pCnt 0) โค
(๐ pCnt ๐ต) โ โ๐ โ โ (๐ pCnt 0) โค (๐ pCnt ๐ต)) |
10 | | id 19 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
11 | | zq 9625 |
. . . . . . . . . . . . . 14
โข (๐ต โ โค โ ๐ต โ
โ) |
12 | 11 | adantl 277 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ต โ โค) โ ๐ต โ
โ) |
13 | | pcxcl 12310 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ต โ โ) โ (๐ pCnt ๐ต) โ
โ*) |
14 | 10, 12, 13 | syl2anr 290 |
. . . . . . . . . . . 12
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ (๐ pCnt ๐ต) โ
โ*) |
15 | | pnfge 9788 |
. . . . . . . . . . . 12
โข ((๐ pCnt ๐ต) โ โ* โ (๐ pCnt ๐ต) โค +โ) |
16 | 14, 15 | syl 14 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ (๐ pCnt ๐ต) โค +โ) |
17 | 16 | biantrurd 305 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ
(+โ โค (๐ pCnt
๐ต) โ ((๐ pCnt ๐ต) โค +โ โง +โ โค (๐ pCnt ๐ต)))) |
18 | | pc0 12303 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (๐ pCnt 0) =
+โ) |
19 | 18 | adantl 277 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ (๐ pCnt 0) =
+โ) |
20 | 19 | breq1d 4013 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ ((๐ pCnt 0) โค (๐ pCnt ๐ต) โ +โ โค (๐ pCnt ๐ต))) |
21 | | pnfxr 8009 |
. . . . . . . . . . 11
โข +โ
โ โ* |
22 | | xrletri3 9803 |
. . . . . . . . . . 11
โข (((๐ pCnt ๐ต) โ โ* โง +โ
โ โ*) โ ((๐ pCnt ๐ต) = +โ โ ((๐ pCnt ๐ต) โค +โ โง +โ โค (๐ pCnt ๐ต)))) |
23 | 14, 21, 22 | sylancl 413 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ ((๐ pCnt ๐ต) = +โ โ ((๐ pCnt ๐ต) โค +โ โง +โ โค (๐ pCnt ๐ต)))) |
24 | 17, 20, 23 | 3bitr4d 220 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ ((๐ pCnt 0) โค (๐ pCnt ๐ต) โ (๐ pCnt ๐ต) = +โ)) |
25 | | pnfnre 7998 |
. . . . . . . . . . . 12
โข +โ
โ โ |
26 | 25 | neli 2444 |
. . . . . . . . . . 11
โข ยฌ
+โ โ โ |
27 | | eleq1 2240 |
. . . . . . . . . . 11
โข ((๐ pCnt ๐ต) = +โ โ ((๐ pCnt ๐ต) โ โ โ +โ โ
โ)) |
28 | 26, 27 | mtbiri 675 |
. . . . . . . . . 10
โข ((๐ pCnt ๐ต) = +โ โ ยฌ (๐ pCnt ๐ต) โ โ) |
29 | | simplr 528 |
. . . . . . . . . . . 12
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ ๐ต โ
โค) |
30 | | 0zd 9264 |
. . . . . . . . . . . 12
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ 0 โ
โค) |
31 | | zdceq 9327 |
. . . . . . . . . . . 12
โข ((๐ต โ โค โง 0 โ
โค) โ DECID ๐ต = 0) |
32 | 29, 30, 31 | syl2anc 411 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ
DECID ๐ต =
0) |
33 | | pczcl 12297 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ pCnt ๐ต) โ
โ0) |
34 | 33 | nn0red 9229 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ pCnt ๐ต) โ โ) |
35 | 34 | adantll 476 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โค โง ๐ โ โ) โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ pCnt ๐ต) โ โ) |
36 | 35 | an4s 588 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โ โง ๐ต โ 0)) โ (๐ pCnt ๐ต) โ โ) |
37 | 36 | expr 375 |
. . . . . . . . . . . . 13
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ (๐ต โ 0 โ (๐ pCnt ๐ต) โ โ)) |
38 | 37 | a1d 22 |
. . . . . . . . . . . 12
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ
(DECID ๐ต = 0
โ (๐ต โ 0 โ
(๐ pCnt ๐ต) โ โ))) |
39 | 38 | necon1bddc 2424 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ
(DECID ๐ต = 0
โ (ยฌ (๐ pCnt ๐ต) โ โ โ ๐ต = 0))) |
40 | 32, 39 | mpd 13 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ (ยฌ
(๐ pCnt ๐ต) โ โ โ ๐ต = 0)) |
41 | 28, 40 | syl5 32 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ ((๐ pCnt ๐ต) = +โ โ ๐ต = 0)) |
42 | 24, 41 | sylbid 150 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ) โ ((๐ pCnt 0) โค (๐ pCnt ๐ต) โ ๐ต = 0)) |
43 | 42 | rexlimdva 2594 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค) โ
(โ๐ โ โ
(๐ pCnt 0) โค (๐ pCnt ๐ต) โ ๐ต = 0)) |
44 | | 0dvds 11817 |
. . . . . . . 8
โข (๐ต โ โค โ (0
โฅ ๐ต โ ๐ต = 0)) |
45 | 44 | adantl 277 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค) โ (0
โฅ ๐ต โ ๐ต = 0)) |
46 | 43, 45 | sylibrd 169 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค) โ
(โ๐ โ โ
(๐ pCnt 0) โค (๐ pCnt ๐ต) โ 0 โฅ ๐ต)) |
47 | 9, 46 | syl5 32 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค) โ
(โ๐ โ โ
(๐ pCnt 0) โค (๐ pCnt ๐ต) โ 0 โฅ ๐ต)) |
48 | 47 | adantr 276 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด = 0) โ (โ๐ โ โ (๐ pCnt 0) โค (๐ pCnt ๐ต) โ 0 โฅ ๐ต)) |
49 | | oveq2 5882 |
. . . . . . . 8
โข (๐ด = 0 โ (๐ pCnt ๐ด) = (๐ pCnt 0)) |
50 | 49 | breq1d 4013 |
. . . . . . 7
โข (๐ด = 0 โ ((๐ pCnt ๐ด) โค (๐ pCnt ๐ต) โ (๐ pCnt 0) โค (๐ pCnt ๐ต))) |
51 | 50 | ralbidv 2477 |
. . . . . 6
โข (๐ด = 0 โ (โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต) โ โ๐ โ โ (๐ pCnt 0) โค (๐ pCnt ๐ต))) |
52 | | breq1 4006 |
. . . . . 6
โข (๐ด = 0 โ (๐ด โฅ ๐ต โ 0 โฅ ๐ต)) |
53 | 51, 52 | imbi12d 234 |
. . . . 5
โข (๐ด = 0 โ ((โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต) โ ๐ด โฅ ๐ต) โ (โ๐ โ โ (๐ pCnt 0) โค (๐ pCnt ๐ต) โ 0 โฅ ๐ต))) |
54 | 53 | adantl 277 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด = 0) โ ((โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต) โ ๐ด โฅ ๐ต) โ (โ๐ โ โ (๐ pCnt 0) โค (๐ pCnt ๐ต) โ 0 โฅ ๐ต))) |
55 | 48, 54 | mpbird 167 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด = 0) โ (โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต) โ ๐ด โฅ ๐ต)) |
56 | | zdvdsdc 11818 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค) โ
DECID ๐ด
โฅ ๐ต) |
57 | 56 | adantr 276 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ
DECID ๐ด
โฅ ๐ต) |
58 | | gcddvds 11963 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ต โ โค) โ ((๐ด gcd ๐ต) โฅ ๐ด โง (๐ด gcd ๐ต) โฅ ๐ต)) |
59 | 58 | simpld 112 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด gcd ๐ต) โฅ ๐ด) |
60 | | gcdcl 11966 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด gcd ๐ต) โ
โ0) |
61 | 60 | nn0zd 9372 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด gcd ๐ต) โ โค) |
62 | | simpl 109 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ต โ โค) โ ๐ด โ
โค) |
63 | | dvdsabsb 11816 |
. . . . . . . . . . . 12
โข (((๐ด gcd ๐ต) โ โค โง ๐ด โ โค) โ ((๐ด gcd ๐ต) โฅ ๐ด โ (๐ด gcd ๐ต) โฅ (absโ๐ด))) |
64 | 61, 62, 63 | syl2anc 411 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ต โ โค) โ ((๐ด gcd ๐ต) โฅ ๐ด โ (๐ด gcd ๐ต) โฅ (absโ๐ด))) |
65 | 59, 64 | mpbid 147 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด gcd ๐ต) โฅ (absโ๐ด)) |
66 | 65 | adantr 276 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (๐ด gcd ๐ต) โฅ (absโ๐ด)) |
67 | | simpl 109 |
. . . . . . . . . . . . 13
โข ((๐ด = 0 โง ๐ต = 0) โ ๐ด = 0) |
68 | 67 | necon3ai 2396 |
. . . . . . . . . . . 12
โข (๐ด โ 0 โ ยฌ (๐ด = 0 โง ๐ต = 0)) |
69 | | gcdn0cl 11962 |
. . . . . . . . . . . 12
โข (((๐ด โ โค โง ๐ต โ โค) โง ยฌ
(๐ด = 0 โง ๐ต = 0)) โ (๐ด gcd ๐ต) โ โ) |
70 | 68, 69 | sylan2 286 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (๐ด gcd ๐ต) โ โ) |
71 | 70 | nnzd 9373 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (๐ด gcd ๐ต) โ โค) |
72 | 70 | nnne0d 8963 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (๐ด gcd ๐ต) โ 0) |
73 | | nnabscl 11108 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ด โ 0) โ (absโ๐ด) โ
โ) |
74 | 73 | adantlr 477 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (absโ๐ด) โ
โ) |
75 | 74 | nnzd 9373 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (absโ๐ด) โ
โค) |
76 | | dvdsval2 11796 |
. . . . . . . . . 10
โข (((๐ด gcd ๐ต) โ โค โง (๐ด gcd ๐ต) โ 0 โง (absโ๐ด) โ โค) โ ((๐ด gcd ๐ต) โฅ (absโ๐ด) โ ((absโ๐ด) / (๐ด gcd ๐ต)) โ โค)) |
77 | 71, 72, 75, 76 | syl3anc 1238 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ ((๐ด gcd ๐ต) โฅ (absโ๐ด) โ ((absโ๐ด) / (๐ด gcd ๐ต)) โ โค)) |
78 | 66, 77 | mpbid 147 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ
((absโ๐ด) / (๐ด gcd ๐ต)) โ โค) |
79 | | nnre 8925 |
. . . . . . . . . . 11
โข
((absโ๐ด)
โ โ โ (absโ๐ด) โ โ) |
80 | | nngt0 8943 |
. . . . . . . . . . 11
โข
((absโ๐ด)
โ โ โ 0 < (absโ๐ด)) |
81 | 79, 80 | jca 306 |
. . . . . . . . . 10
โข
((absโ๐ด)
โ โ โ ((absโ๐ด) โ โ โง 0 <
(absโ๐ด))) |
82 | | nnre 8925 |
. . . . . . . . . . 11
โข ((๐ด gcd ๐ต) โ โ โ (๐ด gcd ๐ต) โ โ) |
83 | | nngt0 8943 |
. . . . . . . . . . 11
โข ((๐ด gcd ๐ต) โ โ โ 0 < (๐ด gcd ๐ต)) |
84 | 82, 83 | jca 306 |
. . . . . . . . . 10
โข ((๐ด gcd ๐ต) โ โ โ ((๐ด gcd ๐ต) โ โ โง 0 < (๐ด gcd ๐ต))) |
85 | | divgt0 8828 |
. . . . . . . . . 10
โข
((((absโ๐ด)
โ โ โง 0 < (absโ๐ด)) โง ((๐ด gcd ๐ต) โ โ โง 0 < (๐ด gcd ๐ต))) โ 0 < ((absโ๐ด) / (๐ด gcd ๐ต))) |
86 | 81, 84, 85 | syl2an 289 |
. . . . . . . . 9
โข
(((absโ๐ด)
โ โ โง (๐ด gcd
๐ต) โ โ) โ 0
< ((absโ๐ด) /
(๐ด gcd ๐ต))) |
87 | 74, 70, 86 | syl2anc 411 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ 0 <
((absโ๐ด) / (๐ด gcd ๐ต))) |
88 | | elnnz 9262 |
. . . . . . . 8
โข
(((absโ๐ด) /
(๐ด gcd ๐ต)) โ โ โ (((absโ๐ด) / (๐ด gcd ๐ต)) โ โค โง 0 <
((absโ๐ด) / (๐ด gcd ๐ต)))) |
89 | 78, 87, 88 | sylanbrc 417 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ
((absโ๐ด) / (๐ด gcd ๐ต)) โ โ) |
90 | | elnn1uz2 9606 |
. . . . . . 7
โข
(((absโ๐ด) /
(๐ด gcd ๐ต)) โ โ โ (((absโ๐ด) / (๐ด gcd ๐ต)) = 1 โจ ((absโ๐ด) / (๐ด gcd ๐ต)) โ
(โคโฅโ2))) |
91 | 89, 90 | sylib 122 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ
(((absโ๐ด) / (๐ด gcd ๐ต)) = 1 โจ ((absโ๐ด) / (๐ด gcd ๐ต)) โ
(โคโฅโ2))) |
92 | 58 | simprd 114 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด gcd ๐ต) โฅ ๐ต) |
93 | 92 | adantr 276 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (๐ด gcd ๐ต) โฅ ๐ต) |
94 | | breq1 4006 |
. . . . . . . . 9
โข ((๐ด gcd ๐ต) = (absโ๐ด) โ ((๐ด gcd ๐ต) โฅ ๐ต โ (absโ๐ด) โฅ ๐ต)) |
95 | 93, 94 | syl5ibcom 155 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ ((๐ด gcd ๐ต) = (absโ๐ด) โ (absโ๐ด) โฅ ๐ต)) |
96 | 74 | nncnd 8932 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (absโ๐ด) โ
โ) |
97 | 70 | nncnd 8932 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (๐ด gcd ๐ต) โ โ) |
98 | | 1cnd 7972 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ 1 โ
โ) |
99 | 70 | nnap0d 8964 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (๐ด gcd ๐ต) # 0) |
100 | 96, 97, 98, 99 | divmulapd 8768 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ
(((absโ๐ด) / (๐ด gcd ๐ต)) = 1 โ ((๐ด gcd ๐ต) ยท 1) = (absโ๐ด))) |
101 | 97 | mulridd 7973 |
. . . . . . . . . 10
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ ((๐ด gcd ๐ต) ยท 1) = (๐ด gcd ๐ต)) |
102 | 101 | eqeq1d 2186 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (((๐ด gcd ๐ต) ยท 1) = (absโ๐ด) โ (๐ด gcd ๐ต) = (absโ๐ด))) |
103 | 100, 102 | bitrd 188 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ
(((absโ๐ด) / (๐ด gcd ๐ต)) = 1 โ (๐ด gcd ๐ต) = (absโ๐ด))) |
104 | | absdvdsb 11815 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด โฅ ๐ต โ (absโ๐ด) โฅ ๐ต)) |
105 | 104 | adantr 276 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (๐ด โฅ ๐ต โ (absโ๐ด) โฅ ๐ต)) |
106 | 95, 103, 105 | 3imtr4d 203 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ
(((absโ๐ด) / (๐ด gcd ๐ต)) = 1 โ ๐ด โฅ ๐ต)) |
107 | | exprmfct 12137 |
. . . . . . . 8
โข
(((absโ๐ด) /
(๐ด gcd ๐ต)) โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ
((absโ๐ด) / (๐ด gcd ๐ต))) |
108 | | simprl 529 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ๐ โ โ) |
109 | 74 | adantr 276 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (absโ๐ด) โ โ) |
110 | 109 | nnzd 9373 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (absโ๐ด) โ โค) |
111 | 109 | nnne0d 8963 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (absโ๐ด) โ 0) |
112 | 70 | adantr 276 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ด gcd ๐ต) โ โ) |
113 | | pcdiv 12301 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง
((absโ๐ด) โ
โค โง (absโ๐ด)
โ 0) โง (๐ด gcd ๐ต) โ โ) โ (๐ pCnt ((absโ๐ด) / (๐ด gcd ๐ต))) = ((๐ pCnt (absโ๐ด)) โ (๐ pCnt (๐ด gcd ๐ต)))) |
114 | 108, 110,
111, 112, 113 | syl121anc 1243 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt ((absโ๐ด) / (๐ด gcd ๐ต))) = ((๐ pCnt (absโ๐ด)) โ (๐ pCnt (๐ด gcd ๐ต)))) |
115 | | simplll 533 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ๐ด โ โค) |
116 | | zq 9625 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ โค โ ๐ด โ
โ) |
117 | 115, 116 | syl 14 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ๐ด โ โ) |
118 | | pcabs 12324 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ pCnt (absโ๐ด)) = (๐ pCnt ๐ด)) |
119 | 108, 117,
118 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt (absโ๐ด)) = (๐ pCnt ๐ด)) |
120 | 119 | oveq1d 5889 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((๐ pCnt (absโ๐ด)) โ (๐ pCnt (๐ด gcd ๐ต))) = ((๐ pCnt ๐ด) โ (๐ pCnt (๐ด gcd ๐ต)))) |
121 | 114, 120 | eqtrd 2210 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt ((absโ๐ด) / (๐ด gcd ๐ต))) = ((๐ pCnt ๐ด) โ (๐ pCnt (๐ด gcd ๐ต)))) |
122 | | simprr 531 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต))) |
123 | 89 | adantr 276 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((absโ๐ด) / (๐ด gcd ๐ต)) โ โ) |
124 | | pcelnn 12319 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง
((absโ๐ด) / (๐ด gcd ๐ต)) โ โ) โ ((๐ pCnt ((absโ๐ด) / (๐ด gcd ๐ต))) โ โ โ ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) |
125 | 108, 123,
124 | syl2anc 411 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((๐ pCnt ((absโ๐ด) / (๐ด gcd ๐ต))) โ โ โ ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) |
126 | 122, 125 | mpbird 167 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt ((absโ๐ด) / (๐ด gcd ๐ต))) โ โ) |
127 | 121, 126 | eqeltrrd 2255 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((๐ pCnt ๐ด) โ (๐ pCnt (๐ด gcd ๐ต))) โ โ) |
128 | 108, 112 | pccld 12299 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt (๐ด gcd ๐ต)) โ
โ0) |
129 | 128 | nn0zd 9372 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt (๐ด gcd ๐ต)) โ โค) |
130 | | simplr 528 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ๐ด โ 0) |
131 | | pczcl 12297 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง (๐ด โ โค โง ๐ด โ 0)) โ (๐ pCnt ๐ด) โ
โ0) |
132 | 108, 115,
130, 131 | syl12anc 1236 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt ๐ด) โ
โ0) |
133 | 132 | nn0zd 9372 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt ๐ด) โ โค) |
134 | | znnsub 9303 |
. . . . . . . . . . . . . 14
โข (((๐ pCnt (๐ด gcd ๐ต)) โ โค โง (๐ pCnt ๐ด) โ โค) โ ((๐ pCnt (๐ด gcd ๐ต)) < (๐ pCnt ๐ด) โ ((๐ pCnt ๐ด) โ (๐ pCnt (๐ด gcd ๐ต))) โ โ)) |
135 | 129, 133,
134 | syl2anc 411 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((๐ pCnt (๐ด gcd ๐ต)) < (๐ pCnt ๐ด) โ ((๐ pCnt ๐ด) โ (๐ pCnt (๐ด gcd ๐ต))) โ โ)) |
136 | 127, 135 | mpbird 167 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt (๐ด gcd ๐ต)) < (๐ pCnt ๐ด)) |
137 | | zltnle 9298 |
. . . . . . . . . . . . 13
โข (((๐ pCnt (๐ด gcd ๐ต)) โ โค โง (๐ pCnt ๐ด) โ โค) โ ((๐ pCnt (๐ด gcd ๐ต)) < (๐ pCnt ๐ด) โ ยฌ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด gcd ๐ต)))) |
138 | 129, 133,
137 | syl2anc 411 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((๐ pCnt (๐ด gcd ๐ต)) < (๐ pCnt ๐ด) โ ยฌ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด gcd ๐ต)))) |
139 | 136, 138 | mpbid 147 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ยฌ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด gcd ๐ต))) |
140 | 132 | nn0red 9229 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt ๐ด) โ โ) |
141 | | simpllr 534 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ๐ต โ โค) |
142 | | nprmdvds1 12139 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ยฌ
๐ โฅ
1) |
143 | 142 | ad2antrl 490 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ยฌ ๐ โฅ 1) |
144 | | gcdid0 11980 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ด โ โค โ (๐ด gcd 0) = (absโ๐ด)) |
145 | 115, 144 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ด gcd 0) = (absโ๐ด)) |
146 | 145 | oveq2d 5890 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((absโ๐ด) / (๐ด gcd 0)) = ((absโ๐ด) / (absโ๐ด))) |
147 | 96 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (absโ๐ด) โ โ) |
148 | 109 | nnap0d 8964 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (absโ๐ด) # 0) |
149 | 147, 148 | dividapd 8742 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((absโ๐ด) / (absโ๐ด)) = 1) |
150 | 146, 149 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((absโ๐ด) / (๐ด gcd 0)) = 1) |
151 | 150 | breq2d 4015 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ โฅ ((absโ๐ด) / (๐ด gcd 0)) โ ๐ โฅ 1)) |
152 | 143, 151 | mtbird 673 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ยฌ ๐ โฅ ((absโ๐ด) / (๐ด gcd 0))) |
153 | | oveq2 5882 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ต = 0 โ (๐ด gcd ๐ต) = (๐ด gcd 0)) |
154 | 153 | oveq2d 5890 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ต = 0 โ ((absโ๐ด) / (๐ด gcd ๐ต)) = ((absโ๐ด) / (๐ด gcd 0))) |
155 | 154 | breq2d 4015 |
. . . . . . . . . . . . . . . . . 18
โข (๐ต = 0 โ (๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)) โ ๐ โฅ ((absโ๐ด) / (๐ด gcd 0)))) |
156 | 122, 155 | syl5ibcom 155 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ต = 0 โ ๐ โฅ ((absโ๐ด) / (๐ด gcd 0)))) |
157 | 156 | necon3bd 2390 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (ยฌ ๐ โฅ ((absโ๐ด) / (๐ด gcd 0)) โ ๐ต โ 0)) |
158 | 152, 157 | mpd 13 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ๐ต โ 0) |
159 | 108, 141,
158, 33 | syl12anc 1236 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt ๐ต) โ
โ0) |
160 | 159 | nn0red 9229 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt ๐ต) โ โ) |
161 | | lemininf 11241 |
. . . . . . . . . . . . 13
โข (((๐ pCnt ๐ด) โ โ โง (๐ pCnt ๐ด) โ โ โง (๐ pCnt ๐ต) โ โ) โ ((๐ pCnt ๐ด) โค inf({(๐ pCnt ๐ด), (๐ pCnt ๐ต)}, โ, < ) โ ((๐ pCnt ๐ด) โค (๐ pCnt ๐ด) โง (๐ pCnt ๐ด) โค (๐ pCnt ๐ต)))) |
162 | 140, 140,
160, 161 | syl3anc 1238 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((๐ pCnt ๐ด) โค inf({(๐ pCnt ๐ด), (๐ pCnt ๐ต)}, โ, < ) โ ((๐ pCnt ๐ด) โค (๐ pCnt ๐ด) โง (๐ pCnt ๐ด) โค (๐ pCnt ๐ต)))) |
163 | | pcgcd 12327 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ (๐ pCnt (๐ด gcd ๐ต)) = if((๐ pCnt ๐ด) โค (๐ pCnt ๐ต), (๐ pCnt ๐ด), (๐ pCnt ๐ต))) |
164 | 108, 115,
141, 163 | syl3anc 1238 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt (๐ด gcd ๐ต)) = if((๐ pCnt ๐ด) โค (๐ pCnt ๐ต), (๐ pCnt ๐ด), (๐ pCnt ๐ต))) |
165 | 159 | nn0zd 9372 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt ๐ต) โ โค) |
166 | | 2zinfmin 11250 |
. . . . . . . . . . . . . . 15
โข (((๐ pCnt ๐ด) โ โค โง (๐ pCnt ๐ต) โ โค) โ inf({(๐ pCnt ๐ด), (๐ pCnt ๐ต)}, โ, < ) = if((๐ pCnt ๐ด) โค (๐ pCnt ๐ต), (๐ pCnt ๐ด), (๐ pCnt ๐ต))) |
167 | 133, 165,
166 | syl2anc 411 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ inf({(๐ pCnt ๐ด), (๐ pCnt ๐ต)}, โ, < ) = if((๐ pCnt ๐ด) โค (๐ pCnt ๐ต), (๐ pCnt ๐ด), (๐ pCnt ๐ต))) |
168 | 164, 167 | eqtr4d 2213 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt (๐ด gcd ๐ต)) = inf({(๐ pCnt ๐ด), (๐ pCnt ๐ต)}, โ, < )) |
169 | 168 | breq2d 4015 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((๐ pCnt ๐ด) โค (๐ pCnt (๐ด gcd ๐ต)) โ (๐ pCnt ๐ด) โค inf({(๐ pCnt ๐ด), (๐ pCnt ๐ต)}, โ, < ))) |
170 | 140 | leidd 8470 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ด)) |
171 | 170 | biantrurd 305 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((๐ pCnt ๐ด) โค (๐ pCnt ๐ต) โ ((๐ pCnt ๐ด) โค (๐ pCnt ๐ด) โง (๐ pCnt ๐ด) โค (๐ pCnt ๐ต)))) |
172 | 162, 169,
171 | 3bitr4rd 221 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ((๐ pCnt ๐ด) โค (๐ pCnt ๐ต) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด gcd ๐ต)))) |
173 | 139, 172 | mtbird 673 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง (๐ โ โ โง ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)))) โ ยฌ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต)) |
174 | 173 | expr 375 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ (๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)) โ ยฌ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต))) |
175 | 174 | reximdva 2579 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (โ๐ โ โ ๐ โฅ ((absโ๐ด) / (๐ด gcd ๐ต)) โ โ๐ โ โ ยฌ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต))) |
176 | | rexnalim 2466 |
. . . . . . . 8
โข
(โ๐ โ
โ ยฌ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต) โ ยฌ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต)) |
177 | 107, 175,
176 | syl56 34 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ
(((absโ๐ด) / (๐ด gcd ๐ต)) โ (โคโฅโ2)
โ ยฌ โ๐
โ โ (๐ pCnt
๐ด) โค (๐ pCnt ๐ต))) |
178 | 106, 177 | orim12d 786 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ
((((absโ๐ด) / (๐ด gcd ๐ต)) = 1 โจ ((absโ๐ด) / (๐ด gcd ๐ต)) โ (โคโฅโ2))
โ (๐ด โฅ ๐ต โจ ยฌ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต)))) |
179 | 91, 178 | mpd 13 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (๐ด โฅ ๐ต โจ ยฌ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต))) |
180 | 179 | ord 724 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (ยฌ ๐ด โฅ ๐ต โ ยฌ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต))) |
181 | | condc 853 |
. . . 4
โข
(DECID ๐ด โฅ ๐ต โ ((ยฌ ๐ด โฅ ๐ต โ ยฌ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต)) โ (โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต) โ ๐ด โฅ ๐ต))) |
182 | 57, 180, 181 | sylc 62 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ด โ 0) โ (โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต) โ ๐ด โฅ ๐ต)) |
183 | | 0zd 9264 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค) โ 0 โ
โค) |
184 | | zdceq 9327 |
. . . . 5
โข ((๐ด โ โค โง 0 โ
โค) โ DECID ๐ด = 0) |
185 | 62, 183, 184 | syl2anc 411 |
. . . 4
โข ((๐ด โ โค โง ๐ต โ โค) โ
DECID ๐ด =
0) |
186 | | dcne 2358 |
. . . 4
โข
(DECID ๐ด = 0 โ (๐ด = 0 โจ ๐ด โ 0)) |
187 | 185, 186 | sylib 122 |
. . 3
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด = 0 โจ ๐ด โ 0)) |
188 | 55, 182, 187 | mpjaodan 798 |
. 2
โข ((๐ด โ โค โง ๐ต โ โค) โ
(โ๐ โ โ
(๐ pCnt ๐ด) โค (๐ pCnt ๐ต) โ ๐ด โฅ ๐ต)) |
189 | 4, 188 | impbid 129 |
1
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด โฅ ๐ต โ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต))) |