Metamath Proof Explorer


Theorem 2sqreunnlem1

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

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

Proof

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