Step | Hyp | Ref
| Expression |
1 | | 4sq.1 |
. . 3
โข ๐ = {๐ โฃ โ๐ฅ โ โค โ๐ฆ โ โค โ๐ง โ โค โ๐ค โ โค ๐ = (((๐ฅโ2) + (๐ฆโ2)) + ((๐งโ2) + (๐คโ2)))} |
2 | | 4sq.2 |
. . 3
โข (๐ โ ๐ โ โ) |
3 | | 4sq.3 |
. . 3
โข (๐ โ ๐ = ((2 ยท ๐) + 1)) |
4 | | 4sq.4 |
. . 3
โข (๐ โ ๐ โ โ) |
5 | | eqid 2733 |
. . 3
โข {๐ข โฃ โ๐ โ (0...๐)๐ข = ((๐โ2) mod ๐)} = {๐ข โฃ โ๐ โ (0...๐)๐ข = ((๐โ2) mod ๐)} |
6 | | eqid 2733 |
. . 3
โข (๐ฃ โ {๐ข โฃ โ๐ โ (0...๐)๐ข = ((๐โ2) mod ๐)} โฆ ((๐ โ 1) โ ๐ฃ)) = (๐ฃ โ {๐ข โฃ โ๐ โ (0...๐)๐ข = ((๐โ2) mod ๐)} โฆ ((๐ โ 1) โ ๐ฃ)) |
7 | 1, 2, 3, 4, 5, 6 | 4sqlem12 16833 |
. 2
โข (๐ โ โ๐ โ (1...(๐ โ 1))โ๐ข โ โค[i] (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) |
8 | | simplrl 776 |
. . . . . . . 8
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โ (1...(๐ โ 1))) |
9 | | elfznn 13476 |
. . . . . . . 8
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โ) |
10 | 8, 9 | syl 17 |
. . . . . . 7
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โ โ) |
11 | | simpr 486 |
. . . . . . . 8
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) |
12 | | abs1 15188 |
. . . . . . . . . . . 12
โข
(absโ1) = 1 |
13 | 12 | oveq1i 7368 |
. . . . . . . . . . 11
โข
((absโ1)โ2) = (1โ2) |
14 | | sq1 14105 |
. . . . . . . . . . 11
โข
(1โ2) = 1 |
15 | 13, 14 | eqtri 2761 |
. . . . . . . . . 10
โข
((absโ1)โ2) = 1 |
16 | 15 | oveq2i 7369 |
. . . . . . . . 9
โข
(((absโ๐ข)โ2) + ((absโ1)โ2)) =
(((absโ๐ข)โ2) +
1) |
17 | | simplrr 777 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ข โ โค[i]) |
18 | | 1z 12538 |
. . . . . . . . . . 11
โข 1 โ
โค |
19 | | zgz 16810 |
. . . . . . . . . . 11
โข (1 โ
โค โ 1 โ โค[i]) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . 10
โข 1 โ
โค[i] |
21 | 1 | 4sqlem4a 16828 |
. . . . . . . . . 10
โข ((๐ข โ โค[i] โง 1
โ โค[i]) โ (((absโ๐ข)โ2) + ((absโ1)โ2)) โ
๐) |
22 | 17, 20, 21 | sylancl 587 |
. . . . . . . . 9
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ (((absโ๐ข)โ2) + ((absโ1)โ2)) โ
๐) |
23 | 16, 22 | eqeltrrid 2839 |
. . . . . . . 8
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ (((absโ๐ข)โ2) + 1) โ ๐) |
24 | 11, 23 | eqeltrrd 2835 |
. . . . . . 7
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ (๐ ยท ๐) โ ๐) |
25 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
26 | 25 | eleq1d 2819 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ ยท ๐) โ ๐ โ (๐ ยท ๐) โ ๐)) |
27 | | 4sq.6 |
. . . . . . . 8
โข ๐ = {๐ โ โ โฃ (๐ ยท ๐) โ ๐} |
28 | 26, 27 | elrab2 3649 |
. . . . . . 7
โข (๐ โ ๐ โ (๐ โ โ โง (๐ ยท ๐) โ ๐)) |
29 | 10, 24, 28 | sylanbrc 584 |
. . . . . 6
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โ ๐) |
30 | 29 | ne0d 4296 |
. . . . 5
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โ โ
) |
31 | 27 | ssrab3 4041 |
. . . . . . . 8
โข ๐ โ
โ |
32 | | 4sq.7 |
. . . . . . . . 9
โข ๐ = inf(๐, โ, < ) |
33 | | nnuz 12811 |
. . . . . . . . . . 11
โข โ =
(โคโฅโ1) |
34 | 31, 33 | sseqtri 3981 |
. . . . . . . . . 10
โข ๐ โ
(โคโฅโ1) |
35 | | infssuzcl 12862 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ1) โง ๐ โ โ
) โ inf(๐, โ, < ) โ ๐) |
36 | 34, 30, 35 | sylancr 588 |
. . . . . . . . 9
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ inf(๐, โ, < ) โ ๐) |
37 | 32, 36 | eqeltrid 2838 |
. . . . . . . 8
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โ ๐) |
38 | 31, 37 | sselid 3943 |
. . . . . . 7
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โ โ) |
39 | 38 | nnred 12173 |
. . . . . 6
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โ โ) |
40 | 10 | nnred 12173 |
. . . . . 6
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โ โ) |
41 | 4 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โ โ) |
42 | | prmnn 16555 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
43 | 41, 42 | syl 17 |
. . . . . . 7
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โ โ) |
44 | 43 | nnred 12173 |
. . . . . 6
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โ โ) |
45 | | infssuzle 12861 |
. . . . . . . 8
โข ((๐ โ
(โคโฅโ1) โง ๐ โ ๐) โ inf(๐, โ, < ) โค ๐) |
46 | 34, 29, 45 | sylancr 588 |
. . . . . . 7
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ inf(๐, โ, < ) โค ๐) |
47 | 32, 46 | eqbrtrid 5141 |
. . . . . 6
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โค ๐) |
48 | | prmz 16556 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
49 | 41, 48 | syl 17 |
. . . . . . . . 9
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ โ โค) |
50 | | elfzm11 13518 |
. . . . . . . . 9
โข ((1
โ โค โง ๐
โ โค) โ (๐
โ (1...(๐ โ 1))
โ (๐ โ โค
โง 1 โค ๐ โง ๐ < ๐))) |
51 | 18, 49, 50 | sylancr 588 |
. . . . . . . 8
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ (๐ โ (1...(๐ โ 1)) โ (๐ โ โค โง 1 โค ๐ โง ๐ < ๐))) |
52 | 8, 51 | mpbid 231 |
. . . . . . 7
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ (๐ โ โค โง 1 โค ๐ โง ๐ < ๐)) |
53 | 52 | simp3d 1145 |
. . . . . 6
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ < ๐) |
54 | 39, 40, 44, 47, 53 | lelttrd 11318 |
. . . . 5
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ ๐ < ๐) |
55 | 30, 54 | jca 513 |
. . . 4
โข (((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โง (((absโ๐ข)โ2) + 1) = (๐ ยท ๐)) โ (๐ โ โ
โง ๐ < ๐)) |
56 | 55 | ex 414 |
. . 3
โข ((๐ โง (๐ โ (1...(๐ โ 1)) โง ๐ข โ โค[i])) โ
((((absโ๐ข)โ2) +
1) = (๐ ยท ๐) โ (๐ โ โ
โง ๐ < ๐))) |
57 | 56 | rexlimdvva 3202 |
. 2
โข (๐ โ (โ๐ โ (1...(๐ โ 1))โ๐ข โ โค[i] (((absโ๐ข)โ2) + 1) = (๐ ยท ๐) โ (๐ โ โ
โง ๐ < ๐))) |
58 | 7, 57 | mpd 15 |
1
โข (๐ โ (๐ โ โ
โง ๐ < ๐)) |