Step | Hyp | Ref
| Expression |
1 | | 4sqlem5.3 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
2 | 1 | adantr 482 |
. . . . 5
โข ((๐ โง ๐) โ ๐ โ โ) |
3 | 2 | nnzd 12527 |
. . . 4
โข ((๐ โง ๐) โ ๐ โ โค) |
4 | | zsqcl 14035 |
. . . 4
โข (๐ โ โค โ (๐โ2) โ
โค) |
5 | 3, 4 | syl 17 |
. . 3
โข ((๐ โง ๐) โ (๐โ2) โ โค) |
6 | | 4sqlem5.2 |
. . . . . 6
โข (๐ โ ๐ด โ โค) |
7 | 6 | adantr 482 |
. . . . 5
โข ((๐ โง ๐) โ ๐ด โ โค) |
8 | 2 | nnred 12169 |
. . . . . . . . 9
โข ((๐ โง ๐) โ ๐ โ โ) |
9 | 8 | rehalfcld 12401 |
. . . . . . . 8
โข ((๐ โง ๐) โ (๐ / 2) โ โ) |
10 | 9 | recnd 11184 |
. . . . . . 7
โข ((๐ โง ๐) โ (๐ / 2) โ โ) |
11 | 10 | negnegd 11504 |
. . . . . 6
โข ((๐ โง ๐) โ --(๐ / 2) = (๐ / 2)) |
12 | | 4sqlem5.4 |
. . . . . . . . . . . . . . 15
โข ๐ต = (((๐ด + (๐ / 2)) mod ๐) โ (๐ / 2)) |
13 | 6, 1, 12 | 4sqlem5 16815 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ต โ โค โง ((๐ด โ ๐ต) / ๐) โ โค)) |
14 | 13 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐) โ (๐ต โ โค โง ((๐ด โ ๐ต) / ๐) โ โค)) |
15 | 14 | simpld 496 |
. . . . . . . . . . . 12
โข ((๐ โง ๐) โ ๐ต โ โค) |
16 | 15 | zred 12608 |
. . . . . . . . . . 11
โข ((๐ โง ๐) โ ๐ต โ โ) |
17 | 6, 1, 12 | 4sqlem6 16816 |
. . . . . . . . . . . . 13
โข (๐ โ (-(๐ / 2) โค ๐ต โง ๐ต < (๐ / 2))) |
18 | 17 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐) โ (-(๐ / 2) โค ๐ต โง ๐ต < (๐ / 2))) |
19 | 18 | simprd 497 |
. . . . . . . . . . 11
โข ((๐ โง ๐) โ ๐ต < (๐ / 2)) |
20 | 16, 19 | ltned 11292 |
. . . . . . . . . 10
โข ((๐ โง ๐) โ ๐ต โ (๐ / 2)) |
21 | 20 | neneqd 2949 |
. . . . . . . . 9
โข ((๐ โง ๐) โ ยฌ ๐ต = (๐ / 2)) |
22 | | 2cnd 12232 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐) โ 2 โ โ) |
23 | 22 | sqvald 14049 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐) โ (2โ2) = (2 ยท
2)) |
24 | 23 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐) โ ((๐โ2) / (2โ2)) = ((๐โ2) / (2 ยท 2))) |
25 | 2 | nncnd 12170 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐) โ ๐ โ โ) |
26 | | 2ne0 12258 |
. . . . . . . . . . . . . . 15
โข 2 โ
0 |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐) โ 2 โ 0) |
28 | 25, 22, 27 | sqdivd 14065 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐) โ ((๐ / 2)โ2) = ((๐โ2) / (2โ2))) |
29 | 25 | sqcld 14050 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐) โ (๐โ2) โ โ) |
30 | 29, 22, 22, 27, 27 | divdiv1d 11963 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐) โ (((๐โ2) / 2) / 2) = ((๐โ2) / (2 ยท 2))) |
31 | 24, 28, 30 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
โข ((๐ โง ๐) โ ((๐ / 2)โ2) = (((๐โ2) / 2) / 2)) |
32 | 29 | halfcld 12399 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐) โ ((๐โ2) / 2) โ
โ) |
33 | 32 | halfcld 12399 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐) โ (((๐โ2) / 2) / 2) โ
โ) |
34 | 15 | zcnd 12609 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐) โ ๐ต โ โ) |
35 | 34 | sqcld 14050 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐) โ (๐ตโ2) โ โ) |
36 | | 4sqlem10.5 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐) โ ((((๐โ2) / 2) / 2) โ (๐ตโ2)) = 0) |
37 | 33, 35, 36 | subeq0d 11521 |
. . . . . . . . . . . 12
โข ((๐ โง ๐) โ (((๐โ2) / 2) / 2) = (๐ตโ2)) |
38 | 31, 37 | eqtr2d 2778 |
. . . . . . . . . . 11
โข ((๐ โง ๐) โ (๐ตโ2) = ((๐ / 2)โ2)) |
39 | | sqeqor 14121 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง (๐ / 2) โ โ) โ
((๐ตโ2) = ((๐ / 2)โ2) โ (๐ต = (๐ / 2) โจ ๐ต = -(๐ / 2)))) |
40 | 34, 10, 39 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โง ๐) โ ((๐ตโ2) = ((๐ / 2)โ2) โ (๐ต = (๐ / 2) โจ ๐ต = -(๐ / 2)))) |
41 | 38, 40 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง ๐) โ (๐ต = (๐ / 2) โจ ๐ต = -(๐ / 2))) |
42 | 41 | ord 863 |
. . . . . . . . 9
โข ((๐ โง ๐) โ (ยฌ ๐ต = (๐ / 2) โ ๐ต = -(๐ / 2))) |
43 | 21, 42 | mpd 15 |
. . . . . . . 8
โข ((๐ โง ๐) โ ๐ต = -(๐ / 2)) |
44 | 43, 15 | eqeltrrd 2839 |
. . . . . . 7
โข ((๐ โง ๐) โ -(๐ / 2) โ โค) |
45 | 44 | znegcld 12610 |
. . . . . 6
โข ((๐ โง ๐) โ --(๐ / 2) โ โค) |
46 | 11, 45 | eqeltrrd 2839 |
. . . . 5
โข ((๐ โง ๐) โ (๐ / 2) โ โค) |
47 | 7, 46 | zaddcld 12612 |
. . . 4
โข ((๐ โง ๐) โ (๐ด + (๐ / 2)) โ โค) |
48 | | zsqcl 14035 |
. . . 4
โข ((๐ด + (๐ / 2)) โ โค โ ((๐ด + (๐ / 2))โ2) โ
โค) |
49 | 47, 48 | syl 17 |
. . 3
โข ((๐ โง ๐) โ ((๐ด + (๐ / 2))โ2) โ
โค) |
50 | 47, 3 | zmulcld 12614 |
. . 3
โข ((๐ โง ๐) โ ((๐ด + (๐ / 2)) ยท ๐) โ โค) |
51 | 47 | zred 12608 |
. . . . . . . 8
โข ((๐ โง ๐) โ (๐ด + (๐ / 2)) โ โ) |
52 | 2 | nnrpd 12956 |
. . . . . . . 8
โข ((๐ โง ๐) โ ๐ โ
โ+) |
53 | 51, 52 | modcld 13781 |
. . . . . . 7
โข ((๐ โง ๐) โ ((๐ด + (๐ / 2)) mod ๐) โ โ) |
54 | 53 | recnd 11184 |
. . . . . 6
โข ((๐ โง ๐) โ ((๐ด + (๐ / 2)) mod ๐) โ โ) |
55 | | 0cnd 11149 |
. . . . . 6
โข ((๐ โง ๐) โ 0 โ โ) |
56 | | df-neg 11389 |
. . . . . . 7
โข -(๐ / 2) = (0 โ (๐ / 2)) |
57 | 43, 12, 56 | 3eqtr3g 2800 |
. . . . . 6
โข ((๐ โง ๐) โ (((๐ด + (๐ / 2)) mod ๐) โ (๐ / 2)) = (0 โ (๐ / 2))) |
58 | 54, 55, 10, 57 | subcan2d 11555 |
. . . . 5
โข ((๐ โง ๐) โ ((๐ด + (๐ / 2)) mod ๐) = 0) |
59 | | dvdsval3 16141 |
. . . . . 6
โข ((๐ โ โ โง (๐ด + (๐ / 2)) โ โค) โ (๐ โฅ (๐ด + (๐ / 2)) โ ((๐ด + (๐ / 2)) mod ๐) = 0)) |
60 | 2, 47, 59 | syl2anc 585 |
. . . . 5
โข ((๐ โง ๐) โ (๐ โฅ (๐ด + (๐ / 2)) โ ((๐ด + (๐ / 2)) mod ๐) = 0)) |
61 | 58, 60 | mpbird 257 |
. . . 4
โข ((๐ โง ๐) โ ๐ โฅ (๐ด + (๐ / 2))) |
62 | | dvdssq 16444 |
. . . . 5
โข ((๐ โ โค โง (๐ด + (๐ / 2)) โ โค) โ (๐ โฅ (๐ด + (๐ / 2)) โ (๐โ2) โฅ ((๐ด + (๐ / 2))โ2))) |
63 | 3, 47, 62 | syl2anc 585 |
. . . 4
โข ((๐ โง ๐) โ (๐ โฅ (๐ด + (๐ / 2)) โ (๐โ2) โฅ ((๐ด + (๐ / 2))โ2))) |
64 | 61, 63 | mpbid 231 |
. . 3
โข ((๐ โง ๐) โ (๐โ2) โฅ ((๐ด + (๐ / 2))โ2)) |
65 | 25 | sqvald 14049 |
. . . 4
โข ((๐ โง ๐) โ (๐โ2) = (๐ ยท ๐)) |
66 | 2 | nnne0d 12204 |
. . . . . 6
โข ((๐ โง ๐) โ ๐ โ 0) |
67 | | dvdsmulcr 16169 |
. . . . . 6
โข ((๐ โ โค โง (๐ด + (๐ / 2)) โ โค โง (๐ โ โค โง ๐ โ 0)) โ ((๐ ยท ๐) โฅ ((๐ด + (๐ / 2)) ยท ๐) โ ๐ โฅ (๐ด + (๐ / 2)))) |
68 | 3, 47, 3, 66, 67 | syl112anc 1375 |
. . . . 5
โข ((๐ โง ๐) โ ((๐ ยท ๐) โฅ ((๐ด + (๐ / 2)) ยท ๐) โ ๐ โฅ (๐ด + (๐ / 2)))) |
69 | 61, 68 | mpbird 257 |
. . . 4
โข ((๐ โง ๐) โ (๐ ยท ๐) โฅ ((๐ด + (๐ / 2)) ยท ๐)) |
70 | 65, 69 | eqbrtrd 5128 |
. . 3
โข ((๐ โง ๐) โ (๐โ2) โฅ ((๐ด + (๐ / 2)) ยท ๐)) |
71 | 5, 49, 50, 64, 70 | dvds2subd 16176 |
. 2
โข ((๐ โง ๐) โ (๐โ2) โฅ (((๐ด + (๐ / 2))โ2) โ ((๐ด + (๐ / 2)) ยท ๐))) |
72 | 47 | zcnd 12609 |
. . . . 5
โข ((๐ โง ๐) โ (๐ด + (๐ / 2)) โ โ) |
73 | 72 | sqvald 14049 |
. . . 4
โข ((๐ โง ๐) โ ((๐ด + (๐ / 2))โ2) = ((๐ด + (๐ / 2)) ยท (๐ด + (๐ / 2)))) |
74 | 73 | oveq1d 7373 |
. . 3
โข ((๐ โง ๐) โ (((๐ด + (๐ / 2))โ2) โ ((๐ด + (๐ / 2)) ยท ๐)) = (((๐ด + (๐ / 2)) ยท (๐ด + (๐ / 2))) โ ((๐ด + (๐ / 2)) ยท ๐))) |
75 | 72, 72, 25 | subdid 11612 |
. . 3
โข ((๐ โง ๐) โ ((๐ด + (๐ / 2)) ยท ((๐ด + (๐ / 2)) โ ๐)) = (((๐ด + (๐ / 2)) ยท (๐ด + (๐ / 2))) โ ((๐ด + (๐ / 2)) ยท ๐))) |
76 | 25 | 2halvesd 12400 |
. . . . . . 7
โข ((๐ โง ๐) โ ((๐ / 2) + (๐ / 2)) = ๐) |
77 | 76 | oveq2d 7374 |
. . . . . 6
โข ((๐ โง ๐) โ ((๐ด + (๐ / 2)) โ ((๐ / 2) + (๐ / 2))) = ((๐ด + (๐ / 2)) โ ๐)) |
78 | 7 | zcnd 12609 |
. . . . . . 7
โข ((๐ โง ๐) โ ๐ด โ โ) |
79 | 78, 10, 10 | pnpcan2d 11551 |
. . . . . 6
โข ((๐ โง ๐) โ ((๐ด + (๐ / 2)) โ ((๐ / 2) + (๐ / 2))) = (๐ด โ (๐ / 2))) |
80 | 77, 79 | eqtr3d 2779 |
. . . . 5
โข ((๐ โง ๐) โ ((๐ด + (๐ / 2)) โ ๐) = (๐ด โ (๐ / 2))) |
81 | 80 | oveq2d 7374 |
. . . 4
โข ((๐ โง ๐) โ ((๐ด + (๐ / 2)) ยท ((๐ด + (๐ / 2)) โ ๐)) = ((๐ด + (๐ / 2)) ยท (๐ด โ (๐ / 2)))) |
82 | | subsq 14115 |
. . . . 5
โข ((๐ด โ โ โง (๐ / 2) โ โ) โ
((๐ดโ2) โ ((๐ / 2)โ2)) = ((๐ด + (๐ / 2)) ยท (๐ด โ (๐ / 2)))) |
83 | 78, 10, 82 | syl2anc 585 |
. . . 4
โข ((๐ โง ๐) โ ((๐ดโ2) โ ((๐ / 2)โ2)) = ((๐ด + (๐ / 2)) ยท (๐ด โ (๐ / 2)))) |
84 | 31 | oveq2d 7374 |
. . . 4
โข ((๐ โง ๐) โ ((๐ดโ2) โ ((๐ / 2)โ2)) = ((๐ดโ2) โ (((๐โ2) / 2) / 2))) |
85 | 81, 83, 84 | 3eqtr2d 2783 |
. . 3
โข ((๐ โง ๐) โ ((๐ด + (๐ / 2)) ยท ((๐ด + (๐ / 2)) โ ๐)) = ((๐ดโ2) โ (((๐โ2) / 2) / 2))) |
86 | 74, 75, 85 | 3eqtr2d 2783 |
. 2
โข ((๐ โง ๐) โ (((๐ด + (๐ / 2))โ2) โ ((๐ด + (๐ / 2)) ยท ๐)) = ((๐ดโ2) โ (((๐โ2) / 2) / 2))) |
87 | 71, 86 | breqtrd 5132 |
1
โข ((๐ โง ๐) โ (๐โ2) โฅ ((๐ดโ2) โ (((๐โ2) / 2) / 2))) |