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	$⊢ φ \to N \in ℕ$
	aks6d1c2p2.2	$⊢ φ \to P \in ℙ$
	aks6d1c2p2.3	$⊢ φ \to P ∥ N$
	aks6d1c2p2.4	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
	aks6d1c2p2.5	$⊢ φ \to Q \in ℙ$
	aks6d1c2p2.6	$⊢ φ \to Q ∥ N$
	aks6d1c2p2.7	$⊢ φ \to P \neq Q$
Assertion	aks6d1c2p2	$⊢ φ \to E : ℕ_{0} \times ℕ_{0} \underset{1-1}{⟶} ℕ$

Proof

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

Metamath Proof Explorer

Theorem aks6d1c2p2

Proof