Metamath Proof Explorer

Theorem 2sqreulem1

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

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

Proof

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