Step | Hyp | Ref
| Expression |
1 | | 4sq.4 |
. . . . 5
โข (๐ โ ๐ โ โ) |
2 | | prmnn 16616 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ) |
3 | 1, 2 | syl 17 |
. . . 4
โข (๐ โ ๐ โ โ) |
4 | 3 | nncnd 12233 |
. . 3
โข (๐ โ ๐ โ โ) |
5 | 4 | mullidd 11237 |
. 2
โข (๐ โ (1 ยท ๐) = ๐) |
6 | | 4sq.7 |
. . . . . . . . . . . 12
โข ๐ = inf(๐, โ, < ) |
7 | | 4sq.6 |
. . . . . . . . . . . . . . 15
โข ๐ = {๐ โ โ โฃ (๐ ยท ๐) โ ๐} |
8 | 7 | ssrab3 4080 |
. . . . . . . . . . . . . 14
โข ๐ โ
โ |
9 | | nnuz 12870 |
. . . . . . . . . . . . . 14
โข โ =
(โคโฅโ1) |
10 | 8, 9 | sseqtri 4018 |
. . . . . . . . . . . . 13
โข ๐ โ
(โคโฅโ1) |
11 | | 4sq.1 |
. . . . . . . . . . . . . . 15
โข ๐ = {๐ โฃ โ๐ฅ โ โค โ๐ฆ โ โค โ๐ง โ โค โ๐ค โ โค ๐ = (((๐ฅโ2) + (๐ฆโ2)) + ((๐งโ2) + (๐คโ2)))} |
12 | | 4sq.2 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โ) |
13 | | 4sq.3 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ = ((2 ยท ๐) + 1)) |
14 | | 4sq.5 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...(2 ยท ๐)) โ ๐) |
15 | 11, 12, 13, 1, 14, 7, 6 | 4sqlem13 16895 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ โ โ
โง ๐ < ๐)) |
16 | 15 | simpld 494 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ
) |
17 | | infssuzcl 12921 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ1) โง ๐ โ โ
) โ inf(๐, โ, < ) โ ๐) |
18 | 10, 16, 17 | sylancr 586 |
. . . . . . . . . . . 12
โข (๐ โ inf(๐, โ, < ) โ ๐) |
19 | 6, 18 | eqeltrid 2836 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ ๐) |
20 | | oveq1 7419 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
21 | 20 | eleq1d 2817 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐ ยท ๐) โ ๐ โ (๐ ยท ๐) โ ๐)) |
22 | 21, 7 | elrab2 3686 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (๐ โ โ โง (๐ ยท ๐) โ ๐)) |
23 | 19, 22 | sylib 217 |
. . . . . . . . . 10
โข (๐ โ (๐ โ โ โง (๐ ยท ๐) โ ๐)) |
24 | 23 | simprd 495 |
. . . . . . . . 9
โข (๐ โ (๐ ยท ๐) โ ๐) |
25 | 11 | 4sqlem2 16887 |
. . . . . . . . 9
โข ((๐ ยท ๐) โ ๐ โ โ๐ โ โค โ๐ โ โค โ๐ โ โค โ๐ โ โค (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) |
26 | 24, 25 | sylib 217 |
. . . . . . . 8
โข (๐ โ โ๐ โ โค โ๐ โ โค โ๐ โ โค โ๐ โ โค (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) |
27 | 26 | adantr 480 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ2))
โ โ๐ โ
โค โ๐ โ
โค โ๐ โ
โค โ๐ โ
โค (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) |
28 | | simp1l 1196 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) โ ๐) |
29 | 28, 12 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) โ ๐ โ โ) |
30 | 28, 13 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) โ ๐ = ((2 ยท ๐) + 1)) |
31 | 28, 1 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) โ ๐ โ โ) |
32 | 28, 14 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) โ (0...(2 ยท ๐)) โ ๐) |
33 | | simp1r 1197 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) โ ๐ โ
(โคโฅโ2)) |
34 | | simp2ll 1239 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) โ ๐ โ โค) |
35 | | simp2lr 1240 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) โ ๐ โ โค) |
36 | | simp2rl 1241 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) โ ๐ โ โค) |
37 | | simp2rr 1242 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) โ ๐ โ โค) |
38 | | eqid 2731 |
. . . . . . . . . . . . 13
โข (((๐ + (๐ / 2)) mod ๐) โ (๐ / 2)) = (((๐ + (๐ / 2)) mod ๐) โ (๐ / 2)) |
39 | | eqid 2731 |
. . . . . . . . . . . . 13
โข (((๐ + (๐ / 2)) mod ๐) โ (๐ / 2)) = (((๐ + (๐ / 2)) mod ๐) โ (๐ / 2)) |
40 | | eqid 2731 |
. . . . . . . . . . . . 13
โข (((๐ + (๐ / 2)) mod ๐) โ (๐ / 2)) = (((๐ + (๐ / 2)) mod ๐) โ (๐ / 2)) |
41 | | eqid 2731 |
. . . . . . . . . . . . 13
โข (((๐ + (๐ / 2)) mod ๐) โ (๐ / 2)) = (((๐ + (๐ / 2)) mod ๐) โ (๐ / 2)) |
42 | | eqid 2731 |
. . . . . . . . . . . . 13
โข
(((((((๐ + (๐ / 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 1137 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) โ (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) |
44 | 11, 29, 30, 31, 32, 7, 6, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43 | 4sqlem17 16899 |
. . . . . . . . . . . 12
โข ยฌ
((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) |
45 | 44 | pm2.21i 119 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) โ ยฌ ๐ โ
(โคโฅโ2)) |
46 | 45 | 3expia 1120 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ2))
โง ((๐ โ โค
โง ๐ โ โค)
โง (๐ โ โค
โง ๐ โ โค)))
โ ((๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) โ ยฌ ๐ โ
(โคโฅโ2))) |
47 | 46 | anassrs 467 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ (โคโฅโ2))
โง (๐ โ โค
โง ๐ โ โค))
โง (๐ โ โค
โง ๐ โ โค))
โ ((๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) โ ยฌ ๐ โ
(โคโฅโ2))) |
48 | 47 | rexlimdvva 3210 |
. . . . . . . 8
โข (((๐ โง ๐ โ (โคโฅโ2))
โง (๐ โ โค
โง ๐ โ โค))
โ (โ๐ โ
โค โ๐ โ
โค (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) โ ยฌ ๐ โ
(โคโฅโ2))) |
49 | 48 | rexlimdvva 3210 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ2))
โ (โ๐ โ
โค โ๐ โ
โค โ๐ โ
โค โ๐ โ
โค (๐ ยท ๐) = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) โ ยฌ ๐ โ
(โคโฅโ2))) |
50 | 27, 49 | mpd 15 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ2))
โ ยฌ ๐ โ
(โคโฅโ2)) |
51 | 50 | pm2.01da 796 |
. . . . 5
โข (๐ โ ยฌ ๐ โ
(โคโฅโ2)) |
52 | 23 | simpld 494 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
53 | | elnn1uz2 12914 |
. . . . . . 7
โข (๐ โ โ โ (๐ = 1 โจ ๐ โ
(โคโฅโ2))) |
54 | 52, 53 | sylib 217 |
. . . . . 6
โข (๐ โ (๐ = 1 โจ ๐ โ
(โคโฅโ2))) |
55 | 54 | ord 861 |
. . . . 5
โข (๐ โ (ยฌ ๐ = 1 โ ๐ โ
(โคโฅโ2))) |
56 | 51, 55 | mt3d 148 |
. . . 4
โข (๐ โ ๐ = 1) |
57 | 56, 19 | eqeltrrd 2833 |
. . 3
โข (๐ โ 1 โ ๐) |
58 | | oveq1 7419 |
. . . . . 6
โข (๐ = 1 โ (๐ ยท ๐) = (1 ยท ๐)) |
59 | 58 | eleq1d 2817 |
. . . . 5
โข (๐ = 1 โ ((๐ ยท ๐) โ ๐ โ (1 ยท ๐) โ ๐)) |
60 | 59, 7 | elrab2 3686 |
. . . 4
โข (1 โ
๐ โ (1 โ โ
โง (1 ยท ๐) โ
๐)) |
61 | 60 | simprbi 496 |
. . 3
โข (1 โ
๐ โ (1 ยท ๐) โ ๐) |
62 | 57, 61 | syl 17 |
. 2
โข (๐ โ (1 ยท ๐) โ ๐) |
63 | 5, 62 | eqeltrrd 2833 |
1
โข (๐ โ ๐ โ ๐) |