Step | Hyp | Ref
| Expression |
1 | | elnn0 12420 |
. . . 4
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
2 | | eleq1 2822 |
. . . . . 6
โข (๐ = 1 โ (๐ โ ๐ โ 1 โ ๐)) |
3 | | eleq1 2822 |
. . . . . 6
โข (๐ = ๐ โ (๐ โ ๐ โ ๐ โ ๐)) |
4 | | eleq1 2822 |
. . . . . 6
โข (๐ = ๐ โ (๐ โ ๐ โ ๐ โ ๐)) |
5 | | eleq1 2822 |
. . . . . 6
โข (๐ = (๐ ยท ๐) โ (๐ โ ๐ โ (๐ ยท ๐) โ ๐)) |
6 | | eleq1 2822 |
. . . . . 6
โข (๐ = ๐ โ (๐ โ ๐ โ ๐ โ ๐)) |
7 | | abs1 15188 |
. . . . . . . . . . 11
โข
(absโ1) = 1 |
8 | 7 | oveq1i 7368 |
. . . . . . . . . 10
โข
((absโ1)โ2) = (1โ2) |
9 | | sq1 14105 |
. . . . . . . . . 10
โข
(1โ2) = 1 |
10 | 8, 9 | eqtri 2761 |
. . . . . . . . 9
โข
((absโ1)โ2) = 1 |
11 | | abs0 15176 |
. . . . . . . . . . 11
โข
(absโ0) = 0 |
12 | 11 | oveq1i 7368 |
. . . . . . . . . 10
โข
((absโ0)โ2) = (0โ2) |
13 | | sq0 14102 |
. . . . . . . . . 10
โข
(0โ2) = 0 |
14 | 12, 13 | eqtri 2761 |
. . . . . . . . 9
โข
((absโ0)โ2) = 0 |
15 | 10, 14 | oveq12i 7370 |
. . . . . . . 8
โข
(((absโ1)โ2) + ((absโ0)โ2)) = (1 +
0) |
16 | | 1p0e1 12282 |
. . . . . . . 8
โข (1 + 0) =
1 |
17 | 15, 16 | eqtri 2761 |
. . . . . . 7
โข
(((absโ1)โ2) + ((absโ0)โ2)) = 1 |
18 | | 1z 12538 |
. . . . . . . . 9
โข 1 โ
โค |
19 | | zgz 16810 |
. . . . . . . . 9
โข (1 โ
โค โ 1 โ โค[i]) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . 8
โข 1 โ
โค[i] |
21 | | 0z 12515 |
. . . . . . . . 9
โข 0 โ
โค |
22 | | zgz 16810 |
. . . . . . . . 9
โข (0 โ
โค โ 0 โ โค[i]) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
โข 0 โ
โค[i] |
24 | | 4sq.1 |
. . . . . . . . 9
โข ๐ = {๐ โฃ โ๐ฅ โ โค โ๐ฆ โ โค โ๐ง โ โค โ๐ค โ โค ๐ = (((๐ฅโ2) + (๐ฆโ2)) + ((๐งโ2) + (๐คโ2)))} |
25 | 24 | 4sqlem4a 16828 |
. . . . . . . 8
โข ((1
โ โค[i] โง 0 โ โค[i]) โ (((absโ1)โ2) +
((absโ0)โ2)) โ ๐) |
26 | 20, 23, 25 | mp2an 691 |
. . . . . . 7
โข
(((absโ1)โ2) + ((absโ0)โ2)) โ ๐ |
27 | 17, 26 | eqeltrri 2831 |
. . . . . 6
โข 1 โ
๐ |
28 | | eleq1 2822 |
. . . . . . 7
โข (๐ = 2 โ (๐ โ ๐ โ 2 โ ๐)) |
29 | | eldifsn 4748 |
. . . . . . . . 9
โข (๐ โ (โ โ {2})
โ (๐ โ โ
โง ๐ โ
2)) |
30 | | oddprm 16687 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โ) |
31 | 30 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ ((๐ โ 1) / 2) โ
โ) |
32 | | eldifi 4087 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
33 | 32 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ ๐ โ โ) |
34 | | prmnn 16555 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ) |
35 | | nncn 12166 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ) |
36 | 33, 34, 35 | 3syl 18 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ ๐ โ โ) |
37 | | ax-1cn 11114 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
38 | | subcl 11405 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
1) โ โ) |
39 | 36, 37, 38 | sylancl 587 |
. . . . . . . . . . . . 13
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ (๐ โ 1) โ โ) |
40 | | 2cnd 12236 |
. . . . . . . . . . . . 13
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ 2 โ โ) |
41 | | 2ne0 12262 |
. . . . . . . . . . . . . 14
โข 2 โ
0 |
42 | 41 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ 2 โ 0) |
43 | 39, 40, 42 | divcan2d 11938 |
. . . . . . . . . . . 12
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ (2 ยท ((๐ โ 1) / 2)) = (๐ โ 1)) |
44 | 43 | oveq1d 7373 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ ((2 ยท ((๐ โ 1) / 2)) + 1) = ((๐ โ 1) + 1)) |
45 | | npcan 11415 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ โ
1) + 1) = ๐) |
46 | 36, 37, 45 | sylancl 587 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ ((๐ โ 1) + 1) = ๐) |
47 | 44, 46 | eqtr2d 2774 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ ๐ = ((2 ยท ((๐ โ 1) / 2)) + 1)) |
48 | 43 | oveq2d 7374 |
. . . . . . . . . . . 12
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ (0...(2 ยท ((๐ โ 1) / 2))) = (0...(๐ โ 1))) |
49 | | nnm1nn0 12459 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
50 | 33, 34, 49 | 3syl 18 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ (๐ โ 1) โ
โ0) |
51 | | elnn0uz 12813 |
. . . . . . . . . . . . . 14
โข ((๐ โ 1) โ
โ0 โ (๐ โ 1) โ
(โคโฅโ0)) |
52 | 50, 51 | sylib 217 |
. . . . . . . . . . . . 13
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ (๐ โ 1) โ
(โคโฅโ0)) |
53 | | eluzfz1 13454 |
. . . . . . . . . . . . 13
โข ((๐ โ 1) โ
(โคโฅโ0) โ 0 โ (0...(๐ โ 1))) |
54 | | fzsplit 13473 |
. . . . . . . . . . . . 13
โข (0 โ
(0...(๐ โ 1)) โ
(0...(๐ โ 1)) =
((0...0) โช ((0 + 1)...(๐ โ 1)))) |
55 | 52, 53, 54 | 3syl 18 |
. . . . . . . . . . . 12
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ (0...(๐ โ 1)) = ((0...0) โช ((0 +
1)...(๐ โ
1)))) |
56 | 48, 55 | eqtrd 2773 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ (0...(2 ยท ((๐ โ 1) / 2))) = ((0...0)
โช ((0 + 1)...(๐ โ
1)))) |
57 | | fz0sn 13547 |
. . . . . . . . . . . . . 14
โข (0...0) =
{0} |
58 | 14, 14 | oveq12i 7370 |
. . . . . . . . . . . . . . . . 17
โข
(((absโ0)โ2) + ((absโ0)โ2)) = (0 +
0) |
59 | | 00id 11335 |
. . . . . . . . . . . . . . . . 17
โข (0 + 0) =
0 |
60 | 58, 59 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
โข
(((absโ0)โ2) + ((absโ0)โ2)) = 0 |
61 | 24 | 4sqlem4a 16828 |
. . . . . . . . . . . . . . . . 17
โข ((0
โ โค[i] โง 0 โ โค[i]) โ (((absโ0)โ2) +
((absโ0)โ2)) โ ๐) |
62 | 23, 23, 61 | mp2an 691 |
. . . . . . . . . . . . . . . 16
โข
(((absโ0)โ2) + ((absโ0)โ2)) โ ๐ |
63 | 60, 62 | eqeltrri 2831 |
. . . . . . . . . . . . . . 15
โข 0 โ
๐ |
64 | | snssi 4769 |
. . . . . . . . . . . . . . 15
โข (0 โ
๐ โ {0} โ ๐) |
65 | 63, 64 | ax-mp 5 |
. . . . . . . . . . . . . 14
โข {0}
โ ๐ |
66 | 57, 65 | eqsstri 3979 |
. . . . . . . . . . . . 13
โข (0...0)
โ ๐ |
67 | 66 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ (0...0) โ ๐) |
68 | | 0p1e1 12280 |
. . . . . . . . . . . . . 14
โข (0 + 1) =
1 |
69 | 68 | oveq1i 7368 |
. . . . . . . . . . . . 13
โข ((0 +
1)...(๐ โ 1)) =
(1...(๐ โ
1)) |
70 | | simpr 486 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ โ๐ โ (1...(๐ โ 1))๐ โ ๐) |
71 | | dfss3 3933 |
. . . . . . . . . . . . . 14
โข
((1...(๐ โ 1))
โ ๐ โ
โ๐ โ
(1...(๐ โ 1))๐ โ ๐) |
72 | 70, 71 | sylibr 233 |
. . . . . . . . . . . . 13
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ (1...(๐ โ 1)) โ ๐) |
73 | 69, 72 | eqsstrid 3993 |
. . . . . . . . . . . 12
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ ((0 + 1)...(๐ โ 1)) โ ๐) |
74 | 67, 73 | unssd 4147 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ ((0...0) โช ((0 + 1)...(๐ โ 1))) โ ๐) |
75 | 56, 74 | eqsstrd 3983 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ (0...(2 ยท ((๐ โ 1) / 2))) โ ๐) |
76 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
77 | 76 | eleq1d 2819 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐ ยท ๐) โ ๐ โ (๐ ยท ๐) โ ๐)) |
78 | 77 | cbvrabv 3416 |
. . . . . . . . . 10
โข {๐ โ โ โฃ (๐ ยท ๐) โ ๐} = {๐ โ โ โฃ (๐ ยท ๐) โ ๐} |
79 | | eqid 2733 |
. . . . . . . . . 10
โข
inf({๐ โ
โ โฃ (๐ ยท
๐) โ ๐}, โ, < ) = inf({๐ โ โ โฃ (๐ ยท ๐) โ ๐}, โ, < ) |
80 | 24, 31, 47, 33, 75, 78, 79 | 4sqlem18 16839 |
. . . . . . . . 9
โข ((๐ โ (โ โ {2})
โง โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ ๐ โ ๐) |
81 | 29, 80 | sylanbr 583 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ 2) โง โ๐ โ (1...(๐ โ 1))๐ โ ๐) โ ๐ โ ๐) |
82 | 81 | an32s 651 |
. . . . . . 7
โข (((๐ โ โ โง
โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โง ๐ โ 2) โ ๐ โ ๐) |
83 | 10, 10 | oveq12i 7370 |
. . . . . . . . . 10
โข
(((absโ1)โ2) + ((absโ1)โ2)) = (1 +
1) |
84 | | df-2 12221 |
. . . . . . . . . 10
โข 2 = (1 +
1) |
85 | 83, 84 | eqtr4i 2764 |
. . . . . . . . 9
โข
(((absโ1)โ2) + ((absโ1)โ2)) = 2 |
86 | 24 | 4sqlem4a 16828 |
. . . . . . . . . 10
โข ((1
โ โค[i] โง 1 โ โค[i]) โ (((absโ1)โ2) +
((absโ1)โ2)) โ ๐) |
87 | 20, 20, 86 | mp2an 691 |
. . . . . . . . 9
โข
(((absโ1)โ2) + ((absโ1)โ2)) โ ๐ |
88 | 85, 87 | eqeltrri 2831 |
. . . . . . . 8
โข 2 โ
๐ |
89 | 88 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ โง
โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ 2 โ ๐) |
90 | 28, 82, 89 | pm2.61ne 3027 |
. . . . . 6
โข ((๐ โ โ โง
โ๐ โ
(1...(๐ โ 1))๐ โ ๐) โ ๐ โ ๐) |
91 | 24 | mul4sq 16831 |
. . . . . . 7
โข ((๐ โ ๐ โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) |
92 | 91 | a1i 11 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง ๐ โ (โคโฅโ2))
โ ((๐ โ ๐ โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐)) |
93 | 2, 3, 4, 5, 6, 27,
90, 92 | prmind2 16566 |
. . . . 5
โข (๐ โ โ โ ๐ โ ๐) |
94 | | id 22 |
. . . . . 6
โข (๐ = 0 โ ๐ = 0) |
95 | 94, 63 | eqeltrdi 2842 |
. . . . 5
โข (๐ = 0 โ ๐ โ ๐) |
96 | 93, 95 | jaoi 856 |
. . . 4
โข ((๐ โ โ โจ ๐ = 0) โ ๐ โ ๐) |
97 | 1, 96 | sylbi 216 |
. . 3
โข (๐ โ โ0
โ ๐ โ ๐) |
98 | 97 | ssriv 3949 |
. 2
โข
โ0 โ ๐ |
99 | 24 | 4sqlem1 16825 |
. 2
โข ๐ โ
โ0 |
100 | 98, 99 | eqssi 3961 |
1
โข
โ0 = ๐ |