Step | Hyp | Ref
| Expression |
1 | | 4sq.r |
. 2
โข ๐
= ((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) |
2 | | 4sq.6 |
. . . . . . . . 9
โข ๐ = {๐ โ โ โฃ (๐ ยท ๐) โ ๐} |
3 | 2 | ssrab3 4039 |
. . . . . . . 8
โข ๐ โ
โ |
4 | | 4sq.7 |
. . . . . . . . 9
โข ๐ = inf(๐, โ, < ) |
5 | | nnuz 12735 |
. . . . . . . . . . 11
โข โ =
(โคโฅโ1) |
6 | 3, 5 | sseqtri 3979 |
. . . . . . . . . 10
โข ๐ โ
(โคโฅโ1) |
7 | | 4sq.1 |
. . . . . . . . . . . 12
โข ๐ = {๐ โฃ โ๐ฅ โ โค โ๐ฆ โ โค โ๐ง โ โค โ๐ค โ โค ๐ = (((๐ฅโ2) + (๐ฆโ2)) + ((๐งโ2) + (๐คโ2)))} |
8 | | 4sq.2 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
9 | | 4sq.3 |
. . . . . . . . . . . 12
โข (๐ โ ๐ = ((2 ยท ๐) + 1)) |
10 | | 4sq.4 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
11 | | 4sq.5 |
. . . . . . . . . . . 12
โข (๐ โ (0...(2 ยท ๐)) โ ๐) |
12 | 7, 8, 9, 10, 11, 2, 4 | 4sqlem13 16764 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ โ
โง ๐ < ๐)) |
13 | 12 | simpld 496 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ
) |
14 | | infssuzcl 12786 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ1) โง ๐ โ โ
) โ inf(๐, โ, < ) โ ๐) |
15 | 6, 13, 14 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ inf(๐, โ, < ) โ ๐) |
16 | 4, 15 | eqeltrid 2843 |
. . . . . . . 8
โข (๐ โ ๐ โ ๐) |
17 | 3, 16 | sselid 3941 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
18 | 17 | nnzd 12539 |
. . . . . 6
โข (๐ โ ๐ โ โค) |
19 | | prmz 16486 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โค) |
20 | 10, 19 | syl 17 |
. . . . . . 7
โข (๐ โ ๐ โ โค) |
21 | 18, 20 | zmulcld 12546 |
. . . . . 6
โข (๐ โ (๐ ยท ๐) โ โค) |
22 | | 4sq.a |
. . . . . . . . . . . . 13
โข (๐ โ ๐ด โ โค) |
23 | | 4sq.e |
. . . . . . . . . . . . 13
โข ๐ธ = (((๐ด + (๐ / 2)) mod ๐) โ (๐ / 2)) |
24 | 22, 17, 23 | 4sqlem5 16749 |
. . . . . . . . . . . 12
โข (๐ โ (๐ธ โ โค โง ((๐ด โ ๐ธ) / ๐) โ โค)) |
25 | 24 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ ๐ธ โ โค) |
26 | | zsqcl2 13970 |
. . . . . . . . . . 11
โข (๐ธ โ โค โ (๐ธโ2) โ
โ0) |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ธโ2) โ
โ0) |
28 | | 4sq.b |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ โค) |
29 | | 4sq.f |
. . . . . . . . . . . . 13
โข ๐น = (((๐ต + (๐ / 2)) mod ๐) โ (๐ / 2)) |
30 | 28, 17, 29 | 4sqlem5 16749 |
. . . . . . . . . . . 12
โข (๐ โ (๐น โ โค โง ((๐ต โ ๐น) / ๐) โ โค)) |
31 | 30 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ ๐น โ โค) |
32 | | zsqcl2 13970 |
. . . . . . . . . . 11
โข (๐น โ โค โ (๐นโ2) โ
โ0) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐นโ2) โ
โ0) |
34 | 27, 33 | nn0addcld 12411 |
. . . . . . . . 9
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โ
โ0) |
35 | 34 | nn0zd 12538 |
. . . . . . . 8
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โ โค) |
36 | | 4sq.c |
. . . . . . . . . . . . 13
โข (๐ โ ๐ถ โ โค) |
37 | | 4sq.g |
. . . . . . . . . . . . 13
โข ๐บ = (((๐ถ + (๐ / 2)) mod ๐) โ (๐ / 2)) |
38 | 36, 17, 37 | 4sqlem5 16749 |
. . . . . . . . . . . 12
โข (๐ โ (๐บ โ โค โง ((๐ถ โ ๐บ) / ๐) โ โค)) |
39 | 38 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ ๐บ โ โค) |
40 | | zsqcl2 13970 |
. . . . . . . . . . 11
โข (๐บ โ โค โ (๐บโ2) โ
โ0) |
41 | 39, 40 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐บโ2) โ
โ0) |
42 | | 4sq.d |
. . . . . . . . . . . . 13
โข (๐ โ ๐ท โ โค) |
43 | | 4sq.h |
. . . . . . . . . . . . 13
โข ๐ป = (((๐ท + (๐ / 2)) mod ๐) โ (๐ / 2)) |
44 | 42, 17, 43 | 4sqlem5 16749 |
. . . . . . . . . . . 12
โข (๐ โ (๐ป โ โค โง ((๐ท โ ๐ป) / ๐) โ โค)) |
45 | 44 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ ๐ป โ โค) |
46 | | zsqcl2 13970 |
. . . . . . . . . . 11
โข (๐ป โ โค โ (๐ปโ2) โ
โ0) |
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ปโ2) โ
โ0) |
48 | 41, 47 | nn0addcld 12411 |
. . . . . . . . 9
โข (๐ โ ((๐บโ2) + (๐ปโ2)) โ
โ0) |
49 | 48 | nn0zd 12538 |
. . . . . . . 8
โข (๐ โ ((๐บโ2) + (๐ปโ2)) โ โค) |
50 | 35, 49 | zaddcld 12544 |
. . . . . . 7
โข (๐ โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) โ โค) |
51 | 21, 50 | zsubcld 12545 |
. . . . . 6
โข (๐ โ ((๐ ยท ๐) โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) โ โค) |
52 | | dvdsmul1 16095 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โฅ (๐ ยท ๐)) |
53 | 18, 20, 52 | syl2anc 585 |
. . . . . 6
โข (๐ โ ๐ โฅ (๐ ยท ๐)) |
54 | | zsqcl 13962 |
. . . . . . . . . . 11
โข (๐ด โ โค โ (๐ดโ2) โ
โค) |
55 | 22, 54 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ดโ2) โ โค) |
56 | | zsqcl 13962 |
. . . . . . . . . . 11
โข (๐ต โ โค โ (๐ตโ2) โ
โค) |
57 | 28, 56 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ตโ2) โ โค) |
58 | 55, 57 | zaddcld 12544 |
. . . . . . . . 9
โข (๐ โ ((๐ดโ2) + (๐ตโ2)) โ โค) |
59 | 58, 35 | zsubcld 12545 |
. . . . . . . 8
โข (๐ โ (((๐ดโ2) + (๐ตโ2)) โ ((๐ธโ2) + (๐นโ2))) โ โค) |
60 | | zsqcl 13962 |
. . . . . . . . . . 11
โข (๐ถ โ โค โ (๐ถโ2) โ
โค) |
61 | 36, 60 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ถโ2) โ โค) |
62 | | zsqcl 13962 |
. . . . . . . . . . 11
โข (๐ท โ โค โ (๐ทโ2) โ
โค) |
63 | 42, 62 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ทโ2) โ โค) |
64 | 61, 63 | zaddcld 12544 |
. . . . . . . . 9
โข (๐ โ ((๐ถโ2) + (๐ทโ2)) โ โค) |
65 | 64, 49 | zsubcld 12545 |
. . . . . . . 8
โข (๐ โ (((๐ถโ2) + (๐ทโ2)) โ ((๐บโ2) + (๐ปโ2))) โ โค) |
66 | 27 | nn0zd 12538 |
. . . . . . . . . . 11
โข (๐ โ (๐ธโ2) โ โค) |
67 | 55, 66 | zsubcld 12545 |
. . . . . . . . . 10
โข (๐ โ ((๐ดโ2) โ (๐ธโ2)) โ โค) |
68 | 33 | nn0zd 12538 |
. . . . . . . . . . 11
โข (๐ โ (๐นโ2) โ โค) |
69 | 57, 68 | zsubcld 12545 |
. . . . . . . . . 10
โข (๐ โ ((๐ตโ2) โ (๐นโ2)) โ โค) |
70 | 22, 17, 23 | 4sqlem8 16752 |
. . . . . . . . . 10
โข (๐ โ ๐ โฅ ((๐ดโ2) โ (๐ธโ2))) |
71 | 28, 17, 29 | 4sqlem8 16752 |
. . . . . . . . . 10
โข (๐ โ ๐ โฅ ((๐ตโ2) โ (๐นโ2))) |
72 | 18, 67, 69, 70, 71 | dvds2addd 16109 |
. . . . . . . . 9
โข (๐ โ ๐ โฅ (((๐ดโ2) โ (๐ธโ2)) + ((๐ตโ2) โ (๐นโ2)))) |
73 | 22 | zcnd 12541 |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ โ) |
74 | 73 | sqcld 13976 |
. . . . . . . . . 10
โข (๐ โ (๐ดโ2) โ โ) |
75 | 28 | zcnd 12541 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ โ) |
76 | 75 | sqcld 13976 |
. . . . . . . . . 10
โข (๐ โ (๐ตโ2) โ โ) |
77 | 25 | zcnd 12541 |
. . . . . . . . . . 11
โข (๐ โ ๐ธ โ โ) |
78 | 77 | sqcld 13976 |
. . . . . . . . . 10
โข (๐ โ (๐ธโ2) โ โ) |
79 | 31 | zcnd 12541 |
. . . . . . . . . . 11
โข (๐ โ ๐น โ โ) |
80 | 79 | sqcld 13976 |
. . . . . . . . . 10
โข (๐ โ (๐นโ2) โ โ) |
81 | 74, 76, 78, 80 | addsub4d 11493 |
. . . . . . . . 9
โข (๐ โ (((๐ดโ2) + (๐ตโ2)) โ ((๐ธโ2) + (๐นโ2))) = (((๐ดโ2) โ (๐ธโ2)) + ((๐ตโ2) โ (๐นโ2)))) |
82 | 72, 81 | breqtrrd 5132 |
. . . . . . . 8
โข (๐ โ ๐ โฅ (((๐ดโ2) + (๐ตโ2)) โ ((๐ธโ2) + (๐นโ2)))) |
83 | 41 | nn0zd 12538 |
. . . . . . . . . . 11
โข (๐ โ (๐บโ2) โ โค) |
84 | 61, 83 | zsubcld 12545 |
. . . . . . . . . 10
โข (๐ โ ((๐ถโ2) โ (๐บโ2)) โ โค) |
85 | 47 | nn0zd 12538 |
. . . . . . . . . . 11
โข (๐ โ (๐ปโ2) โ โค) |
86 | 63, 85 | zsubcld 12545 |
. . . . . . . . . 10
โข (๐ โ ((๐ทโ2) โ (๐ปโ2)) โ โค) |
87 | 36, 17, 37 | 4sqlem8 16752 |
. . . . . . . . . 10
โข (๐ โ ๐ โฅ ((๐ถโ2) โ (๐บโ2))) |
88 | 42, 17, 43 | 4sqlem8 16752 |
. . . . . . . . . 10
โข (๐ โ ๐ โฅ ((๐ทโ2) โ (๐ปโ2))) |
89 | 18, 84, 86, 87, 88 | dvds2addd 16109 |
. . . . . . . . 9
โข (๐ โ ๐ โฅ (((๐ถโ2) โ (๐บโ2)) + ((๐ทโ2) โ (๐ปโ2)))) |
90 | 36 | zcnd 12541 |
. . . . . . . . . . 11
โข (๐ โ ๐ถ โ โ) |
91 | 90 | sqcld 13976 |
. . . . . . . . . 10
โข (๐ โ (๐ถโ2) โ โ) |
92 | 42 | zcnd 12541 |
. . . . . . . . . . 11
โข (๐ โ ๐ท โ โ) |
93 | 92 | sqcld 13976 |
. . . . . . . . . 10
โข (๐ โ (๐ทโ2) โ โ) |
94 | 39 | zcnd 12541 |
. . . . . . . . . . 11
โข (๐ โ ๐บ โ โ) |
95 | 94 | sqcld 13976 |
. . . . . . . . . 10
โข (๐ โ (๐บโ2) โ โ) |
96 | 45 | zcnd 12541 |
. . . . . . . . . . 11
โข (๐ โ ๐ป โ โ) |
97 | 96 | sqcld 13976 |
. . . . . . . . . 10
โข (๐ โ (๐ปโ2) โ โ) |
98 | 91, 93, 95, 97 | addsub4d 11493 |
. . . . . . . . 9
โข (๐ โ (((๐ถโ2) + (๐ทโ2)) โ ((๐บโ2) + (๐ปโ2))) = (((๐ถโ2) โ (๐บโ2)) + ((๐ทโ2) โ (๐ปโ2)))) |
99 | 89, 98 | breqtrrd 5132 |
. . . . . . . 8
โข (๐ โ ๐ โฅ (((๐ถโ2) + (๐ทโ2)) โ ((๐บโ2) + (๐ปโ2)))) |
100 | 18, 59, 65, 82, 99 | dvds2addd 16109 |
. . . . . . 7
โข (๐ โ ๐ โฅ ((((๐ดโ2) + (๐ตโ2)) โ ((๐ธโ2) + (๐นโ2))) + (((๐ถโ2) + (๐ทโ2)) โ ((๐บโ2) + (๐ปโ2))))) |
101 | | 4sq.p |
. . . . . . . . 9
โข (๐ โ (๐ ยท ๐) = (((๐ดโ2) + (๐ตโ2)) + ((๐ถโ2) + (๐ทโ2)))) |
102 | 101 | oveq1d 7365 |
. . . . . . . 8
โข (๐ โ ((๐ ยท ๐) โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) = ((((๐ดโ2) + (๐ตโ2)) + ((๐ถโ2) + (๐ทโ2))) โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))))) |
103 | 74, 76 | addcld 11108 |
. . . . . . . . 9
โข (๐ โ ((๐ดโ2) + (๐ตโ2)) โ โ) |
104 | 91, 93 | addcld 11108 |
. . . . . . . . 9
โข (๐ โ ((๐ถโ2) + (๐ทโ2)) โ โ) |
105 | 78, 80 | addcld 11108 |
. . . . . . . . 9
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โ โ) |
106 | 95, 97 | addcld 11108 |
. . . . . . . . 9
โข (๐ โ ((๐บโ2) + (๐ปโ2)) โ โ) |
107 | 103, 104,
105, 106 | addsub4d 11493 |
. . . . . . . 8
โข (๐ โ ((((๐ดโ2) + (๐ตโ2)) + ((๐ถโ2) + (๐ทโ2))) โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) = ((((๐ดโ2) + (๐ตโ2)) โ ((๐ธโ2) + (๐นโ2))) + (((๐ถโ2) + (๐ทโ2)) โ ((๐บโ2) + (๐ปโ2))))) |
108 | 102, 107 | eqtrd 2778 |
. . . . . . 7
โข (๐ โ ((๐ ยท ๐) โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) = ((((๐ดโ2) + (๐ตโ2)) โ ((๐ธโ2) + (๐นโ2))) + (((๐ถโ2) + (๐ทโ2)) โ ((๐บโ2) + (๐ปโ2))))) |
109 | 100, 108 | breqtrrd 5132 |
. . . . . 6
โข (๐ โ ๐ โฅ ((๐ ยท ๐) โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))))) |
110 | 18, 21, 51, 53, 109 | dvds2subd 16110 |
. . . . 5
โข (๐ โ ๐ โฅ ((๐ ยท ๐) โ ((๐ ยท ๐) โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))))) |
111 | 17 | nncnd 12103 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
112 | | prmnn 16485 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
113 | 10, 112 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
114 | 113 | nncnd 12103 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
115 | 111, 114 | mulcld 11109 |
. . . . . 6
โข (๐ โ (๐ ยท ๐) โ โ) |
116 | 105, 106 | addcld 11108 |
. . . . . 6
โข (๐ โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) โ โ) |
117 | 115, 116 | nncand 11451 |
. . . . 5
โข (๐ โ ((๐ ยท ๐) โ ((๐ ยท ๐) โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))))) = (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) |
118 | 110, 117 | breqtrd 5130 |
. . . 4
โข (๐ โ ๐ โฅ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) |
119 | 17 | nnne0d 12137 |
. . . . 5
โข (๐ โ ๐ โ 0) |
120 | 34, 48 | nn0addcld 12411 |
. . . . . 6
โข (๐ โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) โ
โ0) |
121 | 120 | nn0zd 12538 |
. . . . 5
โข (๐ โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) โ โค) |
122 | | dvdsval2 16074 |
. . . . 5
โข ((๐ โ โค โง ๐ โ 0 โง (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) โ โค) โ (๐ โฅ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) โ ((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) โ โค)) |
123 | 18, 119, 121, 122 | syl3anc 1372 |
. . . 4
โข (๐ โ (๐ โฅ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) โ ((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) โ โค)) |
124 | 118, 123 | mpbid 231 |
. . 3
โข (๐ โ ((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) โ โค) |
125 | 120 | nn0red 12408 |
. . . 4
โข (๐ โ (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) โ โ) |
126 | 120 | nn0ge0d 12410 |
. . . 4
โข (๐ โ 0 โค (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) |
127 | 17 | nnred 12102 |
. . . 4
โข (๐ โ ๐ โ โ) |
128 | 17 | nngt0d 12136 |
. . . 4
โข (๐ โ 0 < ๐) |
129 | | divge0 11958 |
. . . 4
โข
((((((๐ธโ2) +
(๐นโ2)) + ((๐บโ2) + (๐ปโ2))) โ โ โง 0 โค
(((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) โง (๐ โ โ โง 0 < ๐)) โ 0 โค ((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐)) |
130 | 125, 126,
127, 128, 129 | syl22anc 838 |
. . 3
โข (๐ โ 0 โค ((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐)) |
131 | | elnn0z 12446 |
. . 3
โข
(((((๐ธโ2) +
(๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) โ โ0 โ
(((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) โ โค โง 0 โค ((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐))) |
132 | 124, 130,
131 | sylanbrc 584 |
. 2
โข (๐ โ ((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) โ
โ0) |
133 | 1, 132 | eqeltrid 2843 |
1
โข (๐ โ ๐
โ
โ0) |