4sqlem11

Description: Lemma for 4sq . Use the pigeonhole principle to show that the sets { m ^ 2 | m e. ( 0 ... N ) } and { -u 1 - n ^ 2 | n e. ( 0 ... N ) } have a common element, mod P . (Contributed by Mario Carneiro, 15-Jul-2014)

	Ref	Expression
Hypotheses	4sq.1	$⊢ S = \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
	4sq.2	$⊢ φ \to N \in ℕ$
	4sq.3	$⊢ φ \to P = 2 \cdot N + 1$
	4sq.4	$⊢ φ \to P \in ℙ$
	4sqlem11.5	$⊢ A = \{u \| \exists m \in (0 \dots N) u = m^{2} \mod P\}$
	4sqlem11.6	$⊢ F = (v \in A ⟼ P - 1 - v)$
Assertion	4sqlem11	$⊢ φ \to A \cap ran F \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		4sq.1	$⊢ S = \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
2		4sq.2	$⊢ φ \to N \in ℕ$
3		4sq.3	$⊢ φ \to P = 2 \cdot N + 1$
4		4sq.4	$⊢ φ \to P \in ℙ$
5		4sqlem11.5	$⊢ A = \{u \| \exists m \in (0 \dots N) u = m^{2} \mod P\}$
6		4sqlem11.6	$⊢ F = (v \in A ⟼ P - 1 - v)$
7		fzfid	$⊢ φ \to (0 \dots P - 1) \in Fin$
8		elfzelz	$⊢ m \in (0 \dots N) \to m \in ℤ$
9		zsqcl	$⊢ m \in ℤ \to m^{2} \in ℤ$
10	8 9	syl	$⊢ m \in (0 \dots N) \to m^{2} \in ℤ$
11		prmnn	$⊢ P \in ℙ \to P \in ℕ$
12	4 11	syl	$⊢ φ \to P \in ℕ$
13		zmodfz	$⊢ (m^{2} \in ℤ \land P \in ℕ) \to m^{2} \mod P \in (0 \dots P - 1)$
14	10 12 13	syl2anr	$⊢ (φ \land m \in (0 \dots N)) \to m^{2} \mod P \in (0 \dots P - 1)$
15		eleq1a	$⊢ m^{2} \mod P \in (0 \dots P - 1) \to (u = m^{2} \mod P \to u \in (0 \dots P - 1))$
16	14 15	syl	$⊢ (φ \land m \in (0 \dots N)) \to (u = m^{2} \mod P \to u \in (0 \dots P - 1))$
17	16	rexlimdva	$⊢ φ \to (\exists m \in (0 \dots N) u = m^{2} \mod P \to u \in (0 \dots P - 1))$
18	17	abssdv	$⊢ φ \to \{u \| \exists m \in (0 \dots N) u = m^{2} \mod P\} \subseteq (0 \dots P - 1)$
19	5 18	eqsstrid	$⊢ φ \to A \subseteq (0 \dots P - 1)$
20		prmz	$⊢ P \in ℙ \to P \in ℤ$
21	4 20	syl	$⊢ φ \to P \in ℤ$
22		peano2zm	$⊢ P \in ℤ \to P - 1 \in ℤ$
23	21 22	syl	$⊢ φ \to P - 1 \in ℤ$
24	23	zcnd	$⊢ φ \to P - 1 \in ℂ$
25	24	addlidd	$⊢ φ \to 0 + P - 1 = P - 1$
26	25	oveq1d	$⊢ φ \to 0 + (P - 1) - v = P - 1 - v$
27	26	adantr	$⊢ (φ \land v \in A) \to 0 + (P - 1) - v = P - 1 - v$
28	19	sselda	$⊢ (φ \land v \in A) \to v \in (0 \dots P - 1)$
29		fzrev3i	$⊢ v \in (0 \dots P - 1) \to 0 + (P - 1) - v \in (0 \dots P - 1)$
30	28 29	syl	$⊢ (φ \land v \in A) \to 0 + (P - 1) - v \in (0 \dots P - 1)$
31	27 30	eqeltrrd	$⊢ (φ \land v \in A) \to P - 1 - v \in (0 \dots P - 1)$
32	31 6	fmptd	$⊢ φ \to F : A ⟶ (0 \dots P - 1)$
33	32	frnd	$⊢ φ \to ran F \subseteq (0 \dots P - 1)$
34	19 33	unssd	$⊢ φ \to A \cup ran F \subseteq (0 \dots P - 1)$
35	7 34	ssfid	$⊢ φ \to A \cup ran F \in Fin$
36		hashcl	$⊢ A \cup ran F \in Fin \to \|A \cup ran F\| \in ℕ_{0}$
37	35 36	syl	$⊢ φ \to \|A \cup ran F\| \in ℕ_{0}$
38	37	nn0red	$⊢ φ \to \|A \cup ran F\| \in ℝ$
39	21	zred	$⊢ φ \to P \in ℝ$
40		ssdomg	$⊢ (0 \dots P - 1) \in Fin \to (A \cup ran F \subseteq (0 \dots P - 1) \to (A \cup ran F) ≼ (0 \dots P - 1))$
41	7 34 40	sylc	$⊢ φ \to (A \cup ran F) ≼ (0 \dots P - 1)$
42		hashdom	$⊢ (A \cup ran F \in Fin \land (0 \dots P - 1) \in Fin) \to (\|A \cup ran F\| \leq \|(0 \dots P - 1)\| \leftrightarrow (A \cup ran F) ≼ (0 \dots P - 1))$
43	35 7 42	syl2anc	$⊢ φ \to (\|A \cup ran F\| \leq \|(0 \dots P - 1)\| \leftrightarrow (A \cup ran F) ≼ (0 \dots P - 1))$
44	41 43	mpbird	$⊢ φ \to \|A \cup ran F\| \leq \|(0 \dots P - 1)\|$
45		fz01en	$⊢ P \in ℤ \to (0 \dots P - 1) \approx (1 \dots P)$
46	21 45	syl	$⊢ φ \to (0 \dots P - 1) \approx (1 \dots P)$
47		fzfid	$⊢ φ \to (1 \dots P) \in Fin$
48		hashen	$⊢ ((0 \dots P - 1) \in Fin \land (1 \dots P) \in Fin) \to (\|(0 \dots P - 1)\| = \|(1 \dots P)\| \leftrightarrow (0 \dots P - 1) \approx (1 \dots P))$
49	7 47 48	syl2anc	$⊢ φ \to (\|(0 \dots P - 1)\| = \|(1 \dots P)\| \leftrightarrow (0 \dots P - 1) \approx (1 \dots P))$
50	46 49	mpbird	$⊢ φ \to \|(0 \dots P - 1)\| = \|(1 \dots P)\|$
51	12	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
52		hashfz1	$⊢ P \in ℕ_{0} \to \|(1 \dots P)\| = P$
53	51 52	syl	$⊢ φ \to \|(1 \dots P)\| = P$
54	50 53	eqtrd	$⊢ φ \to \|(0 \dots P - 1)\| = P$
55	44 54	breqtrd	$⊢ φ \to \|A \cup ran F\| \leq P$
56	38 39 55	lensymd	$⊢ φ \to \neg P < \|A \cup ran F\|$
57	39	adantr	$⊢ (φ \land A \cap ran F = \emptyset) \to P \in ℝ$
58	57	ltp1d	$⊢ (φ \land A \cap ran F = \emptyset) \to P < P + 1$
59	2	nncnd	$⊢ φ \to N \in ℂ$
60		1cnd	$⊢ φ \to 1 \in ℂ$
61	59 59 60 60	add4d	$⊢ φ \to N + N + 1 + 1 = N + 1 + N + 1$
62	3	oveq1d	$⊢ φ \to P + 1 = 2 \cdot N + 1 + 1$
63		2cn	$⊢ 2 \in ℂ$
64		mulcl	$⊢ (2 \in ℂ \land N \in ℂ) \to 2 \cdot N \in ℂ$
65	63 59 64	sylancr	$⊢ φ \to 2 \cdot N \in ℂ$
66	65 60 60	addassd	$⊢ φ \to 2 \cdot N + 1 + 1 = 2 \cdot N + 1 + 1$
67	59	2timesd	$⊢ φ \to 2 \cdot N = N + N$
68	67	oveq1d	$⊢ φ \to 2 \cdot N + 1 + 1 = N + N + 1 + 1$
69	62 66 68	3eqtrd	$⊢ φ \to P + 1 = N + N + 1 + 1$
70	14	ex	$⊢ φ \to (m \in (0 \dots N) \to m^{2} \mod P \in (0 \dots P - 1))$
71	12	adantr	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to P \in ℕ$
72	8	ad2antrl	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m \in ℤ$
73	72 9	syl	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m^{2} \in ℤ$
74		elfzelz	$⊢ u \in (0 \dots N) \to u \in ℤ$
75	74	ad2antll	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to u \in ℤ$
76		zsqcl	$⊢ u \in ℤ \to u^{2} \in ℤ$
77	75 76	syl	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to u^{2} \in ℤ$
78		moddvds	$⊢ (P \in ℕ \land m^{2} \in ℤ \land u^{2} \in ℤ) \to (m^{2} \mod P = u^{2} \mod P \leftrightarrow P ∥ (m^{2} - u^{2}))$
79	71 73 77 78	syl3anc	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (m^{2} \mod P = u^{2} \mod P \leftrightarrow P ∥ (m^{2} - u^{2}))$
80	72	zcnd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m \in ℂ$
81	75	zcnd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to u \in ℂ$
82		subsq	$⊢ (m \in ℂ \land u \in ℂ) \to m^{2} - u^{2} = (m + u) (m - u)$
83	80 81 82	syl2anc	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m^{2} - u^{2} = (m + u) (m - u)$
84	83	breq2d	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (P ∥ (m^{2} - u^{2}) \leftrightarrow P ∥ (m + u) (m - u))$
85	4	adantr	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to P \in ℙ$
86	72 75	zaddcld	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m + u \in ℤ$
87	72 75	zsubcld	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m - u \in ℤ$
88		euclemma	$⊢ (P \in ℙ \land m + u \in ℤ \land m - u \in ℤ) \to (P ∥ (m + u) (m - u) \leftrightarrow (P ∥ (m + u) \lor P ∥ (m - u)))$
89	85 86 87 88	syl3anc	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (P ∥ (m + u) (m - u) \leftrightarrow (P ∥ (m + u) \lor P ∥ (m - u)))$
90	79 84 89	3bitrd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (m^{2} \mod P = u^{2} \mod P \leftrightarrow (P ∥ (m + u) \lor P ∥ (m - u)))$
91	86	zred	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m + u \in ℝ$
92		2re	$⊢ 2 \in ℝ$
93	2	nnred	$⊢ φ \to N \in ℝ$
94		remulcl	$⊢ (2 \in ℝ \land N \in ℝ) \to 2 \cdot N \in ℝ$
95	92 93 94	sylancr	$⊢ φ \to 2 \cdot N \in ℝ$
96	95	adantr	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to 2 \cdot N \in ℝ$
97	85 20	syl	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to P \in ℤ$
98	97	zred	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to P \in ℝ$
99	72	zred	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m \in ℝ$
100	75	zred	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to u \in ℝ$
101	93	adantr	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to N \in ℝ$
102		elfzle2	$⊢ m \in (0 \dots N) \to m \leq N$
103	102	ad2antrl	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m \leq N$
104		elfzle2	$⊢ u \in (0 \dots N) \to u \leq N$
105	104	ad2antll	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to u \leq N$
106	99 100 101 101 103 105	le2addd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m + u \leq N + N$
107	59	adantr	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to N \in ℂ$
108	107	2timesd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to 2 \cdot N = N + N$
109	106 108	breqtrrd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m + u \leq 2 \cdot N$
110	95	ltp1d	$⊢ φ \to 2 \cdot N < 2 \cdot N + 1$
111	110 3	breqtrrd	$⊢ φ \to 2 \cdot N < P$
112	111	adantr	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to 2 \cdot N < P$
113	91 96 98 109 112	lelttrd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m + u < P$
114	91 98	ltnled	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (m + u < P \leftrightarrow \neg P \leq m + u)$
115	113 114	mpbid	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \neg P \leq m + u$
116	115	adantr	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to \neg P \leq m + u$
117	21	ad2antrr	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to P \in ℤ$
118	86	adantr	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to m + u \in ℤ$
119		1red	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to 1 \in ℝ$
120		nn0abscl	$⊢ m - u \in ℤ \to \|m - u\| \in ℕ_{0}$
121	87 120	syl	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \|m - u\| \in ℕ_{0}$
122	121	nn0red	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \|m - u\| \in ℝ$
123	122	adantr	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to \|m - u\| \in ℝ$
124	118	zred	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to m + u \in ℝ$
125	121	adantr	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to \|m - u\| \in ℕ_{0}$
126	125	nn0zd	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to \|m - u\| \in ℤ$
127	87	zcnd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m - u \in ℂ$
128	127	adantr	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to m - u \in ℂ$
129	80 81	subeq0ad	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (m - u = 0 \leftrightarrow m = u)$
130	129	necon3bid	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (m - u \neq 0 \leftrightarrow m \neq u)$
131	130	biimpar	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to m - u \neq 0$
132	128 131	absrpcld	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to \|m - u\| \in ℝ^{+}$
133	132	rpgt0d	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to 0 < \|m - u\|$
134		elnnz	$⊢ \|m - u\| \in ℕ \leftrightarrow (\|m - u\| \in ℤ \land 0 < \|m - u\|)$
135	126 133 134	sylanbrc	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to \|m - u\| \in ℕ$
136	135	nnge1d	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to 1 \leq \|m - u\|$
137		0cnd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to 0 \in ℂ$
138	80 81 137	abs3difd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \|m - u\| \leq \|m - 0\| + \|0 - u\|$
139	80	subid1d	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to m - 0 = m$
140	139	fveq2d	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \|m - 0\| = \|m\|$
141		elfzle1	$⊢ m \in (0 \dots N) \to 0 \leq m$
142	141	ad2antrl	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to 0 \leq m$
143	99 142	absidd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \|m\| = m$
144	140 143	eqtrd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \|m - 0\| = m$
145		0cn	$⊢ 0 \in ℂ$
146		abssub	$⊢ (0 \in ℂ \land u \in ℂ) \to \|0 - u\| = \|u - 0\|$
147	145 81 146	sylancr	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \|0 - u\| = \|u - 0\|$
148	81	subid1d	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to u - 0 = u$
149	148	fveq2d	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \|u - 0\| = \|u\|$
150		elfzle1	$⊢ u \in (0 \dots N) \to 0 \leq u$
151	150	ad2antll	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to 0 \leq u$
152	100 151	absidd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \|u\| = u$
153	147 149 152	3eqtrd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \|0 - u\| = u$
154	144 153	oveq12d	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \|m - 0\| + \|0 - u\| = m + u$
155	138 154	breqtrd	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \|m - u\| \leq m + u$
156	155	adantr	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to \|m - u\| \leq m + u$
157	119 123 124 136 156	letrd	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to 1 \leq m + u$
158		elnnz1	$⊢ m + u \in ℕ \leftrightarrow (m + u \in ℤ \land 1 \leq m + u)$
159	118 157 158	sylanbrc	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to m + u \in ℕ$
160		dvdsle	$⊢ (P \in ℤ \land m + u \in ℕ) \to (P ∥ (m + u) \to P \leq m + u)$
161	117 159 160	syl2anc	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to (P ∥ (m + u) \to P \leq m + u)$
162	116 161	mtod	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to \neg P ∥ (m + u)$
163	162	ex	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (m \neq u \to \neg P ∥ (m + u))$
164	163	necon4ad	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (P ∥ (m + u) \to m = u)$
165		dvdsabsb	$⊢ (P \in ℤ \land m - u \in ℤ) \to (P ∥ (m - u) \leftrightarrow P ∥ \|m - u\|)$
166	97 87 165	syl2anc	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (P ∥ (m - u) \leftrightarrow P ∥ \|m - u\|)$
167		letr	$⊢ (P \in ℝ \land \|m - u\| \in ℝ \land m + u \in ℝ) \to ((P \leq \|m - u\| \land \|m - u\| \leq m + u) \to P \leq m + u)$
168	98 122 91 167	syl3anc	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to ((P \leq \|m - u\| \land \|m - u\| \leq m + u) \to P \leq m + u)$
169	155 168	mpan2d	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (P \leq \|m - u\| \to P \leq m + u)$
170	115 169	mtod	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to \neg P \leq \|m - u\|$
171	170	adantr	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to \neg P \leq \|m - u\|$
172	97	adantr	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to P \in ℤ$
173		dvdsle	$⊢ (P \in ℤ \land \|m - u\| \in ℕ) \to (P ∥ \|m - u\| \to P \leq \|m - u\|)$
174	172 135 173	syl2anc	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to (P ∥ \|m - u\| \to P \leq \|m - u\|)$
175	171 174	mtod	$⊢ ((φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \land m \neq u) \to \neg P ∥ \|m - u\|$
176	175	ex	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (m \neq u \to \neg P ∥ \|m - u\|)$
177	176	necon4ad	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (P ∥ \|m - u\| \to m = u)$
178	166 177	sylbid	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (P ∥ (m - u) \to m = u)$
179	164 178	jaod	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to ((P ∥ (m + u) \lor P ∥ (m - u)) \to m = u)$
180	90 179	sylbid	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (m^{2} \mod P = u^{2} \mod P \to m = u)$
181		oveq1	$⊢ m = u \to m^{2} = u^{2}$
182	181	oveq1d	$⊢ m = u \to m^{2} \mod P = u^{2} \mod P$
183	180 182	impbid1	$⊢ (φ \land (m \in (0 \dots N) \land u \in (0 \dots N))) \to (m^{2} \mod P = u^{2} \mod P \leftrightarrow m = u)$
184	183	ex	$⊢ φ \to ((m \in (0 \dots N) \land u \in (0 \dots N)) \to (m^{2} \mod P = u^{2} \mod P \leftrightarrow m = u))$
185	70 184	dom2lem	$⊢ φ \to (m \in (0 \dots N) ⟼ m^{2} \mod P) : (0 \dots N) \underset{1-1}{⟶} (0 \dots P - 1)$
186		f1f1orn	$⊢ (m \in (0 \dots N) ⟼ m^{2} \mod P) : (0 \dots N) \underset{1-1}{⟶} (0 \dots P - 1) \to (m \in (0 \dots N) ⟼ m^{2} \mod P) : (0 \dots N) \underset{1-1 onto}{⟶} ran (m \in (0 \dots N) ⟼ m^{2} \mod P)$
187	185 186	syl	$⊢ φ \to (m \in (0 \dots N) ⟼ m^{2} \mod P) : (0 \dots N) \underset{1-1 onto}{⟶} ran (m \in (0 \dots N) ⟼ m^{2} \mod P)$
188		eqid	$⊢ (m \in (0 \dots N) ⟼ m^{2} \mod P) = (m \in (0 \dots N) ⟼ m^{2} \mod P)$
189	188	rnmpt	$⊢ ran (m \in (0 \dots N) ⟼ m^{2} \mod P) = \{u \| \exists m \in (0 \dots N) u = m^{2} \mod P\}$
190	5 189	eqtr4i	$⊢ A = ran (m \in (0 \dots N) ⟼ m^{2} \mod P)$
191		f1oeq3	$⊢ A = ran (m \in (0 \dots N) ⟼ m^{2} \mod P) \to ((m \in (0 \dots N) ⟼ m^{2} \mod P) : (0 \dots N) \underset{1-1 onto}{⟶} A \leftrightarrow (m \in (0 \dots N) ⟼ m^{2} \mod P) : (0 \dots N) \underset{1-1 onto}{⟶} ran (m \in (0 \dots N) ⟼ m^{2} \mod P))$
192	190 191	ax-mp	$⊢ (m \in (0 \dots N) ⟼ m^{2} \mod P) : (0 \dots N) \underset{1-1 onto}{⟶} A \leftrightarrow (m \in (0 \dots N) ⟼ m^{2} \mod P) : (0 \dots N) \underset{1-1 onto}{⟶} ran (m \in (0 \dots N) ⟼ m^{2} \mod P)$
193	187 192	sylibr	$⊢ φ \to (m \in (0 \dots N) ⟼ m^{2} \mod P) : (0 \dots N) \underset{1-1 onto}{⟶} A$
194		ovex	$⊢ (0 \dots N) \in V$
195	194	f1oen	$⊢ (m \in (0 \dots N) ⟼ m^{2} \mod P) : (0 \dots N) \underset{1-1 onto}{⟶} A \to (0 \dots N) \approx A$
196	193 195	syl	$⊢ φ \to (0 \dots N) \approx A$
197	196	ensymd	$⊢ φ \to A \approx (0 \dots N)$
198		ax-1cn	$⊢ 1 \in ℂ$
199		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
200	59 198 199	sylancl	$⊢ φ \to N + 1 - 1 = N$
201	200	oveq2d	$⊢ φ \to (0 \dots N + 1 - 1) = (0 \dots N)$
202	2	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
203		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
204	202 203	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
205	204	nn0zd	$⊢ φ \to N + 1 \in ℤ$
206		fz01en	$⊢ N + 1 \in ℤ \to (0 \dots N + 1 - 1) \approx (1 \dots N + 1)$
207	205 206	syl	$⊢ φ \to (0 \dots N + 1 - 1) \approx (1 \dots N + 1)$
208	201 207	eqbrtrrd	$⊢ φ \to (0 \dots N) \approx (1 \dots N + 1)$
209		entr	$⊢ (A \approx (0 \dots N) \land (0 \dots N) \approx (1 \dots N + 1)) \to A \approx (1 \dots N + 1)$
210	197 208 209	syl2anc	$⊢ φ \to A \approx (1 \dots N + 1)$
211	7 19	ssfid	$⊢ φ \to A \in Fin$
212		fzfid	$⊢ φ \to (1 \dots N + 1) \in Fin$
213		hashen	$⊢ (A \in Fin \land (1 \dots N + 1) \in Fin) \to (\|A\| = \|(1 \dots N + 1)\| \leftrightarrow A \approx (1 \dots N + 1))$
214	211 212 213	syl2anc	$⊢ φ \to (\|A\| = \|(1 \dots N + 1)\| \leftrightarrow A \approx (1 \dots N + 1))$
215	210 214	mpbird	$⊢ φ \to \|A\| = \|(1 \dots N + 1)\|$
216		hashfz1	$⊢ N + 1 \in ℕ_{0} \to \|(1 \dots N + 1)\| = N + 1$
217	204 216	syl	$⊢ φ \to \|(1 \dots N + 1)\| = N + 1$
218	215 217	eqtrd	$⊢ φ \to \|A\| = N + 1$
219	31	ex	$⊢ φ \to (v \in A \to P - 1 - v \in (0 \dots P - 1))$
220	24	adantr	$⊢ (φ \land (v \in A \land k \in A)) \to P - 1 \in ℂ$
221		fzssuz	$⊢ (0 \dots P - 1) \subseteq ℤ_{\geq 0}$
222		uzssz	$⊢ ℤ_{\geq 0} \subseteq ℤ$
223		zsscn	$⊢ ℤ \subseteq ℂ$
224	222 223	sstri	$⊢ ℤ_{\geq 0} \subseteq ℂ$
225	221 224	sstri	$⊢ (0 \dots P - 1) \subseteq ℂ$
226	19 225	sstrdi	$⊢ φ \to A \subseteq ℂ$
227	226	sselda	$⊢ (φ \land v \in A) \to v \in ℂ$
228	227	adantrr	$⊢ (φ \land (v \in A \land k \in A)) \to v \in ℂ$
229	226	sselda	$⊢ (φ \land k \in A) \to k \in ℂ$
230	229	adantrl	$⊢ (φ \land (v \in A \land k \in A)) \to k \in ℂ$
231	220 228 230	subcanad	$⊢ (φ \land (v \in A \land k \in A)) \to (P - 1 - v = P - 1 - k \leftrightarrow v = k)$
232	231	ex	$⊢ φ \to ((v \in A \land k \in A) \to (P - 1 - v = P - 1 - k \leftrightarrow v = k))$
233	219 232	dom2lem	$⊢ φ \to (v \in A ⟼ P - 1 - v) : A \underset{1-1}{⟶} (0 \dots P - 1)$
234		f1eq1	$⊢ F = (v \in A ⟼ P - 1 - v) \to (F : A \underset{1-1}{⟶} (0 \dots P - 1) \leftrightarrow (v \in A ⟼ P - 1 - v) : A \underset{1-1}{⟶} (0 \dots P - 1))$
235	6 234	ax-mp	$⊢ F : A \underset{1-1}{⟶} (0 \dots P - 1) \leftrightarrow (v \in A ⟼ P - 1 - v) : A \underset{1-1}{⟶} (0 \dots P - 1)$
236	233 235	sylibr	$⊢ φ \to F : A \underset{1-1}{⟶} (0 \dots P - 1)$
237		f1f1orn	$⊢ F : A \underset{1-1}{⟶} (0 \dots P - 1) \to F : A \underset{1-1 onto}{⟶} ran F$
238	236 237	syl	$⊢ φ \to F : A \underset{1-1 onto}{⟶} ran F$
239	211 238	hasheqf1od	$⊢ φ \to \|A\| = \|ran F\|$
240	239 218	eqtr3d	$⊢ φ \to \|ran F\| = N + 1$
241	218 240	oveq12d	$⊢ φ \to \|A\| + \|ran F\| = N + 1 + N + 1$
242	61 69 241	3eqtr4d	$⊢ φ \to P + 1 = \|A\| + \|ran F\|$
243	242	adantr	$⊢ (φ \land A \cap ran F = \emptyset) \to P + 1 = \|A\| + \|ran F\|$
244	211	adantr	$⊢ (φ \land A \cap ran F = \emptyset) \to A \in Fin$
245	7 33	ssfid	$⊢ φ \to ran F \in Fin$
246	245	adantr	$⊢ (φ \land A \cap ran F = \emptyset) \to ran F \in Fin$
247		simpr	$⊢ (φ \land A \cap ran F = \emptyset) \to A \cap ran F = \emptyset$
248		hashun	$⊢ (A \in Fin \land ran F \in Fin \land A \cap ran F = \emptyset) \to \|A \cup ran F\| = \|A\| + \|ran F\|$
249	244 246 247 248	syl3anc	$⊢ (φ \land A \cap ran F = \emptyset) \to \|A \cup ran F\| = \|A\| + \|ran F\|$
250	243 249	eqtr4d	$⊢ (φ \land A \cap ran F = \emptyset) \to P + 1 = \|A \cup ran F\|$
251	58 250	breqtrd	$⊢ (φ \land A \cap ran F = \emptyset) \to P < \|A \cup ran F\|$
252	251	ex	$⊢ φ \to (A \cap ran F = \emptyset \to P < \|A \cup ran F\|)$
253	252	necon3bd	$⊢ φ \to (\neg P < \|A \cup ran F\| \to A \cap ran F \neq \emptyset)$
254	56 253	mpd	$⊢ φ \to A \cap ran F \neq \emptyset$

Metamath Proof Explorer

Theorem 4sqlem11

Proof