4sqlem12

Description: Lemma for 4sq . For any odd prime P , there is a k < P such that k P - 1 is a sum of two squares. (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	4sqlem12	$⊢ φ \to \exists k \in (1 \dots P - 1) \exists u \in ℤ [i] {\|u\|}^{2} + 1 = k P$

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	1 2 3 4 5 6	4sqlem11	$⊢ φ \to A \cap ran F \neq \emptyset$
8		n0	$⊢ A \cap ran F \neq \emptyset \leftrightarrow \exists j j \in (A \cap ran F)$
9	7 8	sylib	$⊢ φ \to \exists j j \in (A \cap ran F)$
10		vex	$⊢ j \in V$
11		eqeq1	$⊢ u = j \to (u = m^{2} \mod P \leftrightarrow j = m^{2} \mod P)$
12	11	rexbidv	$⊢ u = j \to (\exists m \in (0 \dots N) u = m^{2} \mod P \leftrightarrow \exists m \in (0 \dots N) j = m^{2} \mod P)$
13	10 12 5	elab2	$⊢ j \in A \leftrightarrow \exists m \in (0 \dots N) j = m^{2} \mod P$
14		abid	$⊢ j \in \{j \| \exists v \in A j = P - 1 - v\} \leftrightarrow \exists v \in A j = P - 1 - v$
15	5	rexeqi	$⊢ \exists v \in A j = P - 1 - v \leftrightarrow \exists v \in \{u \| \exists m \in (0 \dots N) u = m^{2} \mod P\} j = P - 1 - v$
16		oveq1	$⊢ m = n \to m^{2} = n^{2}$
17	16	oveq1d	$⊢ m = n \to m^{2} \mod P = n^{2} \mod P$
18	17	eqeq2d	$⊢ m = n \to (u = m^{2} \mod P \leftrightarrow u = n^{2} \mod P)$
19	18	cbvrexvw	$⊢ \exists m \in (0 \dots N) u = m^{2} \mod P \leftrightarrow \exists n \in (0 \dots N) u = n^{2} \mod P$
20		eqeq1	$⊢ u = v \to (u = n^{2} \mod P \leftrightarrow v = n^{2} \mod P)$
21	20	rexbidv	$⊢ u = v \to (\exists n \in (0 \dots N) u = n^{2} \mod P \leftrightarrow \exists n \in (0 \dots N) v = n^{2} \mod P)$
22	19 21	syl5bb	$⊢ u = v \to (\exists m \in (0 \dots N) u = m^{2} \mod P \leftrightarrow \exists n \in (0 \dots N) v = n^{2} \mod P)$
23	22	rexab	$⊢ \exists v \in \{u \| \exists m \in (0 \dots N) u = m^{2} \mod P\} j = P - 1 - v \leftrightarrow \exists v (\exists n \in (0 \dots N) v = n^{2} \mod P \land j = P - 1 - v)$
24	14 15 23	3bitri	$⊢ j \in \{j \| \exists v \in A j = P - 1 - v\} \leftrightarrow \exists v (\exists n \in (0 \dots N) v = n^{2} \mod P \land j = P - 1 - v)$
25	6	rnmpt	$⊢ ran F = \{j \| \exists v \in A j = P - 1 - v\}$
26	25	eleq2i	$⊢ j \in ran F \leftrightarrow j \in \{j \| \exists v \in A j = P - 1 - v\}$
27		rexcom4	$⊢ \exists n \in (0 \dots N) \exists v (v = n^{2} \mod P \land j = P - 1 - v) \leftrightarrow \exists v \exists n \in (0 \dots N) (v = n^{2} \mod P \land j = P - 1 - v)$
28		r19.41v	$⊢ \exists n \in (0 \dots N) (v = n^{2} \mod P \land j = P - 1 - v) \leftrightarrow (\exists n \in (0 \dots N) v = n^{2} \mod P \land j = P - 1 - v)$
29	28	exbii	$⊢ \exists v \exists n \in (0 \dots N) (v = n^{2} \mod P \land j = P - 1 - v) \leftrightarrow \exists v (\exists n \in (0 \dots N) v = n^{2} \mod P \land j = P - 1 - v)$
30	27 29	bitri	$⊢ \exists n \in (0 \dots N) \exists v (v = n^{2} \mod P \land j = P - 1 - v) \leftrightarrow \exists v (\exists n \in (0 \dots N) v = n^{2} \mod P \land j = P - 1 - v)$
31	24 26 30	3bitr4i	$⊢ j \in ran F \leftrightarrow \exists n \in (0 \dots N) \exists v (v = n^{2} \mod P \land j = P - 1 - v)$
32		ovex	$⊢ n^{2} \mod P \in V$
33		oveq2	$⊢ v = n^{2} \mod P \to P - 1 - v = P - 1 - (n^{2} \mod P)$
34	33	eqeq2d	$⊢ v = n^{2} \mod P \to (j = P - 1 - v \leftrightarrow j = P - 1 - (n^{2} \mod P))$
35	32 34	ceqsexv	$⊢ \exists v (v = n^{2} \mod P \land j = P - 1 - v) \leftrightarrow j = P - 1 - (n^{2} \mod P)$
36	35	rexbii	$⊢ \exists n \in (0 \dots N) \exists v (v = n^{2} \mod P \land j = P - 1 - v) \leftrightarrow \exists n \in (0 \dots N) j = P - 1 - (n^{2} \mod P)$
37	31 36	bitri	$⊢ j \in ran F \leftrightarrow \exists n \in (0 \dots N) j = P - 1 - (n^{2} \mod P)$
38	13 37	anbi12i	$⊢ (j \in A \land j \in ran F) \leftrightarrow (\exists m \in (0 \dots N) j = m^{2} \mod P \land \exists n \in (0 \dots N) j = P - 1 - (n^{2} \mod P))$
39		elin	$⊢ j \in (A \cap ran F) \leftrightarrow (j \in A \land j \in ran F)$
40		reeanv	$⊢ \exists m \in (0 \dots N) \exists n \in (0 \dots N) (j = m^{2} \mod P \land j = P - 1 - (n^{2} \mod P)) \leftrightarrow (\exists m \in (0 \dots N) j = m^{2} \mod P \land \exists n \in (0 \dots N) j = P - 1 - (n^{2} \mod P))$
41	38 39 40	3bitr4i	$⊢ j \in (A \cap ran F) \leftrightarrow \exists m \in (0 \dots N) \exists n \in (0 \dots N) (j = m^{2} \mod P \land j = P - 1 - (n^{2} \mod P))$
42		eqtr2	$⊢ (j = m^{2} \mod P \land j = P - 1 - (n^{2} \mod P)) \to m^{2} \mod P = P - 1 - (n^{2} \mod P)$
43	4	3ad2ant1	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P \in ℙ$
44		prmnn	$⊢ P \in ℙ \to P \in ℕ$
45	43 44	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P \in ℕ$
46		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
47	45 46	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P - 1 \in ℕ_{0}$
48	47	nn0red	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P - 1 \in ℝ$
49	45	nnrpd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P \in ℝ^{+}$
50	47	nn0ge0d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 0 \leq P - 1$
51	45	nnred	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P \in ℝ$
52	51	ltm1d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P - 1 < P$
53		modid	$⊢ ((P - 1 \in ℝ \land P \in ℝ^{+}) \land (0 \leq P - 1 \land P - 1 < P)) \to (P - 1) \mod P = P - 1$
54	48 49 50 52 53	syl22anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to (P - 1) \mod P = P - 1$
55	54	oveq1d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to ((P - 1) \mod P) - (n^{2} \mod P) = P - 1 - (n^{2} \mod P)$
56		simp2r	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n \in (0 \dots N)$
57		elfzelz	$⊢ n \in (0 \dots N) \to n \in ℤ$
58	56 57	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n \in ℤ$
59		zsqcl2	$⊢ n \in ℤ \to n^{2} \in ℕ_{0}$
60	58 59	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n^{2} \in ℕ_{0}$
61	60	nn0red	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n^{2} \in ℝ$
62		modlt	$⊢ (n^{2} \in ℝ \land P \in ℝ^{+}) \to n^{2} \mod P < P$
63	61 49 62	syl2anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n^{2} \mod P < P$
64		zsqcl	$⊢ n \in ℤ \to n^{2} \in ℤ$
65	58 64	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n^{2} \in ℤ$
66	65 45	zmodcld	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n^{2} \mod P \in ℕ_{0}$
67	66	nn0zd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n^{2} \mod P \in ℤ$
68		prmz	$⊢ P \in ℙ \to P \in ℤ$
69	43 68	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P \in ℤ$
70		zltlem1	$⊢ (n^{2} \mod P \in ℤ \land P \in ℤ) \to (n^{2} \mod P < P \leftrightarrow n^{2} \mod P \leq P - 1)$
71	67 69 70	syl2anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to (n^{2} \mod P < P \leftrightarrow n^{2} \mod P \leq P - 1)$
72	63 71	mpbid	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n^{2} \mod P \leq P - 1$
73	72 54	breqtrrd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n^{2} \mod P \leq (P - 1) \mod P$
74		modsubdir	$⊢ (P - 1 \in ℝ \land n^{2} \in ℝ \land P \in ℝ^{+}) \to (n^{2} \mod P \leq (P - 1) \mod P \leftrightarrow (P - 1 - n^{2}) \mod P = ((P - 1) \mod P) - (n^{2} \mod P))$
75	48 61 49 74	syl3anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to (n^{2} \mod P \leq (P - 1) \mod P \leftrightarrow (P - 1 - n^{2}) \mod P = ((P - 1) \mod P) - (n^{2} \mod P))$
76	73 75	mpbid	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to (P - 1 - n^{2}) \mod P = ((P - 1) \mod P) - (n^{2} \mod P)$
77		simp3	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} \mod P = P - 1 - (n^{2} \mod P)$
78	55 76 77	3eqtr4rd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} \mod P = (P - 1 - n^{2}) \mod P$
79		simp2l	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m \in (0 \dots N)$
80		elfzelz	$⊢ m \in (0 \dots N) \to m \in ℤ$
81	79 80	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m \in ℤ$
82		zsqcl	$⊢ m \in ℤ \to m^{2} \in ℤ$
83	81 82	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} \in ℤ$
84	47	nn0zd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P - 1 \in ℤ$
85	84 65	zsubcld	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P - 1 - n^{2} \in ℤ$
86		moddvds	$⊢ (P \in ℕ \land m^{2} \in ℤ \land P - 1 - n^{2} \in ℤ) \to (m^{2} \mod P = (P - 1 - n^{2}) \mod P \leftrightarrow P ∥ (m^{2} - (P - 1 - n^{2})))$
87	45 83 85 86	syl3anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to (m^{2} \mod P = (P - 1 - n^{2}) \mod P \leftrightarrow P ∥ (m^{2} - (P - 1 - n^{2})))$
88	78 87	mpbid	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P ∥ (m^{2} - (P - 1 - n^{2}))$
89		zsqcl2	$⊢ m \in ℤ \to m^{2} \in ℕ_{0}$
90	81 89	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} \in ℕ_{0}$
91	90	nn0cnd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} \in ℂ$
92	47	nn0cnd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P - 1 \in ℂ$
93	60	nn0cnd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n^{2} \in ℂ$
94	91 92 93	subsub3d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} - (P - 1 - n^{2}) = m^{2} + n^{2} - (P - 1)$
95	90 60	nn0addcld	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} \in ℕ_{0}$
96	95	nn0cnd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} \in ℂ$
97	45	nncnd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P \in ℂ$
98		1cnd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 1 \in ℂ$
99	96 97 98	subsub3d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} - (P - 1) = (m^{2} + n^{2}) + 1 - P$
100	94 99	eqtrd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} - (P - 1 - n^{2}) = (m^{2} + n^{2}) + 1 - P$
101	88 100	breqtrd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P ∥ ((m^{2} + n^{2}) + 1 - P)$
102		nn0p1nn	$⊢ m^{2} + n^{2} \in ℕ_{0} \to m^{2} + n^{2} + 1 \in ℕ$
103	95 102	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} + 1 \in ℕ$
104	103	nnzd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} + 1 \in ℤ$
105		dvdssubr	$⊢ (P \in ℤ \land m^{2} + n^{2} + 1 \in ℤ) \to (P ∥ (m^{2} + n^{2} + 1) \leftrightarrow P ∥ ((m^{2} + n^{2}) + 1 - P))$
106	69 104 105	syl2anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to (P ∥ (m^{2} + n^{2} + 1) \leftrightarrow P ∥ ((m^{2} + n^{2}) + 1 - P))$
107	101 106	mpbird	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P ∥ (m^{2} + n^{2} + 1)$
108	45	nnne0d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P \neq 0$
109		dvdsval2	$⊢ (P \in ℤ \land P \neq 0 \land m^{2} + n^{2} + 1 \in ℤ) \to (P ∥ (m^{2} + n^{2} + 1) \leftrightarrow \frac{m^{2} + n^{2} + 1}{P} \in ℤ)$
110	69 108 104 109	syl3anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to (P ∥ (m^{2} + n^{2} + 1) \leftrightarrow \frac{m^{2} + n^{2} + 1}{P} \in ℤ)$
111	107 110	mpbid	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to \frac{m^{2} + n^{2} + 1}{P} \in ℤ$
112		nnrp	$⊢ m^{2} + n^{2} + 1 \in ℕ \to m^{2} + n^{2} + 1 \in ℝ^{+}$
113		nnrp	$⊢ P \in ℕ \to P \in ℝ^{+}$
114		rpdivcl	$⊢ (m^{2} + n^{2} + 1 \in ℝ^{+} \land P \in ℝ^{+}) \to \frac{m^{2} + n^{2} + 1}{P} \in ℝ^{+}$
115	112 113 114	syl2an	$⊢ (m^{2} + n^{2} + 1 \in ℕ \land P \in ℕ) \to \frac{m^{2} + n^{2} + 1}{P} \in ℝ^{+}$
116	103 45 115	syl2anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to \frac{m^{2} + n^{2} + 1}{P} \in ℝ^{+}$
117	116	rpgt0d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 0 < \frac{m^{2} + n^{2} + 1}{P}$
118		elnnz	$⊢ \frac{m^{2} + n^{2} + 1}{P} \in ℕ \leftrightarrow (\frac{m^{2} + n^{2} + 1}{P} \in ℤ \land 0 < \frac{m^{2} + n^{2} + 1}{P})$
119	111 117 118	sylanbrc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to \frac{m^{2} + n^{2} + 1}{P} \in ℕ$
120	119	nnge1d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 1 \leq \frac{m^{2} + n^{2} + 1}{P}$
121	95	nn0red	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} \in ℝ$
122		2nn	$⊢ 2 \in ℕ$
123	2	3ad2ant1	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to N \in ℕ$
124		nnmulcl	$⊢ (2 \in ℕ \land N \in ℕ) \to 2 \cdot N \in ℕ$
125	122 123 124	sylancr	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 2 \cdot N \in ℕ$
126	125	nnred	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 2 \cdot N \in ℝ$
127	126	resqcld	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {2 \cdot N}^{2} \in ℝ$
128		nnmulcl	$⊢ (2 \in ℕ \land 2 \cdot N \in ℕ) \to 2 2 \cdot N \in ℕ$
129	122 125 128	sylancr	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 2 2 \cdot N \in ℕ$
130	129	nnred	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 2 2 \cdot N \in ℝ$
131	127 130	readdcld	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {2 \cdot N}^{2} + 2 2 \cdot N \in ℝ$
132		1red	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 1 \in ℝ$
133	123	nnsqcld	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to N^{2} \in ℕ$
134		nnmulcl	$⊢ (2 \in ℕ \land N^{2} \in ℕ) \to 2 N^{2} \in ℕ$
135	122 133 134	sylancr	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 2 N^{2} \in ℕ$
136	135	nnred	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 2 N^{2} \in ℝ$
137	90	nn0red	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} \in ℝ$
138	133	nnred	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to N^{2} \in ℝ$
139	81	zred	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m \in ℝ$
140		elfzle1	$⊢ m \in (0 \dots N) \to 0 \leq m$
141	79 140	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 0 \leq m$
142	123	nnred	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to N \in ℝ$
143		elfzle2	$⊢ m \in (0 \dots N) \to m \leq N$
144	79 143	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m \leq N$
145		le2sq2	$⊢ ((m \in ℝ \land 0 \leq m) \land (N \in ℝ \land m \leq N)) \to m^{2} \leq N^{2}$
146	139 141 142 144 145	syl22anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} \leq N^{2}$
147	58	zred	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n \in ℝ$
148		elfzle1	$⊢ n \in (0 \dots N) \to 0 \leq n$
149	56 148	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 0 \leq n$
150		elfzle2	$⊢ n \in (0 \dots N) \to n \leq N$
151	56 150	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n \leq N$
152		le2sq2	$⊢ ((n \in ℝ \land 0 \leq n) \land (N \in ℝ \land n \leq N)) \to n^{2} \leq N^{2}$
153	147 149 142 151 152	syl22anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to n^{2} \leq N^{2}$
154	137 61 138 138 146 153	le2addd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} \leq N^{2} + N^{2}$
155	133	nncnd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to N^{2} \in ℂ$
156	155	2timesd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 2 N^{2} = N^{2} + N^{2}$
157	154 156	breqtrrd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} \leq 2 N^{2}$
158		2lt4	$⊢ 2 < 4$
159		2re	$⊢ 2 \in ℝ$
160	159	a1i	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 2 \in ℝ$
161		4re	$⊢ 4 \in ℝ$
162	161	a1i	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 4 \in ℝ$
163	133	nngt0d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 0 < N^{2}$
164		ltmul1	$⊢ (2 \in ℝ \land 4 \in ℝ \land (N^{2} \in ℝ \land 0 < N^{2})) \to (2 < 4 \leftrightarrow 2 N^{2} < 4 N^{2})$
165	160 162 138 163 164	syl112anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to (2 < 4 \leftrightarrow 2 N^{2} < 4 N^{2})$
166	158 165	mpbii	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 2 N^{2} < 4 N^{2}$
167		2cn	$⊢ 2 \in ℂ$
168	123	nncnd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to N \in ℂ$
169		sqmul	$⊢ (2 \in ℂ \land N \in ℂ) \to {2 \cdot N}^{2} = 2^{2} N^{2}$
170	167 168 169	sylancr	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {2 \cdot N}^{2} = 2^{2} N^{2}$
171		sq2	$⊢ 2^{2} = 4$
172	171	oveq1i	$⊢ 2^{2} N^{2} = 4 N^{2}$
173	170 172	eqtrdi	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {2 \cdot N}^{2} = 4 N^{2}$
174	166 173	breqtrrd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 2 N^{2} < {2 \cdot N}^{2}$
175	121 136 127 157 174	lelttrd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} < {2 \cdot N}^{2}$
176	129	nnrpd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 2 2 \cdot N \in ℝ^{+}$
177	127 176	ltaddrpd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {2 \cdot N}^{2} < {2 \cdot N}^{2} + 2 2 \cdot N$
178	121 127 131 175 177	lttrd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} < {2 \cdot N}^{2} + 2 2 \cdot N$
179	121 131 132 178	ltadd1dd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} + 1 < {2 \cdot N}^{2} + 2 2 \cdot N + 1$
180	3	3ad2ant1	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P = 2 \cdot N + 1$
181	180	oveq1d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P^{2} = {(2 \cdot N + 1)}^{2}$
182	97	sqvald	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P^{2} = P P$
183	125	nncnd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 2 \cdot N \in ℂ$
184		binom21	$⊢ 2 \cdot N \in ℂ \to {(2 \cdot N + 1)}^{2} = {2 \cdot N}^{2} + 2 2 \cdot N + 1$
185	183 184	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {(2 \cdot N + 1)}^{2} = {2 \cdot N}^{2} + 2 2 \cdot N + 1$
186	181 182 185	3eqtr3d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to P P = {2 \cdot N}^{2} + 2 2 \cdot N + 1$
187	179 186	breqtrrd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} + 1 < P P$
188	103	nnred	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} + 1 \in ℝ$
189	45	nngt0d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to 0 < P$
190		ltdivmul	$⊢ (m^{2} + n^{2} + 1 \in ℝ \land P \in ℝ \land (P \in ℝ \land 0 < P)) \to (\frac{m^{2} + n^{2} + 1}{P} < P \leftrightarrow m^{2} + n^{2} + 1 < P P)$
191	188 51 51 189 190	syl112anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to (\frac{m^{2} + n^{2} + 1}{P} < P \leftrightarrow m^{2} + n^{2} + 1 < P P)$
192	187 191	mpbird	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to \frac{m^{2} + n^{2} + 1}{P} < P$
193		1z	$⊢ 1 \in ℤ$
194		elfzm11	$⊢ (1 \in ℤ \land P \in ℤ) \to (\frac{m^{2} + n^{2} + 1}{P} \in (1 \dots P - 1) \leftrightarrow (\frac{m^{2} + n^{2} + 1}{P} \in ℤ \land 1 \leq \frac{m^{2} + n^{2} + 1}{P} \land \frac{m^{2} + n^{2} + 1}{P} < P))$
195	193 69 194	sylancr	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to (\frac{m^{2} + n^{2} + 1}{P} \in (1 \dots P - 1) \leftrightarrow (\frac{m^{2} + n^{2} + 1}{P} \in ℤ \land 1 \leq \frac{m^{2} + n^{2} + 1}{P} \land \frac{m^{2} + n^{2} + 1}{P} < P))$
196	111 120 192 195	mpbir3and	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to \frac{m^{2} + n^{2} + 1}{P} \in (1 \dots P - 1)$
197		gzreim	$⊢ (m \in ℤ \land n \in ℤ) \to m + i n \in ℤ [i]$
198	81 58 197	syl2anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m + i n \in ℤ [i]$
199		gzcn	$⊢ m + i n \in ℤ [i] \to m + i n \in ℂ$
200	198 199	syl	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m + i n \in ℂ$
201	200	absvalsq2d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {\|m + i n\|}^{2} = {ℜ (m + i n)}^{2} + {ℑ (m + i n)}^{2}$
202	139 147	crred	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to ℜ (m + i n) = m$
203	202	oveq1d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {ℜ (m + i n)}^{2} = m^{2}$
204	139 147	crimd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to ℑ (m + i n) = n$
205	204	oveq1d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {ℑ (m + i n)}^{2} = n^{2}$
206	203 205	oveq12d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {ℜ (m + i n)}^{2} + {ℑ (m + i n)}^{2} = m^{2} + n^{2}$
207	201 206	eqtrd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {\|m + i n\|}^{2} = m^{2} + n^{2}$
208	207	oveq1d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {\|m + i n\|}^{2} + 1 = m^{2} + n^{2} + 1$
209	103	nncnd	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to m^{2} + n^{2} + 1 \in ℂ$
210	209 97 108	divcan1d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to (\frac{m^{2} + n^{2} + 1}{P}) P = m^{2} + n^{2} + 1$
211	208 210	eqtr4d	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to {\|m + i n\|}^{2} + 1 = (\frac{m^{2} + n^{2} + 1}{P}) P$
212		oveq1	$⊢ k = \frac{m^{2} + n^{2} + 1}{P} \to k P = (\frac{m^{2} + n^{2} + 1}{P}) P$
213	212	eqeq2d	$⊢ k = \frac{m^{2} + n^{2} + 1}{P} \to ({\|u\|}^{2} + 1 = k P \leftrightarrow {\|u\|}^{2} + 1 = (\frac{m^{2} + n^{2} + 1}{P}) P)$
214		fveq2	$⊢ u = m + i n \to \|u\| = \|m + i n\|$
215	214	oveq1d	$⊢ u = m + i n \to {\|u\|}^{2} = {\|m + i n\|}^{2}$
216	215	oveq1d	$⊢ u = m + i n \to {\|u\|}^{2} + 1 = {\|m + i n\|}^{2} + 1$
217	216	eqeq1d	$⊢ u = m + i n \to ({\|u\|}^{2} + 1 = (\frac{m^{2} + n^{2} + 1}{P}) P \leftrightarrow {\|m + i n\|}^{2} + 1 = (\frac{m^{2} + n^{2} + 1}{P}) P)$
218	213 217	rspc2ev	$⊢ (\frac{m^{2} + n^{2} + 1}{P} \in (1 \dots P - 1) \land m + i n \in ℤ [i] \land {\|m + i n\|}^{2} + 1 = (\frac{m^{2} + n^{2} + 1}{P}) P) \to \exists k \in (1 \dots P - 1) \exists u \in ℤ [i] {\|u\|}^{2} + 1 = k P$
219	196 198 211 218	syl3anc	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N)) \land m^{2} \mod P = P - 1 - (n^{2} \mod P)) \to \exists k \in (1 \dots P - 1) \exists u \in ℤ [i] {\|u\|}^{2} + 1 = k P$
220	219	3expia	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N))) \to (m^{2} \mod P = P - 1 - (n^{2} \mod P) \to \exists k \in (1 \dots P - 1) \exists u \in ℤ [i] {\|u\|}^{2} + 1 = k P)$
221	42 220	syl5	$⊢ (φ \land (m \in (0 \dots N) \land n \in (0 \dots N))) \to ((j = m^{2} \mod P \land j = P - 1 - (n^{2} \mod P)) \to \exists k \in (1 \dots P - 1) \exists u \in ℤ [i] {\|u\|}^{2} + 1 = k P)$
222	221	rexlimdvva	$⊢ φ \to (\exists m \in (0 \dots N) \exists n \in (0 \dots N) (j = m^{2} \mod P \land j = P - 1 - (n^{2} \mod P)) \to \exists k \in (1 \dots P - 1) \exists u \in ℤ [i] {\|u\|}^{2} + 1 = k P)$
223	41 222	syl5bi	$⊢ φ \to (j \in (A \cap ran F) \to \exists k \in (1 \dots P - 1) \exists u \in ℤ [i] {\|u\|}^{2} + 1 = k P)$
224	223	exlimdv	$⊢ φ \to (\exists j j \in (A \cap ran F) \to \exists k \in (1 \dots P - 1) \exists u \in ℤ [i] {\|u\|}^{2} + 1 = k P)$
225	9 224	mpd	$⊢ φ \to \exists k \in (1 \dots P - 1) \exists u \in ℤ [i] {\|u\|}^{2} + 1 = k P$

Metamath Proof Explorer

Theorem 4sqlem12

Proof