prmreclem2

Description: Lemma for prmrec . There are at most 2 ^ K squarefree numbers which divide no primes larger than K . (We could strengthen this to 2 ^ # ( Prime i^i ( 1 ... K ) ) but there's no reason to.) We establish the inequality by showing that the prime counts of the number up to K completely determine it because all higher prime counts are zero, and they are all at most 1 because no square divides the number, so there are at most 2 ^ K possibilities. (Contributed by Mario Carneiro, 5-Aug-2014)

	Ref	Expression
Hypotheses	prmrec.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, \frac{1}{n}, 0))$
	prmrec.2	$⊢ φ \to K \in ℕ$
	prmrec.3	$⊢ φ \to N \in ℕ$
	prmrec.4	$⊢ M = \{n \in (1 \dots N) \| \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n\}$
	prmreclem2.5	$⊢ Q = (n \in ℕ ⟼ sup (\{r \in ℕ \| r^{2} ∥ n\} ℝ <))$
Assertion	prmreclem2	$⊢ φ \to \|\{x \in M \| Q (x) = 1\}\| \leq 2^{K}$

Proof

Step	Hyp	Ref	Expression
1		prmrec.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, \frac{1}{n}, 0))$
2		prmrec.2	$⊢ φ \to K \in ℕ$
3		prmrec.3	$⊢ φ \to N \in ℕ$
4		prmrec.4	$⊢ M = \{n \in (1 \dots N) \| \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n\}$
5		prmreclem2.5	$⊢ Q = (n \in ℕ ⟼ sup (\{r \in ℕ \| r^{2} ∥ n\} ℝ <))$
6		ovex	$⊢ {\{0, 1\}}^{(1 \dots K)} \in V$
7		fveqeq2	$⊢ x = y \to (Q (x) = 1 \leftrightarrow Q (y) = 1)$
8	7	elrab	$⊢ y \in \{x \in M \| Q (x) = 1\} \leftrightarrow (y \in M \land Q (y) = 1)$
9	4	ssrab3	$⊢ M \subseteq (1 \dots N)$
10		simprl	$⊢ (φ \land (y \in M \land Q (y) = 1)) \to y \in M$
11	10	ad2antrr	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to y \in M$
12	9 11	sselid	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to y \in (1 \dots N)$
13		elfznn	$⊢ y \in (1 \dots N) \to y \in ℕ$
14	12 13	syl	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to y \in ℕ$
15		simpr	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to n \in ℙ$
16		prmuz2	$⊢ n \in ℙ \to n \in ℤ_{\geq 2}$
17	15 16	syl	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to n \in ℤ_{\geq 2}$
18	5	prmreclem1	$⊢ y \in ℕ \to (Q (y) \in ℕ \land {Q (y)}^{2} ∥ y \land (n \in ℤ_{\geq 2} \to \neg n^{2} ∥ (\frac{y}{{Q (y)}^{2}})))$
19	18	simp3d	$⊢ y \in ℕ \to (n \in ℤ_{\geq 2} \to \neg n^{2} ∥ (\frac{y}{{Q (y)}^{2}}))$
20	14 17 19	sylc	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to \neg n^{2} ∥ (\frac{y}{{Q (y)}^{2}})$
21		simprr	$⊢ (φ \land (y \in M \land Q (y) = 1)) \to Q (y) = 1$
22	21	ad2antrr	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to Q (y) = 1$
23	22	oveq1d	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to {Q (y)}^{2} = 1^{2}$
24		sq1	$⊢ 1^{2} = 1$
25	23 24	eqtrdi	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to {Q (y)}^{2} = 1$
26	25	oveq2d	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to \frac{y}{{Q (y)}^{2}} = \frac{y}{1}$
27	14	nncnd	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to y \in ℂ$
28	27	div1d	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to \frac{y}{1} = y$
29	26 28	eqtrd	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to \frac{y}{{Q (y)}^{2}} = y$
30	29	breq2d	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to (n^{2} ∥ (\frac{y}{{Q (y)}^{2}}) \leftrightarrow n^{2} ∥ y)$
31	14	nnzd	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to y \in ℤ$
32		2nn0	$⊢ 2 \in ℕ_{0}$
33	32	a1i	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to 2 \in ℕ_{0}$
34		pcdvdsb	$⊢ (n \in ℙ \land y \in ℤ \land 2 \in ℕ_{0}) \to (2 \leq n pCnt y \leftrightarrow n^{2} ∥ y)$
35	15 31 33 34	syl3anc	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to (2 \leq n pCnt y \leftrightarrow n^{2} ∥ y)$
36	30 35	bitr4d	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to (n^{2} ∥ (\frac{y}{{Q (y)}^{2}}) \leftrightarrow 2 \leq n pCnt y)$
37	20 36	mtbid	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to \neg 2 \leq n pCnt y$
38	15 14	pccld	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to n pCnt y \in ℕ_{0}$
39	38	nn0red	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to n pCnt y \in ℝ$
40		2re	$⊢ 2 \in ℝ$
41		ltnle	$⊢ (n pCnt y \in ℝ \land 2 \in ℝ) \to (n pCnt y < 2 \leftrightarrow \neg 2 \leq n pCnt y)$
42	39 40 41	sylancl	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to (n pCnt y < 2 \leftrightarrow \neg 2 \leq n pCnt y)$
43	37 42	mpbird	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to n pCnt y < 2$
44		df-2	$⊢ 2 = 1 + 1$
45	43 44	breqtrdi	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to n pCnt y < 1 + 1$
46	38	nn0zd	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to n pCnt y \in ℤ$
47		1z	$⊢ 1 \in ℤ$
48		zleltp1	$⊢ (n pCnt y \in ℤ \land 1 \in ℤ) \to (n pCnt y \leq 1 \leftrightarrow n pCnt y < 1 + 1)$
49	46 47 48	sylancl	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to (n pCnt y \leq 1 \leftrightarrow n pCnt y < 1 + 1)$
50	45 49	mpbird	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to n pCnt y \leq 1$
51		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
52	38 51	eleqtrdi	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to n pCnt y \in ℤ_{\geq 0}$
53		elfz5	$⊢ (n pCnt y \in ℤ_{\geq 0} \land 1 \in ℤ) \to (n pCnt y \in (0 \dots 1) \leftrightarrow n pCnt y \leq 1)$
54	52 47 53	sylancl	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to (n pCnt y \in (0 \dots 1) \leftrightarrow n pCnt y \leq 1)$
55	50 54	mpbird	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to n pCnt y \in (0 \dots 1)$
56		0z	$⊢ 0 \in ℤ$
57		fzpr	$⊢ 0 \in ℤ \to (0 \dots 0 + 1) = \{0, 0 + 1\}$
58	56 57	ax-mp	$⊢ (0 \dots 0 + 1) = \{0, 0 + 1\}$
59		1e0p1	$⊢ 1 = 0 + 1$
60	59	oveq2i	$⊢ (0 \dots 1) = (0 \dots 0 + 1)$
61	59	preq2i	$⊢ \{0, 1\} = \{0, 0 + 1\}$
62	58 60 61	3eqtr4i	$⊢ (0 \dots 1) = \{0, 1\}$
63	55 62	eleqtrdi	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land n \in ℙ) \to n pCnt y \in \{0, 1\}$
64		0elpr01	$⊢ 0 \in \{0, 1\}$
65	64	a1i	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land \neg n \in ℙ) \to 0 \in \{0, 1\}$
66	63 65	ifclda	$⊢ ((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \to if (n \in ℙ, n pCnt y, 0) \in \{0, 1\}$
67	66	fmpttd	$⊢ (φ \land (y \in M \land Q (y) = 1)) \to (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) : (1 \dots K) ⟶ \{0, 1\}$
68		prex	$⊢ \{0, 1\} \in V$
69		ovex	$⊢ (1 \dots K) \in V$
70	68 69	elmap	$⊢ (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) \in ({\{0, 1\}}^{(1 \dots K)}) \leftrightarrow (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) : (1 \dots K) ⟶ \{0, 1\}$
71	67 70	sylibr	$⊢ (φ \land (y \in M \land Q (y) = 1)) \to (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) \in ({\{0, 1\}}^{(1 \dots K)})$
72	71	ex	$⊢ φ \to ((y \in M \land Q (y) = 1) \to (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) \in ({\{0, 1\}}^{(1 \dots K)}))$
73	8 72	biimtrid	$⊢ φ \to (y \in \{x \in M \| Q (x) = 1\} \to (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) \in ({\{0, 1\}}^{(1 \dots K)}))$
74		fveqeq2	$⊢ x = z \to (Q (x) = 1 \leftrightarrow Q (z) = 1)$
75	74	elrab	$⊢ z \in \{x \in M \| Q (x) = 1\} \leftrightarrow (z \in M \land Q (z) = 1)$
76	8 75	anbi12i	$⊢ (y \in \{x \in M \| Q (x) = 1\} \land z \in \{x \in M \| Q (x) = 1\}) \leftrightarrow ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))$
77		ovex	$⊢ n pCnt y \in V$
78		c0ex	$⊢ 0 \in V$
79	77 78	ifex	$⊢ if (n \in ℙ, n pCnt y, 0) \in V$
80		eqid	$⊢ (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) = (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0))$
81	79 80	fnmpti	$⊢ (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) Fn (1 \dots K)$
82		ovex	$⊢ n pCnt z \in V$
83	82 78	ifex	$⊢ if (n \in ℙ, n pCnt z, 0) \in V$
84		eqid	$⊢ (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) = (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0))$
85	83 84	fnmpti	$⊢ (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) Fn (1 \dots K)$
86		eqfnfv	$⊢ ((n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) Fn (1 \dots K) \land (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) Fn (1 \dots K)) \to ((n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) = (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) \leftrightarrow \forall p \in (1 \dots K) (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) (p) = (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) (p))$
87	81 85 86	mp2an	$⊢ (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) = (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) \leftrightarrow \forall p \in (1 \dots K) (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) (p) = (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) (p)$
88		eleq1w	$⊢ n = p \to (n \in ℙ \leftrightarrow p \in ℙ)$
89		oveq1	$⊢ n = p \to n pCnt y = p pCnt y$
90	88 89	ifbieq1d	$⊢ n = p \to if (n \in ℙ, n pCnt y, 0) = if (p \in ℙ, p pCnt y, 0)$
91		ovex	$⊢ p pCnt y \in V$
92	91 78	ifex	$⊢ if (p \in ℙ, p pCnt y, 0) \in V$
93	90 80 92	fvmpt	$⊢ p \in (1 \dots K) \to (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) (p) = if (p \in ℙ, p pCnt y, 0)$
94		oveq1	$⊢ n = p \to n pCnt z = p pCnt z$
95	88 94	ifbieq1d	$⊢ n = p \to if (n \in ℙ, n pCnt z, 0) = if (p \in ℙ, p pCnt z, 0)$
96		ovex	$⊢ p pCnt z \in V$
97	96 78	ifex	$⊢ if (p \in ℙ, p pCnt z, 0) \in V$
98	95 84 97	fvmpt	$⊢ p \in (1 \dots K) \to (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) (p) = if (p \in ℙ, p pCnt z, 0)$
99	93 98	eqeq12d	$⊢ p \in (1 \dots K) \to ((n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) (p) = (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) (p) \leftrightarrow if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0))$
100	99	ralbiia	$⊢ \forall p \in (1 \dots K) (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) (p) = (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) (p) \leftrightarrow \forall p \in (1 \dots K) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0)$
101	87 100	bitri	$⊢ (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) = (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) \leftrightarrow \forall p \in (1 \dots K) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0)$
102		simprll	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to y \in M$
103		breq2	$⊢ n = y \to (p ∥ n \leftrightarrow p ∥ y)$
104	103	notbid	$⊢ n = y \to (\neg p ∥ n \leftrightarrow \neg p ∥ y)$
105	104	ralbidv	$⊢ n = y \to (\forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n \leftrightarrow \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ y)$
106	105 4	elrab2	$⊢ y \in M \leftrightarrow (y \in (1 \dots N) \land \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ y)$
107	106	simprbi	$⊢ y \in M \to \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ y$
108	102 107	syl	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ y$
109		simprrl	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to z \in M$
110		breq2	$⊢ n = z \to (p ∥ n \leftrightarrow p ∥ z)$
111	110	notbid	$⊢ n = z \to (\neg p ∥ n \leftrightarrow \neg p ∥ z)$
112	111	ralbidv	$⊢ n = z \to (\forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n \leftrightarrow \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ z)$
113	112 4	elrab2	$⊢ z \in M \leftrightarrow (z \in (1 \dots N) \land \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ z)$
114	113	simprbi	$⊢ z \in M \to \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ z$
115	109 114	syl	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ z$
116		r19.26	$⊢ \forall p \in (ℙ ∖ (1 \dots K)) (\neg p ∥ y \land \neg p ∥ z) \leftrightarrow (\forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ y \land \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ z)$
117		eldifi	$⊢ p \in (ℙ ∖ (1 \dots K)) \to p \in ℙ$
118		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
119	9 118	sstri	$⊢ M \subseteq ℕ$
120	119 102	sselid	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to y \in ℕ$
121		pceq0	$⊢ (p \in ℙ \land y \in ℕ) \to (p pCnt y = 0 \leftrightarrow \neg p ∥ y)$
122	117 120 121	syl2anr	$⊢ ((φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \land p \in (ℙ ∖ (1 \dots K))) \to (p pCnt y = 0 \leftrightarrow \neg p ∥ y)$
123	119 109	sselid	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to z \in ℕ$
124		pceq0	$⊢ (p \in ℙ \land z \in ℕ) \to (p pCnt z = 0 \leftrightarrow \neg p ∥ z)$
125	117 123 124	syl2anr	$⊢ ((φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \land p \in (ℙ ∖ (1 \dots K))) \to (p pCnt z = 0 \leftrightarrow \neg p ∥ z)$
126	122 125	anbi12d	$⊢ ((φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \land p \in (ℙ ∖ (1 \dots K))) \to ((p pCnt y = 0 \land p pCnt z = 0) \leftrightarrow (\neg p ∥ y \land \neg p ∥ z))$
127		eqtr3	$⊢ (p pCnt y = 0 \land p pCnt z = 0) \to p pCnt y = p pCnt z$
128	126 127	biimtrrdi	$⊢ ((φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \land p \in (ℙ ∖ (1 \dots K))) \to ((\neg p ∥ y \land \neg p ∥ z) \to p pCnt y = p pCnt z)$
129	128	ralimdva	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to (\forall p \in (ℙ ∖ (1 \dots K)) (\neg p ∥ y \land \neg p ∥ z) \to \forall p \in (ℙ ∖ (1 \dots K)) p pCnt y = p pCnt z)$
130	116 129	biimtrrid	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to ((\forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ y \land \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ z) \to \forall p \in (ℙ ∖ (1 \dots K)) p pCnt y = p pCnt z)$
131	108 115 130	mp2and	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to \forall p \in (ℙ ∖ (1 \dots K)) p pCnt y = p pCnt z$
132	131	biantrud	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to (\forall p \in (ℙ \cap (1 \dots K)) p pCnt y = p pCnt z \leftrightarrow (\forall p \in (ℙ \cap (1 \dots K)) p pCnt y = p pCnt z \land \forall p \in (ℙ ∖ (1 \dots K)) p pCnt y = p pCnt z))$
133		incom	$⊢ ℙ \cap (1 \dots K) = (1 \dots K) \cap ℙ$
134	133	uneq1i	$⊢ (ℙ \cap (1 \dots K)) \cup ((1 \dots K) ∖ ℙ) = ((1 \dots K) \cap ℙ) \cup ((1 \dots K) ∖ ℙ)$
135		inundif	$⊢ ((1 \dots K) \cap ℙ) \cup ((1 \dots K) ∖ ℙ) = (1 \dots K)$
136	134 135	eqtri	$⊢ (ℙ \cap (1 \dots K)) \cup ((1 \dots K) ∖ ℙ) = (1 \dots K)$
137	136	raleqi	$⊢ \forall p \in ((ℙ \cap (1 \dots K)) \cup ((1 \dots K) ∖ ℙ)) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \leftrightarrow \forall p \in (1 \dots K) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0)$
138		ralunb	$⊢ \forall p \in ((ℙ \cap (1 \dots K)) \cup ((1 \dots K) ∖ ℙ)) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \leftrightarrow (\forall p \in (ℙ \cap (1 \dots K)) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \land \forall p \in ((1 \dots K) ∖ ℙ) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0))$
139	137 138	bitr3i	$⊢ \forall p \in (1 \dots K) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \leftrightarrow (\forall p \in (ℙ \cap (1 \dots K)) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \land \forall p \in ((1 \dots K) ∖ ℙ) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0))$
140		eldifn	$⊢ p \in ((1 \dots K) ∖ ℙ) \to \neg p \in ℙ$
141		iffalse	$⊢ \neg p \in ℙ \to if (p \in ℙ, p pCnt y, 0) = 0$
142		iffalse	$⊢ \neg p \in ℙ \to if (p \in ℙ, p pCnt z, 0) = 0$
143	141 142	eqtr4d	$⊢ \neg p \in ℙ \to if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0)$
144	140 143	syl	$⊢ p \in ((1 \dots K) ∖ ℙ) \to if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0)$
145	144	rgen	$⊢ \forall p \in ((1 \dots K) ∖ ℙ) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0)$
146	145	biantru	$⊢ \forall p \in (ℙ \cap (1 \dots K)) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \leftrightarrow (\forall p \in (ℙ \cap (1 \dots K)) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \land \forall p \in ((1 \dots K) ∖ ℙ) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0))$
147		elinel1	$⊢ p \in (ℙ \cap (1 \dots K)) \to p \in ℙ$
148		iftrue	$⊢ p \in ℙ \to if (p \in ℙ, p pCnt y, 0) = p pCnt y$
149		iftrue	$⊢ p \in ℙ \to if (p \in ℙ, p pCnt z, 0) = p pCnt z$
150	148 149	eqeq12d	$⊢ p \in ℙ \to (if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \leftrightarrow p pCnt y = p pCnt z)$
151	147 150	syl	$⊢ p \in (ℙ \cap (1 \dots K)) \to (if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \leftrightarrow p pCnt y = p pCnt z)$
152	151	ralbiia	$⊢ \forall p \in (ℙ \cap (1 \dots K)) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \leftrightarrow \forall p \in (ℙ \cap (1 \dots K)) p pCnt y = p pCnt z$
153	146 152	bitr3i	$⊢ (\forall p \in (ℙ \cap (1 \dots K)) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \land \forall p \in ((1 \dots K) ∖ ℙ) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0)) \leftrightarrow \forall p \in (ℙ \cap (1 \dots K)) p pCnt y = p pCnt z$
154	139 153	bitri	$⊢ \forall p \in (1 \dots K) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \leftrightarrow \forall p \in (ℙ \cap (1 \dots K)) p pCnt y = p pCnt z$
155		inundif	$⊢ (ℙ \cap (1 \dots K)) \cup (ℙ ∖ (1 \dots K)) = ℙ$
156	155	raleqi	$⊢ \forall p \in ((ℙ \cap (1 \dots K)) \cup (ℙ ∖ (1 \dots K))) p pCnt y = p pCnt z \leftrightarrow \forall p \in ℙ p pCnt y = p pCnt z$
157		ralunb	$⊢ \forall p \in ((ℙ \cap (1 \dots K)) \cup (ℙ ∖ (1 \dots K))) p pCnt y = p pCnt z \leftrightarrow (\forall p \in (ℙ \cap (1 \dots K)) p pCnt y = p pCnt z \land \forall p \in (ℙ ∖ (1 \dots K)) p pCnt y = p pCnt z)$
158	156 157	bitr3i	$⊢ \forall p \in ℙ p pCnt y = p pCnt z \leftrightarrow (\forall p \in (ℙ \cap (1 \dots K)) p pCnt y = p pCnt z \land \forall p \in (ℙ ∖ (1 \dots K)) p pCnt y = p pCnt z)$
159	132 154 158	3bitr4g	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to (\forall p \in (1 \dots K) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \leftrightarrow \forall p \in ℙ p pCnt y = p pCnt z)$
160	120	nnnn0d	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to y \in ℕ_{0}$
161	123	nnnn0d	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to z \in ℕ_{0}$
162		pc11	$⊢ (y \in ℕ_{0} \land z \in ℕ_{0}) \to (y = z \leftrightarrow \forall p \in ℙ p pCnt y = p pCnt z)$
163	160 161 162	syl2anc	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to (y = z \leftrightarrow \forall p \in ℙ p pCnt y = p pCnt z)$
164	159 163	bitr4d	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to (\forall p \in (1 \dots K) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0) \leftrightarrow y = z)$
165	101 164	bitrid	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to ((n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) = (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) \leftrightarrow y = z)$
166	165	ex	$⊢ φ \to (((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1)) \to ((n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) = (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) \leftrightarrow y = z))$
167	76 166	biimtrid	$⊢ φ \to ((y \in \{x \in M \| Q (x) = 1\} \land z \in \{x \in M \| Q (x) = 1\}) \to ((n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) = (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) \leftrightarrow y = z))$
168	73 167	dom2d	$⊢ φ \to ({\{0, 1\}}^{(1 \dots K)} \in V \to \{x \in M \| Q (x) = 1\} ≼ ({\{0, 1\}}^{(1 \dots K)}))$
169	6 168	mpi	$⊢ φ \to \{x \in M \| Q (x) = 1\} ≼ ({\{0, 1\}}^{(1 \dots K)})$
170		fzfi	$⊢ (1 \dots N) \in Fin$
171		ssrab2	$⊢ \{n \in (1 \dots N) \| \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n\} \subseteq (1 \dots N)$
172		ssfi	$⊢ ((1 \dots N) \in Fin \land \{n \in (1 \dots N) \| \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n\} \subseteq (1 \dots N)) \to \{n \in (1 \dots N) \| \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n\} \in Fin$
173	170 171 172	mp2an	$⊢ \{n \in (1 \dots N) \| \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n\} \in Fin$
174	4 173	eqeltri	$⊢ M \in Fin$
175		ssrab2	$⊢ \{x \in M \| Q (x) = 1\} \subseteq M$
176		ssfi	$⊢ (M \in Fin \land \{x \in M \| Q (x) = 1\} \subseteq M) \to \{x \in M \| Q (x) = 1\} \in Fin$
177	174 175 176	mp2an	$⊢ \{x \in M \| Q (x) = 1\} \in Fin$
178		prfi	$⊢ \{0, 1\} \in Fin$
179		fzfid	$⊢ φ \to (1 \dots K) \in Fin$
180		mapfi	$⊢ (\{0, 1\} \in Fin \land (1 \dots K) \in Fin) \to {\{0, 1\}}^{(1 \dots K)} \in Fin$
181	178 179 180	sylancr	$⊢ φ \to {\{0, 1\}}^{(1 \dots K)} \in Fin$
182		hashdom	$⊢ (\{x \in M \| Q (x) = 1\} \in Fin \land {\{0, 1\}}^{(1 \dots K)} \in Fin) \to (\|\{x \in M \| Q (x) = 1\}\| \leq \|{\{0, 1\}}^{(1 \dots K)}\| \leftrightarrow \{x \in M \| Q (x) = 1\} ≼ ({\{0, 1\}}^{(1 \dots K)}))$
183	177 181 182	sylancr	$⊢ φ \to (\|\{x \in M \| Q (x) = 1\}\| \leq \|{\{0, 1\}}^{(1 \dots K)}\| \leftrightarrow \{x \in M \| Q (x) = 1\} ≼ ({\{0, 1\}}^{(1 \dots K)}))$
184	169 183	mpbird	$⊢ φ \to \|\{x \in M \| Q (x) = 1\}\| \leq \|{\{0, 1\}}^{(1 \dots K)}\|$
185		hashmap	$⊢ (\{0, 1\} \in Fin \land (1 \dots K) \in Fin) \to \|{\{0, 1\}}^{(1 \dots K)}\| = {\|\{0, 1\}\|}^{\|(1 \dots K)\|}$
186	178 179 185	sylancr	$⊢ φ \to \|{\{0, 1\}}^{(1 \dots K)}\| = {\|\{0, 1\}\|}^{\|(1 \dots K)\|}$
187		prhash2ex	$⊢ \|\{0, 1\}\| = 2$
188	187	a1i	$⊢ φ \to \|\{0, 1\}\| = 2$
189	2	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
190		hashfz1	$⊢ K \in ℕ_{0} \to \|(1 \dots K)\| = K$
191	189 190	syl	$⊢ φ \to \|(1 \dots K)\| = K$
192	188 191	oveq12d	$⊢ φ \to {\|\{0, 1\}\|}^{\|(1 \dots K)\|} = 2^{K}$
193	186 192	eqtrd	$⊢ φ \to \|{\{0, 1\}}^{(1 \dots K)}\| = 2^{K}$
194	184 193	breqtrd	$⊢ φ \to \|\{x \in M \| Q (x) = 1\}\| \leq 2^{K}$

Metamath Proof Explorer

Theorem prmreclem2

Proof