| 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 ) ) = 𝑃 ) ) |