Theorem 2sqreulem1 27357

Description: Lemma 1 for 2sqreu 27367. (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 27349	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 𝑃 = ((𝑥↑2) + (𝑦↑2)))
2		simpll 766	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → 𝑥 ∈ ℕ0)
3	2	adantl 481	. . . . . . . 8 ⊢ ((𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → 𝑥 ∈ ℕ0)
4		breq1 5110	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (𝑎 ≤ 𝑏 ↔ 𝑥 ≤ 𝑏))
5		oveq1 7394	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑥 → (𝑎↑2) = (𝑥↑2))
6	5	oveq1d 7402	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑥 → ((𝑎↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑏↑2)))
7	6	eqeq1d 2731	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (((𝑎↑2) + (𝑏↑2)) = 𝑃 ↔ ((𝑥↑2) + (𝑏↑2)) = 𝑃))
8	4, 7	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑎 = 𝑥 → ((𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃)))
9	8	reubidv 3372	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃)))
10	9	adantl 481	. . . . . . . 8 ⊢ (((𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) ∧ 𝑎 = 𝑥) → (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃)))
11		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℕ0)
12	11	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → 𝑦 ∈ ℕ0)
13		breq2 5111	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑦 → (𝑥 ≤ 𝑏 ↔ 𝑥 ≤ 𝑦))
14		oveq1 7394	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑦 → (𝑏↑2) = (𝑦↑2))
15	14	oveq2d 7403	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑦 → ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))
16	15	eqeq1d 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑦 → (((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑥↑2) + (𝑦↑2)) = ((𝑥↑2) + (𝑦↑2))))
17	13, 16	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑦 → ((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ (𝑥 ≤ 𝑦 ∧ ((𝑥↑2) + (𝑦↑2)) = ((𝑥↑2) + (𝑦↑2)))))
18		equequ1 2025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑦 → (𝑏 = 𝑐 ↔ 𝑦 = 𝑐))
19	18	imbi2d 340	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑦 → (((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐) ↔ ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐)))
20	19	ralbidv 3156	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑦 → (∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐) ↔ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐)))
21	17, 20	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑦 → (((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)) ↔ ((𝑥 ≤ 𝑦 ∧ ((𝑥↑2) + (𝑦↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐))))
22	21	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑏 = 𝑦) → (((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)) ↔ ((𝑥 ≤ 𝑦 ∧ ((𝑥↑2) + (𝑦↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐))))
23		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝑦)
24		eqidd 2730	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → ((𝑥↑2) + (𝑦↑2)) = ((𝑥↑2) + (𝑦↑2)))
25		nn0re 12451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ ℕ0 → 𝑐 ∈ ℝ)
26	25	resqcld 14090	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ ℕ0 → (𝑐↑2) ∈ ℝ)
27	26	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → (𝑐↑2) ∈ ℝ)
28		nn0re 12451	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℕ0 → 𝑦 ∈ ℝ)
29	28	resqcld 14090	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℕ0 → (𝑦↑2) ∈ ℝ)
30	29	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑦↑2) ∈ ℝ)
31	30	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → (𝑦↑2) ∈ ℝ)
32		nn0re 12451	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ0 → 𝑥 ∈ ℝ)
33	32	resqcld 14090	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℕ0 → (𝑥↑2) ∈ ℝ)
34	33	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑥↑2) ∈ ℝ)
35	34	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → (𝑥↑2) ∈ ℝ)
36		readdcan 11348	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐↑2) ∈ ℝ ∧ (𝑦↑2) ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑐↑2) = (𝑦↑2)))
37	27, 31, 35, 36	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → (((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑐↑2) = (𝑦↑2)))
38	28	ad4antlr 733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → 𝑦 ∈ ℝ)
39	25	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → 𝑐 ∈ ℝ)
40		nn0ge0 12467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℕ0 → 0 ≤ 𝑦)
41	40	ad4antlr 733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → 0 ≤ 𝑦)
42		nn0ge0 12467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ ℕ0 → 0 ≤ 𝑐)
43	42	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → 0 ≤ 𝑐)
44		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → (𝑐↑2) = (𝑦↑2))
45	44	eqcomd 2735	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → (𝑦↑2) = (𝑐↑2))
46	38, 39, 41, 43, 45	sq11d 14223	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑦↑2)) → 𝑦 = 𝑐)
47	46	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → ((𝑐↑2) = (𝑦↑2) → 𝑦 = 𝑐))
48	37, 47	sylbid 240	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → (((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)) → 𝑦 = 𝑐))
49	48	adantld 490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) ∧ 𝑐 ∈ ℕ0) → ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐))
50	49	ralrimiva 3125	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐))
51	23, 24, 50	jca31 514	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → ((𝑥 ≤ 𝑦 ∧ ((𝑥↑2) + (𝑦↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑦 = 𝑐)))
52	12, 22, 51	rspcedvd 3590	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → ∃𝑏 ∈ ℕ0 ((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)))
53		breq2 5111	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → (𝑥 ≤ 𝑏 ↔ 𝑥 ≤ 𝑐))
54		oveq1 7394	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (𝑏↑2) = (𝑐↑2))
55	54	oveq2d 7403	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑐↑2)))
56	55	eqeq1d 2731	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → (((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))))
57	53, 56	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → ((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ (𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)))))
58	57	reu8 3704	. . . . . . . . . . . . 13 ⊢ (∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑏 ∈ ℕ0 ((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑥 ≤ 𝑐 ∧ ((𝑥↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)))
59	52, 58	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑥 ≤ 𝑦) → ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))))
60	59	ex 412	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑥 ≤ 𝑦 → ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
61	60	adantr 480	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (𝑥 ≤ 𝑦 → ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
62	61	impcom 407	. . . . . . . . 9 ⊢ ((𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))))
63		eqeq2 2741	. . . . . . . . . . . . 13 ⊢ (𝑃 = ((𝑥↑2) + (𝑦↑2)) → (((𝑥↑2) + (𝑏↑2)) = 𝑃 ↔ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))))
64	63	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑃 = ((𝑥↑2) + (𝑦↑2)) → ((𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
65	64	reubidv 3372	. . . . . . . . . . 11 ⊢ (𝑃 = ((𝑥↑2) + (𝑦↑2)) → (∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
66	65	adantl 481	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
67	66	adantl 481	. . . . . . . . 9 ⊢ ((𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → (∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
68	62, 67	mpbird 257	. . . . . . . 8 ⊢ ((𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → ∃!𝑏 ∈ ℕ0 (𝑥 ≤ 𝑏 ∧ ((𝑥↑2) + (𝑏↑2)) = 𝑃))
69	3, 10, 68	rspcedvd 3590	. . . . . . 7 ⊢ ((𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
70	11	adantr 480	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → 𝑦 ∈ ℕ0)
71	70	adantl 481	. . . . . . . 8 ⊢ ((¬ 𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → 𝑦 ∈ ℕ0)
72		breq1 5110	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑦 → (𝑎 ≤ 𝑏 ↔ 𝑦 ≤ 𝑏))
73		oveq1 7394	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑦 → (𝑎↑2) = (𝑦↑2))
74	73	oveq1d 7402	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑦 → ((𝑎↑2) + (𝑏↑2)) = ((𝑦↑2) + (𝑏↑2)))
75	74	eqeq1d 2731	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑦 → (((𝑎↑2) + (𝑏↑2)) = 𝑃 ↔ ((𝑦↑2) + (𝑏↑2)) = 𝑃))
76	72, 75	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑎 = 𝑦 → ((𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃)))
77	76	reubidv 3372	. . . . . . . . 9 ⊢ (𝑎 = 𝑦 → (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃)))
78	77	adantl 481	. . . . . . . 8 ⊢ (((¬ 𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) ∧ 𝑎 = 𝑦) → (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃)))
79		simpll 766	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → 𝑥 ∈ ℕ0)
80		breq2 5111	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑥 → (𝑦 ≤ 𝑏 ↔ 𝑦 ≤ 𝑥))
81		oveq1 7394	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑥 → (𝑏↑2) = (𝑥↑2))
82	81	oveq2d 7403	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑥 → ((𝑦↑2) + (𝑏↑2)) = ((𝑦↑2) + (𝑥↑2)))
83	82	eqeq1d 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑥 → (((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2))))
84	80, 83	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑥 → ((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ (𝑦 ≤ 𝑥 ∧ ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2)))))
85		equequ1 2025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑥 → (𝑏 = 𝑐 ↔ 𝑥 = 𝑐))
86	85	imbi2d 340	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑥 → (((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐) ↔ ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐)))
87	86	ralbidv 3156	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑥 → (∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐) ↔ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐)))
88	84, 87	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑥 → (((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)) ↔ ((𝑦 ≤ 𝑥 ∧ ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐))))
89	88	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) ∧ 𝑏 = 𝑥) → (((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)) ↔ ((𝑦 ≤ 𝑥 ∧ ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐))))
90		ltnle 11253	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 < 𝑥 ↔ ¬ 𝑥 ≤ 𝑦))
91	28, 32, 90	syl2anr 597	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑦 < 𝑥 ↔ ¬ 𝑥 ≤ 𝑦))
92	28	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑦 < 𝑥) → 𝑦 ∈ ℝ)
93	32	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑦 < 𝑥) → 𝑥 ∈ ℝ)
94		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑦 < 𝑥) → 𝑦 < 𝑥)
95	92, 93, 94	ltled 11322	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑦 < 𝑥) → 𝑦 ≤ 𝑥)
96	95	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑦 < 𝑥 → 𝑦 ≤ 𝑥))
97	91, 96	sylbird 260	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (¬ 𝑥 ≤ 𝑦 → 𝑦 ≤ 𝑥))
98	97	imp 406	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → 𝑦 ≤ 𝑥)
99	29	recnd 11202	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ0 → (𝑦↑2) ∈ ℂ)
100	99	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑦↑2) ∈ ℂ)
101	33	recnd 11202	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ0 → (𝑥↑2) ∈ ℂ)
102	101	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑥↑2) ∈ ℂ)
103	100, 102	addcomd 11376	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2)))
104	103	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2)))
105	34	recnd 11202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑥↑2) ∈ ℂ)
106	105	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (𝑥↑2) ∈ ℂ)
107	30	recnd 11202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑦↑2) ∈ ℂ)
108	107	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (𝑦↑2) ∈ ℂ)
109	106, 108	addcomd 11376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → ((𝑥↑2) + (𝑦↑2)) = ((𝑦↑2) + (𝑥↑2)))
110	109	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑦↑2) + (𝑐↑2)) = ((𝑦↑2) + (𝑥↑2))))
111	26	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (𝑐↑2) ∈ ℝ)
112	33	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (𝑥↑2) ∈ ℝ)
113	29	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (𝑦↑2) ∈ ℝ)
114		readdcan 11348	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑐↑2) ∈ ℝ ∧ (𝑥↑2) ∈ ℝ ∧ (𝑦↑2) ∈ ℝ) → (((𝑦↑2) + (𝑐↑2)) = ((𝑦↑2) + (𝑥↑2)) ↔ (𝑐↑2) = (𝑥↑2)))
115	111, 112, 113, 114	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (((𝑦↑2) + (𝑐↑2)) = ((𝑦↑2) + (𝑥↑2)) ↔ (𝑐↑2) = (𝑥↑2)))
116	110, 115	bitrd 279	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑐↑2) = (𝑥↑2)))
117	25	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → 𝑐 ∈ ℝ)
118	32	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → 𝑥 ∈ ℝ)
119	118	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → 𝑥 ∈ ℝ)
120	42	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → 0 ≤ 𝑐)
121		nn0ge0 12467	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℕ0 → 0 ≤ 𝑥)
122	121	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → 0 ≤ 𝑥)
123	122	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → 0 ≤ 𝑥)
124		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → (𝑐↑2) = (𝑥↑2))
125	117, 119, 120, 123, 124	sq11d 14223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → 𝑐 = 𝑥)
126	125	eqcomd 2735	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) ∧ (𝑐↑2) = (𝑥↑2)) → 𝑥 = 𝑐)
127	126	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → ((𝑐↑2) = (𝑥↑2) → 𝑥 = 𝑐))
128	116, 127	sylbid 240	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → (((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)) → 𝑥 = 𝑐))
129	128	adantld 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑐 ∈ ℕ0) → ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐))
130	129	ralrimiva 3125	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐))
131	130	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐))
132	98, 104, 131	jca31 514	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → ((𝑦 ≤ 𝑥 ∧ ((𝑦↑2) + (𝑥↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑥 = 𝑐)))
133	79, 89, 132	rspcedvd 3590	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → ∃𝑏 ∈ ℕ0 ((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)))
134		breq2 5111	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → (𝑦 ≤ 𝑏 ↔ 𝑦 ≤ 𝑐))
135	54	oveq2d 7403	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → ((𝑦↑2) + (𝑏↑2)) = ((𝑦↑2) + (𝑐↑2)))
136	135	eqeq1d 2731	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → (((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))))
137	134, 136	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → ((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ (𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2)))))
138	137	reu8 3704	. . . . . . . . . . . . 13 ⊢ (∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑏 ∈ ℕ0 ((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))) ∧ ∀𝑐 ∈ ℕ0 ((𝑦 ≤ 𝑐 ∧ ((𝑦↑2) + (𝑐↑2)) = ((𝑥↑2) + (𝑦↑2))) → 𝑏 = 𝑐)))
139	133, 138	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ ¬ 𝑥 ≤ 𝑦) → ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))))
140	139	ex 412	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (¬ 𝑥 ≤ 𝑦 → ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
141	140	adantr 480	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (¬ 𝑥 ≤ 𝑦 → ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
142	141	impcom 407	. . . . . . . . 9 ⊢ ((¬ 𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))))
143		eqeq2 2741	. . . . . . . . . . . . 13 ⊢ (𝑃 = ((𝑥↑2) + (𝑦↑2)) → (((𝑦↑2) + (𝑏↑2)) = 𝑃 ↔ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2))))
144	143	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑃 = ((𝑥↑2) + (𝑦↑2)) → ((𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
145	144	reubidv 3372	. . . . . . . . . . 11 ⊢ (𝑃 = ((𝑥↑2) + (𝑦↑2)) → (∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
146	145	adantl 481	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → (∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
147	146	adantl 481	. . . . . . . . 9 ⊢ ((¬ 𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → (∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = ((𝑥↑2) + (𝑦↑2)))))
148	142, 147	mpbird 257	. . . . . . . 8 ⊢ ((¬ 𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → ∃!𝑏 ∈ ℕ0 (𝑦 ≤ 𝑏 ∧ ((𝑦↑2) + (𝑏↑2)) = 𝑃))
149	71, 78, 148	rspcedvd 3590	. . . . . . 7 ⊢ ((¬ 𝑥 ≤ 𝑦 ∧ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2)))) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
150	69, 149	pm2.61ian 811	. . . . . 6 ⊢ (((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) ∧ 𝑃 = ((𝑥↑2) + (𝑦↑2))) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
151	150	ex 412	. . . . 5 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑃 = ((𝑥↑2) + (𝑦↑2)) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
152	151	adantl 481	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)) → (𝑃 = ((𝑥↑2) + (𝑦↑2)) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
153	152	rexlimdvva 3194	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 𝑃 = ((𝑥↑2) + (𝑦↑2)) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
154	1, 153	mpd 15	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
155		reurex 3358	. . . . 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 3125	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∀𝑎 ∈ ℕ0 (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
158		2sqmo 27348	. . . 4 ⊢ (𝑃 ∈ ℙ → ∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
159	158	adantr 480	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
160		rmoim 3711	. . 3 ⊢ (∀𝑎 ∈ ℕ0 (∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) → (∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → ∃*𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
161	157, 159, 160	sylc 65	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃*𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
162		reu5 3356	. 2 ⊢ (∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ (∃𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ∧ ∃*𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
163	154, 161, 162	sylanbrc 583	1 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  ∃!wreu 3352  ∃*wrmo 3353   class class class wbr 5107  (class class class)co 7387  ℂcc 11066  ℝcr 11067  0cc0 11068  1c1 11069   + caddc 11071   < clt 11208   ≤ cle 11209  2c2 12241  4c4 12243  ℕ₀cn0 12442   mod cmo 13831  ↑cexp 14026  ℙcprime 16641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145  ax-pre-sup 11146  ax-addf 11147  ax-mulf 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-iin 4958  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-of 7653  df-ofr 7654  df-om 7843  df-1st 7968  df-2nd 7969  df-supp 8140  df-tpos 8205  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-2o 8435  df-oadd 8438  df-er 8671  df-ec 8673  df-qs 8677  df-map 8801  df-pm 8802  df-ixp 8871  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-fsupp 9313  df-sup 9393  df-inf 9394  df-oi 9463  df-dju 9854  df-card 9892  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-div 11836  df-nn 12187  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255  df-9 12256  df-n0 12443  df-xnn0 12516  df-z 12530  df-dec 12650  df-uz 12794  df-q 12908  df-rp 12952  df-fz 13469  df-fzo 13616  df-fl 13754  df-mod 13832  df-seq 13967  df-exp 14027  df-hash 14296  df-cj 15065  df-re 15066  df-im 15067  df-sqrt 15201  df-abs 15202  df-dvds 16223  df-gcd 16465  df-prm 16642  df-phi 16736  df-pc 16808  df-gz 16901  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-starv 17235  df-sca 17236  df-vsca 17237  df-ip 17238  df-tset 17239  df-ple 17240  df-ds 17242  df-unif 17243  df-hom 17244  df-cco 17245  df-0g 17404  df-gsum 17405  df-prds 17410  df-pws 17412  df-imas 17471  df-qus 17472  df-mre 17547  df-mrc 17548  df-acs 17550  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-mhm 18710  df-submnd 18711  df-grp 18868  df-minusg 18869  df-sbg 18870  df-mulg 19000  df-subg 19055  df-nsg 19056  df-eqg 19057  df-ghm 19145  df-cntz 19249  df-cmn 19712  df-abl 19713  df-mgp 20050  df-rng 20062  df-ur 20091  df-srg 20096  df-ring 20144  df-cring 20145  df-oppr 20246  df-dvdsr 20266  df-unit 20267  df-invr 20297  df-dvr 20310  df-rhm 20381  df-nzr 20422  df-subrng 20455  df-subrg 20479  df-rlreg 20603  df-domn 20604  df-idom 20605  df-drng 20640  df-field 20641  df-lmod 20768  df-lss 20838  df-lsp 20878  df-sra 21080  df-rgmod 21081  df-lidl 21118  df-rsp 21119  df-2idl 21160  df-cnfld 21265  df-zring 21357  df-zrh 21413  df-zn 21416  df-assa 21762  df-asp 21763  df-ascl 21764  df-psr 21818  df-mvr 21819  df-mpl 21820  df-opsr 21822  df-evls 21981  df-evl 21982  df-psr1 22064  df-vr1 22065  df-ply1 22066  df-coe1 22067  df-evl1 22203  df-mdeg 25960  df-deg1 25961  df-mon1 26036  df-uc1p 26037  df-q1p 26038  df-r1p 26039  df-lgs 27206

This theorem is referenced by:  2sqreultlem  27358  2sqreu  27367