Theorem aks6d1c2p2

Description: Injective condition for countability argument assuming that N is not a prime power. (Contributed by metakunt, 7-Jan-2025)

	Ref	Expression
Hypotheses	aks6d1c2p2.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	aks6d1c2p2.2	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	aks6d1c2p2.3	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
	aks6d1c2p2.4	⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
	aks6d1c2p2.5	⊢ ( 𝜑 → 𝑄 ∈ ℙ )
	aks6d1c2p2.6	⊢ ( 𝜑 → 𝑄 ∥ 𝑁 )
	aks6d1c2p2.7	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
Assertion	aks6d1c2p2	⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) –1-1→ ℕ )

Proof

Step	Hyp	Ref	Expression
1		aks6d1c2p2.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		aks6d1c2p2.2	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
3		aks6d1c2p2.3	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
4		aks6d1c2p2.4	⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
5		aks6d1c2p2.5	⊢ ( 𝜑 → 𝑄 ∈ ℙ )
6		aks6d1c2p2.6	⊢ ( 𝜑 → 𝑄 ∥ 𝑁 )
7		aks6d1c2p2.7	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
8	1 2 3 4	aks6d1c2p1	⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ )
9		neneq	⊢ ( 𝑏 ≠ 𝑑 → ¬ 𝑏 = 𝑑 )
10	9	orcd	⊢ ( 𝑏 ≠ 𝑑 → ( ¬ 𝑏 = 𝑑 ∨ ¬ 𝑎 = 𝑐 ) )
11		simpr	⊢ ( ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) → 𝑎 ≠ 𝑐 )
12	11	neneqd	⊢ ( ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) → ¬ 𝑎 = 𝑐 )
13	12	olcd	⊢ ( ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) → ( ¬ 𝑏 = 𝑑 ∨ ¬ 𝑎 = 𝑐 ) )
14	10 13	jaoi	⊢ ( ( 𝑏 ≠ 𝑑 ∨ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( ¬ 𝑏 = 𝑑 ∨ ¬ 𝑎 = 𝑐 ) )
15		neqne	⊢ ( ¬ 𝑏 = 𝑑 → 𝑏 ≠ 𝑑 )
16	15	orcd	⊢ ( ¬ 𝑏 = 𝑑 → ( 𝑏 ≠ 𝑑 ∨ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) )
17		neqne	⊢ ( ¬ 𝑎 = 𝑐 → 𝑎 ≠ 𝑐 )
18	17	anim1ci	⊢ ( ( ¬ 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) )
19	18	olcd	⊢ ( ( ¬ 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑏 ≠ 𝑑 ∨ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) )
20	16	adantl	⊢ ( ( ¬ 𝑎 = 𝑐 ∧ ¬ 𝑏 = 𝑑 ) → ( 𝑏 ≠ 𝑑 ∨ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) )
21	19 20	pm2.61dan	⊢ ( ¬ 𝑎 = 𝑐 → ( 𝑏 ≠ 𝑑 ∨ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) )
22	16 21	jaoi	⊢ ( ( ¬ 𝑏 = 𝑑 ∨ ¬ 𝑎 = 𝑐 ) → ( 𝑏 ≠ 𝑑 ∨ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) )
23	14 22	impbii	⊢ ( ( 𝑏 ≠ 𝑑 ∨ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) ↔ ( ¬ 𝑏 = 𝑑 ∨ ¬ 𝑎 = 𝑐 ) )
24		orcom	⊢ ( ( ¬ 𝑏 = 𝑑 ∨ ¬ 𝑎 = 𝑐 ) ↔ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑 ) )
25	23 24	bitri	⊢ ( ( 𝑏 ≠ 𝑑 ∨ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) ↔ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑 ) )
26		ianor	⊢ ( ¬ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ↔ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑 ) )
27	26	bicomi	⊢ ( ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑 ) ↔ ¬ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) )
28	25 27	bitri	⊢ ( ( 𝑏 ≠ 𝑑 ∨ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) ↔ ¬ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) )
29	5	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → 𝑄 ∈ ℙ )
30		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) ∧ 𝑝 = 𝑄 ) → 𝑝 = 𝑄 )
31	30	oveq1d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) ∧ 𝑝 = 𝑄 ) → ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
32	30	oveq1d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) ∧ 𝑝 = 𝑄 ) → ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) = ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
33	31 32	neeq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) ∧ 𝑝 = 𝑄 ) → ( ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ↔ ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
34		0cnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → 0 ∈ ℂ )
35		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
36	2 35	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
37	1 36	jca	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℕ ) )
38		nndivdvds	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℕ ) → ( 𝑃 ∥ 𝑁 ↔ ( 𝑁 / 𝑃 ) ∈ ℕ ) )
39	37 38	syl	⊢ ( 𝜑 → ( 𝑃 ∥ 𝑁 ↔ ( 𝑁 / 𝑃 ) ∈ ℕ ) )
40	3 39	mpbid	⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ∈ ℕ )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) → ( 𝑁 / 𝑃 ) ∈ ℕ )
42	41	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝑁 / 𝑃 ) ∈ ℕ )
43	42	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑁 / 𝑃 ) ∈ ℕ )
44	43	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑁 / 𝑃 ) ∈ ℕ )
45		simp-4r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → 𝑏 ∈ ℕ0 )
46	44 45	nnexpcld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ∈ ℕ )
47	29 46	pccld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ∈ ℕ0 )
48	47	nn0cnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ∈ ℂ )
49		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → 𝑑 ∈ ℕ0 )
50	44 49	nnexpcld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ∈ ℕ )
51	29 50	pccld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ∈ ℕ0 )
52	51	nn0cnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ∈ ℂ )
53		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → 𝑏 ≠ 𝑑 )
54	45	nn0cnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → 𝑏 ∈ ℂ )
55	49	nn0cnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → 𝑑 ∈ ℂ )
56	29 44	pccld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ∈ ℕ0 )
57	56	nn0cnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ∈ ℂ )
58		simp-5l	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → 𝜑 )
59	1	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
60	36	nncnd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
61	36	nnne0d	⊢ ( 𝜑 → 𝑃 ≠ 0 )
62	59 60 61	divcan2d	⊢ ( 𝜑 → ( 𝑃 · ( 𝑁 / 𝑃 ) ) = 𝑁 )
63	62	eqcomd	⊢ ( 𝜑 → 𝑁 = ( 𝑃 · ( 𝑁 / 𝑃 ) ) )
64	63	breq2d	⊢ ( 𝜑 → ( 𝑄 ∥ 𝑁 ↔ 𝑄 ∥ ( 𝑃 · ( 𝑁 / 𝑃 ) ) ) )
65	6 64	mpbid	⊢ ( 𝜑 → 𝑄 ∥ ( 𝑃 · ( 𝑁 / 𝑃 ) ) )
66	36	nnzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
67	40	nnzd	⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ∈ ℤ )
68		euclemma	⊢ ( ( 𝑄 ∈ ℙ ∧ 𝑃 ∈ ℤ ∧ ( 𝑁 / 𝑃 ) ∈ ℤ ) → ( 𝑄 ∥ ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↔ ( 𝑄 ∥ 𝑃 ∨ 𝑄 ∥ ( 𝑁 / 𝑃 ) ) ) )
69	5 66 67 68	syl3anc	⊢ ( 𝜑 → ( 𝑄 ∥ ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↔ ( 𝑄 ∥ 𝑃 ∨ 𝑄 ∥ ( 𝑁 / 𝑃 ) ) ) )
70	69	biimpd	⊢ ( 𝜑 → ( 𝑄 ∥ ( 𝑃 · ( 𝑁 / 𝑃 ) ) → ( 𝑄 ∥ 𝑃 ∨ 𝑄 ∥ ( 𝑁 / 𝑃 ) ) ) )
71	65 70	mpd	⊢ ( 𝜑 → ( 𝑄 ∥ 𝑃 ∨ 𝑄 ∥ ( 𝑁 / 𝑃 ) ) )
72		necom	⊢ ( 𝑃 ≠ 𝑄 ↔ 𝑄 ≠ 𝑃 )
73	72	imbi2i	⊢ ( ( 𝜑 → 𝑃 ≠ 𝑄 ) ↔ ( 𝜑 → 𝑄 ≠ 𝑃 ) )
74	7 73	mpbi	⊢ ( 𝜑 → 𝑄 ≠ 𝑃 )
75	74	neneqd	⊢ ( 𝜑 → ¬ 𝑄 = 𝑃 )
76		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
77		prmgt1	⊢ ( 𝑄 ∈ ℙ → 1 < 𝑄 )
78	5 77	syl	⊢ ( 𝜑 → 1 < 𝑄 )
79	76 78	ltned	⊢ ( 𝜑 → 1 ≠ 𝑄 )
80	79	necomd	⊢ ( 𝜑 → 𝑄 ≠ 1 )
81	80	neneqd	⊢ ( 𝜑 → ¬ 𝑄 = 1 )
82	75 81	jca	⊢ ( 𝜑 → ( ¬ 𝑄 = 𝑃 ∧ ¬ 𝑄 = 1 ) )
83		pm4.56	⊢ ( ( ¬ 𝑄 = 𝑃 ∧ ¬ 𝑄 = 1 ) ↔ ¬ ( 𝑄 = 𝑃 ∨ 𝑄 = 1 ) )
84	82 83	sylib	⊢ ( 𝜑 → ¬ ( 𝑄 = 𝑃 ∨ 𝑄 = 1 ) )
85		prmnn	⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℕ )
86	5 85	syl	⊢ ( 𝜑 → 𝑄 ∈ ℕ )
87		dvdsprime	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℕ ) → ( 𝑄 ∥ 𝑃 ↔ ( 𝑄 = 𝑃 ∨ 𝑄 = 1 ) ) )
88	2 86 87	syl2anc	⊢ ( 𝜑 → ( 𝑄 ∥ 𝑃 ↔ ( 𝑄 = 𝑃 ∨ 𝑄 = 1 ) ) )
89	84 88	mtbird	⊢ ( 𝜑 → ¬ 𝑄 ∥ 𝑃 )
90	71 89	orcnd	⊢ ( 𝜑 → 𝑄 ∥ ( 𝑁 / 𝑃 ) )
91	5 40	jca	⊢ ( 𝜑 → ( 𝑄 ∈ ℙ ∧ ( 𝑁 / 𝑃 ) ∈ ℕ ) )
92		pcelnn	⊢ ( ( 𝑄 ∈ ℙ ∧ ( 𝑁 / 𝑃 ) ∈ ℕ ) → ( ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ∈ ℕ ↔ 𝑄 ∥ ( 𝑁 / 𝑃 ) ) )
93	91 92	syl	⊢ ( 𝜑 → ( ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ∈ ℕ ↔ 𝑄 ∥ ( 𝑁 / 𝑃 ) ) )
94	90 93	mpbird	⊢ ( 𝜑 → ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ∈ ℕ )
95	58 94	syl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ∈ ℕ )
96	95	nnne0d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ≠ 0 )
97	54 55 57 96	mulcan2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( ( 𝑏 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) = ( 𝑑 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) ↔ 𝑏 = 𝑑 ) )
98	97	necon3bid	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( ( 𝑏 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) ≠ ( 𝑑 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) ↔ 𝑏 ≠ 𝑑 ) )
99	53 98	mpbird	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑏 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) ≠ ( 𝑑 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) )
100	5	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑄 ∈ ℙ )
101		nnq	⊢ ( ( 𝑁 / 𝑃 ) ∈ ℕ → ( 𝑁 / 𝑃 ) ∈ ℚ )
102	43 101	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑁 / 𝑃 ) ∈ ℚ )
103	1	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑁 ∈ ℕ )
104	103	nncnd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
105	36	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) → 𝑃 ∈ ℕ )
106	105	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) → 𝑃 ∈ ℕ )
107	106	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑃 ∈ ℕ )
108	107	nncnd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑃 ∈ ℂ )
109	103	nnne0d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑁 ≠ 0 )
110	107	nnne0d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑃 ≠ 0 )
111	104 108 109 110	divne0d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑁 / 𝑃 ) ≠ 0 )
112	102 111	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑁 / 𝑃 ) ∈ ℚ ∧ ( 𝑁 / 𝑃 ) ≠ 0 ) )
113		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑏 ∈ ℕ0 )
114	113	nn0zd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑏 ∈ ℤ )
115	100 112 114	3jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 ∈ ℙ ∧ ( ( 𝑁 / 𝑃 ) ∈ ℚ ∧ ( 𝑁 / 𝑃 ) ≠ 0 ) ∧ 𝑏 ∈ ℤ ) )
116		pcexp	⊢ ( ( 𝑄 ∈ ℙ ∧ ( ( 𝑁 / 𝑃 ) ∈ ℚ ∧ ( 𝑁 / 𝑃 ) ≠ 0 ) ∧ 𝑏 ∈ ℤ ) → ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) = ( 𝑏 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) )
117	115 116	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) = ( 𝑏 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) )
118	117	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) = ( 𝑏 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) )
119	118	eqcomd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑏 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) = ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) )
120		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑑 ∈ ℕ0 )
121	120	nn0zd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑑 ∈ ℤ )
122	100 112 121	3jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 ∈ ℙ ∧ ( ( 𝑁 / 𝑃 ) ∈ ℚ ∧ ( 𝑁 / 𝑃 ) ≠ 0 ) ∧ 𝑑 ∈ ℤ ) )
123		pcexp	⊢ ( ( 𝑄 ∈ ℙ ∧ ( ( 𝑁 / 𝑃 ) ∈ ℚ ∧ ( 𝑁 / 𝑃 ) ≠ 0 ) ∧ 𝑑 ∈ ℤ ) → ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) = ( 𝑑 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) )
124	122 123	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) = ( 𝑑 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) )
125	124	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) = ( 𝑑 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) )
126	125	eqcomd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑑 · ( 𝑄 pCnt ( 𝑁 / 𝑃 ) ) ) = ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) )
127	99 119 126	3netr3d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ≠ ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) )
128	34 48 52 127	addneintrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 0 + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 0 + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
129	75	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ¬ 𝑄 = 𝑃 )
130	2	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑃 ∈ ℙ )
131		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑎 ∈ ℕ0 )
132		prmdvdsexpr	⊢ ( ( 𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) → ( 𝑄 ∥ ( 𝑃 ↑ 𝑎 ) → 𝑄 = 𝑃 ) )
133	100 130 131 132	syl3anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 ∥ ( 𝑃 ↑ 𝑎 ) → 𝑄 = 𝑃 ) )
134	133	con3d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ¬ 𝑄 = 𝑃 → ¬ 𝑄 ∥ ( 𝑃 ↑ 𝑎 ) ) )
135	129 134	mpd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ¬ 𝑄 ∥ ( 𝑃 ↑ 𝑎 ) )
136		simplr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) → 𝑎 ∈ ℕ0 )
137	106 136	nnexpcld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑎 ) ∈ ℕ )
138	137	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑎 ) ∈ ℕ )
139	100 138	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 ∈ ℙ ∧ ( 𝑃 ↑ 𝑎 ) ∈ ℕ ) )
140		pceq0	⊢ ( ( 𝑄 ∈ ℙ ∧ ( 𝑃 ↑ 𝑎 ) ∈ ℕ ) → ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑎 ) ) = 0 ↔ ¬ 𝑄 ∥ ( 𝑃 ↑ 𝑎 ) ) )
141	139 140	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑎 ) ) = 0 ↔ ¬ 𝑄 ∥ ( 𝑃 ↑ 𝑎 ) ) )
142	135 141	mpbird	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 pCnt ( 𝑃 ↑ 𝑎 ) ) = 0 )
143	142	eqcomd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 0 = ( 𝑄 pCnt ( 𝑃 ↑ 𝑎 ) ) )
144	143	oveq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 0 + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
145	144	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 0 + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
146		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑐 ∈ ℕ0 )
147		prmdvdsexpr	⊢ ( ( 𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ 𝑐 ∈ ℕ0 ) → ( 𝑄 ∥ ( 𝑃 ↑ 𝑐 ) → 𝑄 = 𝑃 ) )
148	100 130 146 147	syl3anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 ∥ ( 𝑃 ↑ 𝑐 ) → 𝑄 = 𝑃 ) )
149	129 148	mtod	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ¬ 𝑄 ∥ ( 𝑃 ↑ 𝑐 ) )
150	107 146	nnexpcld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑐 ) ∈ ℕ )
151	100 150	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 ∈ ℙ ∧ ( 𝑃 ↑ 𝑐 ) ∈ ℕ ) )
152		pceq0	⊢ ( ( 𝑄 ∈ ℙ ∧ ( 𝑃 ↑ 𝑐 ) ∈ ℕ ) → ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑐 ) ) = 0 ↔ ¬ 𝑄 ∥ ( 𝑃 ↑ 𝑐 ) ) )
153	151 152	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑐 ) ) = 0 ↔ ¬ 𝑄 ∥ ( 𝑃 ↑ 𝑐 ) ) )
154	149 153	mpbird	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 pCnt ( 𝑃 ↑ 𝑐 ) ) = 0 )
155	154	eqcomd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 0 = ( 𝑄 pCnt ( 𝑃 ↑ 𝑐 ) ) )
156	155	oveq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 0 + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) = ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
157	156	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 0 + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) = ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
158	128 145 157	3netr3d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
159	107	nnzd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑃 ∈ ℤ )
160	159 131	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑃 ∈ ℤ ∧ 𝑎 ∈ ℕ0 ) )
161		zexpcl	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑎 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑎 ) ∈ ℤ )
162	160 161	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑎 ) ∈ ℤ )
163	131	nn0zd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝑎 ∈ ℤ )
164	108 110 163	expne0d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑎 ) ≠ 0 )
165	162 164	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑃 ↑ 𝑎 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑎 ) ≠ 0 ) )
166	43	nnzd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑁 / 𝑃 ) ∈ ℤ )
167	166 113	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑁 / 𝑃 ) ∈ ℤ ∧ 𝑏 ∈ ℕ0 ) )
168		zexpcl	⊢ ( ( ( 𝑁 / 𝑃 ) ∈ ℤ ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ∈ ℤ )
169	167 168	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ∈ ℤ )
170	104 108 110	divcld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑁 / 𝑃 ) ∈ ℂ )
171	170 111 114	expne0d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ≠ 0 )
172	169 171	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ∈ ℤ ∧ ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ≠ 0 ) )
173	100 165 172	3jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 ∈ ℙ ∧ ( ( 𝑃 ↑ 𝑎 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑎 ) ≠ 0 ) ∧ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ∈ ℤ ∧ ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ≠ 0 ) ) )
174		pcmul	⊢ ( ( 𝑄 ∈ ℙ ∧ ( ( 𝑃 ↑ 𝑎 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑎 ) ≠ 0 ) ∧ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ∈ ℤ ∧ ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ≠ 0 ) ) → ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
175	173 174	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
176	175	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
177	176	eqcomd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
178	150	nnzd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑐 ) ∈ ℤ )
179	150	nnne0d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑐 ) ≠ 0 )
180	178 179	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑃 ↑ 𝑐 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑐 ) ≠ 0 ) )
181	43 120	nnexpcld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ∈ ℕ )
182	181	nnzd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ∈ ℤ )
183	181	nnne0d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ≠ 0 )
184	182 183	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ∈ ℤ ∧ ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ≠ 0 ) )
185	100 180 184	3jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 ∈ ℙ ∧ ( ( 𝑃 ↑ 𝑐 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑐 ) ≠ 0 ) ∧ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ∈ ℤ ∧ ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ≠ 0 ) ) )
186		pcmul	⊢ ( ( 𝑄 ∈ ℙ ∧ ( ( 𝑃 ↑ 𝑐 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑐 ) ≠ 0 ) ∧ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ∈ ℤ ∧ ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ≠ 0 ) ) → ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) = ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
187	185 186	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) = ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
188	187	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) = ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
189	188	eqcomd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( ( 𝑄 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑄 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) = ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
190	158 177 189	3netr3d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑄 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
191	29 33 190	rspcedvd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ≠ 𝑑 ) → ∃ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
192	2	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → 𝑃 ∈ ℙ )
193		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) ∧ 𝑝 = 𝑃 ) → 𝑝 = 𝑃 )
194	193	oveq1d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) ∧ 𝑝 = 𝑃 ) → ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
195	193	oveq1d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) ∧ 𝑝 = 𝑃 ) → ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) = ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
196	194 195	neeq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) ∧ 𝑝 = 𝑃 ) → ( ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ↔ ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
197	130	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → 𝑃 ∈ ℙ )
198	197 35	syl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → 𝑃 ∈ ℕ )
199		simp-5r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → 𝑎 ∈ ℕ0 )
200	198 199	nnexpcld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 ↑ 𝑎 ) ∈ ℕ )
201	197 200	pccld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) ∈ ℕ0 )
202	201	nn0cnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) ∈ ℂ )
203		simpllr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → 𝑐 ∈ ℕ0 )
204	198 203	nnexpcld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 ↑ 𝑐 ) ∈ ℕ )
205	197 204	pccld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) ∈ ℕ0 )
206	205	nn0cnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) ∈ ℂ )
207	43	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑁 / 𝑃 ) ∈ ℕ )
208		simp-4r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → 𝑏 ∈ ℕ0 )
209	207 208	nnexpcld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ∈ ℕ )
210	197 209	pccld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ∈ ℕ0 )
211	210	nn0cnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ∈ ℂ )
212	11	adantl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → 𝑎 ≠ 𝑐 )
213	197 199	jca	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) )
214		pcidlem	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑎 ∈ ℕ0 ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) = 𝑎 )
215	213 214	syl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) = 𝑎 )
216	215	eqcomd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → 𝑎 = ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) )
217	197 203	jca	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 ∈ ℙ ∧ 𝑐 ∈ ℕ0 ) )
218		pcidlem	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑐 ∈ ℕ0 ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) = 𝑐 )
219	217 218	syl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) = 𝑐 )
220	219	eqcomd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → 𝑐 = ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) )
221	212 216 220	3netr3d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) ≠ ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) )
222	202 206 211 221	addneintr2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
223		eqidd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
224		simprl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → 𝑏 = 𝑑 )
225	224	oveq2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) )
226	225	oveq2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) = ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) )
227	226	oveq2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
228	222 223 227	3netr3d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
229	130 165 172	3jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑃 ∈ ℙ ∧ ( ( 𝑃 ↑ 𝑎 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑎 ) ≠ 0 ) ∧ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ∈ ℤ ∧ ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ≠ 0 ) ) )
230		pcmul	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝑃 ↑ 𝑎 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑎 ) ≠ 0 ) ∧ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ∈ ℤ ∧ ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ≠ 0 ) ) → ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
231	229 230	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
232	231	eqcomd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
233	232	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑎 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) )
234	130 180 184	3jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑃 ∈ ℙ ∧ ( ( 𝑃 ↑ 𝑐 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑐 ) ≠ 0 ) ∧ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ∈ ℤ ∧ ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ≠ 0 ) ) )
235		pcmul	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝑃 ↑ 𝑐 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑐 ) ≠ 0 ) ∧ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ∈ ℤ ∧ ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ≠ 0 ) ) → ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) = ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
236	235	eqcomd	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝑃 ↑ 𝑐 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑐 ) ≠ 0 ) ∧ ( ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ∈ ℤ ∧ ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ≠ 0 ) ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) = ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
237	234 236	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) = ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
238	237	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝑐 ) ) + ( 𝑃 pCnt ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) = ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
239	228 233 238	3netr3d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑃 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
240	192 196 239	rspcedvd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) → ∃ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
241	191 240	jaodan	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 ≠ 𝑑 ∨ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) ) → ∃ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
242		biidd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) = ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ↔ ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) = ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
243	242	necon3abid	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ≠ ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ↔ ¬ ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) = ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
244		simpr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) → 𝑏 ∈ ℕ0 )
245	42 244	nnexpcld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ∈ ℕ )
246	137 245	nnmulcld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ∈ ℕ )
247	246	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) → ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ∈ ℕ )
248	247	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ∈ ℕ )
249	248	nnnn0d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ∈ ℕ0 )
250	150 181	nnmulcld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ∈ ℕ )
251	250	nnnn0d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ∈ ℕ0 )
252	249 251	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ∈ ℕ0 ∧ ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ∈ ℕ0 ) )
253		pc11	⊢ ( ( ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ∈ ℕ0 ∧ ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ∈ ℕ0 ) → ( ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) = ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
254	252 253	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) = ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
255	254	notbid	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ¬ ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) = ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ↔ ¬ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
256	243 255	bitrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ≠ ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ↔ ¬ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
257		rexnal	⊢ ( ∃ 𝑝 ∈ ℙ ¬ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ↔ ¬ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
258	257	bicomi	⊢ ( ¬ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ↔ ∃ 𝑝 ∈ ℙ ¬ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
259	258	a1i	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ¬ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ↔ ∃ 𝑝 ∈ ℙ ¬ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
260	256 259	bitrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ≠ ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ↔ ∃ 𝑝 ∈ ℙ ¬ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
261		biidd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ↔ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
262	261	necon3bbid	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ¬ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ↔ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
263	262	rexbidv	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ∃ 𝑝 ∈ ℙ ¬ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) = ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
264	260 263	bitrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ≠ ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
265	264	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 ≠ 𝑑 ∨ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) ) → ( ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ≠ ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ) ≠ ( 𝑝 pCnt ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) ) )
266	241 265	mpbird	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑏 ≠ 𝑑 ∨ ( 𝑏 = 𝑑 ∧ 𝑎 ≠ 𝑐 ) ) ) → ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ≠ ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) )
267	28 266	sylan2br	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ¬ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) → ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ≠ ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) )
268	4	a1i	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) )
269		simprl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑘 = 𝑎 ∧ 𝑙 = 𝑏 ) ) → 𝑘 = 𝑎 )
270	269	oveq2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑘 = 𝑎 ∧ 𝑙 = 𝑏 ) ) → ( 𝑃 ↑ 𝑘 ) = ( 𝑃 ↑ 𝑎 ) )
271		simprr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑘 = 𝑎 ∧ 𝑙 = 𝑏 ) ) → 𝑙 = 𝑏 )
272	271	oveq2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑘 = 𝑎 ∧ 𝑙 = 𝑏 ) ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) )
273	270 272	oveq12d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑘 = 𝑎 ∧ 𝑙 = 𝑏 ) ) → ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) = ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) )
274	268 273 131 113 248	ovmpod	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑎 𝐸 𝑏 ) = ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) )
275		simprl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑘 = 𝑐 ∧ 𝑙 = 𝑑 ) ) → 𝑘 = 𝑐 )
276	275	oveq2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑘 = 𝑐 ∧ 𝑙 = 𝑑 ) ) → ( 𝑃 ↑ 𝑘 ) = ( 𝑃 ↑ 𝑐 ) )
277		simprr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑘 = 𝑐 ∧ 𝑙 = 𝑑 ) ) → 𝑙 = 𝑑 )
278	277	oveq2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑘 = 𝑐 ∧ 𝑙 = 𝑑 ) ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) )
279	276 278	oveq12d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ( 𝑘 = 𝑐 ∧ 𝑙 = 𝑑 ) ) → ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) = ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) )
280	268 279 146 120 250	ovmpod	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑐 𝐸 𝑑 ) = ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) )
281	274 280	neeq12d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑎 𝐸 𝑏 ) ≠ ( 𝑐 𝐸 𝑑 ) ↔ ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ≠ ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
282	281	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ¬ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) → ( ( 𝑎 𝐸 𝑏 ) ≠ ( 𝑐 𝐸 𝑑 ) ↔ ( ( 𝑃 ↑ 𝑎 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑏 ) ) ≠ ( ( 𝑃 ↑ 𝑐 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑑 ) ) ) )
283	267 282	mpbird	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ¬ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) → ( 𝑎 𝐸 𝑏 ) ≠ ( 𝑐 𝐸 𝑑 ) )
284	283	neneqd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) ∧ ¬ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) → ¬ ( 𝑎 𝐸 𝑏 ) = ( 𝑐 𝐸 𝑑 ) )
285	284	ex	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ¬ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ¬ ( 𝑎 𝐸 𝑏 ) = ( 𝑐 𝐸 𝑑 ) ) )
286	285	con4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( 𝑎 𝐸 𝑏 ) = ( 𝑐 𝐸 𝑑 ) → ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) )
287	286	ralrimiva	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) ∧ 𝑐 ∈ ℕ0 ) → ∀ 𝑑 ∈ ℕ0 ( ( 𝑎 𝐸 𝑏 ) = ( 𝑐 𝐸 𝑑 ) → ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) )
288	287	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℕ0 ) → ∀ 𝑐 ∈ ℕ0 ∀ 𝑑 ∈ ℕ0 ( ( 𝑎 𝐸 𝑏 ) = ( 𝑐 𝐸 𝑑 ) → ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) )
289	288	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ) → ∀ 𝑏 ∈ ℕ0 ∀ 𝑐 ∈ ℕ0 ∀ 𝑑 ∈ ℕ0 ( ( 𝑎 𝐸 𝑏 ) = ( 𝑐 𝐸 𝑑 ) → ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) )
290	289	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ ℕ0 ∀ 𝑏 ∈ ℕ0 ∀ 𝑐 ∈ ℕ0 ∀ 𝑑 ∈ ℕ0 ( ( 𝑎 𝐸 𝑏 ) = ( 𝑐 𝐸 𝑑 ) → ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) )
291	8 290	jca	⊢ ( 𝜑 → ( 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ ∧ ∀ 𝑎 ∈ ℕ0 ∀ 𝑏 ∈ ℕ0 ∀ 𝑐 ∈ ℕ0 ∀ 𝑑 ∈ ℕ0 ( ( 𝑎 𝐸 𝑏 ) = ( 𝑐 𝐸 𝑑 ) → ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) ) )
292		f1opr	⊢ ( 𝐸 : ( ℕ0 × ℕ0 ) –1-1→ ℕ ↔ ( 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ ∧ ∀ 𝑎 ∈ ℕ0 ∀ 𝑏 ∈ ℕ0 ∀ 𝑐 ∈ ℕ0 ∀ 𝑑 ∈ ℕ0 ( ( 𝑎 𝐸 𝑏 ) = ( 𝑐 𝐸 𝑑 ) → ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) ) )
293	291 292	sylibr	⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) –1-1→ ℕ )