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	56	elfzelzd	$⊢ (φ \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 ℤ$
58		zsqcl2	$⊢ n \in ℤ \to n^{2} \in ℕ_{0}$
59	57 58	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}$
60	59	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 ℝ$
61		modlt	$⊢ (n^{2} \in ℝ \land P \in ℝ^{+}) \to n^{2} \mod P < P$
62	60 49 61	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$
63		zsqcl	$⊢ n \in ℤ \to n^{2} \in ℤ$
64	57 63	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 ℤ$
65	64 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}$
66	65	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 ℤ$
67		prmz	$⊢ P \in ℙ \to P \in ℤ$
68	43 67	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 ℤ$
69		zltlem1	$⊢ (n^{2} \mod P \in ℤ \land P \in ℤ) \to (n^{2} \mod P < P \leftrightarrow n^{2} \mod P \leq P - 1)$
70	66 68 69	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)$
71	62 70	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$
72	71 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$
73		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))$
74	48 60 49 73	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))$
75	72 74	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)$
76		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)$
77	55 75 76	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$
78		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)$
79	78	elfzelzd	$⊢ (φ \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 ℤ$
80		zsqcl	$⊢ m \in ℤ \to m^{2} \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^{2} \in ℤ$
82	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 ℤ$
83	82 64	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 ℤ$
84		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})))$
85	45 81 83 84	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})))$
86	77 85	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}))$
87		zsqcl2	$⊢ m \in ℤ \to m^{2} \in ℕ_{0}$
88	79 87	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}$
89	88	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 ℂ$
90	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 ℂ$
91	59	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 ℂ$
92	89 90 91	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)$
93	88 59	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}$
94	93	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 ℂ$
95	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 ℂ$
96		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 ℂ$
97	94 95 96	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$
98	92 97	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$
99	86 98	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)$
100		nn0p1nn	$⊢ m^{2} + n^{2} \in ℕ_{0} \to m^{2} + n^{2} + 1 \in ℕ$
101	93 100	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 ℕ$
102	101	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 ℤ$
103		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))$
104	68 102 103	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))$
105	99 104	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)$
106	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$
107		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 ℤ)$
108	68 106 102 107	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 ℤ)$
109	105 108	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 ℤ$
110		nnrp	$⊢ m^{2} + n^{2} + 1 \in ℕ \to m^{2} + n^{2} + 1 \in ℝ^{+}$
111		nnrp	$⊢ P \in ℕ \to P \in ℝ^{+}$
112		rpdivcl	$⊢ (m^{2} + n^{2} + 1 \in ℝ^{+} \land P \in ℝ^{+}) \to \frac{m^{2} + n^{2} + 1}{P} \in ℝ^{+}$
113	110 111 112	syl2an	$⊢ (m^{2} + n^{2} + 1 \in ℕ \land P \in ℕ) \to \frac{m^{2} + n^{2} + 1}{P} \in ℝ^{+}$
114	101 45 113	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 ℝ^{+}$
115	114	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}$
116		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})$
117	109 115 116	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 ℕ$
118	117	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}$
119	93	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 ℝ$
120		2nn	$⊢ 2 \in ℕ$
121	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 ℕ$
122		nnmulcl	$⊢ (2 \in ℕ \land N \in ℕ) \to 2 \cdot N \in ℕ$
123	120 121 122	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 ℕ$
124	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 2 \cdot N \in ℝ$
125	124	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 ℝ$
126		nnmulcl	$⊢ (2 \in ℕ \land 2 \cdot N \in ℕ) \to 2 2 \cdot N \in ℕ$
127	120 123 126	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 ℕ$
128	127	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 ℝ$
129	125 128	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 ℝ$
130		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 ℝ$
131	121	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 ℕ$
132		nnmulcl	$⊢ (2 \in ℕ \land N^{2} \in ℕ) \to 2 N^{2} \in ℕ$
133	120 131 132	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 ℕ$
134	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 2 N^{2} \in ℝ$
135	88	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 ℝ$
136	131	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 ℝ$
137	79	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 ℝ$
138		elfzle1	$⊢ m \in (0 \dots N) \to 0 \leq m$
139	78 138	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$
140	121	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 ℝ$
141		elfzle2	$⊢ m \in (0 \dots N) \to m \leq N$
142	78 141	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$
143		le2sq2	$⊢ ((m \in ℝ \land 0 \leq m) \land (N \in ℝ \land m \leq N)) \to m^{2} \leq N^{2}$
144	137 139 140 142 143	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}$
145	57	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 ℝ$
146		elfzle1	$⊢ n \in (0 \dots N) \to 0 \leq n$
147	56 146	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$
148		elfzle2	$⊢ n \in (0 \dots N) \to n \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 n \leq N$
150		le2sq2	$⊢ ((n \in ℝ \land 0 \leq n) \land (N \in ℝ \land n \leq N)) \to n^{2} \leq N^{2}$
151	145 147 140 149 150	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}$
152	135 60 136 136 144 151	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}$
153	131	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 ℂ$
154	153	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}$
155	152 154	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}$
156		2lt4	$⊢ 2 < 4$
157		2re	$⊢ 2 \in ℝ$
158	157	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 ℝ$
159		4re	$⊢ 4 \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 4 \in ℝ$
161	131	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}$
162		ltmul1	$⊢ (2 \in ℝ \land 4 \in ℝ \land (N^{2} \in ℝ \land 0 < N^{2})) \to (2 < 4 \leftrightarrow 2 N^{2} < 4 N^{2})$
163	158 160 136 161 162	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})$
164	156 163	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}$
165		2cn	$⊢ 2 \in ℂ$
166	121	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 ℂ$
167		sqmul	$⊢ (2 \in ℂ \land N \in ℂ) \to {2 \cdot N}^{2} = 2^{2} N^{2}$
168	165 166 167	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}$
169		sq2	$⊢ 2^{2} = 4$
170	169	oveq1i	$⊢ 2^{2} N^{2} = 4 N^{2}$
171	168 170	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}$
172	164 171	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}$
173	119 134 125 155 172	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}$
174	127	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 ℝ^{+}$
175	125 174	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$
176	119 125 129 173 175	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$
177	119 129 130 176	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$
178	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$
179	178	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}$
180	95	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$
181	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 2 \cdot N \in ℂ$
182		binom21	$⊢ 2 \cdot N \in ℂ \to {(2 \cdot N + 1)}^{2} = {2 \cdot N}^{2} + 2 2 \cdot N + 1$
183	181 182	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$
184	179 180 183	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$
185	177 184	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$
186	101	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 ℝ$
187	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$
188		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)$
189	186 51 51 187 188	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)$
190	185 189	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$
191		1z	$⊢ 1 \in ℤ$
192		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))$
193	191 68 192	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))$
194	109 118 190 193	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)$
195		gzreim	$⊢ (m \in ℤ \land n \in ℤ) \to m + i n \in ℤ [i]$
196	79 57 195	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]$
197		gzcn	$⊢ m + i n \in ℤ [i] \to m + i n \in ℂ$
198	196 197	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 ℂ$
199	198	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}$
200	137 145	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$
201	200	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}$
202	137 145	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$
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} = n^{2}$
204	201 203	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}$
205	199 204	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}$
206	205	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$
207	101	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 ℂ$
208	207 95 106	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$
209	206 208	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$
210		oveq1	$⊢ k = \frac{m^{2} + n^{2} + 1}{P} \to k P = (\frac{m^{2} + n^{2} + 1}{P}) P$
211	210	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)$
212		fveq2	$⊢ u = m + i n \to \|u\| = \|m + i n\|$
213	212	oveq1d	$⊢ u = m + i n \to {\|u\|}^{2} = {\|m + i n\|}^{2}$
214	213	oveq1d	$⊢ u = m + i n \to {\|u\|}^{2} + 1 = {\|m + i n\|}^{2} + 1$
215	214	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)$
216	211 215	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$
217	194 196 209 216	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$
218	217	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)$
219	42 218	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)$
220	219	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)$
221	41 220	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)$
222	221	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)$
223	9 222	mpd	$⊢ φ \to \exists k \in (1 \dots P - 1) \exists u \in ℤ [i] {\|u\|}^{2} + 1 = k P$

Metamath Proof Explorer

Theorem 4sqlem12

Proof