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) (Proof shortened by Timothy J. O'Malley, 9-Oct-2026)

	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		fz01pr	$⊢ (0 \dots 1) = \{0, 1\}$
57	55 56	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\}$
58		0elpr01	$⊢ 0 \in \{0, 1\}$
59	58	a1i	$⊢ (((φ \land (y \in M \land Q (y) = 1)) \land n \in (1 \dots K)) \land \neg n \in ℙ) \to 0 \in \{0, 1\}$
60	57 59	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\}$
61	60	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\}$
62		prex	$⊢ \{0, 1\} \in V$
63		ovex	$⊢ (1 \dots K) \in V$
64	62 63	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\}$
65	61 64	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)})$
66	65	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)}))$
67	8 66	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)}))$
68		fveqeq2	$⊢ x = z \to (Q (x) = 1 \leftrightarrow Q (z) = 1)$
69	68	elrab	$⊢ z \in \{x \in M \| Q (x) = 1\} \leftrightarrow (z \in M \land Q (z) = 1)$
70	8 69	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))$
71		ovex	$⊢ n pCnt y \in V$
72		c0ex	$⊢ 0 \in V$
73	71 72	ifex	$⊢ if (n \in ℙ, n pCnt y, 0) \in V$
74		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))$
75	73 74	fnmpti	$⊢ (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt y, 0)) Fn (1 \dots K)$
76		ovex	$⊢ n pCnt z \in V$
77	76 72	ifex	$⊢ if (n \in ℙ, n pCnt z, 0) \in V$
78		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))$
79	77 78	fnmpti	$⊢ (n \in (1 \dots K) ⟼ if (n \in ℙ, n pCnt z, 0)) Fn (1 \dots K)$
80		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))$
81	75 79 80	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)$
82		eleq1w	$⊢ n = p \to (n \in ℙ \leftrightarrow p \in ℙ)$
83		oveq1	$⊢ n = p \to n pCnt y = p pCnt y$
84	82 83	ifbieq1d	$⊢ n = p \to if (n \in ℙ, n pCnt y, 0) = if (p \in ℙ, p pCnt y, 0)$
85		ovex	$⊢ p pCnt y \in V$
86	85 72	ifex	$⊢ if (p \in ℙ, p pCnt y, 0) \in V$
87	84 74 86	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)$
88		oveq1	$⊢ n = p \to n pCnt z = p pCnt z$
89	82 88	ifbieq1d	$⊢ n = p \to if (n \in ℙ, n pCnt z, 0) = if (p \in ℙ, p pCnt z, 0)$
90		ovex	$⊢ p pCnt z \in V$
91	90 72	ifex	$⊢ if (p \in ℙ, p pCnt z, 0) \in V$
92	89 78 91	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)$
93	87 92	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))$
94	93	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)$
95	81 94	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)$
96		simprll	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to y \in M$
97		breq2	$⊢ n = y \to (p ∥ n \leftrightarrow p ∥ y)$
98	97	notbid	$⊢ n = y \to (\neg p ∥ n \leftrightarrow \neg p ∥ y)$
99	98	ralbidv	$⊢ n = y \to (\forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n \leftrightarrow \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ y)$
100	99 4	elrab2	$⊢ y \in M \leftrightarrow (y \in (1 \dots N) \land \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ y)$
101	100	simprbi	$⊢ y \in M \to \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ y$
102	96 101	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$
103		simprrl	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to z \in M$
104		breq2	$⊢ n = z \to (p ∥ n \leftrightarrow p ∥ z)$
105	104	notbid	$⊢ n = z \to (\neg p ∥ n \leftrightarrow \neg p ∥ z)$
106	105	ralbidv	$⊢ n = z \to (\forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n \leftrightarrow \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ z)$
107	106 4	elrab2	$⊢ z \in M \leftrightarrow (z \in (1 \dots N) \land \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ z)$
108	107	simprbi	$⊢ z \in M \to \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ z$
109	103 108	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$
110		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)$
111		eldifi	$⊢ p \in (ℙ ∖ (1 \dots K)) \to p \in ℙ$
112		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
113	9 112	sstri	$⊢ M \subseteq ℕ$
114	113 96	sselid	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to y \in ℕ$
115		pceq0	$⊢ (p \in ℙ \land y \in ℕ) \to (p pCnt y = 0 \leftrightarrow \neg p ∥ y)$
116	111 114 115	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)$
117	113 103	sselid	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to z \in ℕ$
118		pceq0	$⊢ (p \in ℙ \land z \in ℕ) \to (p pCnt z = 0 \leftrightarrow \neg p ∥ z)$
119	111 117 118	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)$
120	116 119	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))$
121		eqtr3	$⊢ (p pCnt y = 0 \land p pCnt z = 0) \to p pCnt y = p pCnt z$
122	120 121	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)$
123	122	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)$
124	110 123	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)$
125	102 109 124	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$
126	125	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))$
127		incom	$⊢ ℙ \cap (1 \dots K) = (1 \dots K) \cap ℙ$
128	127	uneq1i	$⊢ (ℙ \cap (1 \dots K)) \cup ((1 \dots K) ∖ ℙ) = ((1 \dots K) \cap ℙ) \cup ((1 \dots K) ∖ ℙ)$
129		inundif	$⊢ ((1 \dots K) \cap ℙ) \cup ((1 \dots K) ∖ ℙ) = (1 \dots K)$
130	128 129	eqtri	$⊢ (ℙ \cap (1 \dots K)) \cup ((1 \dots K) ∖ ℙ) = (1 \dots K)$
131	130	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)$
132		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))$
133	131 132	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))$
134		eldifn	$⊢ p \in ((1 \dots K) ∖ ℙ) \to \neg p \in ℙ$
135		iffalse	$⊢ \neg p \in ℙ \to if (p \in ℙ, p pCnt y, 0) = 0$
136		iffalse	$⊢ \neg p \in ℙ \to if (p \in ℙ, p pCnt z, 0) = 0$
137	135 136	eqtr4d	$⊢ \neg p \in ℙ \to if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0)$
138	134 137	syl	$⊢ p \in ((1 \dots K) ∖ ℙ) \to if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0)$
139	138	rgen	$⊢ \forall p \in ((1 \dots K) ∖ ℙ) if (p \in ℙ, p pCnt y, 0) = if (p \in ℙ, p pCnt z, 0)$
140	139	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))$
141		elinel1	$⊢ p \in (ℙ \cap (1 \dots K)) \to p \in ℙ$
142		iftrue	$⊢ p \in ℙ \to if (p \in ℙ, p pCnt y, 0) = p pCnt y$
143		iftrue	$⊢ p \in ℙ \to if (p \in ℙ, p pCnt z, 0) = p pCnt z$
144	142 143	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)$
145	141 144	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)$
146	145	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$
147	140 146	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$
148	133 147	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$
149		inundif	$⊢ (ℙ \cap (1 \dots K)) \cup (ℙ ∖ (1 \dots K)) = ℙ$
150	149	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$
151		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)$
152	150 151	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)$
153	126 148 152	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)$
154	114	nnnn0d	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to y \in ℕ_{0}$
155	117	nnnn0d	$⊢ (φ \land ((y \in M \land Q (y) = 1) \land (z \in M \land Q (z) = 1))) \to z \in ℕ_{0}$
156		pc11	$⊢ (y \in ℕ_{0} \land z \in ℕ_{0}) \to (y = z \leftrightarrow \forall p \in ℙ p pCnt y = p pCnt z)$
157	154 155 156	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)$
158	153 157	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)$
159	95 158	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)$
160	159	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))$
161	70 160	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))$
162	67 161	dom2d	$⊢ φ \to ({\{0, 1\}}^{(1 \dots K)} \in V \to \{x \in M \| Q (x) = 1\} ≼ ({\{0, 1\}}^{(1 \dots K)}))$
163	6 162	mpi	$⊢ φ \to \{x \in M \| Q (x) = 1\} ≼ ({\{0, 1\}}^{(1 \dots K)})$
164		hashdomi	$⊢ \{x \in M \| Q (x) = 1\} ≼ ({\{0, 1\}}^{(1 \dots K)}) \to \|\{x \in M \| Q (x) = 1\}\| \leq \|{\{0, 1\}}^{(1 \dots K)}\|$
165	163 164	syl	$⊢ φ \to \|\{x \in M \| Q (x) = 1\}\| \leq \|{\{0, 1\}}^{(1 \dots K)}\|$
166		prfi	$⊢ \{0, 1\} \in Fin$
167		fzfid	$⊢ φ \to (1 \dots K) \in Fin$
168		hashmap	$⊢ (\{0, 1\} \in Fin \land (1 \dots K) \in Fin) \to \|{\{0, 1\}}^{(1 \dots K)}\| = {\|\{0, 1\}\|}^{\|(1 \dots K)\|}$
169	166 167 168	sylancr	$⊢ φ \to \|{\{0, 1\}}^{(1 \dots K)}\| = {\|\{0, 1\}\|}^{\|(1 \dots K)\|}$
170		prhash2ex	$⊢ \|\{0, 1\}\| = 2$
171	170	a1i	$⊢ φ \to \|\{0, 1\}\| = 2$
172	2	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
173		hashfz1	$⊢ K \in ℕ_{0} \to \|(1 \dots K)\| = K$
174	172 173	syl	$⊢ φ \to \|(1 \dots K)\| = K$
175	171 174	oveq12d	$⊢ φ \to {\|\{0, 1\}\|}^{\|(1 \dots K)\|} = 2^{K}$
176	169 175	eqtrd	$⊢ φ \to \|{\{0, 1\}}^{(1 \dots K)}\| = 2^{K}$
177	165 176	breqtrd	$⊢ φ \to \|\{x \in M \| Q (x) = 1\}\| \leq 2^{K}$

Metamath Proof Explorer

Theorem prmreclem2

Proof