Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic number theory
All primes 4n+1 are the sum of two squares
2sqreunnlem1
Next ⟩
2sqreunnltlem
Metamath Proof Explorer
Ascii
Unicode
Theorem
2sqreunnlem1
Description:
Lemma 1 for
2sqreunn
.
(Contributed by
AV
, 11-Jun-2023)
Ref
Expression
Assertion
2sqreunnlem1
⊢
P
∈
ℙ
∧
P
mod
4
=
1
→
∃!
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
Proof
Step
Hyp
Ref
Expression
1
2sqnn
⊢
P
∈
ℙ
∧
P
mod
4
=
1
→
∃
x
∈
ℕ
∃
y
∈
ℕ
P
=
x
2
+
y
2
2
simpll
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
x
∈
ℕ
3
2
adantl
⊢
x
≤
y
∧
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
x
∈
ℕ
4
breq1
⊢
a
=
x
→
a
≤
b
↔
x
≤
b
5
oveq1
⊢
a
=
x
→
a
2
=
x
2
6
5
oveq1d
⊢
a
=
x
→
a
2
+
b
2
=
x
2
+
b
2
7
6
eqeq1d
⊢
a
=
x
→
a
2
+
b
2
=
P
↔
x
2
+
b
2
=
P
8
4
7
anbi12d
⊢
a
=
x
→
a
≤
b
∧
a
2
+
b
2
=
P
↔
x
≤
b
∧
x
2
+
b
2
=
P
9
8
reubidv
⊢
a
=
x
→
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
↔
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
P
10
9
adantl
⊢
x
≤
y
∧
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
∧
a
=
x
→
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
↔
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
P
11
simpr
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
y
∈
ℕ
12
11
adantr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
→
y
∈
ℕ
13
breq2
⊢
b
=
y
→
x
≤
b
↔
x
≤
y
14
oveq1
⊢
b
=
y
→
b
2
=
y
2
15
14
oveq2d
⊢
b
=
y
→
x
2
+
b
2
=
x
2
+
y
2
16
15
eqeq1d
⊢
b
=
y
→
x
2
+
b
2
=
x
2
+
y
2
↔
x
2
+
y
2
=
x
2
+
y
2
17
13
16
anbi12d
⊢
b
=
y
→
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
↔
x
≤
y
∧
x
2
+
y
2
=
x
2
+
y
2
18
equequ1
⊢
b
=
y
→
b
=
c
↔
y
=
c
19
18
imbi2d
⊢
b
=
y
→
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
b
=
c
↔
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
y
=
c
20
19
ralbidv
⊢
b
=
y
→
∀
c
∈
ℕ
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
b
=
c
↔
∀
c
∈
ℕ
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
y
=
c
21
17
20
anbi12d
⊢
b
=
y
→
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
b
=
c
↔
x
≤
y
∧
x
2
+
y
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
y
=
c
22
21
adantl
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
b
=
y
→
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
b
=
c
↔
x
≤
y
∧
x
2
+
y
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
y
=
c
23
simpr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
→
x
≤
y
24
eqidd
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
→
x
2
+
y
2
=
x
2
+
y
2
25
nnre
⊢
c
∈
ℕ
→
c
∈
ℝ
26
25
resqcld
⊢
c
∈
ℕ
→
c
2
∈
ℝ
27
26
adantl
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
→
c
2
∈
ℝ
28
nnre
⊢
y
∈
ℕ
→
y
∈
ℝ
29
28
resqcld
⊢
y
∈
ℕ
→
y
2
∈
ℝ
30
29
adantl
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
y
2
∈
ℝ
31
30
ad2antrr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
→
y
2
∈
ℝ
32
nnre
⊢
x
∈
ℕ
→
x
∈
ℝ
33
32
resqcld
⊢
x
∈
ℕ
→
x
2
∈
ℝ
34
33
adantr
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
x
2
∈
ℝ
35
34
ad2antrr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
→
x
2
∈
ℝ
36
readdcan
⊢
c
2
∈
ℝ
∧
y
2
∈
ℝ
∧
x
2
∈
ℝ
→
x
2
+
c
2
=
x
2
+
y
2
↔
c
2
=
y
2
37
27
31
35
36
syl3anc
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
→
x
2
+
c
2
=
x
2
+
y
2
↔
c
2
=
y
2
38
28
ad4antlr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
∧
c
2
=
y
2
→
y
∈
ℝ
39
25
ad2antlr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
∧
c
2
=
y
2
→
c
∈
ℝ
40
nnnn0
⊢
y
∈
ℕ
→
y
∈
ℕ
0
41
40
nn0ge0d
⊢
y
∈
ℕ
→
0
≤
y
42
41
ad4antlr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
∧
c
2
=
y
2
→
0
≤
y
43
nnnn0
⊢
c
∈
ℕ
→
c
∈
ℕ
0
44
43
nn0ge0d
⊢
c
∈
ℕ
→
0
≤
c
45
44
ad2antlr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
∧
c
2
=
y
2
→
0
≤
c
46
simpr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
∧
c
2
=
y
2
→
c
2
=
y
2
47
46
eqcomd
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
∧
c
2
=
y
2
→
y
2
=
c
2
48
38
39
42
45
47
sq11d
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
∧
c
2
=
y
2
→
y
=
c
49
48
ex
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
→
c
2
=
y
2
→
y
=
c
50
37
49
sylbid
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
→
x
2
+
c
2
=
x
2
+
y
2
→
y
=
c
51
50
adantld
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
∧
c
∈
ℕ
→
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
y
=
c
52
51
ralrimiva
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
→
∀
c
∈
ℕ
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
y
=
c
53
23
24
52
jca31
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
→
x
≤
y
∧
x
2
+
y
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
y
=
c
54
12
22
53
rspcedvd
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
→
∃
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
b
=
c
55
breq2
⊢
b
=
c
→
x
≤
b
↔
x
≤
c
56
oveq1
⊢
b
=
c
→
b
2
=
c
2
57
56
oveq2d
⊢
b
=
c
→
x
2
+
b
2
=
x
2
+
c
2
58
57
eqeq1d
⊢
b
=
c
→
x
2
+
b
2
=
x
2
+
y
2
↔
x
2
+
c
2
=
x
2
+
y
2
59
55
58
anbi12d
⊢
b
=
c
→
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
↔
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
60
59
reu8
⊢
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
↔
∃
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
x
≤
c
∧
x
2
+
c
2
=
x
2
+
y
2
→
b
=
c
61
54
60
sylibr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
x
≤
y
→
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
62
61
ex
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
x
≤
y
→
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
63
62
adantr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
x
≤
y
→
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
64
63
impcom
⊢
x
≤
y
∧
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
65
eqeq2
⊢
P
=
x
2
+
y
2
→
x
2
+
b
2
=
P
↔
x
2
+
b
2
=
x
2
+
y
2
66
65
anbi2d
⊢
P
=
x
2
+
y
2
→
x
≤
b
∧
x
2
+
b
2
=
P
↔
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
67
66
reubidv
⊢
P
=
x
2
+
y
2
→
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
P
↔
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
68
67
adantl
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
P
↔
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
69
68
adantl
⊢
x
≤
y
∧
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
P
↔
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
x
2
+
y
2
70
64
69
mpbird
⊢
x
≤
y
∧
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
∃!
b
∈
ℕ
x
≤
b
∧
x
2
+
b
2
=
P
71
3
10
70
rspcedvd
⊢
x
≤
y
∧
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
∃
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
72
11
adantr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
y
∈
ℕ
73
72
adantl
⊢
¬
x
≤
y
∧
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
y
∈
ℕ
74
breq1
⊢
a
=
y
→
a
≤
b
↔
y
≤
b
75
oveq1
⊢
a
=
y
→
a
2
=
y
2
76
75
oveq1d
⊢
a
=
y
→
a
2
+
b
2
=
y
2
+
b
2
77
76
eqeq1d
⊢
a
=
y
→
a
2
+
b
2
=
P
↔
y
2
+
b
2
=
P
78
74
77
anbi12d
⊢
a
=
y
→
a
≤
b
∧
a
2
+
b
2
=
P
↔
y
≤
b
∧
y
2
+
b
2
=
P
79
78
reubidv
⊢
a
=
y
→
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
↔
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
P
80
79
adantl
⊢
¬
x
≤
y
∧
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
∧
a
=
y
→
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
↔
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
P
81
simpll
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
¬
x
≤
y
→
x
∈
ℕ
82
breq2
⊢
b
=
x
→
y
≤
b
↔
y
≤
x
83
oveq1
⊢
b
=
x
→
b
2
=
x
2
84
83
oveq2d
⊢
b
=
x
→
y
2
+
b
2
=
y
2
+
x
2
85
84
eqeq1d
⊢
b
=
x
→
y
2
+
b
2
=
x
2
+
y
2
↔
y
2
+
x
2
=
x
2
+
y
2
86
82
85
anbi12d
⊢
b
=
x
→
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
↔
y
≤
x
∧
y
2
+
x
2
=
x
2
+
y
2
87
equequ1
⊢
b
=
x
→
b
=
c
↔
x
=
c
88
87
imbi2d
⊢
b
=
x
→
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
b
=
c
↔
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
x
=
c
89
88
ralbidv
⊢
b
=
x
→
∀
c
∈
ℕ
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
b
=
c
↔
∀
c
∈
ℕ
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
x
=
c
90
86
89
anbi12d
⊢
b
=
x
→
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
b
=
c
↔
y
≤
x
∧
y
2
+
x
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
x
=
c
91
90
adantl
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
¬
x
≤
y
∧
b
=
x
→
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
b
=
c
↔
y
≤
x
∧
y
2
+
x
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
x
=
c
92
ltnle
⊢
y
∈
ℝ
∧
x
∈
ℝ
→
y
<
x
↔
¬
x
≤
y
93
28
32
92
syl2anr
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
y
<
x
↔
¬
x
≤
y
94
28
ad2antlr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
y
<
x
→
y
∈
ℝ
95
32
ad2antrr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
y
<
x
→
x
∈
ℝ
96
simpr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
y
<
x
→
y
<
x
97
94
95
96
ltled
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
y
<
x
→
y
≤
x
98
97
ex
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
y
<
x
→
y
≤
x
99
93
98
sylbird
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
¬
x
≤
y
→
y
≤
x
100
99
imp
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
¬
x
≤
y
→
y
≤
x
101
29
recnd
⊢
y
∈
ℕ
→
y
2
∈
ℂ
102
101
adantl
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
y
2
∈
ℂ
103
33
recnd
⊢
x
∈
ℕ
→
x
2
∈
ℂ
104
103
adantr
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
x
2
∈
ℂ
105
102
104
addcomd
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
y
2
+
x
2
=
x
2
+
y
2
106
105
adantr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
¬
x
≤
y
→
y
2
+
x
2
=
x
2
+
y
2
107
34
recnd
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
x
2
∈
ℂ
108
107
adantr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
→
x
2
∈
ℂ
109
30
recnd
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
y
2
∈
ℂ
110
109
adantr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
→
y
2
∈
ℂ
111
108
110
addcomd
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
→
x
2
+
y
2
=
y
2
+
x
2
112
111
eqeq2d
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
→
y
2
+
c
2
=
x
2
+
y
2
↔
y
2
+
c
2
=
y
2
+
x
2
113
26
adantl
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
→
c
2
∈
ℝ
114
33
ad2antrr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
→
x
2
∈
ℝ
115
29
ad2antlr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
→
y
2
∈
ℝ
116
readdcan
⊢
c
2
∈
ℝ
∧
x
2
∈
ℝ
∧
y
2
∈
ℝ
→
y
2
+
c
2
=
y
2
+
x
2
↔
c
2
=
x
2
117
113
114
115
116
syl3anc
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
→
y
2
+
c
2
=
y
2
+
x
2
↔
c
2
=
x
2
118
112
117
bitrd
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
→
y
2
+
c
2
=
x
2
+
y
2
↔
c
2
=
x
2
119
25
ad2antlr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
∧
c
2
=
x
2
→
c
∈
ℝ
120
32
adantr
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
x
∈
ℝ
121
120
ad2antrr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
∧
c
2
=
x
2
→
x
∈
ℝ
122
44
ad2antlr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
∧
c
2
=
x
2
→
0
≤
c
123
nnnn0
⊢
x
∈
ℕ
→
x
∈
ℕ
0
124
123
nn0ge0d
⊢
x
∈
ℕ
→
0
≤
x
125
124
adantr
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
0
≤
x
126
125
ad2antrr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
∧
c
2
=
x
2
→
0
≤
x
127
simpr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
∧
c
2
=
x
2
→
c
2
=
x
2
128
119
121
122
126
127
sq11d
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
∧
c
2
=
x
2
→
c
=
x
129
128
eqcomd
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
∧
c
2
=
x
2
→
x
=
c
130
129
ex
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
→
c
2
=
x
2
→
x
=
c
131
118
130
sylbid
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
→
y
2
+
c
2
=
x
2
+
y
2
→
x
=
c
132
131
adantld
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
c
∈
ℕ
→
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
x
=
c
133
132
ralrimiva
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
∀
c
∈
ℕ
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
x
=
c
134
133
adantr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
¬
x
≤
y
→
∀
c
∈
ℕ
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
x
=
c
135
100
106
134
jca31
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
¬
x
≤
y
→
y
≤
x
∧
y
2
+
x
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
x
=
c
136
81
91
135
rspcedvd
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
¬
x
≤
y
→
∃
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
b
=
c
137
breq2
⊢
b
=
c
→
y
≤
b
↔
y
≤
c
138
56
oveq2d
⊢
b
=
c
→
y
2
+
b
2
=
y
2
+
c
2
139
138
eqeq1d
⊢
b
=
c
→
y
2
+
b
2
=
x
2
+
y
2
↔
y
2
+
c
2
=
x
2
+
y
2
140
137
139
anbi12d
⊢
b
=
c
→
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
↔
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
141
140
reu8
⊢
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
↔
∃
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
∧
∀
c
∈
ℕ
y
≤
c
∧
y
2
+
c
2
=
x
2
+
y
2
→
b
=
c
142
136
141
sylibr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
¬
x
≤
y
→
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
143
142
ex
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
¬
x
≤
y
→
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
144
143
adantr
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
¬
x
≤
y
→
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
145
144
impcom
⊢
¬
x
≤
y
∧
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
146
eqeq2
⊢
P
=
x
2
+
y
2
→
y
2
+
b
2
=
P
↔
y
2
+
b
2
=
x
2
+
y
2
147
146
anbi2d
⊢
P
=
x
2
+
y
2
→
y
≤
b
∧
y
2
+
b
2
=
P
↔
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
148
147
reubidv
⊢
P
=
x
2
+
y
2
→
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
P
↔
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
149
148
adantl
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
P
↔
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
150
149
adantl
⊢
¬
x
≤
y
∧
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
P
↔
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
x
2
+
y
2
151
145
150
mpbird
⊢
¬
x
≤
y
∧
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
∃!
b
∈
ℕ
y
≤
b
∧
y
2
+
b
2
=
P
152
73
80
151
rspcedvd
⊢
¬
x
≤
y
∧
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
∃
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
153
71
152
pm2.61ian
⊢
x
∈
ℕ
∧
y
∈
ℕ
∧
P
=
x
2
+
y
2
→
∃
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
154
153
ex
⊢
x
∈
ℕ
∧
y
∈
ℕ
→
P
=
x
2
+
y
2
→
∃
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
155
154
adantl
⊢
P
∈
ℙ
∧
P
mod
4
=
1
∧
x
∈
ℕ
∧
y
∈
ℕ
→
P
=
x
2
+
y
2
→
∃
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
156
155
rexlimdvva
⊢
P
∈
ℙ
∧
P
mod
4
=
1
→
∃
x
∈
ℕ
∃
y
∈
ℕ
P
=
x
2
+
y
2
→
∃
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
157
1
156
mpd
⊢
P
∈
ℙ
∧
P
mod
4
=
1
→
∃
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
158
reurex
⊢
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
→
∃
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
159
158
a1i
⊢
P
∈
ℙ
∧
P
mod
4
=
1
∧
a
∈
ℕ
→
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
→
∃
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
160
159
ralrimiva
⊢
P
∈
ℙ
∧
P
mod
4
=
1
→
∀
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
→
∃
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
161
2sqmo
⊢
P
∈
ℙ
→
∃
*
a
∈
ℕ
0
∃
b
∈
ℕ
0
a
≤
b
∧
a
2
+
b
2
=
P
162
nnssnn0
⊢
ℕ
⊆
ℕ
0
163
nfcv
⊢
Ⅎ
_
a
ℕ
164
nfcv
⊢
Ⅎ
_
a
ℕ
0
165
163
164
ssrmof
⊢
ℕ
⊆
ℕ
0
→
∃
*
a
∈
ℕ
0
∃
b
∈
ℕ
0
a
≤
b
∧
a
2
+
b
2
=
P
→
∃
*
a
∈
ℕ
∃
b
∈
ℕ
0
a
≤
b
∧
a
2
+
b
2
=
P
166
162
165
ax-mp
⊢
∃
*
a
∈
ℕ
0
∃
b
∈
ℕ
0
a
≤
b
∧
a
2
+
b
2
=
P
→
∃
*
a
∈
ℕ
∃
b
∈
ℕ
0
a
≤
b
∧
a
2
+
b
2
=
P
167
ssrexv
⊢
ℕ
⊆
ℕ
0
→
∃
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
→
∃
b
∈
ℕ
0
a
≤
b
∧
a
2
+
b
2
=
P
168
162
167
ax-mp
⊢
∃
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
→
∃
b
∈
ℕ
0
a
≤
b
∧
a
2
+
b
2
=
P
169
168
rmoimi
⊢
∃
*
a
∈
ℕ
∃
b
∈
ℕ
0
a
≤
b
∧
a
2
+
b
2
=
P
→
∃
*
a
∈
ℕ
∃
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
170
161
166
169
3syl
⊢
P
∈
ℙ
→
∃
*
a
∈
ℕ
∃
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
171
170
adantr
⊢
P
∈
ℙ
∧
P
mod
4
=
1
→
∃
*
a
∈
ℕ
∃
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
172
rmoim
⊢
∀
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
→
∃
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
→
∃
*
a
∈
ℕ
∃
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
→
∃
*
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
173
160
171
172
sylc
⊢
P
∈
ℙ
∧
P
mod
4
=
1
→
∃
*
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
174
reu5
⊢
∃!
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
↔
∃
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
∧
∃
*
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P
175
157
173
174
sylanbrc
⊢
P
∈
ℙ
∧
P
mod
4
=
1
→
∃!
a
∈
ℕ
∃!
b
∈
ℕ
a
≤
b
∧
a
2
+
b
2
=
P