Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aks6d1c2p2 Structured version   Visualization version   GIF version
Theorem aks6d1c2p2 40946
Description: Injective condition for countability argument assuming that 𝑁 is not a prime power. (Contributed by metakunt, 7-Jan-2025.)
Hypotheses
Ref Expression
aks6d1c2p2.1 (πœ‘ β†’ 𝑁 ∈ β„•)
aks6d1c2p2.2 (πœ‘ β†’ 𝑃 ∈ β„™)
aks6d1c2p2.3 (πœ‘ β†’ 𝑃 βˆ₯ 𝑁)
aks6d1c2p2.4 𝐸 = (π‘˜ ∈ β„•0, 𝑙 ∈ β„•0 ↦ ((π‘ƒβ†‘π‘˜) Β· ((𝑁 / 𝑃)↑𝑙)))
aks6d1c2p2.5 (πœ‘ β†’ 𝑄 ∈ β„™)
aks6d1c2p2.6 (πœ‘ β†’ 𝑄 βˆ₯ 𝑁)
aks6d1c2p2.7 (πœ‘ β†’ 𝑃 β‰  𝑄)
Assertion
Ref Expression
aks6d1c2p2 (πœ‘ β†’ 𝐸:(β„•0 Γ— β„•0)–1-1β†’β„•)
Distinct variable groups:   π‘˜,𝑁,𝑙   𝑃,π‘˜,𝑙   πœ‘,π‘˜,𝑙
Allowed substitution hints:   𝑄(π‘˜,𝑙)   𝐸(π‘˜,𝑙)
Proof of Theorem aks6d1c2p2
Dummy variables π‘Ž 𝑏 𝑐 𝑑 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 aks6d1c2p2.1 . . . 4 (πœ‘ β†’ 𝑁 ∈ β„•)
2 aks6d1c2p2.2 . . . 4 (πœ‘ β†’ 𝑃 ∈ β„™)
3 aks6d1c2p2.3 . . . 4 (πœ‘ β†’ 𝑃 βˆ₯ 𝑁)
4 aks6d1c2p2.4 . . . 4 𝐸 = (π‘˜ ∈ β„•0, 𝑙 ∈ β„•0 ↦ ((π‘ƒβ†‘π‘˜) Β· ((𝑁 / 𝑃)↑𝑙)))
51, 2, 3, 4aks6d1c2p1 40945 . . 3 (πœ‘ β†’ 𝐸:(β„•0 Γ— β„•0)βŸΆβ„•)
6 neneq 2947 . . . . . . . . . . . . . . . . 17 (𝑏 β‰  𝑑 β†’ Β¬ 𝑏 = 𝑑)
76orcd 872 . . . . . . . . . . . . . . . 16 (𝑏 β‰  𝑑 β†’ (Β¬ 𝑏 = 𝑑 ∨ Β¬ π‘Ž = 𝑐))
8 simpr 486 . . . . . . . . . . . . . . . . . 18 ((𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐) β†’ π‘Ž β‰  𝑐)
98neneqd 2946 . . . . . . . . . . . . . . . . 17 ((𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐) β†’ Β¬ π‘Ž = 𝑐)
109olcd 873 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐) β†’ (Β¬ 𝑏 = 𝑑 ∨ Β¬ π‘Ž = 𝑐))
117, 10jaoi 856 . . . . . . . . . . . . . . 15 ((𝑏 β‰  𝑑 ∨ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (Β¬ 𝑏 = 𝑑 ∨ Β¬ π‘Ž = 𝑐))
12 neqne 2949 . . . . . . . . . . . . . . . . 17 (Β¬ 𝑏 = 𝑑 β†’ 𝑏 β‰  𝑑)
1312orcd 872 . . . . . . . . . . . . . . . 16 (Β¬ 𝑏 = 𝑑 β†’ (𝑏 β‰  𝑑 ∨ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)))
14 neqne 2949 . . . . . . . . . . . . . . . . . . 19 (Β¬ π‘Ž = 𝑐 β†’ π‘Ž β‰  𝑐)
1514anim1ci 617 . . . . . . . . . . . . . . . . . 18 ((Β¬ π‘Ž = 𝑐 ∧ 𝑏 = 𝑑) β†’ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐))
1615olcd 873 . . . . . . . . . . . . . . . . 17 ((Β¬ π‘Ž = 𝑐 ∧ 𝑏 = 𝑑) β†’ (𝑏 β‰  𝑑 ∨ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)))
1713adantl 483 . . . . . . . . . . . . . . . . 17 ((Β¬ π‘Ž = 𝑐 ∧ Β¬ 𝑏 = 𝑑) β†’ (𝑏 β‰  𝑑 ∨ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)))
1816, 17pm2.61dan 812 . . . . . . . . . . . . . . . 16 (Β¬ π‘Ž = 𝑐 β†’ (𝑏 β‰  𝑑 ∨ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)))
1913, 18jaoi 856 . . . . . . . . . . . . . . 15 ((Β¬ 𝑏 = 𝑑 ∨ Β¬ π‘Ž = 𝑐) β†’ (𝑏 β‰  𝑑 ∨ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)))
2011, 19impbii 208 . . . . . . . . . . . . . 14 ((𝑏 β‰  𝑑 ∨ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) ↔ (Β¬ 𝑏 = 𝑑 ∨ Β¬ π‘Ž = 𝑐))
21 orcom 869 . . . . . . . . . . . . . 14 ((Β¬ 𝑏 = 𝑑 ∨ Β¬ π‘Ž = 𝑐) ↔ (Β¬ π‘Ž = 𝑐 ∨ Β¬ 𝑏 = 𝑑))
2220, 21bitri 275 . . . . . . . . . . . . 13 ((𝑏 β‰  𝑑 ∨ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) ↔ (Β¬ π‘Ž = 𝑐 ∨ Β¬ 𝑏 = 𝑑))
23 ianor 981 . . . . . . . . . . . . . 14 (Β¬ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑) ↔ (Β¬ π‘Ž = 𝑐 ∨ Β¬ 𝑏 = 𝑑))
2423bicomi 223 . . . . . . . . . . . . 13 ((Β¬ π‘Ž = 𝑐 ∨ Β¬ 𝑏 = 𝑑) ↔ Β¬ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑))
2522, 24bitri 275 . . . . . . . . . . . 12 ((𝑏 β‰  𝑑 ∨ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) ↔ Β¬ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑))
26 aks6d1c2p2.5 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑄 ∈ β„™)
2726ad5antr 733 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ 𝑄 ∈ β„™)
28 simpr 486 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) ∧ 𝑝 = 𝑄) β†’ 𝑝 = 𝑄)
2928oveq1d 7421 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) ∧ 𝑝 = 𝑄) β†’ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑄 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))))
3028oveq1d 7421 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) ∧ 𝑝 = 𝑄) β†’ (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) = (𝑄 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
3129, 30neeq12d 3003 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) ∧ 𝑝 = 𝑄) β†’ ((𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) ↔ (𝑄 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑄 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
32 0cnd 11204 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ 0 ∈ β„‚)
33 prmnn 16608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„•)
342, 33syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ 𝑃 ∈ β„•)
351, 34jca 513 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝑁 ∈ β„• ∧ 𝑃 ∈ β„•))
36 nndivdvds 16203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ β„• ∧ 𝑃 ∈ β„•) β†’ (𝑃 βˆ₯ 𝑁 ↔ (𝑁 / 𝑃) ∈ β„•))
3735, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝑃 βˆ₯ 𝑁 ↔ (𝑁 / 𝑃) ∈ β„•))
383, 37mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝑁 / 𝑃) ∈ β„•)
3938adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘Ž ∈ β„•0) β†’ (𝑁 / 𝑃) ∈ β„•)
4039adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) β†’ (𝑁 / 𝑃) ∈ β„•)
4140ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑁 / 𝑃) ∈ β„•)
4241adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑁 / 𝑃) ∈ β„•)
43 simp-4r 783 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ 𝑏 ∈ β„•0)
4442, 43nnexpcld 14205 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ ((𝑁 / 𝑃)↑𝑏) ∈ β„•)
4527, 44pccld 16780 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏)) ∈ β„•0)
4645nn0cnd 12531 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏)) ∈ β„‚)
47 simplr 768 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ 𝑑 ∈ β„•0)
4842, 47nnexpcld 14205 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ ((𝑁 / 𝑃)↑𝑑) ∈ β„•)
4927, 48pccld 16780 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑)) ∈ β„•0)
5049nn0cnd 12531 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑)) ∈ β„‚)
51 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ 𝑏 β‰  𝑑)
5243nn0cnd 12531 . . . . . . . . . . . . . . . . . . . . . 22 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ 𝑏 ∈ β„‚)
5347nn0cnd 12531 . . . . . . . . . . . . . . . . . . . . . 22 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ 𝑑 ∈ β„‚)
5427, 42pccld 16780 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt (𝑁 / 𝑃)) ∈ β„•0)
5554nn0cnd 12531 . . . . . . . . . . . . . . . . . . . . . 22 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt (𝑁 / 𝑃)) ∈ β„‚)
56 simp-5l 784 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ πœ‘)
57 aks6d1c2p2.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ 𝑄 βˆ₯ 𝑁)
581nncnd 12225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (πœ‘ β†’ 𝑁 ∈ β„‚)
5934nncnd 12225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (πœ‘ β†’ 𝑃 ∈ β„‚)
6034nnne0d 12259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (πœ‘ β†’ 𝑃 β‰  0)
6158, 59, 60divcan2d 11989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ (𝑃 Β· (𝑁 / 𝑃)) = 𝑁)
6261eqcomd 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ 𝑁 = (𝑃 Β· (𝑁 / 𝑃)))
6362breq2d 5160 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝑄 βˆ₯ 𝑁 ↔ 𝑄 βˆ₯ (𝑃 Β· (𝑁 / 𝑃))))
6457, 63mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝑄 βˆ₯ (𝑃 Β· (𝑁 / 𝑃)))
6534nnzd 12582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ 𝑃 ∈ β„€)
6638nnzd 12582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ (𝑁 / 𝑃) ∈ β„€)
67 euclemma 16647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑄 ∈ β„™ ∧ 𝑃 ∈ β„€ ∧ (𝑁 / 𝑃) ∈ β„€) β†’ (𝑄 βˆ₯ (𝑃 Β· (𝑁 / 𝑃)) ↔ (𝑄 βˆ₯ 𝑃 ∨ 𝑄 βˆ₯ (𝑁 / 𝑃))))
6826, 65, 66, 67syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝑄 βˆ₯ (𝑃 Β· (𝑁 / 𝑃)) ↔ (𝑄 βˆ₯ 𝑃 ∨ 𝑄 βˆ₯ (𝑁 / 𝑃))))
6968biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝑄 βˆ₯ (𝑃 Β· (𝑁 / 𝑃)) β†’ (𝑄 βˆ₯ 𝑃 ∨ 𝑄 βˆ₯ (𝑁 / 𝑃))))
7064, 69mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝑄 βˆ₯ 𝑃 ∨ 𝑄 βˆ₯ (𝑁 / 𝑃)))
71 aks6d1c2p2.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (πœ‘ β†’ 𝑃 β‰  𝑄)
72 necom 2995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑃 β‰  𝑄 ↔ 𝑄 β‰  𝑃)
7372imbi2i 336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ β†’ 𝑃 β‰  𝑄) ↔ (πœ‘ β†’ 𝑄 β‰  𝑃))
7471, 73mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ 𝑄 β‰  𝑃)
7574neneqd 2946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ Β¬ 𝑄 = 𝑃)
76 1red 11212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (πœ‘ β†’ 1 ∈ ℝ)
77 prmgt1 16631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑄 ∈ β„™ β†’ 1 < 𝑄)
7826, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (πœ‘ β†’ 1 < 𝑄)
7976, 78ltned 11347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (πœ‘ β†’ 1 β‰  𝑄)
8079necomd 2997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ 𝑄 β‰  1)
8180neneqd 2946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ Β¬ 𝑄 = 1)
8275, 81jca 513 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (Β¬ 𝑄 = 𝑃 ∧ Β¬ 𝑄 = 1))
83 pm4.56 988 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Β¬ 𝑄 = 𝑃 ∧ Β¬ 𝑄 = 1) ↔ Β¬ (𝑄 = 𝑃 ∨ 𝑄 = 1))
8482, 83sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ Β¬ (𝑄 = 𝑃 ∨ 𝑄 = 1))
85 prmnn 16608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑄 ∈ β„™ β†’ 𝑄 ∈ β„•)
8626, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ 𝑄 ∈ β„•)
87 dvdsprime 16621 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑃 ∈ β„™ ∧ 𝑄 ∈ β„•) β†’ (𝑄 βˆ₯ 𝑃 ↔ (𝑄 = 𝑃 ∨ 𝑄 = 1)))
882, 86, 87syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝑄 βˆ₯ 𝑃 ↔ (𝑄 = 𝑃 ∨ 𝑄 = 1)))
8984, 88mtbird 325 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ Β¬ 𝑄 βˆ₯ 𝑃)
9070, 89orcnd 878 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑄 βˆ₯ (𝑁 / 𝑃))
9126, 38jca 513 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝑄 ∈ β„™ ∧ (𝑁 / 𝑃) ∈ β„•))
92 pcelnn 16800 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑄 ∈ β„™ ∧ (𝑁 / 𝑃) ∈ β„•) β†’ ((𝑄 pCnt (𝑁 / 𝑃)) ∈ β„• ↔ 𝑄 βˆ₯ (𝑁 / 𝑃)))
9391, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ ((𝑄 pCnt (𝑁 / 𝑃)) ∈ β„• ↔ 𝑄 βˆ₯ (𝑁 / 𝑃)))
9490, 93mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑄 pCnt (𝑁 / 𝑃)) ∈ β„•)
9556, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt (𝑁 / 𝑃)) ∈ β„•)
9695nnne0d 12259 . . . . . . . . . . . . . . . . . . . . . 22 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt (𝑁 / 𝑃)) β‰  0)
9752, 53, 55, 96mulcan2d 11845 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ ((𝑏 Β· (𝑄 pCnt (𝑁 / 𝑃))) = (𝑑 Β· (𝑄 pCnt (𝑁 / 𝑃))) ↔ 𝑏 = 𝑑))
9897necon3bid 2986 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ ((𝑏 Β· (𝑄 pCnt (𝑁 / 𝑃))) β‰  (𝑑 Β· (𝑄 pCnt (𝑁 / 𝑃))) ↔ 𝑏 β‰  𝑑))
9951, 98mpbird 257 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑏 Β· (𝑄 pCnt (𝑁 / 𝑃))) β‰  (𝑑 Β· (𝑄 pCnt (𝑁 / 𝑃))))
10026ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑄 ∈ β„™)
101 nnq 12943 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 / 𝑃) ∈ β„• β†’ (𝑁 / 𝑃) ∈ β„š)
10241, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑁 / 𝑃) ∈ β„š)
1031ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑁 ∈ β„•)
104103nncnd 12225 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑁 ∈ β„‚)
10534adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ π‘Ž ∈ β„•0) β†’ 𝑃 ∈ β„•)
106105adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) β†’ 𝑃 ∈ β„•)
107106ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑃 ∈ β„•)
108107nncnd 12225 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑃 ∈ β„‚)
109103nnne0d 12259 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑁 β‰  0)
110107nnne0d 12259 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑃 β‰  0)
111104, 108, 109, 110divne0d 12003 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑁 / 𝑃) β‰  0)
112102, 111jca 513 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑁 / 𝑃) ∈ β„š ∧ (𝑁 / 𝑃) β‰  0))
113 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑏 ∈ β„•0)
114113nn0zd 12581 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑏 ∈ β„€)
115100, 112, 1143jca 1129 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 ∈ β„™ ∧ ((𝑁 / 𝑃) ∈ β„š ∧ (𝑁 / 𝑃) β‰  0) ∧ 𝑏 ∈ β„€))
116 pcexp 16789 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑄 ∈ β„™ ∧ ((𝑁 / 𝑃) ∈ β„š ∧ (𝑁 / 𝑃) β‰  0) ∧ 𝑏 ∈ β„€) β†’ (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏)) = (𝑏 Β· (𝑄 pCnt (𝑁 / 𝑃))))
117115, 116syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏)) = (𝑏 Β· (𝑄 pCnt (𝑁 / 𝑃))))
118117adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏)) = (𝑏 Β· (𝑄 pCnt (𝑁 / 𝑃))))
119118eqcomd 2739 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑏 Β· (𝑄 pCnt (𝑁 / 𝑃))) = (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏)))
120 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑑 ∈ β„•0)
121120nn0zd 12581 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑑 ∈ β„€)
122100, 112, 1213jca 1129 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 ∈ β„™ ∧ ((𝑁 / 𝑃) ∈ β„š ∧ (𝑁 / 𝑃) β‰  0) ∧ 𝑑 ∈ β„€))
123 pcexp 16789 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑄 ∈ β„™ ∧ ((𝑁 / 𝑃) ∈ β„š ∧ (𝑁 / 𝑃) β‰  0) ∧ 𝑑 ∈ β„€) β†’ (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑)) = (𝑑 Β· (𝑄 pCnt (𝑁 / 𝑃))))
124122, 123syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑)) = (𝑑 Β· (𝑄 pCnt (𝑁 / 𝑃))))
125124adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑)) = (𝑑 Β· (𝑄 pCnt (𝑁 / 𝑃))))
126125eqcomd 2739 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑑 Β· (𝑄 pCnt (𝑁 / 𝑃))) = (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑)))
12799, 119, 1263netr3d 3018 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏)) β‰  (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑)))
12832, 46, 50, 127addneintrd 11418 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (0 + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏))) β‰  (0 + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑))))
12975ad4antr 731 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ Β¬ 𝑄 = 𝑃)
1302ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑃 ∈ β„™)
131 simp-4r 783 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ π‘Ž ∈ β„•0)
132 prmdvdsexpr 16651 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄 ∈ β„™ ∧ 𝑃 ∈ β„™ ∧ π‘Ž ∈ β„•0) β†’ (𝑄 βˆ₯ (π‘ƒβ†‘π‘Ž) β†’ 𝑄 = 𝑃))
133100, 130, 131, 132syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 βˆ₯ (π‘ƒβ†‘π‘Ž) β†’ 𝑄 = 𝑃))
134133con3d 152 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (Β¬ 𝑄 = 𝑃 β†’ Β¬ 𝑄 βˆ₯ (π‘ƒβ†‘π‘Ž)))
135129, 134mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ Β¬ 𝑄 βˆ₯ (π‘ƒβ†‘π‘Ž))
136 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) β†’ π‘Ž ∈ β„•0)
137106, 136nnexpcld 14205 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) β†’ (π‘ƒβ†‘π‘Ž) ∈ β„•)
138137ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (π‘ƒβ†‘π‘Ž) ∈ β„•)
139100, 138jca 513 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 ∈ β„™ ∧ (π‘ƒβ†‘π‘Ž) ∈ β„•))
140 pceq0 16801 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑄 ∈ β„™ ∧ (π‘ƒβ†‘π‘Ž) ∈ β„•) β†’ ((𝑄 pCnt (π‘ƒβ†‘π‘Ž)) = 0 ↔ Β¬ 𝑄 βˆ₯ (π‘ƒβ†‘π‘Ž)))
141139, 140syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑄 pCnt (π‘ƒβ†‘π‘Ž)) = 0 ↔ Β¬ 𝑄 βˆ₯ (π‘ƒβ†‘π‘Ž)))
142135, 141mpbird 257 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 pCnt (π‘ƒβ†‘π‘Ž)) = 0)
143142eqcomd 2739 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 0 = (𝑄 pCnt (π‘ƒβ†‘π‘Ž)))
144143oveq1d 7421 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (0 + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏))) = ((𝑄 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏))))
145144adantr 482 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (0 + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏))) = ((𝑄 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏))))
146 simplr 768 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑐 ∈ β„•0)
147 prmdvdsexpr 16651 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑄 ∈ β„™ ∧ 𝑃 ∈ β„™ ∧ 𝑐 ∈ β„•0) β†’ (𝑄 βˆ₯ (𝑃↑𝑐) β†’ 𝑄 = 𝑃))
148100, 130, 146, 147syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 βˆ₯ (𝑃↑𝑐) β†’ 𝑄 = 𝑃))
149129, 148mtod 197 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ Β¬ 𝑄 βˆ₯ (𝑃↑𝑐))
150107, 146nnexpcld 14205 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑃↑𝑐) ∈ β„•)
151100, 150jca 513 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 ∈ β„™ ∧ (𝑃↑𝑐) ∈ β„•))
152 pceq0 16801 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑄 ∈ β„™ ∧ (𝑃↑𝑐) ∈ β„•) β†’ ((𝑄 pCnt (𝑃↑𝑐)) = 0 ↔ Β¬ 𝑄 βˆ₯ (𝑃↑𝑐)))
153151, 152syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑄 pCnt (𝑃↑𝑐)) = 0 ↔ Β¬ 𝑄 βˆ₯ (𝑃↑𝑐)))
154149, 153mpbird 257 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 pCnt (𝑃↑𝑐)) = 0)
155154eqcomd 2739 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 0 = (𝑄 pCnt (𝑃↑𝑐)))
156155oveq1d 7421 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (0 + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑))) = ((𝑄 pCnt (𝑃↑𝑐)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑))))
157156adantr 482 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (0 + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑))) = ((𝑄 pCnt (𝑃↑𝑐)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑))))
158128, 145, 1573netr3d 3018 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ ((𝑄 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏))) β‰  ((𝑄 pCnt (𝑃↑𝑐)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑))))
159107nnzd 12582 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝑃 ∈ β„€)
160159, 131jca 513 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑃 ∈ β„€ ∧ π‘Ž ∈ β„•0))
161 zexpcl 14039 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ β„€ ∧ π‘Ž ∈ β„•0) β†’ (π‘ƒβ†‘π‘Ž) ∈ β„€)
162160, 161syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (π‘ƒβ†‘π‘Ž) ∈ β„€)
163131nn0zd 12581 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ π‘Ž ∈ β„€)
164108, 110, 163expne0d 14114 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (π‘ƒβ†‘π‘Ž) β‰  0)
165162, 164jca 513 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((π‘ƒβ†‘π‘Ž) ∈ β„€ ∧ (π‘ƒβ†‘π‘Ž) β‰  0))
16641nnzd 12582 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑁 / 𝑃) ∈ β„€)
167166, 113jca 513 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑁 / 𝑃) ∈ β„€ ∧ 𝑏 ∈ β„•0))
168 zexpcl 14039 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 / 𝑃) ∈ β„€ ∧ 𝑏 ∈ β„•0) β†’ ((𝑁 / 𝑃)↑𝑏) ∈ β„€)
169167, 168syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑁 / 𝑃)↑𝑏) ∈ β„€)
170104, 108, 110divcld 11987 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑁 / 𝑃) ∈ β„‚)
171170, 111, 114expne0d 14114 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑁 / 𝑃)↑𝑏) β‰  0)
172169, 171jca 513 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (((𝑁 / 𝑃)↑𝑏) ∈ β„€ ∧ ((𝑁 / 𝑃)↑𝑏) β‰  0))
173100, 165, 1723jca 1129 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 ∈ β„™ ∧ ((π‘ƒβ†‘π‘Ž) ∈ β„€ ∧ (π‘ƒβ†‘π‘Ž) β‰  0) ∧ (((𝑁 / 𝑃)↑𝑏) ∈ β„€ ∧ ((𝑁 / 𝑃)↑𝑏) β‰  0)))
174 pcmul 16781 . . . . . . . . . . . . . . . . . . 19 ((𝑄 ∈ β„™ ∧ ((π‘ƒβ†‘π‘Ž) ∈ β„€ ∧ (π‘ƒβ†‘π‘Ž) β‰  0) ∧ (((𝑁 / 𝑃)↑𝑏) ∈ β„€ ∧ ((𝑁 / 𝑃)↑𝑏) β‰  0)) β†’ (𝑄 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = ((𝑄 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏))))
175173, 174syl 17 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = ((𝑄 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏))))
176175adantr 482 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = ((𝑄 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏))))
177176eqcomd 2739 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ ((𝑄 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑏))) = (𝑄 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))))
178150nnzd 12582 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑃↑𝑐) ∈ β„€)
179150nnne0d 12259 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑃↑𝑐) β‰  0)
180178, 179jca 513 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑃↑𝑐) ∈ β„€ ∧ (𝑃↑𝑐) β‰  0))
18141, 120nnexpcld 14205 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑁 / 𝑃)↑𝑑) ∈ β„•)
182181nnzd 12582 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑁 / 𝑃)↑𝑑) ∈ β„€)
183181nnne0d 12259 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑁 / 𝑃)↑𝑑) β‰  0)
184182, 183jca 513 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (((𝑁 / 𝑃)↑𝑑) ∈ β„€ ∧ ((𝑁 / 𝑃)↑𝑑) β‰  0))
185100, 180, 1843jca 1129 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 ∈ β„™ ∧ ((𝑃↑𝑐) ∈ β„€ ∧ (𝑃↑𝑐) β‰  0) ∧ (((𝑁 / 𝑃)↑𝑑) ∈ β„€ ∧ ((𝑁 / 𝑃)↑𝑑) β‰  0)))
186 pcmul 16781 . . . . . . . . . . . . . . . . . . 19 ((𝑄 ∈ β„™ ∧ ((𝑃↑𝑐) ∈ β„€ ∧ (𝑃↑𝑐) β‰  0) ∧ (((𝑁 / 𝑃)↑𝑑) ∈ β„€ ∧ ((𝑁 / 𝑃)↑𝑑) β‰  0)) β†’ (𝑄 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) = ((𝑄 pCnt (𝑃↑𝑐)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑))))
187185, 186syl 17 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑄 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) = ((𝑄 pCnt (𝑃↑𝑐)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑))))
188187adantr 482 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) = ((𝑄 pCnt (𝑃↑𝑐)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑))))
189188eqcomd 2739 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ ((𝑄 pCnt (𝑃↑𝑐)) + (𝑄 pCnt ((𝑁 / 𝑃)↑𝑑))) = (𝑄 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
190158, 177, 1893netr3d 3018 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ (𝑄 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑄 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
19127, 31, 190rspcedvd 3615 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ 𝑏 β‰  𝑑) β†’ βˆƒπ‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
1922ad5antr 733 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ 𝑃 ∈ β„™)
193 simpr 486 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) ∧ 𝑝 = 𝑃) β†’ 𝑝 = 𝑃)
194193oveq1d 7421 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) ∧ 𝑝 = 𝑃) β†’ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑃 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))))
195193oveq1d 7421 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) ∧ 𝑝 = 𝑃) β†’ (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) = (𝑃 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
196194, 195neeq12d 3003 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) ∧ 𝑝 = 𝑃) β†’ ((𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) ↔ (𝑃 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑃 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
197130adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ 𝑃 ∈ β„™)
198197, 33syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ 𝑃 ∈ β„•)
199 simp-5r 785 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ π‘Ž ∈ β„•0)
200198, 199nnexpcld 14205 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (π‘ƒβ†‘π‘Ž) ∈ β„•)
201197, 200pccld 16780 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 pCnt (π‘ƒβ†‘π‘Ž)) ∈ β„•0)
202201nn0cnd 12531 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 pCnt (π‘ƒβ†‘π‘Ž)) ∈ β„‚)
203 simpllr 775 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ 𝑐 ∈ β„•0)
204198, 203nnexpcld 14205 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃↑𝑐) ∈ β„•)
205197, 204pccld 16780 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 pCnt (𝑃↑𝑐)) ∈ β„•0)
206205nn0cnd 12531 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 pCnt (𝑃↑𝑐)) ∈ β„‚)
20741adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑁 / 𝑃) ∈ β„•)
208 simp-4r 783 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ 𝑏 ∈ β„•0)
209207, 208nnexpcld 14205 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ ((𝑁 / 𝑃)↑𝑏) ∈ β„•)
210197, 209pccld 16780 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏)) ∈ β„•0)
211210nn0cnd 12531 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏)) ∈ β„‚)
2128adantl 483 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ π‘Ž β‰  𝑐)
213197, 199jca 513 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 ∈ β„™ ∧ π‘Ž ∈ β„•0))
214 pcidlem 16802 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ β„™ ∧ π‘Ž ∈ β„•0) β†’ (𝑃 pCnt (π‘ƒβ†‘π‘Ž)) = π‘Ž)
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 pCnt (π‘ƒβ†‘π‘Ž)) = π‘Ž)
216215eqcomd 2739 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ π‘Ž = (𝑃 pCnt (π‘ƒβ†‘π‘Ž)))
217197, 203jca 513 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 ∈ β„™ ∧ 𝑐 ∈ β„•0))
218 pcidlem 16802 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ β„™ ∧ 𝑐 ∈ β„•0) β†’ (𝑃 pCnt (𝑃↑𝑐)) = 𝑐)
219217, 218syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 pCnt (𝑃↑𝑐)) = 𝑐)
220219eqcomd 2739 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ 𝑐 = (𝑃 pCnt (𝑃↑𝑐)))
221212, 216, 2203netr3d 3018 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 pCnt (π‘ƒβ†‘π‘Ž)) β‰  (𝑃 pCnt (𝑃↑𝑐)))
222202, 206, 211, 221addneintr2d 11419 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ ((𝑃 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏))) β‰  ((𝑃 pCnt (𝑃↑𝑐)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏))))
223 eqidd 2734 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ ((𝑃 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏))) = ((𝑃 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏))))
224 simprl 770 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ 𝑏 = 𝑑)
225224oveq2d 7422 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ ((𝑁 / 𝑃)↑𝑏) = ((𝑁 / 𝑃)↑𝑑))
226225oveq2d 7422 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏)) = (𝑃 pCnt ((𝑁 / 𝑃)↑𝑑)))
227226oveq2d 7422 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ ((𝑃 pCnt (𝑃↑𝑐)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏))) = ((𝑃 pCnt (𝑃↑𝑐)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑑))))
228222, 223, 2273netr3d 3018 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ ((𝑃 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏))) β‰  ((𝑃 pCnt (𝑃↑𝑐)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑑))))
229130, 165, 1723jca 1129 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑃 ∈ β„™ ∧ ((π‘ƒβ†‘π‘Ž) ∈ β„€ ∧ (π‘ƒβ†‘π‘Ž) β‰  0) ∧ (((𝑁 / 𝑃)↑𝑏) ∈ β„€ ∧ ((𝑁 / 𝑃)↑𝑏) β‰  0)))
230 pcmul 16781 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ β„™ ∧ ((π‘ƒβ†‘π‘Ž) ∈ β„€ ∧ (π‘ƒβ†‘π‘Ž) β‰  0) ∧ (((𝑁 / 𝑃)↑𝑏) ∈ β„€ ∧ ((𝑁 / 𝑃)↑𝑏) β‰  0)) β†’ (𝑃 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = ((𝑃 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏))))
231229, 230syl 17 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑃 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = ((𝑃 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏))))
232231eqcomd 2739 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑃 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏))) = (𝑃 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))))
233232adantr 482 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ ((𝑃 pCnt (π‘ƒβ†‘π‘Ž)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑏))) = (𝑃 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))))
234130, 180, 1843jca 1129 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑃 ∈ β„™ ∧ ((𝑃↑𝑐) ∈ β„€ ∧ (𝑃↑𝑐) β‰  0) ∧ (((𝑁 / 𝑃)↑𝑑) ∈ β„€ ∧ ((𝑁 / 𝑃)↑𝑑) β‰  0)))
235 pcmul 16781 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ β„™ ∧ ((𝑃↑𝑐) ∈ β„€ ∧ (𝑃↑𝑐) β‰  0) ∧ (((𝑁 / 𝑃)↑𝑑) ∈ β„€ ∧ ((𝑁 / 𝑃)↑𝑑) β‰  0)) β†’ (𝑃 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) = ((𝑃 pCnt (𝑃↑𝑐)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑑))))
236235eqcomd 2739 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ β„™ ∧ ((𝑃↑𝑐) ∈ β„€ ∧ (𝑃↑𝑐) β‰  0) ∧ (((𝑁 / 𝑃)↑𝑑) ∈ β„€ ∧ ((𝑁 / 𝑃)↑𝑑) β‰  0)) β†’ ((𝑃 pCnt (𝑃↑𝑐)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑑))) = (𝑃 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
237234, 236syl 17 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑃 pCnt (𝑃↑𝑐)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑑))) = (𝑃 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
238237adantr 482 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ ((𝑃 pCnt (𝑃↑𝑐)) + (𝑃 pCnt ((𝑁 / 𝑃)↑𝑑))) = (𝑃 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
239228, 233, 2383netr3d 3018 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ (𝑃 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑃 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
240192, 196, 239rspcedvd 3615 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐)) β†’ βˆƒπ‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
241191, 240jaodan 957 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 β‰  𝑑 ∨ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐))) β†’ βˆƒπ‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
242 biidd 262 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) = ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ↔ ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) = ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
243242necon3abid 2978 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) β‰  ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ↔ Β¬ ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) = ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
244 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) β†’ 𝑏 ∈ β„•0)
24540, 244nnexpcld 14205 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) β†’ ((𝑁 / 𝑃)↑𝑏) ∈ β„•)
246137, 245nnmulcld 12262 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) β†’ ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) ∈ β„•)
247246adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) β†’ ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) ∈ β„•)
248247adantr 482 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) ∈ β„•)
249248nnnn0d 12529 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) ∈ β„•0)
250150, 181nnmulcld 12262 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ∈ β„•)
251250nnnn0d 12529 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ∈ β„•0)
252249, 251jca 513 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) ∈ β„•0 ∧ ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ∈ β„•0))
253 pc11 16810 . . . . . . . . . . . . . . . . . . 19 ((((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) ∈ β„•0 ∧ ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ∈ β„•0) β†’ (((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) = ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ↔ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
254252, 253syl 17 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) = ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ↔ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
255254notbid 318 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (Β¬ ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) = ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ↔ Β¬ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
256243, 255bitrd 279 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) β‰  ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ↔ Β¬ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
257 rexnal 3101 . . . . . . . . . . . . . . . . . 18 (βˆƒπ‘ ∈ β„™ Β¬ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) ↔ Β¬ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
258257bicomi 223 . . . . . . . . . . . . . . . . 17 (Β¬ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) ↔ βˆƒπ‘ ∈ β„™ Β¬ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
259258a1i 11 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (Β¬ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) ↔ βˆƒπ‘ ∈ β„™ Β¬ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
260256, 259bitrd 279 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) β‰  ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ↔ βˆƒπ‘ ∈ β„™ Β¬ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
261 biidd 262 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) ↔ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
262261necon3bbid 2979 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (Β¬ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) ↔ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
263262rexbidv 3179 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (βˆƒπ‘ ∈ β„™ Β¬ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) = (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))) ↔ βˆƒπ‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
264260, 263bitrd 279 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) β‰  ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ↔ βˆƒπ‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
265264adantr 482 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 β‰  𝑑 ∨ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐))) β†’ (((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) β‰  ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)) ↔ βˆƒπ‘ ∈ β„™ (𝑝 pCnt ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏))) β‰  (𝑝 pCnt ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))))
266241, 265mpbird 257 . . . . . . . . . . . 12 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (𝑏 β‰  𝑑 ∨ (𝑏 = 𝑑 ∧ π‘Ž β‰  𝑐))) β†’ ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) β‰  ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))
26725, 266sylan2br 596 . . . . . . . . . . 11 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ Β¬ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑)) β†’ ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) β‰  ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))
2684a1i 11 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ 𝐸 = (π‘˜ ∈ β„•0, 𝑙 ∈ β„•0 ↦ ((π‘ƒβ†‘π‘˜) Β· ((𝑁 / 𝑃)↑𝑙))))
269 simprl 770 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (π‘˜ = π‘Ž ∧ 𝑙 = 𝑏)) β†’ π‘˜ = π‘Ž)
270269oveq2d 7422 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (π‘˜ = π‘Ž ∧ 𝑙 = 𝑏)) β†’ (π‘ƒβ†‘π‘˜) = (π‘ƒβ†‘π‘Ž))
271 simprr 772 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (π‘˜ = π‘Ž ∧ 𝑙 = 𝑏)) β†’ 𝑙 = 𝑏)
272271oveq2d 7422 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (π‘˜ = π‘Ž ∧ 𝑙 = 𝑏)) β†’ ((𝑁 / 𝑃)↑𝑙) = ((𝑁 / 𝑃)↑𝑏))
273270, 272oveq12d 7424 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (π‘˜ = π‘Ž ∧ 𝑙 = 𝑏)) β†’ ((π‘ƒβ†‘π‘˜) Β· ((𝑁 / 𝑃)↑𝑙)) = ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)))
274268, 273, 131, 113, 248ovmpod 7557 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (π‘ŽπΈπ‘) = ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)))
275 simprl 770 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (π‘˜ = 𝑐 ∧ 𝑙 = 𝑑)) β†’ π‘˜ = 𝑐)
276275oveq2d 7422 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (π‘˜ = 𝑐 ∧ 𝑙 = 𝑑)) β†’ (π‘ƒβ†‘π‘˜) = (𝑃↑𝑐))
277 simprr 772 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (π‘˜ = 𝑐 ∧ 𝑙 = 𝑑)) β†’ 𝑙 = 𝑑)
278277oveq2d 7422 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (π‘˜ = 𝑐 ∧ 𝑙 = 𝑑)) β†’ ((𝑁 / 𝑃)↑𝑙) = ((𝑁 / 𝑃)↑𝑑))
279276, 278oveq12d 7424 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ (π‘˜ = 𝑐 ∧ 𝑙 = 𝑑)) β†’ ((π‘ƒβ†‘π‘˜) Β· ((𝑁 / 𝑃)↑𝑙)) = ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))
280268, 279, 146, 120, 250ovmpod 7557 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (𝑐𝐸𝑑) = ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑)))
281274, 280neeq12d 3003 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((π‘ŽπΈπ‘) β‰  (𝑐𝐸𝑑) ↔ ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) β‰  ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
282281adantr 482 . . . . . . . . . . 11 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ Β¬ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑)) β†’ ((π‘ŽπΈπ‘) β‰  (𝑐𝐸𝑑) ↔ ((π‘ƒβ†‘π‘Ž) Β· ((𝑁 / 𝑃)↑𝑏)) β‰  ((𝑃↑𝑐) Β· ((𝑁 / 𝑃)↑𝑑))))
283267, 282mpbird 257 . . . . . . . . . 10 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ Β¬ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑)) β†’ (π‘ŽπΈπ‘) β‰  (𝑐𝐸𝑑))
284283neneqd 2946 . . . . . . . . 9 ((((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) ∧ Β¬ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑)) β†’ Β¬ (π‘ŽπΈπ‘) = (𝑐𝐸𝑑))
285284ex 414 . . . . . . . 8 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ (Β¬ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑) β†’ Β¬ (π‘ŽπΈπ‘) = (𝑐𝐸𝑑)))
286285con4d 115 . . . . . . 7 (((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) ∧ 𝑑 ∈ β„•0) β†’ ((π‘ŽπΈπ‘) = (𝑐𝐸𝑑) β†’ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑)))
287286ralrimiva 3147 . . . . . 6 ((((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) ∧ 𝑐 ∈ β„•0) β†’ βˆ€π‘‘ ∈ β„•0 ((π‘ŽπΈπ‘) = (𝑐𝐸𝑑) β†’ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑)))
288287ralrimiva 3147 . . . . 5 (((πœ‘ ∧ π‘Ž ∈ β„•0) ∧ 𝑏 ∈ β„•0) β†’ βˆ€π‘ ∈ β„•0 βˆ€π‘‘ ∈ β„•0 ((π‘ŽπΈπ‘) = (𝑐𝐸𝑑) β†’ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑)))
289288ralrimiva 3147 . . . 4 ((πœ‘ ∧ π‘Ž ∈ β„•0) β†’ βˆ€π‘ ∈ β„•0 βˆ€π‘ ∈ β„•0 βˆ€π‘‘ ∈ β„•0 ((π‘ŽπΈπ‘) = (𝑐𝐸𝑑) β†’ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑)))
290289ralrimiva 3147 . . 3 (πœ‘ β†’ βˆ€π‘Ž ∈ β„•0 βˆ€π‘ ∈ β„•0 βˆ€π‘ ∈ β„•0 βˆ€π‘‘ ∈ β„•0 ((π‘ŽπΈπ‘) = (𝑐𝐸𝑑) β†’ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑)))
2915, 290jca 513 . 2 (πœ‘ β†’ (𝐸:(β„•0 Γ— β„•0)βŸΆβ„• ∧ βˆ€π‘Ž ∈ β„•0 βˆ€π‘ ∈ β„•0 βˆ€π‘ ∈ β„•0 βˆ€π‘‘ ∈ β„•0 ((π‘ŽπΈπ‘) = (𝑐𝐸𝑑) β†’ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑))))
292 f1opr 7462 . 2 (𝐸:(β„•0 Γ— β„•0)–1-1β†’β„• ↔ (𝐸:(β„•0 Γ— β„•0)βŸΆβ„• ∧ βˆ€π‘Ž ∈ β„•0 βˆ€π‘ ∈ β„•0 βˆ€π‘ ∈ β„•0 βˆ€π‘‘ ∈ β„•0 ((π‘ŽπΈπ‘) = (𝑐𝐸𝑑) β†’ (π‘Ž = 𝑐 ∧ 𝑏 = 𝑑))))
293291, 292sylibr 233 1 (πœ‘ β†’ 𝐸:(β„•0 Γ— β„•0)–1-1β†’β„•)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071   class class class wbr 5148   Γ— cxp 5674  βŸΆwf 6537  β€“1-1β†’wf1 6538  (class class class)co 7406   ∈ cmpo 7408  0cc0 11107  1c1 11108   + caddc 11110   Β· cmul 11112   < clt 11245   / cdiv 11868  β„•cn 12209  β„•0cn0 12469  β„€cz 12555  β„šcq 12929  β†‘cexp 14024   βˆ₯ cdvds 16194  β„™cprime 16605   pCnt cpc 16766
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-sup 9434  df-inf 9435  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-q 12930  df-rp 12972  df-fz 13482  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-dvds 16195  df-gcd 16433  df-prm 16606  df-pc 16767
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator