2sqreunnlem1

		Ref	Expression
	Assertion	2sqreunnlem1	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists! a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P)$

Proof

Step	Hyp	Ref	Expression
1		2sqnn	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}$
2		simpll	$⊢ ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2}) \to x \in ℕ$
3	2	adantl	$⊢ (x \leq y \land ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2})) \to x \in ℕ$
4		breq1	$⊢ a = x \to (a \leq b \leftrightarrow x \leq b)$
5		oveq1	$⊢ a = x \to a^{2} = x^{2}$
6	5	oveq1d	$⊢ a = x \to a^{2} + b^{2} = x^{2} + b^{2}$
7	6	eqeq1d	$⊢ a = x \to (a^{2} + b^{2} = P \leftrightarrow x^{2} + b^{2} = P)$
8	4 7	anbi12d	$⊢ a = x \to ((a \leq b \land a^{2} + b^{2} = P) \leftrightarrow (x \leq b \land x^{2} + b^{2} = P))$
9	8	reubidv	$⊢ a = x \to (\exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \leftrightarrow \exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = P))$
10	9	adantl	$⊢ ((x \leq y \land ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2})) \land a = x) \to (\exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \leftrightarrow \exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = P))$
11		simpr	$⊢ (x \in ℕ \land y \in ℕ) \to y \in ℕ$
12	11	adantr	$⊢ ((x \in ℕ \land y \in ℕ) \land x \leq y) \to y \in ℕ$
13		breq2	$⊢ b = y \to (x \leq b \leftrightarrow x \leq y)$
14		oveq1	$⊢ b = y \to b^{2} = y^{2}$
15	14	oveq2d	$⊢ b = y \to x^{2} + b^{2} = x^{2} + y^{2}$
16	15	eqeq1d	$⊢ b = y \to (x^{2} + b^{2} = x^{2} + y^{2} \leftrightarrow x^{2} + y^{2} = x^{2} + y^{2})$
17	13 16	anbi12d	$⊢ b = y \to ((x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}) \leftrightarrow (x \leq y \land x^{2} + y^{2} = x^{2} + y^{2}))$
18		equequ1	$⊢ b = y \to (b = c \leftrightarrow y = c)$
19	18	imbi2d	$⊢ b = y \to (((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to b = c) \leftrightarrow ((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to y = c))$
20	19	ralbidv	$⊢ b = y \to (\forall c \in ℕ ((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to b = c) \leftrightarrow \forall c \in ℕ ((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to y = c))$
21	17 20	anbi12d	$⊢ b = y \to (((x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to b = c)) \leftrightarrow ((x \leq y \land x^{2} + y^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to y = c)))$
22	21	adantl	$⊢ (((x \in ℕ \land y \in ℕ) \land x \leq y) \land b = y) \to (((x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to b = c)) \leftrightarrow ((x \leq y \land x^{2} + y^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to y = c)))$
23		simpr	$⊢ ((x \in ℕ \land y \in ℕ) \land x \leq y) \to x \leq y$
24		eqidd	$⊢ ((x \in ℕ \land y \in ℕ) \land x \leq y) \to x^{2} + y^{2} = x^{2} + y^{2}$
25		nnre	$⊢ c \in ℕ \to c \in ℝ$
26	25	resqcld	$⊢ c \in ℕ \to c^{2} \in ℝ$
27	26	adantl	$⊢ (((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \to c^{2} \in ℝ$
28		nnre	$⊢ y \in ℕ \to y \in ℝ$
29	28	resqcld	$⊢ y \in ℕ \to y^{2} \in ℝ$
30	29	adantl	$⊢ (x \in ℕ \land y \in ℕ) \to y^{2} \in ℝ$
31	30	ad2antrr	$⊢ (((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \to y^{2} \in ℝ$
32		nnre	$⊢ x \in ℕ \to x \in ℝ$
33	32	resqcld	$⊢ x \in ℕ \to x^{2} \in ℝ$
34	33	adantr	$⊢ (x \in ℕ \land y \in ℕ) \to x^{2} \in ℝ$
35	34	ad2antrr	$⊢ (((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \to x^{2} \in ℝ$
36		readdcan	$⊢ (c^{2} \in ℝ \land y^{2} \in ℝ \land x^{2} \in ℝ) \to (x^{2} + c^{2} = x^{2} + y^{2} \leftrightarrow c^{2} = y^{2})$
37	27 31 35 36	syl3anc	$⊢ (((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \to (x^{2} + c^{2} = x^{2} + y^{2} \leftrightarrow c^{2} = y^{2})$
38	28	ad4antlr	$⊢ ((((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \land c^{2} = y^{2}) \to y \in ℝ$
39	25	ad2antlr	$⊢ ((((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \land c^{2} = y^{2}) \to c \in ℝ$
40		nnnn0	$⊢ y \in ℕ \to y \in ℕ_{0}$
41	40	nn0ge0d	$⊢ y \in ℕ \to 0 \leq y$
42	41	ad4antlr	$⊢ ((((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \land c^{2} = y^{2}) \to 0 \leq y$
43		nnnn0	$⊢ c \in ℕ \to c \in ℕ_{0}$
44	43	nn0ge0d	$⊢ c \in ℕ \to 0 \leq c$
45	44	ad2antlr	$⊢ ((((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \land c^{2} = y^{2}) \to 0 \leq c$
46		simpr	$⊢ ((((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \land c^{2} = y^{2}) \to c^{2} = y^{2}$
47	46	eqcomd	$⊢ ((((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \land c^{2} = y^{2}) \to y^{2} = c^{2}$
48	38 39 42 45 47	sq11d	$⊢ ((((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \land c^{2} = y^{2}) \to y = c$
49	48	ex	$⊢ (((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \to (c^{2} = y^{2} \to y = c)$
50	37 49	sylbid	$⊢ (((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \to (x^{2} + c^{2} = x^{2} + y^{2} \to y = c)$
51	50	adantld	$⊢ (((x \in ℕ \land y \in ℕ) \land x \leq y) \land c \in ℕ) \to ((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to y = c)$
52	51	ralrimiva	$⊢ ((x \in ℕ \land y \in ℕ) \land x \leq y) \to \forall c \in ℕ ((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to y = c)$
53	23 24 52	jca31	$⊢ ((x \in ℕ \land y \in ℕ) \land x \leq y) \to ((x \leq y \land x^{2} + y^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to y = c))$
54	12 22 53	rspcedvd	$⊢ ((x \in ℕ \land y \in ℕ) \land x \leq y) \to \exists b \in ℕ ((x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to b = c))$
55		breq2	$⊢ b = c \to (x \leq b \leftrightarrow x \leq c)$
56		oveq1	$⊢ b = c \to b^{2} = c^{2}$
57	56	oveq2d	$⊢ b = c \to x^{2} + b^{2} = x^{2} + c^{2}$
58	57	eqeq1d	$⊢ b = c \to (x^{2} + b^{2} = x^{2} + y^{2} \leftrightarrow x^{2} + c^{2} = x^{2} + y^{2})$
59	55 58	anbi12d	$⊢ b = c \to ((x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}) \leftrightarrow (x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}))$
60	59	reu8	$⊢ \exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}) \leftrightarrow \exists b \in ℕ ((x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((x \leq c \land x^{2} + c^{2} = x^{2} + y^{2}) \to b = c))$
61	54 60	sylibr	$⊢ ((x \in ℕ \land y \in ℕ) \land x \leq y) \to \exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = x^{2} + y^{2})$
62	61	ex	$⊢ (x \in ℕ \land y \in ℕ) \to (x \leq y \to \exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}))$
63	62	adantr	$⊢ ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2}) \to (x \leq y \to \exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}))$
64	63	impcom	$⊢ (x \leq y \land ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2})) \to \exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = x^{2} + y^{2})$
65		eqeq2	$⊢ P = x^{2} + y^{2} \to (x^{2} + b^{2} = P \leftrightarrow x^{2} + b^{2} = x^{2} + y^{2})$
66	65	anbi2d	$⊢ P = x^{2} + y^{2} \to ((x \leq b \land x^{2} + b^{2} = P) \leftrightarrow (x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}))$
67	66	reubidv	$⊢ P = x^{2} + y^{2} \to (\exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = P) \leftrightarrow \exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}))$
68	67	adantl	$⊢ ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2}) \to (\exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = P) \leftrightarrow \exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}))$
69	68	adantl	$⊢ (x \leq y \land ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2})) \to (\exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = P) \leftrightarrow \exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = x^{2} + y^{2}))$
70	64 69	mpbird	$⊢ (x \leq y \land ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2})) \to \exists! b \in ℕ (x \leq b \land x^{2} + b^{2} = P)$
71	3 10 70	rspcedvd	$⊢ (x \leq y \land ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2})) \to \exists a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P)$
72	11	adantr	$⊢ ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2}) \to y \in ℕ$
73	72	adantl	$⊢ (\neg x \leq y \land ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2})) \to y \in ℕ$
74		breq1	$⊢ a = y \to (a \leq b \leftrightarrow y \leq b)$
75		oveq1	$⊢ a = y \to a^{2} = y^{2}$
76	75	oveq1d	$⊢ a = y \to a^{2} + b^{2} = y^{2} + b^{2}$
77	76	eqeq1d	$⊢ a = y \to (a^{2} + b^{2} = P \leftrightarrow y^{2} + b^{2} = P)$
78	74 77	anbi12d	$⊢ a = y \to ((a \leq b \land a^{2} + b^{2} = P) \leftrightarrow (y \leq b \land y^{2} + b^{2} = P))$
79	78	reubidv	$⊢ a = y \to (\exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \leftrightarrow \exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = P))$
80	79	adantl	$⊢ ((\neg x \leq y \land ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2})) \land a = y) \to (\exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \leftrightarrow \exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = P))$
81		simpll	$⊢ ((x \in ℕ \land y \in ℕ) \land \neg x \leq y) \to x \in ℕ$
82		breq2	$⊢ b = x \to (y \leq b \leftrightarrow y \leq x)$
83		oveq1	$⊢ b = x \to b^{2} = x^{2}$
84	83	oveq2d	$⊢ b = x \to y^{2} + b^{2} = y^{2} + x^{2}$
85	84	eqeq1d	$⊢ b = x \to (y^{2} + b^{2} = x^{2} + y^{2} \leftrightarrow y^{2} + x^{2} = x^{2} + y^{2})$
86	82 85	anbi12d	$⊢ b = x \to ((y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}) \leftrightarrow (y \leq x \land y^{2} + x^{2} = x^{2} + y^{2}))$
87		equequ1	$⊢ b = x \to (b = c \leftrightarrow x = c)$
88	87	imbi2d	$⊢ b = x \to (((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to b = c) \leftrightarrow ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to x = c))$
89	88	ralbidv	$⊢ b = x \to (\forall c \in ℕ ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to b = c) \leftrightarrow \forall c \in ℕ ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to x = c))$
90	86 89	anbi12d	$⊢ b = x \to (((y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to b = c)) \leftrightarrow ((y \leq x \land y^{2} + x^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to x = c)))$
91	90	adantl	$⊢ (((x \in ℕ \land y \in ℕ) \land \neg x \leq y) \land b = x) \to (((y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to b = c)) \leftrightarrow ((y \leq x \land y^{2} + x^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to x = c)))$
92		ltnle	$⊢ (y \in ℝ \land x \in ℝ) \to (y < x \leftrightarrow \neg x \leq y)$
93	28 32 92	syl2anr	$⊢ (x \in ℕ \land y \in ℕ) \to (y < x \leftrightarrow \neg x \leq y)$
94	28	ad2antlr	$⊢ ((x \in ℕ \land y \in ℕ) \land y < x) \to y \in ℝ$
95	32	ad2antrr	$⊢ ((x \in ℕ \land y \in ℕ) \land y < x) \to x \in ℝ$
96		simpr	$⊢ ((x \in ℕ \land y \in ℕ) \land y < x) \to y < x$
97	94 95 96	ltled	$⊢ ((x \in ℕ \land y \in ℕ) \land y < x) \to y \leq x$
98	97	ex	$⊢ (x \in ℕ \land y \in ℕ) \to (y < x \to y \leq x)$
99	93 98	sylbird	$⊢ (x \in ℕ \land y \in ℕ) \to (\neg x \leq y \to y \leq x)$
100	99	imp	$⊢ ((x \in ℕ \land y \in ℕ) \land \neg x \leq y) \to y \leq x$
101	29	recnd	$⊢ y \in ℕ \to y^{2} \in ℂ$
102	101	adantl	$⊢ (x \in ℕ \land y \in ℕ) \to y^{2} \in ℂ$
103	33	recnd	$⊢ x \in ℕ \to x^{2} \in ℂ$
104	103	adantr	$⊢ (x \in ℕ \land y \in ℕ) \to x^{2} \in ℂ$
105	102 104	addcomd	$⊢ (x \in ℕ \land y \in ℕ) \to y^{2} + x^{2} = x^{2} + y^{2}$
106	105	adantr	$⊢ ((x \in ℕ \land y \in ℕ) \land \neg x \leq y) \to y^{2} + x^{2} = x^{2} + y^{2}$
107	34	recnd	$⊢ (x \in ℕ \land y \in ℕ) \to x^{2} \in ℂ$
108	107	adantr	$⊢ ((x \in ℕ \land y \in ℕ) \land c \in ℕ) \to x^{2} \in ℂ$
109	30	recnd	$⊢ (x \in ℕ \land y \in ℕ) \to y^{2} \in ℂ$
110	109	adantr	$⊢ ((x \in ℕ \land y \in ℕ) \land c \in ℕ) \to y^{2} \in ℂ$
111	108 110	addcomd	$⊢ ((x \in ℕ \land y \in ℕ) \land c \in ℕ) \to x^{2} + y^{2} = y^{2} + x^{2}$
112	111	eqeq2d	$⊢ ((x \in ℕ \land y \in ℕ) \land c \in ℕ) \to (y^{2} + c^{2} = x^{2} + y^{2} \leftrightarrow y^{2} + c^{2} = y^{2} + x^{2})$
113	26	adantl	$⊢ ((x \in ℕ \land y \in ℕ) \land c \in ℕ) \to c^{2} \in ℝ$
114	33	ad2antrr	$⊢ ((x \in ℕ \land y \in ℕ) \land c \in ℕ) \to x^{2} \in ℝ$
115	29	ad2antlr	$⊢ ((x \in ℕ \land y \in ℕ) \land c \in ℕ) \to y^{2} \in ℝ$
116		readdcan	$⊢ (c^{2} \in ℝ \land x^{2} \in ℝ \land y^{2} \in ℝ) \to (y^{2} + c^{2} = y^{2} + x^{2} \leftrightarrow c^{2} = x^{2})$
117	113 114 115 116	syl3anc	$⊢ ((x \in ℕ \land y \in ℕ) \land c \in ℕ) \to (y^{2} + c^{2} = y^{2} + x^{2} \leftrightarrow c^{2} = x^{2})$
118	112 117	bitrd	$⊢ ((x \in ℕ \land y \in ℕ) \land c \in ℕ) \to (y^{2} + c^{2} = x^{2} + y^{2} \leftrightarrow c^{2} = x^{2})$
119	25	ad2antlr	$⊢ (((x \in ℕ \land y \in ℕ) \land c \in ℕ) \land c^{2} = x^{2}) \to c \in ℝ$
120	32	adantr	$⊢ (x \in ℕ \land y \in ℕ) \to x \in ℝ$
121	120	ad2antrr	$⊢ (((x \in ℕ \land y \in ℕ) \land c \in ℕ) \land c^{2} = x^{2}) \to x \in ℝ$
122	44	ad2antlr	$⊢ (((x \in ℕ \land y \in ℕ) \land c \in ℕ) \land c^{2} = x^{2}) \to 0 \leq c$
123		nnnn0	$⊢ x \in ℕ \to x \in ℕ_{0}$
124	123	nn0ge0d	$⊢ x \in ℕ \to 0 \leq x$
125	124	adantr	$⊢ (x \in ℕ \land y \in ℕ) \to 0 \leq x$
126	125	ad2antrr	$⊢ (((x \in ℕ \land y \in ℕ) \land c \in ℕ) \land c^{2} = x^{2}) \to 0 \leq x$
127		simpr	$⊢ (((x \in ℕ \land y \in ℕ) \land c \in ℕ) \land c^{2} = x^{2}) \to c^{2} = x^{2}$
128	119 121 122 126 127	sq11d	$⊢ (((x \in ℕ \land y \in ℕ) \land c \in ℕ) \land c^{2} = x^{2}) \to c = x$
129	128	eqcomd	$⊢ (((x \in ℕ \land y \in ℕ) \land c \in ℕ) \land c^{2} = x^{2}) \to x = c$
130	129	ex	$⊢ ((x \in ℕ \land y \in ℕ) \land c \in ℕ) \to (c^{2} = x^{2} \to x = c)$
131	118 130	sylbid	$⊢ ((x \in ℕ \land y \in ℕ) \land c \in ℕ) \to (y^{2} + c^{2} = x^{2} + y^{2} \to x = c)$
132	131	adantld	$⊢ ((x \in ℕ \land y \in ℕ) \land c \in ℕ) \to ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to x = c)$
133	132	ralrimiva	$⊢ (x \in ℕ \land y \in ℕ) \to \forall c \in ℕ ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to x = c)$
134	133	adantr	$⊢ ((x \in ℕ \land y \in ℕ) \land \neg x \leq y) \to \forall c \in ℕ ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to x = c)$
135	100 106 134	jca31	$⊢ ((x \in ℕ \land y \in ℕ) \land \neg x \leq y) \to ((y \leq x \land y^{2} + x^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to x = c))$
136	81 91 135	rspcedvd	$⊢ ((x \in ℕ \land y \in ℕ) \land \neg x \leq y) \to \exists b \in ℕ ((y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to b = c))$
137		breq2	$⊢ b = c \to (y \leq b \leftrightarrow y \leq c)$
138	56	oveq2d	$⊢ b = c \to y^{2} + b^{2} = y^{2} + c^{2}$
139	138	eqeq1d	$⊢ b = c \to (y^{2} + b^{2} = x^{2} + y^{2} \leftrightarrow y^{2} + c^{2} = x^{2} + y^{2})$
140	137 139	anbi12d	$⊢ b = c \to ((y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}) \leftrightarrow (y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}))$
141	140	reu8	$⊢ \exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}) \leftrightarrow \exists b \in ℕ ((y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}) \land \forall c \in ℕ ((y \leq c \land y^{2} + c^{2} = x^{2} + y^{2}) \to b = c))$
142	136 141	sylibr	$⊢ ((x \in ℕ \land y \in ℕ) \land \neg x \leq y) \to \exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = x^{2} + y^{2})$
143	142	ex	$⊢ (x \in ℕ \land y \in ℕ) \to (\neg x \leq y \to \exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}))$
144	143	adantr	$⊢ ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2}) \to (\neg x \leq y \to \exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}))$
145	144	impcom	$⊢ (\neg x \leq y \land ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2})) \to \exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = x^{2} + y^{2})$
146		eqeq2	$⊢ P = x^{2} + y^{2} \to (y^{2} + b^{2} = P \leftrightarrow y^{2} + b^{2} = x^{2} + y^{2})$
147	146	anbi2d	$⊢ P = x^{2} + y^{2} \to ((y \leq b \land y^{2} + b^{2} = P) \leftrightarrow (y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}))$
148	147	reubidv	$⊢ P = x^{2} + y^{2} \to (\exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = P) \leftrightarrow \exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}))$
149	148	adantl	$⊢ ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2}) \to (\exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = P) \leftrightarrow \exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}))$
150	149	adantl	$⊢ (\neg x \leq y \land ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2})) \to (\exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = P) \leftrightarrow \exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = x^{2} + y^{2}))$
151	145 150	mpbird	$⊢ (\neg x \leq y \land ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2})) \to \exists! b \in ℕ (y \leq b \land y^{2} + b^{2} = P)$
152	73 80 151	rspcedvd	$⊢ (\neg x \leq y \land ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2})) \to \exists a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P)$
153	71 152	pm2.61ian	$⊢ ((x \in ℕ \land y \in ℕ) \land P = x^{2} + y^{2}) \to \exists a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P)$
154	153	ex	$⊢ (x \in ℕ \land y \in ℕ) \to (P = x^{2} + y^{2} \to \exists a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P))$
155	154	adantl	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (x \in ℕ \land y \in ℕ)) \to (P = x^{2} + y^{2} \to \exists a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P))$
156	155	rexlimdvva	$⊢ (P \in ℙ \land P \mod 4 = 1) \to (\exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2} \to \exists a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P))$
157	1 156	mpd	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P)$
158		reurex	$⊢ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \to \exists b \in ℕ (a \leq b \land a^{2} + b^{2} = P)$
159	158	a1i	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ) \to (\exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \to \exists b \in ℕ (a \leq b \land a^{2} + b^{2} = P))$
160	159	ralrimiva	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \forall a \in ℕ (\exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \to \exists b \in ℕ (a \leq b \land a^{2} + b^{2} = P))$
161		2sqmo	$⊢ P \in ℙ \to \exists^{*} a \in ℕ_{0} \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)$
162		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
163		nfcv	$⊢ \underline{Ⅎ} a ℕ$
164		nfcv	$⊢ \underline{Ⅎ} a ℕ_{0}$
165	163 164	ssrmof	$⊢ ℕ \subseteq ℕ_{0} \to (\exists^{} a \in ℕ_{0} \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P) \to \exists^{} a \in ℕ \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P))$
166	162 165	ax-mp	$⊢ \exists^{} a \in ℕ_{0} \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P) \to \exists^{} a \in ℕ \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)$
167		ssrexv	$⊢ ℕ \subseteq ℕ_{0} \to (\exists b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \to \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P))$
168	162 167	ax-mp	$⊢ \exists b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \to \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)$
169	168	rmoimi	$⊢ \exists^{} a \in ℕ \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P) \to \exists^{} a \in ℕ \exists b \in ℕ (a \leq b \land a^{2} + b^{2} = P)$
170	161 166 169	3syl	$⊢ P \in ℙ \to \exists^{*} a \in ℕ \exists b \in ℕ (a \leq b \land a^{2} + b^{2} = P)$
171	170	adantr	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists^{*} a \in ℕ \exists b \in ℕ (a \leq b \land a^{2} + b^{2} = P)$
172		rmoim	$⊢ \forall a \in ℕ (\exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \to \exists b \in ℕ (a \leq b \land a^{2} + b^{2} = P)) \to (\exists^{} a \in ℕ \exists b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \to \exists^{} a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P))$
173	160 171 172	sylc	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists^{*} a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P)$
174		reu5	$⊢ \exists! a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \leftrightarrow (\exists a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P) \land \exists^{*} a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P))$
175	157 173 174	sylanbrc	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists! a \in ℕ \exists! b \in ℕ (a \leq b \land a^{2} + b^{2} = P)$

Metamath Proof Explorer

Theorem 2sqreunnlem1

Proof