ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pc2dvds GIF version

Theorem pc2dvds 12328
Description: A characterization of divisibility in terms of prime count. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.)
Assertion
Ref Expression
pc2dvds ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด โˆฅ ๐ต โ†” โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต)))
Distinct variable groups:   ๐ด,๐‘   ๐ต,๐‘

Proof of Theorem pc2dvds
StepHypRef Expression
1 pcdvdstr 12325 . . . . 5 ((๐‘ โˆˆ โ„™ โˆง (๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ด โˆฅ ๐ต)) โ†’ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต))
21ancoms 268 . . . 4 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ด โˆฅ ๐ต) โˆง ๐‘ โˆˆ โ„™) โ†’ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต))
32ralrimiva 2550 . . 3 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ด โˆฅ ๐ต) โ†’ โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต))
433expia 1205 . 2 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด โˆฅ ๐ต โ†’ โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต)))
5 2prm 12126 . . . . . . . 8 2 โˆˆ โ„™
6 elex2 2753 . . . . . . . 8 (2 โˆˆ โ„™ โ†’ โˆƒ๐‘ค ๐‘ค โˆˆ โ„™)
75, 6ax-mp 5 . . . . . . 7 โˆƒ๐‘ค ๐‘ค โˆˆ โ„™
8 r19.2m 3509 . . . . . . 7 ((โˆƒ๐‘ค ๐‘ค โˆˆ โ„™ โˆง โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต)) โ†’ โˆƒ๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต))
97, 8mpan 424 . . . . . 6 (โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†’ โˆƒ๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต))
10 id 19 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„™ โ†’ ๐‘ โˆˆ โ„™)
11 zq 9625 . . . . . . . . . . . . . 14 (๐ต โˆˆ โ„ค โ†’ ๐ต โˆˆ โ„š)
1211adantl 277 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ ๐ต โˆˆ โ„š)
13 pcxcl 12310 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„™ โˆง ๐ต โˆˆ โ„š) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„*)
1410, 12, 13syl2anr 290 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„*)
15 pnfge 9788 . . . . . . . . . . . 12 ((๐‘ pCnt ๐ต) โˆˆ โ„* โ†’ (๐‘ pCnt ๐ต) โ‰ค +โˆž)
1614, 15syl 14 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ (๐‘ pCnt ๐ต) โ‰ค +โˆž)
1716biantrurd 305 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ (+โˆž โ‰ค (๐‘ pCnt ๐ต) โ†” ((๐‘ pCnt ๐ต) โ‰ค +โˆž โˆง +โˆž โ‰ค (๐‘ pCnt ๐ต))))
18 pc0 12303 . . . . . . . . . . . 12 (๐‘ โˆˆ โ„™ โ†’ (๐‘ pCnt 0) = +โˆž)
1918adantl 277 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ (๐‘ pCnt 0) = +โˆž)
2019breq1d 4013 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ ((๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†” +โˆž โ‰ค (๐‘ pCnt ๐ต)))
21 pnfxr 8009 . . . . . . . . . . 11 +โˆž โˆˆ โ„*
22 xrletri3 9803 . . . . . . . . . . 11 (((๐‘ pCnt ๐ต) โˆˆ โ„* โˆง +โˆž โˆˆ โ„*) โ†’ ((๐‘ pCnt ๐ต) = +โˆž โ†” ((๐‘ pCnt ๐ต) โ‰ค +โˆž โˆง +โˆž โ‰ค (๐‘ pCnt ๐ต))))
2314, 21, 22sylancl 413 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ ((๐‘ pCnt ๐ต) = +โˆž โ†” ((๐‘ pCnt ๐ต) โ‰ค +โˆž โˆง +โˆž โ‰ค (๐‘ pCnt ๐ต))))
2417, 20, 233bitr4d 220 . . . . . . . . 9 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ ((๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†” (๐‘ pCnt ๐ต) = +โˆž))
25 pnfnre 7998 . . . . . . . . . . . 12 +โˆž โˆ‰ โ„
2625neli 2444 . . . . . . . . . . 11 ยฌ +โˆž โˆˆ โ„
27 eleq1 2240 . . . . . . . . . . 11 ((๐‘ pCnt ๐ต) = +โˆž โ†’ ((๐‘ pCnt ๐ต) โˆˆ โ„ โ†” +โˆž โˆˆ โ„))
2826, 27mtbiri 675 . . . . . . . . . 10 ((๐‘ pCnt ๐ต) = +โˆž โ†’ ยฌ (๐‘ pCnt ๐ต) โˆˆ โ„)
29 simplr 528 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ ๐ต โˆˆ โ„ค)
30 0zd 9264 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ 0 โˆˆ โ„ค)
31 zdceq 9327 . . . . . . . . . . . 12 ((๐ต โˆˆ โ„ค โˆง 0 โˆˆ โ„ค) โ†’ DECID ๐ต = 0)
3229, 30, 31syl2anc 411 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ DECID ๐ต = 0)
33 pczcl 12297 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„™ โˆง (๐ต โˆˆ โ„ค โˆง ๐ต โ‰  0)) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„•0)
3433nn0red 9229 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ โ„™ โˆง (๐ต โˆˆ โ„ค โˆง ๐ต โ‰  0)) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„)
3534adantll 476 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„™) โˆง (๐ต โˆˆ โ„ค โˆง ๐ต โ‰  0)) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„)
3635an4s 588 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„™ โˆง ๐ต โ‰  0)) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„)
3736expr 375 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ (๐ต โ‰  0 โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„))
3837a1d 22 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ (DECID ๐ต = 0 โ†’ (๐ต โ‰  0 โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„)))
3938necon1bddc 2424 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ (DECID ๐ต = 0 โ†’ (ยฌ (๐‘ pCnt ๐ต) โˆˆ โ„ โ†’ ๐ต = 0)))
4032, 39mpd 13 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ (ยฌ (๐‘ pCnt ๐ต) โˆˆ โ„ โ†’ ๐ต = 0))
4128, 40syl5 32 . . . . . . . . 9 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ ((๐‘ pCnt ๐ต) = +โˆž โ†’ ๐ต = 0))
4224, 41sylbid 150 . . . . . . . 8 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ ((๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†’ ๐ต = 0))
4342rexlimdva 2594 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (โˆƒ๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†’ ๐ต = 0))
44 0dvds 11817 . . . . . . . 8 (๐ต โˆˆ โ„ค โ†’ (0 โˆฅ ๐ต โ†” ๐ต = 0))
4544adantl 277 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (0 โˆฅ ๐ต โ†” ๐ต = 0))
4643, 45sylibrd 169 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (โˆƒ๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†’ 0 โˆฅ ๐ต))
479, 46syl5 32 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†’ 0 โˆฅ ๐ต))
4847adantr 276 . . . 4 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด = 0) โ†’ (โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†’ 0 โˆฅ ๐ต))
49 oveq2 5882 . . . . . . . 8 (๐ด = 0 โ†’ (๐‘ pCnt ๐ด) = (๐‘ pCnt 0))
5049breq1d 4013 . . . . . . 7 (๐ด = 0 โ†’ ((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†” (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต)))
5150ralbidv 2477 . . . . . 6 (๐ด = 0 โ†’ (โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†” โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต)))
52 breq1 4006 . . . . . 6 (๐ด = 0 โ†’ (๐ด โˆฅ ๐ต โ†” 0 โˆฅ ๐ต))
5351, 52imbi12d 234 . . . . 5 (๐ด = 0 โ†’ ((โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†’ ๐ด โˆฅ ๐ต) โ†” (โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†’ 0 โˆฅ ๐ต)))
5453adantl 277 . . . 4 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด = 0) โ†’ ((โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†’ ๐ด โˆฅ ๐ต) โ†” (โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†’ 0 โˆฅ ๐ต)))
5548, 54mpbird 167 . . 3 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด = 0) โ†’ (โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†’ ๐ด โˆฅ ๐ต))
56 zdvdsdc 11818 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ DECID ๐ด โˆฅ ๐ต)
5756adantr 276 . . . 4 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ DECID ๐ด โˆฅ ๐ต)
58 gcddvds 11963 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ ((๐ด gcd ๐ต) โˆฅ ๐ด โˆง (๐ด gcd ๐ต) โˆฅ ๐ต))
5958simpld 112 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด gcd ๐ต) โˆฅ ๐ด)
60 gcdcl 11966 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด gcd ๐ต) โˆˆ โ„•0)
6160nn0zd 9372 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด gcd ๐ต) โˆˆ โ„ค)
62 simpl 109 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ ๐ด โˆˆ โ„ค)
63 dvdsabsb 11816 . . . . . . . . . . . 12 (((๐ด gcd ๐ต) โˆˆ โ„ค โˆง ๐ด โˆˆ โ„ค) โ†’ ((๐ด gcd ๐ต) โˆฅ ๐ด โ†” (๐ด gcd ๐ต) โˆฅ (absโ€˜๐ด)))
6461, 62, 63syl2anc 411 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ ((๐ด gcd ๐ต) โˆฅ ๐ด โ†” (๐ด gcd ๐ต) โˆฅ (absโ€˜๐ด)))
6559, 64mpbid 147 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด gcd ๐ต) โˆฅ (absโ€˜๐ด))
6665adantr 276 . . . . . . . . 9 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด gcd ๐ต) โˆฅ (absโ€˜๐ด))
67 simpl 109 . . . . . . . . . . . . 13 ((๐ด = 0 โˆง ๐ต = 0) โ†’ ๐ด = 0)
6867necon3ai 2396 . . . . . . . . . . . 12 (๐ด โ‰  0 โ†’ ยฌ (๐ด = 0 โˆง ๐ต = 0))
69 gcdn0cl 11962 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ยฌ (๐ด = 0 โˆง ๐ต = 0)) โ†’ (๐ด gcd ๐ต) โˆˆ โ„•)
7068, 69sylan2 286 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด gcd ๐ต) โˆˆ โ„•)
7170nnzd 9373 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด gcd ๐ต) โˆˆ โ„ค)
7270nnne0d 8963 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด gcd ๐ต) โ‰  0)
73 nnabscl 11108 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„•)
7473adantlr 477 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„•)
7574nnzd 9373 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„ค)
76 dvdsval2 11796 . . . . . . . . . 10 (((๐ด gcd ๐ต) โˆˆ โ„ค โˆง (๐ด gcd ๐ต) โ‰  0 โˆง (absโ€˜๐ด) โˆˆ โ„ค) โ†’ ((๐ด gcd ๐ต) โˆฅ (absโ€˜๐ด) โ†” ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ โ„ค))
7771, 72, 75, 76syl3anc 1238 . . . . . . . . 9 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ ((๐ด gcd ๐ต) โˆฅ (absโ€˜๐ด) โ†” ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ โ„ค))
7866, 77mpbid 147 . . . . . . . 8 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ โ„ค)
79 nnre 8925 . . . . . . . . . . 11 ((absโ€˜๐ด) โˆˆ โ„• โ†’ (absโ€˜๐ด) โˆˆ โ„)
80 nngt0 8943 . . . . . . . . . . 11 ((absโ€˜๐ด) โˆˆ โ„• โ†’ 0 < (absโ€˜๐ด))
8179, 80jca 306 . . . . . . . . . 10 ((absโ€˜๐ด) โˆˆ โ„• โ†’ ((absโ€˜๐ด) โˆˆ โ„ โˆง 0 < (absโ€˜๐ด)))
82 nnre 8925 . . . . . . . . . . 11 ((๐ด gcd ๐ต) โˆˆ โ„• โ†’ (๐ด gcd ๐ต) โˆˆ โ„)
83 nngt0 8943 . . . . . . . . . . 11 ((๐ด gcd ๐ต) โˆˆ โ„• โ†’ 0 < (๐ด gcd ๐ต))
8482, 83jca 306 . . . . . . . . . 10 ((๐ด gcd ๐ต) โˆˆ โ„• โ†’ ((๐ด gcd ๐ต) โˆˆ โ„ โˆง 0 < (๐ด gcd ๐ต)))
85 divgt0 8828 . . . . . . . . . 10 ((((absโ€˜๐ด) โˆˆ โ„ โˆง 0 < (absโ€˜๐ด)) โˆง ((๐ด gcd ๐ต) โˆˆ โ„ โˆง 0 < (๐ด gcd ๐ต))) โ†’ 0 < ((absโ€˜๐ด) / (๐ด gcd ๐ต)))
8681, 84, 85syl2an 289 . . . . . . . . 9 (((absโ€˜๐ด) โˆˆ โ„• โˆง (๐ด gcd ๐ต) โˆˆ โ„•) โ†’ 0 < ((absโ€˜๐ด) / (๐ด gcd ๐ต)))
8774, 70, 86syl2anc 411 . . . . . . . 8 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ 0 < ((absโ€˜๐ด) / (๐ด gcd ๐ต)))
88 elnnz 9262 . . . . . . . 8 (((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ โ„• โ†” (((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ โ„ค โˆง 0 < ((absโ€˜๐ด) / (๐ด gcd ๐ต))))
8978, 87, 88sylanbrc 417 . . . . . . 7 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ โ„•)
90 elnn1uz2 9606 . . . . . . 7 (((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ โ„• โ†” (((absโ€˜๐ด) / (๐ด gcd ๐ต)) = 1 โˆจ ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ (โ„คโ‰ฅโ€˜2)))
9189, 90sylib 122 . . . . . 6 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (((absโ€˜๐ด) / (๐ด gcd ๐ต)) = 1 โˆจ ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ (โ„คโ‰ฅโ€˜2)))
9258simprd 114 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด gcd ๐ต) โˆฅ ๐ต)
9392adantr 276 . . . . . . . . 9 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด gcd ๐ต) โˆฅ ๐ต)
94 breq1 4006 . . . . . . . . 9 ((๐ด gcd ๐ต) = (absโ€˜๐ด) โ†’ ((๐ด gcd ๐ต) โˆฅ ๐ต โ†” (absโ€˜๐ด) โˆฅ ๐ต))
9593, 94syl5ibcom 155 . . . . . . . 8 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ ((๐ด gcd ๐ต) = (absโ€˜๐ด) โ†’ (absโ€˜๐ด) โˆฅ ๐ต))
9674nncnd 8932 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
9770nncnd 8932 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด gcd ๐ต) โˆˆ โ„‚)
98 1cnd 7972 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ 1 โˆˆ โ„‚)
9970nnap0d 8964 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด gcd ๐ต) # 0)
10096, 97, 98, 99divmulapd 8768 . . . . . . . . 9 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (((absโ€˜๐ด) / (๐ด gcd ๐ต)) = 1 โ†” ((๐ด gcd ๐ต) ยท 1) = (absโ€˜๐ด)))
10197mulridd 7973 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ ((๐ด gcd ๐ต) ยท 1) = (๐ด gcd ๐ต))
102101eqeq1d 2186 . . . . . . . . 9 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (((๐ด gcd ๐ต) ยท 1) = (absโ€˜๐ด) โ†” (๐ด gcd ๐ต) = (absโ€˜๐ด)))
103100, 102bitrd 188 . . . . . . . 8 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (((absโ€˜๐ด) / (๐ด gcd ๐ต)) = 1 โ†” (๐ด gcd ๐ต) = (absโ€˜๐ด)))
104 absdvdsb 11815 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด โˆฅ ๐ต โ†” (absโ€˜๐ด) โˆฅ ๐ต))
105104adantr 276 . . . . . . . 8 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด โˆฅ ๐ต โ†” (absโ€˜๐ด) โˆฅ ๐ต))
10695, 103, 1053imtr4d 203 . . . . . . 7 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (((absโ€˜๐ด) / (๐ด gcd ๐ต)) = 1 โ†’ ๐ด โˆฅ ๐ต))
107 exprmfct 12137 . . . . . . . 8 (((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ โˆƒ๐‘ โˆˆ โ„™ ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))
108 simprl 529 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ๐‘ โˆˆ โ„™)
10974adantr 276 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (absโ€˜๐ด) โˆˆ โ„•)
110109nnzd 9373 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (absโ€˜๐ด) โˆˆ โ„ค)
111109nnne0d 8963 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (absโ€˜๐ด) โ‰  0)
11270adantr 276 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐ด gcd ๐ต) โˆˆ โ„•)
113 pcdiv 12301 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ โ„™ โˆง ((absโ€˜๐ด) โˆˆ โ„ค โˆง (absโ€˜๐ด) โ‰  0) โˆง (๐ด gcd ๐ต) โˆˆ โ„•) โ†’ (๐‘ pCnt ((absโ€˜๐ด) / (๐ด gcd ๐ต))) = ((๐‘ pCnt (absโ€˜๐ด)) โˆ’ (๐‘ pCnt (๐ด gcd ๐ต))))
114108, 110, 111, 112, 113syl121anc 1243 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ((absโ€˜๐ด) / (๐ด gcd ๐ต))) = ((๐‘ pCnt (absโ€˜๐ด)) โˆ’ (๐‘ pCnt (๐ด gcd ๐ต))))
115 simplll 533 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ๐ด โˆˆ โ„ค)
116 zq 9625 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„ค โ†’ ๐ด โˆˆ โ„š)
117115, 116syl 14 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ๐ด โˆˆ โ„š)
118 pcabs 12324 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„™ โˆง ๐ด โˆˆ โ„š) โ†’ (๐‘ pCnt (absโ€˜๐ด)) = (๐‘ pCnt ๐ด))
119108, 117, 118syl2anc 411 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt (absโ€˜๐ด)) = (๐‘ pCnt ๐ด))
120119oveq1d 5889 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((๐‘ pCnt (absโ€˜๐ด)) โˆ’ (๐‘ pCnt (๐ด gcd ๐ต))) = ((๐‘ pCnt ๐ด) โˆ’ (๐‘ pCnt (๐ด gcd ๐ต))))
121114, 120eqtrd 2210 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ((absโ€˜๐ด) / (๐ด gcd ๐ต))) = ((๐‘ pCnt ๐ด) โˆ’ (๐‘ pCnt (๐ด gcd ๐ต))))
122 simprr 531 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))
12389adantr 276 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ โ„•)
124 pcelnn 12319 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ โ„™ โˆง ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ โ„•) โ†’ ((๐‘ pCnt ((absโ€˜๐ด) / (๐ด gcd ๐ต))) โˆˆ โ„• โ†” ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต))))
125108, 123, 124syl2anc 411 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((๐‘ pCnt ((absโ€˜๐ด) / (๐ด gcd ๐ต))) โˆˆ โ„• โ†” ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต))))
126122, 125mpbird 167 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ((absโ€˜๐ด) / (๐ด gcd ๐ต))) โˆˆ โ„•)
127121, 126eqeltrrd 2255 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((๐‘ pCnt ๐ด) โˆ’ (๐‘ pCnt (๐ด gcd ๐ต))) โˆˆ โ„•)
128108, 112pccld 12299 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt (๐ด gcd ๐ต)) โˆˆ โ„•0)
129128nn0zd 9372 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt (๐ด gcd ๐ต)) โˆˆ โ„ค)
130 simplr 528 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ๐ด โ‰  0)
131 pczcl 12297 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ โ„™ โˆง (๐ด โˆˆ โ„ค โˆง ๐ด โ‰  0)) โ†’ (๐‘ pCnt ๐ด) โˆˆ โ„•0)
132108, 115, 130, 131syl12anc 1236 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ๐ด) โˆˆ โ„•0)
133132nn0zd 9372 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ๐ด) โˆˆ โ„ค)
134 znnsub 9303 . . . . . . . . . . . . . 14 (((๐‘ pCnt (๐ด gcd ๐ต)) โˆˆ โ„ค โˆง (๐‘ pCnt ๐ด) โˆˆ โ„ค) โ†’ ((๐‘ pCnt (๐ด gcd ๐ต)) < (๐‘ pCnt ๐ด) โ†” ((๐‘ pCnt ๐ด) โˆ’ (๐‘ pCnt (๐ด gcd ๐ต))) โˆˆ โ„•))
135129, 133, 134syl2anc 411 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((๐‘ pCnt (๐ด gcd ๐ต)) < (๐‘ pCnt ๐ด) โ†” ((๐‘ pCnt ๐ด) โˆ’ (๐‘ pCnt (๐ด gcd ๐ต))) โˆˆ โ„•))
136127, 135mpbird 167 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt (๐ด gcd ๐ต)) < (๐‘ pCnt ๐ด))
137 zltnle 9298 . . . . . . . . . . . . 13 (((๐‘ pCnt (๐ด gcd ๐ต)) โˆˆ โ„ค โˆง (๐‘ pCnt ๐ด) โˆˆ โ„ค) โ†’ ((๐‘ pCnt (๐ด gcd ๐ต)) < (๐‘ pCnt ๐ด) โ†” ยฌ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt (๐ด gcd ๐ต))))
138129, 133, 137syl2anc 411 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((๐‘ pCnt (๐ด gcd ๐ต)) < (๐‘ pCnt ๐ด) โ†” ยฌ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt (๐ด gcd ๐ต))))
139136, 138mpbid 147 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ยฌ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt (๐ด gcd ๐ต)))
140132nn0red 9229 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ๐ด) โˆˆ โ„)
141 simpllr 534 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ๐ต โˆˆ โ„ค)
142 nprmdvds1 12139 . . . . . . . . . . . . . . . . . 18 (๐‘ โˆˆ โ„™ โ†’ ยฌ ๐‘ โˆฅ 1)
143142ad2antrl 490 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ยฌ ๐‘ โˆฅ 1)
144 gcdid0 11980 . . . . . . . . . . . . . . . . . . . . 21 (๐ด โˆˆ โ„ค โ†’ (๐ด gcd 0) = (absโ€˜๐ด))
145115, 144syl 14 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐ด gcd 0) = (absโ€˜๐ด))
146145oveq2d 5890 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((absโ€˜๐ด) / (๐ด gcd 0)) = ((absโ€˜๐ด) / (absโ€˜๐ด)))
14796adantr 276 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
148109nnap0d 8964 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (absโ€˜๐ด) # 0)
149147, 148dividapd 8742 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((absโ€˜๐ด) / (absโ€˜๐ด)) = 1)
150146, 149eqtrd 2210 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((absโ€˜๐ด) / (๐ด gcd 0)) = 1)
151150breq2d 4015 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd 0)) โ†” ๐‘ โˆฅ 1))
152143, 151mtbird 673 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ยฌ ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd 0)))
153 oveq2 5882 . . . . . . . . . . . . . . . . . . . 20 (๐ต = 0 โ†’ (๐ด gcd ๐ต) = (๐ด gcd 0))
154153oveq2d 5890 . . . . . . . . . . . . . . . . . . 19 (๐ต = 0 โ†’ ((absโ€˜๐ด) / (๐ด gcd ๐ต)) = ((absโ€˜๐ด) / (๐ด gcd 0)))
155154breq2d 4015 . . . . . . . . . . . . . . . . . 18 (๐ต = 0 โ†’ (๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โ†” ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd 0))))
156122, 155syl5ibcom 155 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐ต = 0 โ†’ ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd 0))))
157156necon3bd 2390 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (ยฌ ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd 0)) โ†’ ๐ต โ‰  0))
158152, 157mpd 13 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ๐ต โ‰  0)
159108, 141, 158, 33syl12anc 1236 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„•0)
160159nn0red 9229 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„)
161 lemininf 11241 . . . . . . . . . . . . 13 (((๐‘ pCnt ๐ด) โˆˆ โ„ โˆง (๐‘ pCnt ๐ด) โˆˆ โ„ โˆง (๐‘ pCnt ๐ต) โˆˆ โ„) โ†’ ((๐‘ pCnt ๐ด) โ‰ค inf({(๐‘ pCnt ๐ด), (๐‘ pCnt ๐ต)}, โ„, < ) โ†” ((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ด) โˆง (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต))))
162140, 140, 160, 161syl3anc 1238 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((๐‘ pCnt ๐ด) โ‰ค inf({(๐‘ pCnt ๐ด), (๐‘ pCnt ๐ต)}, โ„, < ) โ†” ((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ด) โˆง (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต))))
163 pcgcd 12327 . . . . . . . . . . . . . . 15 ((๐‘ โˆˆ โ„™ โˆง ๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐‘ pCnt (๐ด gcd ๐ต)) = if((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต), (๐‘ pCnt ๐ด), (๐‘ pCnt ๐ต)))
164108, 115, 141, 163syl3anc 1238 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt (๐ด gcd ๐ต)) = if((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต), (๐‘ pCnt ๐ด), (๐‘ pCnt ๐ต)))
165159nn0zd 9372 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„ค)
166 2zinfmin 11250 . . . . . . . . . . . . . . 15 (((๐‘ pCnt ๐ด) โˆˆ โ„ค โˆง (๐‘ pCnt ๐ต) โˆˆ โ„ค) โ†’ inf({(๐‘ pCnt ๐ด), (๐‘ pCnt ๐ต)}, โ„, < ) = if((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต), (๐‘ pCnt ๐ด), (๐‘ pCnt ๐ต)))
167133, 165, 166syl2anc 411 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ inf({(๐‘ pCnt ๐ด), (๐‘ pCnt ๐ต)}, โ„, < ) = if((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต), (๐‘ pCnt ๐ด), (๐‘ pCnt ๐ต)))
168164, 167eqtr4d 2213 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt (๐ด gcd ๐ต)) = inf({(๐‘ pCnt ๐ด), (๐‘ pCnt ๐ต)}, โ„, < ))
169168breq2d 4015 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt (๐ด gcd ๐ต)) โ†” (๐‘ pCnt ๐ด) โ‰ค inf({(๐‘ pCnt ๐ด), (๐‘ pCnt ๐ต)}, โ„, < )))
170140leidd 8470 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ด))
171170biantrurd 305 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†” ((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ด) โˆง (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต))))
172162, 169, 1713bitr4rd 221 . . . . . . . . . . 11 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†” (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt (๐ด gcd ๐ต))))
173139, 172mtbird 673 . . . . . . . . . 10 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ยฌ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต))
174173expr 375 . . . . . . . . 9 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง ๐‘ โˆˆ โ„™) โ†’ (๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โ†’ ยฌ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต)))
175174reximdva 2579 . . . . . . . 8 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (โˆƒ๐‘ โˆˆ โ„™ ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โ†’ โˆƒ๐‘ โˆˆ โ„™ ยฌ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต)))
176 rexnalim 2466 . . . . . . . 8 (โˆƒ๐‘ โˆˆ โ„™ ยฌ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†’ ยฌ โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต))
177107, 175, 176syl56 34 . . . . . . 7 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ยฌ โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต)))
178106, 177orim12d 786 . . . . . 6 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ ((((absโ€˜๐ด) / (๐ด gcd ๐ต)) = 1 โˆจ ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ (๐ด โˆฅ ๐ต โˆจ ยฌ โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต))))
17991, 178mpd 13 . . . . 5 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด โˆฅ ๐ต โˆจ ยฌ โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต)))
180179ord 724 . . . 4 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (ยฌ ๐ด โˆฅ ๐ต โ†’ ยฌ โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต)))
181 condc 853 . . . 4 (DECID ๐ด โˆฅ ๐ต โ†’ ((ยฌ ๐ด โˆฅ ๐ต โ†’ ยฌ โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต)) โ†’ (โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†’ ๐ด โˆฅ ๐ต)))
18257, 180, 181sylc 62 . . 3 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†’ ๐ด โˆฅ ๐ต))
183 0zd 9264 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ 0 โˆˆ โ„ค)
184 zdceq 9327 . . . . 5 ((๐ด โˆˆ โ„ค โˆง 0 โˆˆ โ„ค) โ†’ DECID ๐ด = 0)
18562, 183, 184syl2anc 411 . . . 4 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ DECID ๐ด = 0)
186 dcne 2358 . . . 4 (DECID ๐ด = 0 โ†” (๐ด = 0 โˆจ ๐ด โ‰  0))
187185, 186sylib 122 . . 3 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด = 0 โˆจ ๐ด โ‰  0))
18855, 182, 187mpjaodan 798 . 2 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†’ ๐ด โˆฅ ๐ต))
1894, 188impbid 129 1 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด โˆฅ ๐ต โ†” โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต)))
Colors of variables: wff set class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆจ wo 708  DECID wdc 834   โˆง w3a 978   = wceq 1353  โˆƒwex 1492   โˆˆ wcel 2148   โ‰  wne 2347  โˆ€wral 2455  โˆƒwrex 2456  ifcif 3534  {cpr 3593   class class class wbr 4003  โ€˜cfv 5216  (class class class)co 5874  infcinf 6981  โ„‚cc 7808  โ„cr 7809  0cc0 7810  1c1 7811   ยท cmul 7815  +โˆžcpnf 7988  โ„*cxr 7990   < clt 7991   โ‰ค cle 7992   โˆ’ cmin 8127   / cdiv 8628  โ„•cn 8918  2c2 8969  โ„•0cn0 9175  โ„คcz 9252  โ„คโ‰ฅcuz 9527  โ„šcq 9618  abscabs 11005   โˆฅ cdvds 11793   gcd cgcd 11942  โ„™cprime 12106   pCnt cpc 12283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulrcl 7909  ax-addcom 7910  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-1rid 7917  ax-0id 7918  ax-rnegex 7919  ax-precex 7920  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-apti 7925  ax-pre-ltadd 7926  ax-pre-mulgt0 7927  ax-pre-mulext 7928  ax-arch 7929  ax-caucvg 7930
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-po 4296  df-iso 4297  df-iord 4366  df-on 4368  df-ilim 4369  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-isom 5225  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-frec 6391  df-1o 6416  df-2o 6417  df-er 6534  df-en 6740  df-sup 6982  df-inf 6983  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-reap 8531  df-ap 8538  df-div 8629  df-inn 8919  df-2 8977  df-3 8978  df-4 8979  df-n0 9176  df-xnn0 9239  df-z 9253  df-uz 9528  df-q 9619  df-rp 9653  df-fz 10008  df-fzo 10142  df-fl 10269  df-mod 10322  df-seqfrec 10445  df-exp 10519  df-cj 10850  df-re 10851  df-im 10852  df-rsqrt 11006  df-abs 11007  df-dvds 11794  df-gcd 11943  df-prm 12107  df-pc 12284
This theorem is referenced by:  pc11  12329  pcz  12330  pcprmpw2  12331  pockthg  12354
  Copyright terms: Public domain W3C validator