Step |
Hyp |
Ref |
Expression |
1 |
|
4sq.1 |
โข ๐ = { ๐ โฃ โ ๐ฅ โ โค โ ๐ฆ โ โค โ ๐ง โ โค โ ๐ค โ โค ๐ = ( ( ( ๐ฅ โ 2 ) + ( ๐ฆ โ 2 ) ) + ( ( ๐ง โ 2 ) + ( ๐ค โ 2 ) ) ) } |
2 |
|
4sq.2 |
โข ( ๐ โ ๐ โ โ ) |
3 |
|
4sq.3 |
โข ( ๐ โ ๐ = ( ( 2 ยท ๐ ) + 1 ) ) |
4 |
|
4sq.4 |
โข ( ๐ โ ๐ โ โ ) |
5 |
|
4sq.5 |
โข ( ๐ โ ( 0 ... ( 2 ยท ๐ ) ) โ ๐ ) |
6 |
|
4sq.6 |
โข ๐ = { ๐ โ โ โฃ ( ๐ ยท ๐ ) โ ๐ } |
7 |
|
4sq.7 |
โข ๐ = inf ( ๐ , โ , < ) |
8 |
|
prmnn |
โข ( ๐ โ โ โ ๐ โ โ ) |
9 |
4 8
|
syl |
โข ( ๐ โ ๐ โ โ ) |
10 |
9
|
nncnd |
โข ( ๐ โ ๐ โ โ ) |
11 |
10
|
mullidd |
โข ( ๐ โ ( 1 ยท ๐ ) = ๐ ) |
12 |
6
|
ssrab3 |
โข ๐ โ โ |
13 |
|
nnuz |
โข โ = ( โคโฅ โ 1 ) |
14 |
12 13
|
sseqtri |
โข ๐ โ ( โคโฅ โ 1 ) |
15 |
1 2 3 4 5 6 7
|
4sqlem13 |
โข ( ๐ โ ( ๐ โ โ
โง ๐ < ๐ ) ) |
16 |
15
|
simpld |
โข ( ๐ โ ๐ โ โ
) |
17 |
|
infssuzcl |
โข ( ( ๐ โ ( โคโฅ โ 1 ) โง ๐ โ โ
) โ inf ( ๐ , โ , < ) โ ๐ ) |
18 |
14 16 17
|
sylancr |
โข ( ๐ โ inf ( ๐ , โ , < ) โ ๐ ) |
19 |
7 18
|
eqeltrid |
โข ( ๐ โ ๐ โ ๐ ) |
20 |
|
oveq1 |
โข ( ๐ = ๐ โ ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) ) |
21 |
20
|
eleq1d |
โข ( ๐ = ๐ โ ( ( ๐ ยท ๐ ) โ ๐ โ ( ๐ ยท ๐ ) โ ๐ ) ) |
22 |
21 6
|
elrab2 |
โข ( ๐ โ ๐ โ ( ๐ โ โ โง ( ๐ ยท ๐ ) โ ๐ ) ) |
23 |
19 22
|
sylib |
โข ( ๐ โ ( ๐ โ โ โง ( ๐ ยท ๐ ) โ ๐ ) ) |
24 |
23
|
simprd |
โข ( ๐ โ ( ๐ ยท ๐ ) โ ๐ ) |
25 |
1
|
4sqlem2 |
โข ( ( ๐ ยท ๐ ) โ ๐ โ โ ๐ โ โค โ ๐ โ โค โ ๐ โ โค โ ๐ โ โค ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) |
26 |
24 25
|
sylib |
โข ( ๐ โ โ ๐ โ โค โ ๐ โ โค โ ๐ โ โค โ ๐ โ โค ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) |
27 |
26
|
adantr |
โข ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โ โ ๐ โ โค โ ๐ โ โค โ ๐ โ โค โ ๐ โ โค ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) |
28 |
|
simp1l |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ๐ ) |
29 |
28 2
|
syl |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ๐ โ โ ) |
30 |
28 3
|
syl |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ๐ = ( ( 2 ยท ๐ ) + 1 ) ) |
31 |
28 4
|
syl |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ๐ โ โ ) |
32 |
28 5
|
syl |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ( 0 ... ( 2 ยท ๐ ) ) โ ๐ ) |
33 |
|
simp1r |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ๐ โ ( โคโฅ โ 2 ) ) |
34 |
|
simp2ll |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ๐ โ โค ) |
35 |
|
simp2lr |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ๐ โ โค ) |
36 |
|
simp2rl |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ๐ โ โค ) |
37 |
|
simp2rr |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ๐ โ โค ) |
38 |
|
eqid |
โข ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) = ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) |
39 |
|
eqid |
โข ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) = ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) |
40 |
|
eqid |
โข ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) = ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) |
41 |
|
eqid |
โข ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) = ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) |
42 |
|
eqid |
โข ( ( ( ( ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) โ 2 ) + ( ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) โ 2 ) ) + ( ( ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) โ 2 ) + ( ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) โ 2 ) ) ) / ๐ ) = ( ( ( ( ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) โ 2 ) + ( ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) โ 2 ) ) + ( ( ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) โ 2 ) + ( ( ( ( ๐ + ( ๐ / 2 ) ) mod ๐ ) โ ( ๐ / 2 ) ) โ 2 ) ) ) / ๐ ) |
43 |
|
simp3 |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) |
44 |
1 29 30 31 32 6 7 33 34 35 36 37 38 39 40 41 42 43
|
4sqlem17 |
โข ยฌ ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) |
45 |
44
|
pm2.21i |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ยฌ ๐ โ ( โคโฅ โ 2 ) ) |
46 |
45
|
3expia |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ( ๐ โ โค โง ๐ โ โค ) โง ( ๐ โ โค โง ๐ โ โค ) ) ) โ ( ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) โ ยฌ ๐ โ ( โคโฅ โ 2 ) ) ) |
47 |
46
|
anassrs |
โข ( ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ๐ โ โค โง ๐ โ โค ) ) โง ( ๐ โ โค โง ๐ โ โค ) ) โ ( ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) โ ยฌ ๐ โ ( โคโฅ โ 2 ) ) ) |
48 |
47
|
rexlimdvva |
โข ( ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โง ( ๐ โ โค โง ๐ โ โค ) ) โ ( โ ๐ โ โค โ ๐ โ โค ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) โ ยฌ ๐ โ ( โคโฅ โ 2 ) ) ) |
49 |
48
|
rexlimdvva |
โข ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โ ( โ ๐ โ โค โ ๐ โ โค โ ๐ โ โค โ ๐ โ โค ( ๐ ยท ๐ ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) + ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) โ ยฌ ๐ โ ( โคโฅ โ 2 ) ) ) |
50 |
27 49
|
mpd |
โข ( ( ๐ โง ๐ โ ( โคโฅ โ 2 ) ) โ ยฌ ๐ โ ( โคโฅ โ 2 ) ) |
51 |
50
|
pm2.01da |
โข ( ๐ โ ยฌ ๐ โ ( โคโฅ โ 2 ) ) |
52 |
23
|
simpld |
โข ( ๐ โ ๐ โ โ ) |
53 |
|
elnn1uz2 |
โข ( ๐ โ โ โ ( ๐ = 1 โจ ๐ โ ( โคโฅ โ 2 ) ) ) |
54 |
52 53
|
sylib |
โข ( ๐ โ ( ๐ = 1 โจ ๐ โ ( โคโฅ โ 2 ) ) ) |
55 |
54
|
ord |
โข ( ๐ โ ( ยฌ ๐ = 1 โ ๐ โ ( โคโฅ โ 2 ) ) ) |
56 |
51 55
|
mt3d |
โข ( ๐ โ ๐ = 1 ) |
57 |
56 19
|
eqeltrrd |
โข ( ๐ โ 1 โ ๐ ) |
58 |
|
oveq1 |
โข ( ๐ = 1 โ ( ๐ ยท ๐ ) = ( 1 ยท ๐ ) ) |
59 |
58
|
eleq1d |
โข ( ๐ = 1 โ ( ( ๐ ยท ๐ ) โ ๐ โ ( 1 ยท ๐ ) โ ๐ ) ) |
60 |
59 6
|
elrab2 |
โข ( 1 โ ๐ โ ( 1 โ โ โง ( 1 ยท ๐ ) โ ๐ ) ) |
61 |
60
|
simprbi |
โข ( 1 โ ๐ โ ( 1 ยท ๐ ) โ ๐ ) |
62 |
57 61
|
syl |
โข ( ๐ โ ( 1 ยท ๐ ) โ ๐ ) |
63 |
11 62
|
eqeltrrd |
โข ( ๐ โ ๐ โ ๐ ) |