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

Theorem pc2dvds 12332
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 12329 . . . . 5 ((๐‘ โˆˆ โ„™ โˆง (๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ด โˆฅ ๐ต)) โ†’ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต))
21ancoms 268 . . . 4 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ด โˆฅ ๐ต) โˆง ๐‘ โˆˆ โ„™) โ†’ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต))
32ralrimiva 2550 . . 3 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ด โˆฅ ๐ต) โ†’ โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต))
433expia 1205 . 2 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด โˆฅ ๐ต โ†’ โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต)))
5 2prm 12130 . . . . . . . 8 2 โˆˆ โ„™
6 elex2 2755 . . . . . . . 8 (2 โˆˆ โ„™ โ†’ โˆƒ๐‘ค ๐‘ค โˆˆ โ„™)
75, 6ax-mp 5 . . . . . . 7 โˆƒ๐‘ค ๐‘ค โˆˆ โ„™
8 r19.2m 3511 . . . . . . 7 ((โˆƒ๐‘ค ๐‘ค โˆˆ โ„™ โˆง โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต)) โ†’ โˆƒ๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต))
97, 8mpan 424 . . . . . 6 (โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†’ โˆƒ๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต))
10 id 19 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„™ โ†’ ๐‘ โˆˆ โ„™)
11 zq 9629 . . . . . . . . . . . . . 14 (๐ต โˆˆ โ„ค โ†’ ๐ต โˆˆ โ„š)
1211adantl 277 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ ๐ต โˆˆ โ„š)
13 pcxcl 12314 . . . . . . . . . . . . 13 ((๐‘ โˆˆ โ„™ โˆง ๐ต โˆˆ โ„š) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„*)
1410, 12, 13syl2anr 290 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„*)
15 pnfge 9792 . . . . . . . . . . . 12 ((๐‘ pCnt ๐ต) โˆˆ โ„* โ†’ (๐‘ pCnt ๐ต) โ‰ค +โˆž)
1614, 15syl 14 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ (๐‘ pCnt ๐ต) โ‰ค +โˆž)
1716biantrurd 305 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ (+โˆž โ‰ค (๐‘ pCnt ๐ต) โ†” ((๐‘ pCnt ๐ต) โ‰ค +โˆž โˆง +โˆž โ‰ค (๐‘ pCnt ๐ต))))
18 pc0 12307 . . . . . . . . . . . 12 (๐‘ โˆˆ โ„™ โ†’ (๐‘ pCnt 0) = +โˆž)
1918adantl 277 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ (๐‘ pCnt 0) = +โˆž)
2019breq1d 4015 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ ((๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†” +โˆž โ‰ค (๐‘ pCnt ๐ต)))
21 pnfxr 8013 . . . . . . . . . . 11 +โˆž โˆˆ โ„*
22 xrletri3 9807 . . . . . . . . . . 11 (((๐‘ pCnt ๐ต) โˆˆ โ„* โˆง +โˆž โˆˆ โ„*) โ†’ ((๐‘ pCnt ๐ต) = +โˆž โ†” ((๐‘ pCnt ๐ต) โ‰ค +โˆž โˆง +โˆž โ‰ค (๐‘ pCnt ๐ต))))
2314, 21, 22sylancl 413 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ ((๐‘ pCnt ๐ต) = +โˆž โ†” ((๐‘ pCnt ๐ต) โ‰ค +โˆž โˆง +โˆž โ‰ค (๐‘ pCnt ๐ต))))
2417, 20, 233bitr4d 220 . . . . . . . . 9 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ ((๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต) โ†” (๐‘ pCnt ๐ต) = +โˆž))
25 pnfnre 8002 . . . . . . . . . . . 12 +โˆž โˆ‰ โ„
2625neli 2444 . . . . . . . . . . 11 ยฌ +โˆž โˆˆ โ„
27 eleq1 2240 . . . . . . . . . . 11 ((๐‘ pCnt ๐ต) = +โˆž โ†’ ((๐‘ pCnt ๐ต) โˆˆ โ„ โ†” +โˆž โˆˆ โ„))
2826, 27mtbiri 675 . . . . . . . . . 10 ((๐‘ pCnt ๐ต) = +โˆž โ†’ ยฌ (๐‘ pCnt ๐ต) โˆˆ โ„)
29 simplr 528 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ ๐ต โˆˆ โ„ค)
30 0zd 9268 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ 0 โˆˆ โ„ค)
31 zdceq 9331 . . . . . . . . . . . 12 ((๐ต โˆˆ โ„ค โˆง 0 โˆˆ โ„ค) โ†’ DECID ๐ต = 0)
3229, 30, 31syl2anc 411 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘ โˆˆ โ„™) โ†’ DECID ๐ต = 0)
33 pczcl 12301 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„™ โˆง (๐ต โˆˆ โ„ค โˆง ๐ต โ‰  0)) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„•0)
3433nn0red 9233 . . . . . . . . . . . . . . . 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 11821 . . . . . . . 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 5886 . . . . . . . 8 (๐ด = 0 โ†’ (๐‘ pCnt ๐ด) = (๐‘ pCnt 0))
5049breq1d 4015 . . . . . . 7 (๐ด = 0 โ†’ ((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†” (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต)))
5150ralbidv 2477 . . . . . 6 (๐ด = 0 โ†’ (โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt ๐ต) โ†” โˆ€๐‘ โˆˆ โ„™ (๐‘ pCnt 0) โ‰ค (๐‘ pCnt ๐ต)))
52 breq1 4008 . . . . . 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 11822 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ DECID ๐ด โˆฅ ๐ต)
5756adantr 276 . . . 4 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ DECID ๐ด โˆฅ ๐ต)
58 gcddvds 11967 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ ((๐ด gcd ๐ต) โˆฅ ๐ด โˆง (๐ด gcd ๐ต) โˆฅ ๐ต))
5958simpld 112 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด gcd ๐ต) โˆฅ ๐ด)
60 gcdcl 11970 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด gcd ๐ต) โˆˆ โ„•0)
6160nn0zd 9376 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด gcd ๐ต) โˆˆ โ„ค)
62 simpl 109 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ ๐ด โˆˆ โ„ค)
63 dvdsabsb 11820 . . . . . . . . . . . 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 11966 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ยฌ (๐ด = 0 โˆง ๐ต = 0)) โ†’ (๐ด gcd ๐ต) โˆˆ โ„•)
7068, 69sylan2 286 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด gcd ๐ต) โˆˆ โ„•)
7170nnzd 9377 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด gcd ๐ต) โˆˆ โ„ค)
7270nnne0d 8967 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด gcd ๐ต) โ‰  0)
73 nnabscl 11112 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„•)
7473adantlr 477 . . . . . . . . . . 11 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„•)
7574nnzd 9377 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„ค)
76 dvdsval2 11800 . . . . . . . . . 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 8929 . . . . . . . . . . 11 ((absโ€˜๐ด) โˆˆ โ„• โ†’ (absโ€˜๐ด) โˆˆ โ„)
80 nngt0 8947 . . . . . . . . . . 11 ((absโ€˜๐ด) โˆˆ โ„• โ†’ 0 < (absโ€˜๐ด))
8179, 80jca 306 . . . . . . . . . 10 ((absโ€˜๐ด) โˆˆ โ„• โ†’ ((absโ€˜๐ด) โˆˆ โ„ โˆง 0 < (absโ€˜๐ด)))
82 nnre 8929 . . . . . . . . . . 11 ((๐ด gcd ๐ต) โˆˆ โ„• โ†’ (๐ด gcd ๐ต) โˆˆ โ„)
83 nngt0 8947 . . . . . . . . . . 11 ((๐ด gcd ๐ต) โˆˆ โ„• โ†’ 0 < (๐ด gcd ๐ต))
8482, 83jca 306 . . . . . . . . . 10 ((๐ด gcd ๐ต) โˆˆ โ„• โ†’ ((๐ด gcd ๐ต) โˆˆ โ„ โˆง 0 < (๐ด gcd ๐ต)))
85 divgt0 8832 . . . . . . . . . 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 9266 . . . . . . . 8 (((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ โ„• โ†” (((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ โ„ค โˆง 0 < ((absโ€˜๐ด) / (๐ด gcd ๐ต))))
8978, 87, 88sylanbrc 417 . . . . . . 7 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ ((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ โ„•)
90 elnn1uz2 9610 . . . . . . 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 4008 . . . . . . . . 9 ((๐ด gcd ๐ต) = (absโ€˜๐ด) โ†’ ((๐ด gcd ๐ต) โˆฅ ๐ต โ†” (absโ€˜๐ด) โˆฅ ๐ต))
9593, 94syl5ibcom 155 . . . . . . . 8 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ ((๐ด gcd ๐ต) = (absโ€˜๐ด) โ†’ (absโ€˜๐ด) โˆฅ ๐ต))
9674nncnd 8936 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
9770nncnd 8936 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด gcd ๐ต) โˆˆ โ„‚)
98 1cnd 7976 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ 1 โˆˆ โ„‚)
9970nnap0d 8968 . . . . . . . . . 10 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด gcd ๐ต) # 0)
10096, 97, 98, 99divmulapd 8772 . . . . . . . . 9 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (((absโ€˜๐ด) / (๐ด gcd ๐ต)) = 1 โ†” ((๐ด gcd ๐ต) ยท 1) = (absโ€˜๐ด)))
10197mulridd 7977 . . . . . . . . . 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 11819 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด โˆฅ ๐ต โ†” (absโ€˜๐ด) โˆฅ ๐ต))
105104adantr 276 . . . . . . . 8 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (๐ด โˆฅ ๐ต โ†” (absโ€˜๐ด) โˆฅ ๐ต))
10695, 103, 1053imtr4d 203 . . . . . . 7 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โ†’ (((absโ€˜๐ด) / (๐ด gcd ๐ต)) = 1 โ†’ ๐ด โˆฅ ๐ต))
107 exprmfct 12141 . . . . . . . 8 (((absโ€˜๐ด) / (๐ด gcd ๐ต)) โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ โˆƒ๐‘ โˆˆ โ„™ ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))
108 simprl 529 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ๐‘ โˆˆ โ„™)
10974adantr 276 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (absโ€˜๐ด) โˆˆ โ„•)
110109nnzd 9377 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (absโ€˜๐ด) โˆˆ โ„ค)
111109nnne0d 8967 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (absโ€˜๐ด) โ‰  0)
11270adantr 276 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐ด gcd ๐ต) โˆˆ โ„•)
113 pcdiv 12305 . . . . . . . . . . . . . . . 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 9629 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„ค โ†’ ๐ด โˆˆ โ„š)
117115, 116syl 14 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ๐ด โˆˆ โ„š)
118 pcabs 12328 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„™ โˆง ๐ด โˆˆ โ„š) โ†’ (๐‘ pCnt (absโ€˜๐ด)) = (๐‘ pCnt ๐ด))
119108, 117, 118syl2anc 411 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt (absโ€˜๐ด)) = (๐‘ pCnt ๐ด))
120119oveq1d 5893 . . . . . . . . . . . . . . 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 12323 . . . . . . . . . . . . . . . 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 12303 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt (๐ด gcd ๐ต)) โˆˆ โ„•0)
129128nn0zd 9376 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt (๐ด gcd ๐ต)) โˆˆ โ„ค)
130 simplr 528 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ๐ด โ‰  0)
131 pczcl 12301 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ โ„™ โˆง (๐ด โˆˆ โ„ค โˆง ๐ด โ‰  0)) โ†’ (๐‘ pCnt ๐ด) โˆˆ โ„•0)
132108, 115, 130, 131syl12anc 1236 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ๐ด) โˆˆ โ„•0)
133132nn0zd 9376 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ๐ด) โˆˆ โ„ค)
134 znnsub 9307 . . . . . . . . . . . . . 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 9302 . . . . . . . . . . . . 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 9233 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ๐ด) โˆˆ โ„)
141 simpllr 534 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ๐ต โˆˆ โ„ค)
142 nprmdvds1 12143 . . . . . . . . . . . . . . . . . 18 (๐‘ โˆˆ โ„™ โ†’ ยฌ ๐‘ โˆฅ 1)
143142ad2antrl 490 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ยฌ ๐‘ โˆฅ 1)
144 gcdid0 11984 . . . . . . . . . . . . . . . . . . . . 21 (๐ด โˆˆ โ„ค โ†’ (๐ด gcd 0) = (absโ€˜๐ด))
145115, 144syl 14 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐ด gcd 0) = (absโ€˜๐ด))
146145oveq2d 5894 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((absโ€˜๐ด) / (๐ด gcd 0)) = ((absโ€˜๐ด) / (absโ€˜๐ด)))
14796adantr 276 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
148109nnap0d 8968 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (absโ€˜๐ด) # 0)
149147, 148dividapd 8746 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((absโ€˜๐ด) / (absโ€˜๐ด)) = 1)
150146, 149eqtrd 2210 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((absโ€˜๐ด) / (๐ด gcd 0)) = 1)
151150breq2d 4017 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd 0)) โ†” ๐‘ โˆฅ 1))
152143, 151mtbird 673 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ยฌ ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd 0)))
153 oveq2 5886 . . . . . . . . . . . . . . . . . . . 20 (๐ต = 0 โ†’ (๐ด gcd ๐ต) = (๐ด gcd 0))
154153oveq2d 5894 . . . . . . . . . . . . . . . . . . 19 (๐ต = 0 โ†’ ((absโ€˜๐ด) / (๐ด gcd ๐ต)) = ((absโ€˜๐ด) / (๐ด gcd 0)))
155154breq2d 4017 . . . . . . . . . . . . . . . . . 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 9233 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„)
161 lemininf 11245 . . . . . . . . . . . . 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 12331 . . . . . . . . . . . . . . 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 9376 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ (๐‘ pCnt ๐ต) โˆˆ โ„ค)
166 2zinfmin 11254 . . . . . . . . . . . . . . 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 4017 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐ด โ‰  0) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ((absโ€˜๐ด) / (๐ด gcd ๐ต)))) โ†’ ((๐‘ pCnt ๐ด) โ‰ค (๐‘ pCnt (๐ด gcd ๐ต)) โ†” (๐‘ pCnt ๐ด) โ‰ค inf({(๐‘ pCnt ๐ด), (๐‘ pCnt ๐ต)}, โ„, < )))
170140leidd 8474 . . . . . . . . . . . . 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 9268 . . . . 5 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ 0 โˆˆ โ„ค)
184 zdceq 9331 . . . . 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 3536  {cpr 3595   class class class wbr 4005  โ€˜cfv 5218  (class class class)co 5878  infcinf 6985  โ„‚cc 7812  โ„cr 7813  0cc0 7814  1c1 7815   ยท cmul 7819  +โˆžcpnf 7992  โ„*cxr 7994   < clt 7995   โ‰ค cle 7996   โˆ’ cmin 8131   / cdiv 8632  โ„•cn 8922  2c2 8973  โ„•0cn0 9179  โ„คcz 9256  โ„คโ‰ฅcuz 9531  โ„šcq 9622  abscabs 11009   โˆฅ cdvds 11797   gcd cgcd 11946  โ„™cprime 12110   pCnt cpc 12287
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 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589  ax-cnex 7905  ax-resscn 7906  ax-1cn 7907  ax-1re 7908  ax-icn 7909  ax-addcl 7910  ax-addrcl 7911  ax-mulcl 7912  ax-mulrcl 7913  ax-addcom 7914  ax-mulcom 7915  ax-addass 7916  ax-mulass 7917  ax-distr 7918  ax-i2m1 7919  ax-0lt1 7920  ax-1rid 7921  ax-0id 7922  ax-rnegex 7923  ax-precex 7924  ax-cnre 7925  ax-pre-ltirr 7926  ax-pre-ltwlin 7927  ax-pre-lttrn 7928  ax-pre-apti 7929  ax-pre-ltadd 7930  ax-pre-mulgt0 7931  ax-pre-mulext 7932  ax-arch 7933  ax-caucvg 7934
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 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-po 4298  df-iso 4299  df-iord 4368  df-on 4370  df-ilim 4371  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-isom 5227  df-riota 5834  df-ov 5881  df-oprab 5882  df-mpo 5883  df-1st 6144  df-2nd 6145  df-recs 6309  df-frec 6395  df-1o 6420  df-2o 6421  df-er 6538  df-en 6744  df-sup 6986  df-inf 6987  df-pnf 7997  df-mnf 7998  df-xr 7999  df-ltxr 8000  df-le 8001  df-sub 8133  df-neg 8134  df-reap 8535  df-ap 8542  df-div 8633  df-inn 8923  df-2 8981  df-3 8982  df-4 8983  df-n0 9180  df-xnn0 9243  df-z 9257  df-uz 9532  df-q 9623  df-rp 9657  df-fz 10012  df-fzo 10146  df-fl 10273  df-mod 10326  df-seqfrec 10449  df-exp 10523  df-cj 10854  df-re 10855  df-im 10856  df-rsqrt 11010  df-abs 11011  df-dvds 11798  df-gcd 11947  df-prm 12111  df-pc 12288
This theorem is referenced by:  pc11  12333  pcz  12334  pcprmpw2  12335  pockthg  12358
  Copyright terms: Public domain W3C validator