Theorem 2sqreulem1 27714

Description: Lemma 1 for 2sqreu 27724. (Contributed by AV, 4-Jun-2023.)

Assertion

Ref	Expression
2sqreulem1	⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))

Distinct variable group:   𝑃,𝑎,𝑏

Proof of Theorem 2sqreulem1

Dummy variables 𝑐 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2sqnn0 27706	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 𝑃 = ((𝑥↑2) + (𝑦↑2)))
2		simpll 779	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → 𝑥 ∈ ℕ0)
3	2	adantl 487	. . . . . . . 8 ⊢ ((𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → 𝑥 ∈ ℕ0)
4		breq1 5106	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (𝑎 ≤ 𝑏 ↔ 𝑥 ≤ 𝑏))
5		oveq1 7423	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑥 → (𝑎↑2) = (𝑥↑2))
6	5	oveq1d 7431	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑥 → ((𝑎↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑏↑2)))
7	6	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (((𝑎↑2) + (𝑏↑2)) = 𝑃 ↔ ((𝑥↑2) + (𝑏↑2)) = 𝑃))
8	4, 7	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑎 = 𝑥 → ((𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃)))
9	8	reubidv 3381	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃)))
10	9	adantl 487	. . . . . . . 8 ⊢ (((𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) ∧ 𝑎 = 𝑥) → (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃)))
11		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℕ0)
12	11	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → 𝑦 ∈ ℕ0)
13		breq2 5107	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑦 → (𝑥 ≤ 𝑏 ↔ 𝑥 ≤ 𝑦))
14		oveq1 7423	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑦 → (𝑏↑2) = (𝑦↑2))
15	14	oveq2d 7432	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑦 → ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))
16	15	eqeq1d 2762	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑦 → (((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑥↑2) + (𝑦↑2)) = ((𝑥↑2) + (𝑦↑2))))
17	13, 16	anbi12d 644	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑦 → ((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ (𝑥 ≤ 𝑦 ∧ ((𝑥↑2) + (𝑦↑2)) = ((𝑥↑2) + (𝑦↑2)))))
18		equequ1 2058	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑦 → (𝑏 = 𝑐 ↔ 𝑦 = 𝑐))
19	18	imbi2d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑦 → (((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐) ↔ ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐)))
20	19	ralbidv 3185	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑦 → (∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐) ↔ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐)))
21	17, 20	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑦 → (((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)) ↔ ((𝑥 ≤ 𝑦 ∧ ((𝑥↑2) + (𝑦↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐))))
22	21	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑏 = 𝑦) → (((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)) ↔ ((𝑥 ≤ 𝑦 ∧ ((𝑥↑2) + (𝑦↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐))))
23		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝑦)
24		eqidd 2761	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → ((𝑥↑2) + (𝑦↑2)) = ((𝑥↑2) + (𝑦↑2)))
25		nn0re 12562	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ ℕ0 → 𝑐 ∈ ℝ)
26	25	resqcld 14214	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ ℕ0 → (𝑐↑2) ∈ ℝ)
27	26	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → (𝑐↑2) ∈ ℝ)
28		nn0re 12562	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℕ0 → 𝑦 ∈ ℝ)
29	28	resqcld 14214	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℕ0 → (𝑦↑2) ∈ ℝ)
30	29	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑦↑2) ∈ ℝ)
31	30	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → (𝑦↑2) ∈ ℝ)
32		nn0re 12562	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ0 → 𝑥 ∈ ℝ)
33	32	resqcld 14214	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℕ0 → (𝑥↑2) ∈ ℝ)
34	33	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑥↑2) ∈ ℝ)
35	34	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → (𝑥↑2) ∈ ℝ)
36		readdcan 11433	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐↑2) ∈ ℝ ∧ (𝑦↑2) ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑐↑2) = (𝑦↑2)))
37	27, 31, 35, 36	syl3anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → (((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑐↑2) = (𝑦↑2)))
38	28	ad4antlr 746	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → 𝑦 ∈ ℝ)
39	25	ad2antlr 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → 𝑐 ∈ ℝ)
40		nn0ge0 12578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℕ0 → 0 ≤ 𝑦)
41	40	ad4antlr 746	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → 0 ≤ 𝑦)
42		nn0ge0 12578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ ℕ0 → 0 ≤ 𝑐)
43	42	ad2antlr 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → 0 ≤ 𝑐)
44		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → (𝑐↑2) = (𝑦↑2))
45	44	eqcomd 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → (𝑦↑2) = (𝑐↑2))
46	38, 39, 41, 43, 45	sq11d 14347	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → 𝑦 = 𝑐)
47	46	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → ((𝑐↑2) = (𝑦↑2) → 𝑦 = 𝑐))
48	37, 47	sylbid 243	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → (((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)) → 𝑦 = 𝑐))
49	48	adantld 496	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐))
50	49	ralrimiva 3154	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐))
51	23, 24, 50	jca31 524	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → ((𝑥 ≤ 𝑦 ∧ ((𝑥↑2) + (𝑦↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐)))
52	12, 22, 51	rspcedvd 3578	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → ∃𝑏 ∈ ℕ0 ((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)))
53		breq2 5107	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → (𝑥 ≤ 𝑏 ↔ 𝑥 ≤ 𝑐))
54		oveq1 7423	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (𝑏↑2) = (𝑐↑2))
55	54	oveq2d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑐↑2)))
56	55	eqeq1d 2762	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → (((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))))
57	53, 56	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → ((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ (𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)))))
58	57	reu8 3691	. . . . . . . . . . . . 13 ⊢ (∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑏 ∈ ℕ0 ((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)))
59	52, 58	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))))
60	59	ex 418	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑥 ≤ 𝑦 → ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
61	60	adantr 486	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (𝑥 ≤ 𝑦 → ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
62	61	impcom 413	. . . . . . . . 9 ⊢ ((𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))))
63		eqeq2 2772	. . . . . . . . . . . . 13 ⊢ (𝑃 = ((𝑥↑2) + (𝑦↑2)) → (((𝑥↑2) + (𝑏↑2)) = 𝑃 ↔ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))))
64	63	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑃 = ((𝑥↑2) + (𝑦↑2)) → ((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
65	64	reubidv 3381	. . . . . . . . . . 11 ⊢ (𝑃 = ((𝑥↑2) + (𝑦↑2)) → (∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
66	65	adantl 487	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
67	66	adantl 487	. . . . . . . . 9 ⊢ ((𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → (∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
68	62, 67	mpbird 260	. . . . . . . 8 ⊢ ((𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃))
69	3, 10, 68	rspcedvd 3578	. . . . . . 7 ⊢ ((𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
70	11	adantr 486	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → 𝑦 ∈ ℕ0)
71	70	adantl 487	. . . . . . . 8 ⊢ ((¬ 𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → 𝑦 ∈ ℕ0)
72		breq1 5106	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑦 → (𝑎 ≤ 𝑏 ↔ 𝑦 ≤ 𝑏))
73		oveq1 7423	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑦 → (𝑎↑2) = (𝑦↑2))
74	73	oveq1d 7431	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑦 → ((𝑎↑2) + (𝑏↑2)) = ((𝑦↑2) + (𝑏↑2)))
75	74	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑦 → (((𝑎↑2) + (𝑏↑2)) = 𝑃 ↔ ((𝑦↑2) + (𝑏↑2)) = 𝑃))
76	72, 75	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑎 = 𝑦 → ((𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃)))
77	76	reubidv 3381	. . . . . . . . 9 ⊢ (𝑎 = 𝑦 → (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃)))
78	77	adantl 487	. . . . . . . 8 ⊢ (((¬ 𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) ∧ 𝑎 = 𝑦) → (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃)))
79		simpll 779	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → 𝑥 ∈ ℕ0)
80		breq2 5107	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑥 → (𝑦 ≤ 𝑏 ↔ 𝑦 ≤ 𝑥))
81		oveq1 7423	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑥 → (𝑏↑2) = (𝑥↑2))
82	81	oveq2d 7432	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑥 → ((𝑦↑2) + (𝑏↑2)) = ((𝑦↑2) + (𝑥↑2)))
83	82	eqeq1d 2762	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑥 → (((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2))))
84	80, 83	anbi12d 644	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑥 → ((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ (𝑦 ≤ 𝑥 ∧ ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2)))))
85		equequ1 2058	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑥 → (𝑏 = 𝑐 ↔ 𝑥 = 𝑐))
86	85	imbi2d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑥 → (((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐) ↔ ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐)))
87	86	ralbidv 3185	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑥 → (∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐) ↔ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐)))
88	84, 87	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑥 → (((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)) ↔ ((𝑦 ≤ 𝑥 ∧ ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐))))
89	88	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) ∧ 𝑏 = 𝑥) → (((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)) ↔ ((𝑦 ≤ 𝑥 ∧ ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐))))
90		ltnle 11338	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 < 𝑥 ↔ ¬ 𝑥 ≤ 𝑦))
91	28, 32, 90	syl2anr 609	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑦 < 𝑥 ↔ ¬ 𝑥 ≤ 𝑦))
92	28	ad2antlr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑦 < 𝑥) → 𝑦 ∈ ℝ)
93	32	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑦 < 𝑥) → 𝑥 ∈ ℝ)
94		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑦 < 𝑥) → 𝑦 < 𝑥)
95	92, 93, 94	ltled 11407	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑦 < 𝑥) → 𝑦 ≤ 𝑥)
96	95	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑦 < 𝑥 → 𝑦 ≤ 𝑥))
97	91, 96	sylbird 263	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (¬ 𝑥 ≤ 𝑦 → 𝑦 ≤ 𝑥))
98	97	imp 412	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → 𝑦 ≤ 𝑥)
99	29	recnd 11286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ0 → (𝑦↑2) ∈ ℂ)
100	99	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑦↑2) ∈ ℂ)
101	33	recnd 11286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ0 → (𝑥↑2) ∈ ℂ)
102	101	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑥↑2) ∈ ℂ)
103	100, 102	addcomd 11461	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2)))
104	103	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2)))
105	34	recnd 11286	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑥↑2) ∈ ℂ)
106	105	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (𝑥↑2) ∈ ℂ)
107	30	recnd 11286	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑦↑2) ∈ ℂ)
108	107	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (𝑦↑2) ∈ ℂ)
109	106, 108	addcomd 11461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → ((𝑥↑2) + (𝑦↑2)) = ((𝑦↑2) + (𝑥↑2)))
110	109	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑦↑2) + (𝑐↑2)) = ((𝑦↑2) + (𝑥↑2))))
111	26	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (𝑐↑2) ∈ ℝ)
112	33	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (𝑥↑2) ∈ ℝ)
113	29	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (𝑦↑2) ∈ ℝ)
114		readdcan 11433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑐↑2) ∈ ℝ ∧ (𝑥↑2) ∈ ℝ ∧ (𝑦↑2) ∈ ℝ) → (((𝑦↑2) + (𝑐↑2)) = ((𝑦↑2) + (𝑥↑2)) ↔ (𝑐↑2) = (𝑥↑2)))
115	111, 112, 113, 114	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (((𝑦↑2) + (𝑐↑2)) = ((𝑦↑2) + (𝑥↑2)) ↔ (𝑐↑2) = (𝑥↑2)))
116	110, 115	bitrd 282	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑐↑2) = (𝑥↑2)))
117	25	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → 𝑐 ∈ ℝ)
118	32	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → 𝑥 ∈ ℝ)
119	118	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → 𝑥 ∈ ℝ)
120	42	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → 0 ≤ 𝑐)
121		nn0ge0 12578	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℕ0 → 0 ≤ 𝑥)
122	121	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → 0 ≤ 𝑥)
123	122	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → 0 ≤ 𝑥)
124		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → (𝑐↑2) = (𝑥↑2))
125	117, 119, 120, 123, 124	sq11d 14347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → 𝑐 = 𝑥)
126	125	eqcomd 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → 𝑥 = 𝑐)
127	126	ex 418	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → ((𝑐↑2) = (𝑥↑2) → 𝑥 = 𝑐))
128	116, 127	sylbid 243	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)) → 𝑥 = 𝑐))
129	128	adantld 496	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐))
130	129	ralrimiva 3154	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐))
131	130	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐))
132	98, 104, 131	jca31 524	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → ((𝑦 ≤ 𝑥 ∧ ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐)))
133	79, 89, 132	rspcedvd 3578	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → ∃𝑏 ∈ ℕ0 ((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)))
134		breq2 5107	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → (𝑦 ≤ 𝑏 ↔ 𝑦 ≤ 𝑐))
135	54	oveq2d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → ((𝑦↑2) + (𝑏↑2)) = ((𝑦↑2) + (𝑐↑2)))
136	135	eqeq1d 2762	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → (((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))))
137	134, 136	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → ((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ (𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)))))
138	137	reu8 3691	. . . . . . . . . . . . 13 ⊢ (∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑏 ∈ ℕ0 ((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)))
139	133, 138	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))))
140	139	ex 418	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (¬ 𝑥 ≤ 𝑦 → ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
141	140	adantr 486	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (¬ 𝑥 ≤ 𝑦 → ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
142	141	impcom 413	. . . . . . . . 9 ⊢ ((¬ 𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))))
143		eqeq2 2772	. . . . . . . . . . . . 13 ⊢ (𝑃 = ((𝑥↑2) + (𝑦↑2)) → (((𝑦↑2) + (𝑏↑2)) = 𝑃 ↔ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))))
144	143	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑃 = ((𝑥↑2) + (𝑦↑2)) → ((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
145	144	reubidv 3381	. . . . . . . . . . 11 ⊢ (𝑃 = ((𝑥↑2) + (𝑦↑2)) → (∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
146	145	adantl 487	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
147	146	adantl 487	. . . . . . . . 9 ⊢ ((¬ 𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → (∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
148	142, 147	mpbird 260	. . . . . . . 8 ⊢ ((¬ 𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃))
149	71, 78, 148	rspcedvd 3578	. . . . . . 7 ⊢ ((¬ 𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
150	69, 149	pm2.61ian 824	. . . . . 6 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
151	150	ex 418	. . . . 5 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑃 = ((𝑥↑2) + (𝑦↑2)) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
152	151	adantl 487	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)) → (𝑃 = ((𝑥↑2) + (𝑦↑2)) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
153	152	rexlimdvva 3219	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 𝑃 = ((𝑥↑2) + (𝑦↑2)) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
154	1, 153	mpd 16	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
155		reurex 3369	. . . . 5 ⊢ (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
156	155	a1i 11	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) → (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
157	156	ralrimiva 3154	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∀𝑎 ∈ ℕ0 (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
158		2sqmo 27705	. . . 4 ⊢ (𝑃 ∈ ℙ → ∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
159	158	adantr 486	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
160		rmoim 3698	. . 3 ⊢ (∀𝑎 ∈ ℕ0 (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) → (∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → ∃*𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
161	157, 159, 160	sylc 66	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃*𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
162		reu5 3367	. 2 ⊢ (∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ (∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ∧ ∃*𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
163	154, 161, 162	sylanbrc 595	1 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086  ∃!wreu 3363  ∃*wrmo 3364   class class class wbr 5103  (class class class)co 7416  ℂcc 11147  ℝcr 11148  0cc0 11149  1c1 11150   + caddc 11152   < clt 11292   ≤ cle 11293  2c2 12344  4c4 12346  ℕ₀cn0 12553   mod cmo 13955  ↑cexp 14150  ℙcprime 16786

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7742  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-pre-sup 11227  ax-addf 11228  ax-mulf 11229

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6301  df-ord 6362  df-on 6363  df-lim 6364  df-suc 6365  df-iota 6491  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-isom 6544  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7684  df-ofr 7685  df-om 7869  df-1st 7992  df-2nd 7993  df-supp 8164  df-tpos 8229  df-frecs 8285  df-wrecs 8316  df-recs 8365  df-rdg 8404  df-1o 8462  df-2o 8463  df-oadd 8466  df-er 8703  df-ec 8705  df-qs 8709  df-map 8835  df-pm 8836  df-ixp 8912  df-en 8960  df-dom 8961  df-sdom 8962  df-fin 8963  df-fsupp 9339  df-sup 9419  df-inf 9420  df-oi 9489  df-dju 9931  df-card 9969  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11492  df-neg 11493  df-div 11921  df-nn 12283  df-2 12352  df-3 12353  df-4 12354  df-5 12355  df-6 12356  df-7 12357  df-8 12358  df-9 12359  df-n0 12554  df-xnn0 12627  df-z 12641  df-dec 12762  df-uz 12913  df-q 13023  df-rp 13068  df-fz 13587  df-fzo 13735  df-fl 13878  df-mod 13956  df-seq 14091  df-exp 14151  df-hash 14420  df-cj 15211  df-re 15212  df-im 15213  df-sqrt 15347  df-abs 15348  df-dvds 16368  df-gcd 16610  df-prm 16787  df-phi 16882  df-pc 16954  df-gz 17047  df-struct 17264  df-sets 17281  df-slot 17299  df-ndx 17311  df-base 17327  df-ress 17348  df-plusg 17380  df-mulr 17381  df-starv 17382  df-sca 17383  df-vsca 17384  df-ip 17385  df-tset 17386  df-ple 17387  df-ds 17389  df-unif 17390  df-hom 17391  df-cco 17392  df-0g 17551  df-gsum 17552  df-prds 17557  df-pws 17559  df-imas 17619  df-qus 17620  df-mre 17695  df-mrc 17696  df-acs 17698  df-mgm 18755  df-sgrp 18847  df-mnd 18863  df-mhm 18917  df-submnd 18918  df-grp 19086  df-minusg 19087  df-sbg 19088  df-mulg 19217  df-subg 19272  df-nsg 19273  df-eqg 19274  df-ghm 19367  df-cntz 19470  df-cmn 19935  df-abl 19936  df-mgp 20300  df-rng 20314  df-ur 20347  df-srg 20352  df-ring 20400  df-cring 20401  df-oppr 20506  df-dvdsr 20526  df-unit 20527  df-invr 20557  df-dvr 20570  df-rhm 20641  df-nzr 20702  df-subrng 20737  df-subrg 20761  df-rlreg 20885  df-domn 20886  df-idom 20887  df-drng 20921  df-field 20922  df-lmod 21076  df-lss 21146  df-lsp 21186  df-sra 21387  df-rgmod 21388  df-lidl 21425  df-rsp 21426  df-2idl 21482  df-cnfld 21618  df-zring 21692  df-zrh 21748  df-zn 21751  df-assa 22100  df-asp 22101  df-ascl 22102  df-psr 22156  df-mvr 22157  df-mpl 22158  df-opsr 22160  df-evls 22322  df-evl 22323  df-psr1 22437  df-vr1 22438  df-ply1 22439  df-coe1 22440  df-evl1 22573  df-mdeg 26312  df-deg1 26313  df-mon1 26388  df-uc1p 26389  df-q1p 26390  df-r1p 26391  df-lgs 27563

This theorem is used by:  2sqreultlem  27715  2sqreu  27724