2sqreulem1

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

Proof

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

Metamath Proof Explorer

Theorem 2sqreulem1

Proof