Step | Hyp | Ref
| Expression |
1 | | df-ne 2945 |
. . . 4
โข (๐ โ 2 โ ยฌ ๐ = 2) |
2 | | prmz 16558 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
3 | 2 | ad3antrrr 729 |
. . . . . . . . 9
โข ((((๐ โ โ โง ๐ โ 2) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โ ๐ โ โค) |
4 | | simplrr 777 |
. . . . . . . . 9
โข ((((๐ โ โ โง ๐ โ 2) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โ ๐ฆ โ โค) |
5 | | bezout 16431 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ฆ โ โค) โ
โ๐ โ โค
โ๐ โ โค
(๐ gcd ๐ฆ) = ((๐ ยท ๐) + (๐ฆ ยท ๐))) |
6 | 3, 4, 5 | syl2anc 585 |
. . . . . . . 8
โข ((((๐ โ โ โง ๐ โ 2) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โ โ๐ โ โค โ๐ โ โค (๐ gcd ๐ฆ) = ((๐ ยท ๐) + (๐ฆ ยท ๐))) |
7 | | simplll 774 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ โง ๐ โ 2)
โง (๐ฅ โ โค
โง ๐ฆ โ โค))
โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โง ((๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐ฆ) = ((๐ ยท ๐) + (๐ฆ ยท ๐)))) โ (๐ โ โ โง ๐ โ 2)) |
8 | | simpllr 775 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ โง ๐ โ 2)
โง (๐ฅ โ โค
โง ๐ฆ โ โค))
โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โง ((๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐ฆ) = ((๐ ยท ๐) + (๐ฆ ยท ๐)))) โ (๐ฅ โ โค โง ๐ฆ โ โค)) |
9 | | simplr 768 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ โง ๐ โ 2)
โง (๐ฅ โ โค
โง ๐ฆ โ โค))
โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โง ((๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐ฆ) = ((๐ ยท ๐) + (๐ฆ ยท ๐)))) โ ๐ = ((๐ฅโ2) + (๐ฆโ2))) |
10 | | simprll 778 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ โง ๐ โ 2)
โง (๐ฅ โ โค
โง ๐ฆ โ โค))
โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โง ((๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐ฆ) = ((๐ ยท ๐) + (๐ฆ ยท ๐)))) โ ๐ โ โค) |
11 | | simprlr 779 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ โง ๐ โ 2)
โง (๐ฅ โ โค
โง ๐ฆ โ โค))
โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โง ((๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐ฆ) = ((๐ ยท ๐) + (๐ฆ ยท ๐)))) โ ๐ โ โค) |
12 | | simprr 772 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ โง ๐ โ 2)
โง (๐ฅ โ โค
โง ๐ฆ โ โค))
โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โง ((๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐ฆ) = ((๐ ยท ๐) + (๐ฆ ยท ๐)))) โ (๐ gcd ๐ฆ) = ((๐ ยท ๐) + (๐ฆ ยท ๐))) |
13 | 7, 8, 9, 10, 11, 12 | 2sqblem 26795 |
. . . . . . . . . 10
โข
(((((๐ โ
โ โง ๐ โ 2)
โง (๐ฅ โ โค
โง ๐ฆ โ โค))
โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โง ((๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐ฆ) = ((๐ ยท ๐) + (๐ฆ ยท ๐)))) โ (๐ mod 4) = 1) |
14 | 13 | expr 458 |
. . . . . . . . 9
โข
(((((๐ โ
โ โง ๐ โ 2)
โง (๐ฅ โ โค
โง ๐ฆ โ โค))
โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ gcd ๐ฆ) = ((๐ ยท ๐) + (๐ฆ ยท ๐)) โ (๐ mod 4) = 1)) |
15 | 14 | rexlimdvva 3206 |
. . . . . . . 8
โข ((((๐ โ โ โง ๐ โ 2) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โ (โ๐ โ โค โ๐ โ โค (๐ gcd ๐ฆ) = ((๐ ยท ๐) + (๐ฆ ยท ๐)) โ (๐ mod 4) = 1)) |
16 | 6, 15 | mpd 15 |
. . . . . . 7
โข ((((๐ โ โ โง ๐ โ 2) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ฅโ2) + (๐ฆโ2))) โ (๐ mod 4) = 1) |
17 | 16 | ex 414 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ 2) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ = ((๐ฅโ2) + (๐ฆโ2)) โ (๐ mod 4) = 1)) |
18 | 17 | rexlimdvva 3206 |
. . . . 5
โข ((๐ โ โ โง ๐ โ 2) โ (โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ฅโ2) + (๐ฆโ2)) โ (๐ mod 4) = 1)) |
19 | 18 | impancom 453 |
. . . 4
โข ((๐ โ โ โง
โ๐ฅ โ โค
โ๐ฆ โ โค
๐ = ((๐ฅโ2) + (๐ฆโ2))) โ (๐ โ 2 โ (๐ mod 4) = 1)) |
20 | 1, 19 | biimtrrid 242 |
. . 3
โข ((๐ โ โ โง
โ๐ฅ โ โค
โ๐ฆ โ โค
๐ = ((๐ฅโ2) + (๐ฆโ2))) โ (ยฌ ๐ = 2 โ (๐ mod 4) = 1)) |
21 | 20 | orrd 862 |
. 2
โข ((๐ โ โ โง
โ๐ฅ โ โค
โ๐ฆ โ โค
๐ = ((๐ฅโ2) + (๐ฆโ2))) โ (๐ = 2 โจ (๐ mod 4) = 1)) |
22 | | 1z 12540 |
. . . . 5
โข 1 โ
โค |
23 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ฅ = 1 โ (๐ฅโ2) = (1โ2)) |
24 | | sq1 14106 |
. . . . . . . . 9
โข
(1โ2) = 1 |
25 | 23, 24 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ฅ = 1 โ (๐ฅโ2) = 1) |
26 | 25 | oveq1d 7377 |
. . . . . . 7
โข (๐ฅ = 1 โ ((๐ฅโ2) + (๐ฆโ2)) = (1 + (๐ฆโ2))) |
27 | 26 | eqeq2d 2748 |
. . . . . 6
โข (๐ฅ = 1 โ (๐ = ((๐ฅโ2) + (๐ฆโ2)) โ ๐ = (1 + (๐ฆโ2)))) |
28 | | oveq1 7369 |
. . . . . . . . . 10
โข (๐ฆ = 1 โ (๐ฆโ2) = (1โ2)) |
29 | 28, 24 | eqtrdi 2793 |
. . . . . . . . 9
โข (๐ฆ = 1 โ (๐ฆโ2) = 1) |
30 | 29 | oveq2d 7378 |
. . . . . . . 8
โข (๐ฆ = 1 โ (1 + (๐ฆโ2)) = (1 +
1)) |
31 | | 1p1e2 12285 |
. . . . . . . 8
โข (1 + 1) =
2 |
32 | 30, 31 | eqtrdi 2793 |
. . . . . . 7
โข (๐ฆ = 1 โ (1 + (๐ฆโ2)) = 2) |
33 | 32 | eqeq2d 2748 |
. . . . . 6
โข (๐ฆ = 1 โ (๐ = (1 + (๐ฆโ2)) โ ๐ = 2)) |
34 | 27, 33 | rspc2ev 3595 |
. . . . 5
โข ((1
โ โค โง 1 โ โค โง ๐ = 2) โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ฅโ2) + (๐ฆโ2))) |
35 | 22, 22, 34 | mp3an12 1452 |
. . . 4
โข (๐ = 2 โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ฅโ2) + (๐ฆโ2))) |
36 | 35 | adantl 483 |
. . 3
โข ((๐ โ โ โง ๐ = 2) โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ฅโ2) + (๐ฆโ2))) |
37 | | 2sq 26794 |
. . 3
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ฅโ2) + (๐ฆโ2))) |
38 | 36, 37 | jaodan 957 |
. 2
โข ((๐ โ โ โง (๐ = 2 โจ (๐ mod 4) = 1)) โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ฅโ2) + (๐ฆโ2))) |
39 | 21, 38 | impbida 800 |
1
โข (๐ โ โ โ
(โ๐ฅ โ โค
โ๐ฆ โ โค
๐ = ((๐ฅโ2) + (๐ฆโ2)) โ (๐ = 2 โจ (๐ mod 4) = 1))) |