2sqmo

Description: There exists at most one decomposition of a prime as a sum of two squares. See 2sqb for the existence of such a decomposition. (Contributed by Thierry Arnoux, 2-Feb-2020)

		Ref	Expression
	Assertion	2sqmo	$⊢ P \in ℙ \to \exists^{*} a \in ℕ_{0} \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ b ((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0})$
2		nfre1	$⊢ Ⅎ b \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)$
3	1 2	nfan	$⊢ Ⅎ b (((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P))$
4		nfv	$⊢ Ⅎ b d \in ℕ_{0}$
5	3 4	nfan	$⊢ Ⅎ b ((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)) \land d \in ℕ_{0})$
6		nfv	$⊢ Ⅎ b c \leq d$
7	5 6	nfan	$⊢ Ⅎ b (((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)) \land d \in ℕ_{0}) \land c \leq d)$
8		nfv	$⊢ Ⅎ b c^{2} + d^{2} = P$
9	7 8	nfan	$⊢ Ⅎ b ((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P)$
10		simp-8l	$⊢ ((((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land a \leq b) \land a^{2} + b^{2} = P) \to P \in ℙ$
11		simp-8r	$⊢ ((((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land a \leq b) \land a^{2} + b^{2} = P) \to a \in ℕ_{0}$
12		simpllr	$⊢ ((((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land a \leq b) \land a^{2} + b^{2} = P) \to b \in ℕ_{0}$
13		simp-7r	$⊢ ((((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land a \leq b) \land a^{2} + b^{2} = P) \to c \in ℕ_{0}$
14		simp-6r	$⊢ ((((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land a \leq b) \land a^{2} + b^{2} = P) \to d \in ℕ_{0}$
15		simplr	$⊢ ((((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land a \leq b) \land a^{2} + b^{2} = P) \to a \leq b$
16		simp-5r	$⊢ ((((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land a \leq b) \land a^{2} + b^{2} = P) \to c \leq d$
17		simpr	$⊢ ((((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land a \leq b) \land a^{2} + b^{2} = P) \to a^{2} + b^{2} = P$
18		simp-4r	$⊢ ((((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land a \leq b) \land a^{2} + b^{2} = P) \to c^{2} + d^{2} = P$
19	10 11 12 13 14 15 16 17 18	2sqmod	$⊢ ((((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land a \leq b) \land a^{2} + b^{2} = P) \to (a = c \land b = d)$
20	19	simpld	$⊢ ((((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land a \leq b) \land a^{2} + b^{2} = P) \to a = c$
21	20	anasss	$⊢ (((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land (a \leq b \land a^{2} + b^{2} = P)) \to a = c$
22	21	adantl5r	$⊢ ((((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \land b \in ℕ_{0}) \land (a \leq b \land a^{2} + b^{2} = P)) \to a = c$
23		simp-4r	$⊢ ((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \to \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)$
24	9 22 23	r19.29af	$⊢ ((((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)) \land d \in ℕ_{0}) \land c \leq d) \land c^{2} + d^{2} = P) \to a = c$
25	24	anasss	$⊢ (((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)) \land d \in ℕ_{0}) \land (c \leq d \land c^{2} + d^{2} = P)) \to a = c$
26	25	r19.29an	$⊢ ((((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \land \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)) \land \exists d \in ℕ_{0} (c \leq d \land c^{2} + d^{2} = P)) \to a = c$
27	26	expl	$⊢ ((P \in ℙ \land a \in ℕ_{0}) \land c \in ℕ_{0}) \to ((\exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P) \land \exists d \in ℕ_{0} (c \leq d \land c^{2} + d^{2} = P)) \to a = c)$
28	27	ralrimiva	$⊢ (P \in ℙ \land a \in ℕ_{0}) \to \forall c \in ℕ_{0} ((\exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P) \land \exists d \in ℕ_{0} (c \leq d \land c^{2} + d^{2} = P)) \to a = c)$
29	28	ralrimiva	$⊢ P \in ℙ \to \forall a \in ℕ_{0} \forall c \in ℕ_{0} ((\exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P) \land \exists d \in ℕ_{0} (c \leq d \land c^{2} + d^{2} = P)) \to a = c)$
30		breq12	$⊢ (a = c \land b = d) \to (a \leq b \leftrightarrow c \leq d)$
31		simpl	$⊢ (a = c \land b = d) \to a = c$
32	31	oveq1d	$⊢ (a = c \land b = d) \to a^{2} = c^{2}$
33		simpr	$⊢ (a = c \land b = d) \to b = d$
34	33	oveq1d	$⊢ (a = c \land b = d) \to b^{2} = d^{2}$
35	32 34	oveq12d	$⊢ (a = c \land b = d) \to a^{2} + b^{2} = c^{2} + d^{2}$
36	35	eqeq1d	$⊢ (a = c \land b = d) \to (a^{2} + b^{2} = P \leftrightarrow c^{2} + d^{2} = P)$
37	30 36	anbi12d	$⊢ (a = c \land b = d) \to ((a \leq b \land a^{2} + b^{2} = P) \leftrightarrow (c \leq d \land c^{2} + d^{2} = P))$
38	37	cbvrexdva	$⊢ a = c \to (\exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P) \leftrightarrow \exists d \in ℕ_{0} (c \leq d \land c^{2} + d^{2} = P))$
39	38	rmo4	$⊢ \exists^{*} a \in ℕ_{0} \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P) \leftrightarrow \forall a \in ℕ_{0} \forall c \in ℕ_{0} ((\exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P) \land \exists d \in ℕ_{0} (c \leq d \land c^{2} + d^{2} = P)) \to a = c)$
40	29 39	sylibr	$⊢ P \in ℙ \to \exists^{*} a \in ℕ_{0} \exists b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)$

Metamath Proof Explorer

Theorem 2sqmo

Proof