Step | Hyp | Ref
| Expression |
1 | | 2sq.1 |
. 2
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) |
2 | | 2sqlem8.m |
. . . 4
โข (๐ โ ๐ โ
(โคโฅโ2)) |
3 | | eluz2b3 12776 |
. . . 4
โข (๐ โ
(โคโฅโ2) โ (๐ โ โ โง ๐ โ 1)) |
4 | 2, 3 | sylib 217 |
. . 3
โข (๐ โ (๐ โ โ โง ๐ โ 1)) |
5 | 4 | simpld 496 |
. 2
โข (๐ โ ๐ โ โ) |
6 | | 2sqlem9.7 |
. . . . . . 7
โข (๐ โ ๐ โฅ ๐) |
7 | | eluzelz 12706 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ2) โ ๐ โ โค) |
8 | 2, 7 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
9 | | 2sqlem8.n |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
10 | 9 | nnzd 12539 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
11 | | 2sqlem8.1 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โค) |
12 | | 2sqlem8.c |
. . . . . . . . . . . 12
โข ๐ถ = (((๐ด + (๐ / 2)) mod ๐) โ (๐ / 2)) |
13 | 11, 5, 12 | 4sqlem5 16749 |
. . . . . . . . . . 11
โข (๐ โ (๐ถ โ โค โง ((๐ด โ ๐ถ) / ๐) โ โค)) |
14 | 13 | simpld 496 |
. . . . . . . . . 10
โข (๐ โ ๐ถ โ โค) |
15 | | zsqcl 13962 |
. . . . . . . . . 10
โข (๐ถ โ โค โ (๐ถโ2) โ
โค) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ถโ2) โ โค) |
17 | | 2sqlem8.2 |
. . . . . . . . . . . 12
โข (๐ โ ๐ต โ โค) |
18 | | 2sqlem8.d |
. . . . . . . . . . . 12
โข ๐ท = (((๐ต + (๐ / 2)) mod ๐) โ (๐ / 2)) |
19 | 17, 5, 18 | 4sqlem5 16749 |
. . . . . . . . . . 11
โข (๐ โ (๐ท โ โค โง ((๐ต โ ๐ท) / ๐) โ โค)) |
20 | 19 | simpld 496 |
. . . . . . . . . 10
โข (๐ โ ๐ท โ โค) |
21 | | zsqcl 13962 |
. . . . . . . . . 10
โข (๐ท โ โค โ (๐ทโ2) โ
โค) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ทโ2) โ โค) |
23 | 16, 22 | zaddcld 12544 |
. . . . . . . 8
โข (๐ โ ((๐ถโ2) + (๐ทโ2)) โ โค) |
24 | | zsqcl 13962 |
. . . . . . . . . . . 12
โข (๐ด โ โค โ (๐ดโ2) โ
โค) |
25 | 11, 24 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (๐ดโ2) โ โค) |
26 | 25, 16 | zsubcld 12545 |
. . . . . . . . . 10
โข (๐ โ ((๐ดโ2) โ (๐ถโ2)) โ โค) |
27 | | zsqcl 13962 |
. . . . . . . . . . . 12
โข (๐ต โ โค โ (๐ตโ2) โ
โค) |
28 | 17, 27 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (๐ตโ2) โ โค) |
29 | 28, 22 | zsubcld 12545 |
. . . . . . . . . 10
โข (๐ โ ((๐ตโ2) โ (๐ทโ2)) โ โค) |
30 | 11, 5, 12 | 4sqlem8 16752 |
. . . . . . . . . 10
โข (๐ โ ๐ โฅ ((๐ดโ2) โ (๐ถโ2))) |
31 | 17, 5, 18 | 4sqlem8 16752 |
. . . . . . . . . 10
โข (๐ โ ๐ โฅ ((๐ตโ2) โ (๐ทโ2))) |
32 | 8, 26, 29, 30, 31 | dvds2addd 16109 |
. . . . . . . . 9
โข (๐ โ ๐ โฅ (((๐ดโ2) โ (๐ถโ2)) + ((๐ตโ2) โ (๐ทโ2)))) |
33 | | 2sqlem8.4 |
. . . . . . . . . . 11
โข (๐ โ ๐ = ((๐ดโ2) + (๐ตโ2))) |
34 | 33 | oveq1d 7365 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ((๐ถโ2) + (๐ทโ2))) = (((๐ดโ2) + (๐ตโ2)) โ ((๐ถโ2) + (๐ทโ2)))) |
35 | 25 | zcnd 12541 |
. . . . . . . . . . 11
โข (๐ โ (๐ดโ2) โ โ) |
36 | 28 | zcnd 12541 |
. . . . . . . . . . 11
โข (๐ โ (๐ตโ2) โ โ) |
37 | 16 | zcnd 12541 |
. . . . . . . . . . 11
โข (๐ โ (๐ถโ2) โ โ) |
38 | 22 | zcnd 12541 |
. . . . . . . . . . 11
โข (๐ โ (๐ทโ2) โ โ) |
39 | 35, 36, 37, 38 | addsub4d 11493 |
. . . . . . . . . 10
โข (๐ โ (((๐ดโ2) + (๐ตโ2)) โ ((๐ถโ2) + (๐ทโ2))) = (((๐ดโ2) โ (๐ถโ2)) + ((๐ตโ2) โ (๐ทโ2)))) |
40 | 34, 39 | eqtrd 2778 |
. . . . . . . . 9
โข (๐ โ (๐ โ ((๐ถโ2) + (๐ทโ2))) = (((๐ดโ2) โ (๐ถโ2)) + ((๐ตโ2) โ (๐ทโ2)))) |
41 | 32, 40 | breqtrrd 5132 |
. . . . . . . 8
โข (๐ โ ๐ โฅ (๐ โ ((๐ถโ2) + (๐ทโ2)))) |
42 | | dvdssub2 16118 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โค โง ((๐ถโ2) + (๐ทโ2)) โ โค) โง ๐ โฅ (๐ โ ((๐ถโ2) + (๐ทโ2)))) โ (๐ โฅ ๐ โ ๐ โฅ ((๐ถโ2) + (๐ทโ2)))) |
43 | 8, 10, 23, 41, 42 | syl31anc 1374 |
. . . . . . 7
โข (๐ โ (๐ โฅ ๐ โ ๐ โฅ ((๐ถโ2) + (๐ทโ2)))) |
44 | 6, 43 | mpbid 231 |
. . . . . 6
โข (๐ โ ๐ โฅ ((๐ถโ2) + (๐ทโ2))) |
45 | | 2sqlem7.2 |
. . . . . . . . . . . 12
โข ๐ = {๐ง โฃ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ๐ง = ((๐ฅโ2) + (๐ฆโ2)))} |
46 | | 2sqlem9.5 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ โ (1...(๐ โ 1))โ๐ โ ๐ (๐ โฅ ๐ โ ๐ โ ๐)) |
47 | | 2sqlem8.3 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด gcd ๐ต) = 1) |
48 | 1, 45, 46, 6, 9, 2,
11, 17, 47, 33, 12, 18 | 2sqlem8a 26695 |
. . . . . . . . . . 11
โข (๐ โ (๐ถ gcd ๐ท) โ โ) |
49 | 48 | nnzd 12539 |
. . . . . . . . . 10
โข (๐ โ (๐ถ gcd ๐ท) โ โค) |
50 | | zsqcl2 13970 |
. . . . . . . . . 10
โข ((๐ถ gcd ๐ท) โ โค โ ((๐ถ gcd ๐ท)โ2) โ
โ0) |
51 | 49, 50 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((๐ถ gcd ๐ท)โ2) โ
โ0) |
52 | 51 | nn0cnd 12409 |
. . . . . . . 8
โข (๐ โ ((๐ถ gcd ๐ท)โ2) โ โ) |
53 | | 2sqlem8.e |
. . . . . . . . . . 11
โข ๐ธ = (๐ถ / (๐ถ gcd ๐ท)) |
54 | | gcddvds 16318 |
. . . . . . . . . . . . . 14
โข ((๐ถ โ โค โง ๐ท โ โค) โ ((๐ถ gcd ๐ท) โฅ ๐ถ โง (๐ถ gcd ๐ท) โฅ ๐ท)) |
55 | 14, 20, 54 | syl2anc 585 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ถ gcd ๐ท) โฅ ๐ถ โง (๐ถ gcd ๐ท) โฅ ๐ท)) |
56 | 55 | simpld 496 |
. . . . . . . . . . . 12
โข (๐ โ (๐ถ gcd ๐ท) โฅ ๐ถ) |
57 | 48 | nnne0d 12137 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ถ gcd ๐ท) โ 0) |
58 | | dvdsval2 16074 |
. . . . . . . . . . . . 13
โข (((๐ถ gcd ๐ท) โ โค โง (๐ถ gcd ๐ท) โ 0 โง ๐ถ โ โค) โ ((๐ถ gcd ๐ท) โฅ ๐ถ โ (๐ถ / (๐ถ gcd ๐ท)) โ โค)) |
59 | 49, 57, 14, 58 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ถ gcd ๐ท) โฅ ๐ถ โ (๐ถ / (๐ถ gcd ๐ท)) โ โค)) |
60 | 56, 59 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ (๐ถ / (๐ถ gcd ๐ท)) โ โค) |
61 | 53, 60 | eqeltrid 2843 |
. . . . . . . . . 10
โข (๐ โ ๐ธ โ โค) |
62 | | zsqcl2 13970 |
. . . . . . . . . 10
โข (๐ธ โ โค โ (๐ธโ2) โ
โ0) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ธโ2) โ
โ0) |
64 | 63 | nn0cnd 12409 |
. . . . . . . 8
โข (๐ โ (๐ธโ2) โ โ) |
65 | | 2sqlem8.f |
. . . . . . . . . . 11
โข ๐น = (๐ท / (๐ถ gcd ๐ท)) |
66 | 55 | simprd 497 |
. . . . . . . . . . . 12
โข (๐ โ (๐ถ gcd ๐ท) โฅ ๐ท) |
67 | | dvdsval2 16074 |
. . . . . . . . . . . . 13
โข (((๐ถ gcd ๐ท) โ โค โง (๐ถ gcd ๐ท) โ 0 โง ๐ท โ โค) โ ((๐ถ gcd ๐ท) โฅ ๐ท โ (๐ท / (๐ถ gcd ๐ท)) โ โค)) |
68 | 49, 57, 20, 67 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ถ gcd ๐ท) โฅ ๐ท โ (๐ท / (๐ถ gcd ๐ท)) โ โค)) |
69 | 66, 68 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ (๐ท / (๐ถ gcd ๐ท)) โ โค) |
70 | 65, 69 | eqeltrid 2843 |
. . . . . . . . . 10
โข (๐ โ ๐น โ โค) |
71 | | zsqcl2 13970 |
. . . . . . . . . 10
โข (๐น โ โค โ (๐นโ2) โ
โ0) |
72 | 70, 71 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐นโ2) โ
โ0) |
73 | 72 | nn0cnd 12409 |
. . . . . . . 8
โข (๐ โ (๐นโ2) โ โ) |
74 | 52, 64, 73 | adddid 11113 |
. . . . . . 7
โข (๐ โ (((๐ถ gcd ๐ท)โ2) ยท ((๐ธโ2) + (๐นโ2))) = ((((๐ถ gcd ๐ท)โ2) ยท (๐ธโ2)) + (((๐ถ gcd ๐ท)โ2) ยท (๐นโ2)))) |
75 | 49 | zcnd 12541 |
. . . . . . . . . 10
โข (๐ โ (๐ถ gcd ๐ท) โ โ) |
76 | 61 | zcnd 12541 |
. . . . . . . . . 10
โข (๐ โ ๐ธ โ โ) |
77 | 75, 76 | sqmuld 13990 |
. . . . . . . . 9
โข (๐ โ (((๐ถ gcd ๐ท) ยท ๐ธ)โ2) = (((๐ถ gcd ๐ท)โ2) ยท (๐ธโ2))) |
78 | 53 | oveq2i 7361 |
. . . . . . . . . . 11
โข ((๐ถ gcd ๐ท) ยท ๐ธ) = ((๐ถ gcd ๐ท) ยท (๐ถ / (๐ถ gcd ๐ท))) |
79 | 14 | zcnd 12541 |
. . . . . . . . . . . 12
โข (๐ โ ๐ถ โ โ) |
80 | 79, 75, 57 | divcan2d 11867 |
. . . . . . . . . . 11
โข (๐ โ ((๐ถ gcd ๐ท) ยท (๐ถ / (๐ถ gcd ๐ท))) = ๐ถ) |
81 | 78, 80 | eqtrid 2790 |
. . . . . . . . . 10
โข (๐ โ ((๐ถ gcd ๐ท) ยท ๐ธ) = ๐ถ) |
82 | 81 | oveq1d 7365 |
. . . . . . . . 9
โข (๐ โ (((๐ถ gcd ๐ท) ยท ๐ธ)โ2) = (๐ถโ2)) |
83 | 77, 82 | eqtr3d 2780 |
. . . . . . . 8
โข (๐ โ (((๐ถ gcd ๐ท)โ2) ยท (๐ธโ2)) = (๐ถโ2)) |
84 | 70 | zcnd 12541 |
. . . . . . . . . 10
โข (๐ โ ๐น โ โ) |
85 | 75, 84 | sqmuld 13990 |
. . . . . . . . 9
โข (๐ โ (((๐ถ gcd ๐ท) ยท ๐น)โ2) = (((๐ถ gcd ๐ท)โ2) ยท (๐นโ2))) |
86 | 65 | oveq2i 7361 |
. . . . . . . . . . 11
โข ((๐ถ gcd ๐ท) ยท ๐น) = ((๐ถ gcd ๐ท) ยท (๐ท / (๐ถ gcd ๐ท))) |
87 | 20 | zcnd 12541 |
. . . . . . . . . . . 12
โข (๐ โ ๐ท โ โ) |
88 | 87, 75, 57 | divcan2d 11867 |
. . . . . . . . . . 11
โข (๐ โ ((๐ถ gcd ๐ท) ยท (๐ท / (๐ถ gcd ๐ท))) = ๐ท) |
89 | 86, 88 | eqtrid 2790 |
. . . . . . . . . 10
โข (๐ โ ((๐ถ gcd ๐ท) ยท ๐น) = ๐ท) |
90 | 89 | oveq1d 7365 |
. . . . . . . . 9
โข (๐ โ (((๐ถ gcd ๐ท) ยท ๐น)โ2) = (๐ทโ2)) |
91 | 85, 90 | eqtr3d 2780 |
. . . . . . . 8
โข (๐ โ (((๐ถ gcd ๐ท)โ2) ยท (๐นโ2)) = (๐ทโ2)) |
92 | 83, 91 | oveq12d 7368 |
. . . . . . 7
โข (๐ โ ((((๐ถ gcd ๐ท)โ2) ยท (๐ธโ2)) + (((๐ถ gcd ๐ท)โ2) ยท (๐นโ2))) = ((๐ถโ2) + (๐ทโ2))) |
93 | 74, 92 | eqtrd 2778 |
. . . . . 6
โข (๐ โ (((๐ถ gcd ๐ท)โ2) ยท ((๐ธโ2) + (๐นโ2))) = ((๐ถโ2) + (๐ทโ2))) |
94 | 44, 93 | breqtrrd 5132 |
. . . . 5
โข (๐ โ ๐ โฅ (((๐ถ gcd ๐ท)โ2) ยท ((๐ธโ2) + (๐นโ2)))) |
95 | | zsqcl 13962 |
. . . . . . . 8
โข ((๐ถ gcd ๐ท) โ โค โ ((๐ถ gcd ๐ท)โ2) โ โค) |
96 | 49, 95 | syl 17 |
. . . . . . 7
โข (๐ โ ((๐ถ gcd ๐ท)โ2) โ โค) |
97 | 8, 96 | gcdcomd 16329 |
. . . . . 6
โข (๐ โ (๐ gcd ((๐ถ gcd ๐ท)โ2)) = (((๐ถ gcd ๐ท)โ2) gcd ๐)) |
98 | 49, 8 | gcdcld 16323 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โ
โ0) |
99 | 98 | nn0zd 12538 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โ โค) |
100 | | gcddvds 16318 |
. . . . . . . . . . . . . 14
โข (((๐ถ gcd ๐ท) โ โค โง ๐ โ โค) โ (((๐ถ gcd ๐ท) gcd ๐) โฅ (๐ถ gcd ๐ท) โง ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐)) |
101 | 49, 8, 100 | syl2anc 585 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐ถ gcd ๐ท) gcd ๐) โฅ (๐ถ gcd ๐ท) โง ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐)) |
102 | 101 | simpld 496 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โฅ (๐ถ gcd ๐ท)) |
103 | 99, 49, 14, 102, 56 | dvdstrd 16112 |
. . . . . . . . . . 11
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ถ) |
104 | 11, 14 | zsubcld 12545 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ด โ ๐ถ) โ โค) |
105 | 101 | simprd 497 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐) |
106 | 13 | simprd 497 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ด โ ๐ถ) / ๐) โ โค) |
107 | 5 | nnne0d 12137 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ 0) |
108 | | dvdsval2 16074 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ๐ โ 0 โง (๐ด โ ๐ถ) โ โค) โ (๐ โฅ (๐ด โ ๐ถ) โ ((๐ด โ ๐ถ) / ๐) โ โค)) |
109 | 8, 107, 104, 108 | syl3anc 1372 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ โฅ (๐ด โ ๐ถ) โ ((๐ด โ ๐ถ) / ๐) โ โค)) |
110 | 106, 109 | mpbird 257 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โฅ (๐ด โ ๐ถ)) |
111 | 99, 8, 104, 105, 110 | dvdstrd 16112 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โฅ (๐ด โ ๐ถ)) |
112 | | dvdssub2 16118 |
. . . . . . . . . . . 12
โข
(((((๐ถ gcd ๐ท) gcd ๐) โ โค โง ๐ด โ โค โง ๐ถ โ โค) โง ((๐ถ gcd ๐ท) gcd ๐) โฅ (๐ด โ ๐ถ)) โ (((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ด โ ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ถ)) |
113 | 99, 11, 14, 111, 112 | syl31anc 1374 |
. . . . . . . . . . 11
โข (๐ โ (((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ด โ ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ถ)) |
114 | 103, 113 | mpbird 257 |
. . . . . . . . . 10
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ด) |
115 | 99, 49, 20, 102, 66 | dvdstrd 16112 |
. . . . . . . . . . 11
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ท) |
116 | 17, 20 | zsubcld 12545 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ต โ ๐ท) โ โค) |
117 | 19 | simprd 497 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ต โ ๐ท) / ๐) โ โค) |
118 | | dvdsval2 16074 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ๐ โ 0 โง (๐ต โ ๐ท) โ โค) โ (๐ โฅ (๐ต โ ๐ท) โ ((๐ต โ ๐ท) / ๐) โ โค)) |
119 | 8, 107, 116, 118 | syl3anc 1372 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ โฅ (๐ต โ ๐ท) โ ((๐ต โ ๐ท) / ๐) โ โค)) |
120 | 117, 119 | mpbird 257 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โฅ (๐ต โ ๐ท)) |
121 | 99, 8, 116, 105, 120 | dvdstrd 16112 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โฅ (๐ต โ ๐ท)) |
122 | | dvdssub2 16118 |
. . . . . . . . . . . 12
โข
(((((๐ถ gcd ๐ท) gcd ๐) โ โค โง ๐ต โ โค โง ๐ท โ โค) โง ((๐ถ gcd ๐ท) gcd ๐) โฅ (๐ต โ ๐ท)) โ (((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ต โ ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ท)) |
123 | 99, 17, 20, 121, 122 | syl31anc 1374 |
. . . . . . . . . . 11
โข (๐ โ (((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ต โ ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ท)) |
124 | 115, 123 | mpbird 257 |
. . . . . . . . . 10
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ต) |
125 | | ax-1ne0 11054 |
. . . . . . . . . . . . . . 15
โข 1 โ
0 |
126 | 125 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 1 โ 0) |
127 | 47, 126 | eqnetrd 3010 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ด gcd ๐ต) โ 0) |
128 | 127 | neneqd 2947 |
. . . . . . . . . . . 12
โข (๐ โ ยฌ (๐ด gcd ๐ต) = 0) |
129 | | gcdeq0 16332 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ต โ โค) โ ((๐ด gcd ๐ต) = 0 โ (๐ด = 0 โง ๐ต = 0))) |
130 | 11, 17, 129 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ด gcd ๐ต) = 0 โ (๐ด = 0 โง ๐ต = 0))) |
131 | 128, 130 | mtbid 324 |
. . . . . . . . . . 11
โข (๐ โ ยฌ (๐ด = 0 โง ๐ต = 0)) |
132 | | dvdslegcd 16319 |
. . . . . . . . . . 11
โข
(((((๐ถ gcd ๐ท) gcd ๐) โ โค โง ๐ด โ โค โง ๐ต โ โค) โง ยฌ (๐ด = 0 โง ๐ต = 0)) โ ((((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ด โง ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ต) โ ((๐ถ gcd ๐ท) gcd ๐) โค (๐ด gcd ๐ต))) |
133 | 99, 11, 17, 131, 132 | syl31anc 1374 |
. . . . . . . . . 10
โข (๐ โ ((((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ด โง ((๐ถ gcd ๐ท) gcd ๐) โฅ ๐ต) โ ((๐ถ gcd ๐ท) gcd ๐) โค (๐ด gcd ๐ต))) |
134 | 114, 124,
133 | mp2and 698 |
. . . . . . . . 9
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โค (๐ด gcd ๐ต)) |
135 | 134, 47 | breqtrd 5130 |
. . . . . . . 8
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โค 1) |
136 | | simpr 486 |
. . . . . . . . . . . 12
โข (((๐ถ gcd ๐ท) = 0 โง ๐ = 0) โ ๐ = 0) |
137 | 136 | necon3ai 2967 |
. . . . . . . . . . 11
โข (๐ โ 0 โ ยฌ ((๐ถ gcd ๐ท) = 0 โง ๐ = 0)) |
138 | 107, 137 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ยฌ ((๐ถ gcd ๐ท) = 0 โง ๐ = 0)) |
139 | | gcdn0cl 16317 |
. . . . . . . . . 10
โข ((((๐ถ gcd ๐ท) โ โค โง ๐ โ โค) โง ยฌ ((๐ถ gcd ๐ท) = 0 โง ๐ = 0)) โ ((๐ถ gcd ๐ท) gcd ๐) โ โ) |
140 | 49, 8, 138, 139 | syl21anc 837 |
. . . . . . . . 9
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) โ โ) |
141 | | nnle1eq1 12117 |
. . . . . . . . 9
โข (((๐ถ gcd ๐ท) gcd ๐) โ โ โ (((๐ถ gcd ๐ท) gcd ๐) โค 1 โ ((๐ถ gcd ๐ท) gcd ๐) = 1)) |
142 | 140, 141 | syl 17 |
. . . . . . . 8
โข (๐ โ (((๐ถ gcd ๐ท) gcd ๐) โค 1 โ ((๐ถ gcd ๐ท) gcd ๐) = 1)) |
143 | 135, 142 | mpbid 231 |
. . . . . . 7
โข (๐ โ ((๐ถ gcd ๐ท) gcd ๐) = 1) |
144 | | 2nn 12160 |
. . . . . . . . 9
โข 2 โ
โ |
145 | 144 | a1i 11 |
. . . . . . . 8
โข (๐ โ 2 โ
โ) |
146 | | rplpwr 16373 |
. . . . . . . 8
โข (((๐ถ gcd ๐ท) โ โ โง ๐ โ โ โง 2 โ โ)
โ (((๐ถ gcd ๐ท) gcd ๐) = 1 โ (((๐ถ gcd ๐ท)โ2) gcd ๐) = 1)) |
147 | 48, 5, 145, 146 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ (((๐ถ gcd ๐ท) gcd ๐) = 1 โ (((๐ถ gcd ๐ท)โ2) gcd ๐) = 1)) |
148 | 143, 147 | mpd 15 |
. . . . . 6
โข (๐ โ (((๐ถ gcd ๐ท)โ2) gcd ๐) = 1) |
149 | 97, 148 | eqtrd 2778 |
. . . . 5
โข (๐ โ (๐ gcd ((๐ถ gcd ๐ท)โ2)) = 1) |
150 | 63, 72 | nn0addcld 12411 |
. . . . . . 7
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โ
โ0) |
151 | 150 | nn0zd 12538 |
. . . . . 6
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โ โค) |
152 | | coprmdvds 16464 |
. . . . . 6
โข ((๐ โ โค โง ((๐ถ gcd ๐ท)โ2) โ โค โง ((๐ธโ2) + (๐นโ2)) โ โค) โ ((๐ โฅ (((๐ถ gcd ๐ท)โ2) ยท ((๐ธโ2) + (๐นโ2))) โง (๐ gcd ((๐ถ gcd ๐ท)โ2)) = 1) โ ๐ โฅ ((๐ธโ2) + (๐นโ2)))) |
153 | 8, 96, 151, 152 | syl3anc 1372 |
. . . . 5
โข (๐ โ ((๐ โฅ (((๐ถ gcd ๐ท)โ2) ยท ((๐ธโ2) + (๐นโ2))) โง (๐ gcd ((๐ถ gcd ๐ท)โ2)) = 1) โ ๐ โฅ ((๐ธโ2) + (๐นโ2)))) |
154 | 94, 149, 153 | mp2and 698 |
. . . 4
โข (๐ โ ๐ โฅ ((๐ธโ2) + (๐นโ2))) |
155 | | dvdsval2 16074 |
. . . . 5
โข ((๐ โ โค โง ๐ โ 0 โง ((๐ธโ2) + (๐นโ2)) โ โค) โ (๐ โฅ ((๐ธโ2) + (๐นโ2)) โ (((๐ธโ2) + (๐นโ2)) / ๐) โ โค)) |
156 | 8, 107, 151, 155 | syl3anc 1372 |
. . . 4
โข (๐ โ (๐ โฅ ((๐ธโ2) + (๐นโ2)) โ (((๐ธโ2) + (๐นโ2)) / ๐) โ โค)) |
157 | 154, 156 | mpbid 231 |
. . 3
โข (๐ โ (((๐ธโ2) + (๐นโ2)) / ๐) โ โค) |
158 | 63 | nn0red 12408 |
. . . . 5
โข (๐ โ (๐ธโ2) โ โ) |
159 | 72 | nn0red 12408 |
. . . . 5
โข (๐ โ (๐นโ2) โ โ) |
160 | 158, 159 | readdcld 11118 |
. . . 4
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โ โ) |
161 | 5 | nnred 12102 |
. . . 4
โข (๐ โ ๐ โ โ) |
162 | 1, 45 | 2sqlem7 26694 |
. . . . . . 7
โข ๐ โ (๐ โฉ โ) |
163 | | inss2 4188 |
. . . . . . 7
โข (๐ โฉ โ) โ
โ |
164 | 162, 163 | sstri 3952 |
. . . . . 6
โข ๐ โ
โ |
165 | 61, 70 | gcdcld 16323 |
. . . . . . . . . 10
โข (๐ โ (๐ธ gcd ๐น) โ
โ0) |
166 | 165 | nn0cnd 12409 |
. . . . . . . . 9
โข (๐ โ (๐ธ gcd ๐น) โ โ) |
167 | | 1cnd 11084 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
168 | 75 | mulid1d 11106 |
. . . . . . . . . 10
โข (๐ โ ((๐ถ gcd ๐ท) ยท 1) = (๐ถ gcd ๐ท)) |
169 | 81, 89 | oveq12d 7368 |
. . . . . . . . . 10
โข (๐ โ (((๐ถ gcd ๐ท) ยท ๐ธ) gcd ((๐ถ gcd ๐ท) ยท ๐น)) = (๐ถ gcd ๐ท)) |
170 | 14, 20 | gcdcld 16323 |
. . . . . . . . . . 11
โข (๐ โ (๐ถ gcd ๐ท) โ
โ0) |
171 | | mulgcd 16364 |
. . . . . . . . . . 11
โข (((๐ถ gcd ๐ท) โ โ0 โง ๐ธ โ โค โง ๐น โ โค) โ (((๐ถ gcd ๐ท) ยท ๐ธ) gcd ((๐ถ gcd ๐ท) ยท ๐น)) = ((๐ถ gcd ๐ท) ยท (๐ธ gcd ๐น))) |
172 | 170, 61, 70, 171 | syl3anc 1372 |
. . . . . . . . . 10
โข (๐ โ (((๐ถ gcd ๐ท) ยท ๐ธ) gcd ((๐ถ gcd ๐ท) ยท ๐น)) = ((๐ถ gcd ๐ท) ยท (๐ธ gcd ๐น))) |
173 | 168, 169,
172 | 3eqtr2rd 2785 |
. . . . . . . . 9
โข (๐ โ ((๐ถ gcd ๐ท) ยท (๐ธ gcd ๐น)) = ((๐ถ gcd ๐ท) ยท 1)) |
174 | 166, 167,
75, 57, 173 | mulcanad 11724 |
. . . . . . . 8
โข (๐ โ (๐ธ gcd ๐น) = 1) |
175 | | eqidd 2739 |
. . . . . . . 8
โข (๐ โ ((๐ธโ2) + (๐นโ2)) = ((๐ธโ2) + (๐นโ2))) |
176 | | oveq1 7357 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ธ โ (๐ฅ gcd ๐ฆ) = (๐ธ gcd ๐ฆ)) |
177 | 176 | eqeq1d 2740 |
. . . . . . . . . 10
โข (๐ฅ = ๐ธ โ ((๐ฅ gcd ๐ฆ) = 1 โ (๐ธ gcd ๐ฆ) = 1)) |
178 | | oveq1 7357 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ธ โ (๐ฅโ2) = (๐ธโ2)) |
179 | 178 | oveq1d 7365 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ธ โ ((๐ฅโ2) + (๐ฆโ2)) = ((๐ธโ2) + (๐ฆโ2))) |
180 | 179 | eqeq2d 2749 |
. . . . . . . . . 10
โข (๐ฅ = ๐ธ โ (((๐ธโ2) + (๐นโ2)) = ((๐ฅโ2) + (๐ฆโ2)) โ ((๐ธโ2) + (๐นโ2)) = ((๐ธโ2) + (๐ฆโ2)))) |
181 | 177, 180 | anbi12d 632 |
. . . . . . . . 9
โข (๐ฅ = ๐ธ โ (((๐ฅ gcd ๐ฆ) = 1 โง ((๐ธโ2) + (๐นโ2)) = ((๐ฅโ2) + (๐ฆโ2))) โ ((๐ธ gcd ๐ฆ) = 1 โง ((๐ธโ2) + (๐นโ2)) = ((๐ธโ2) + (๐ฆโ2))))) |
182 | | oveq2 7358 |
. . . . . . . . . . 11
โข (๐ฆ = ๐น โ (๐ธ gcd ๐ฆ) = (๐ธ gcd ๐น)) |
183 | 182 | eqeq1d 2740 |
. . . . . . . . . 10
โข (๐ฆ = ๐น โ ((๐ธ gcd ๐ฆ) = 1 โ (๐ธ gcd ๐น) = 1)) |
184 | | oveq1 7357 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐น โ (๐ฆโ2) = (๐นโ2)) |
185 | 184 | oveq2d 7366 |
. . . . . . . . . . 11
โข (๐ฆ = ๐น โ ((๐ธโ2) + (๐ฆโ2)) = ((๐ธโ2) + (๐นโ2))) |
186 | 185 | eqeq2d 2749 |
. . . . . . . . . 10
โข (๐ฆ = ๐น โ (((๐ธโ2) + (๐นโ2)) = ((๐ธโ2) + (๐ฆโ2)) โ ((๐ธโ2) + (๐นโ2)) = ((๐ธโ2) + (๐นโ2)))) |
187 | 183, 186 | anbi12d 632 |
. . . . . . . . 9
โข (๐ฆ = ๐น โ (((๐ธ gcd ๐ฆ) = 1 โง ((๐ธโ2) + (๐นโ2)) = ((๐ธโ2) + (๐ฆโ2))) โ ((๐ธ gcd ๐น) = 1 โง ((๐ธโ2) + (๐นโ2)) = ((๐ธโ2) + (๐นโ2))))) |
188 | 181, 187 | rspc2ev 3591 |
. . . . . . . 8
โข ((๐ธ โ โค โง ๐น โ โค โง ((๐ธ gcd ๐น) = 1 โง ((๐ธโ2) + (๐นโ2)) = ((๐ธโ2) + (๐นโ2)))) โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ((๐ธโ2) + (๐นโ2)) = ((๐ฅโ2) + (๐ฆโ2)))) |
189 | 61, 70, 174, 175, 188 | syl112anc 1375 |
. . . . . . 7
โข (๐ โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ((๐ธโ2) + (๐นโ2)) = ((๐ฅโ2) + (๐ฆโ2)))) |
190 | | ovex 7383 |
. . . . . . . 8
โข ((๐ธโ2) + (๐นโ2)) โ V |
191 | | eqeq1 2742 |
. . . . . . . . . 10
โข (๐ง = ((๐ธโ2) + (๐นโ2)) โ (๐ง = ((๐ฅโ2) + (๐ฆโ2)) โ ((๐ธโ2) + (๐นโ2)) = ((๐ฅโ2) + (๐ฆโ2)))) |
192 | 191 | anbi2d 630 |
. . . . . . . . 9
โข (๐ง = ((๐ธโ2) + (๐นโ2)) โ (((๐ฅ gcd ๐ฆ) = 1 โง ๐ง = ((๐ฅโ2) + (๐ฆโ2))) โ ((๐ฅ gcd ๐ฆ) = 1 โง ((๐ธโ2) + (๐นโ2)) = ((๐ฅโ2) + (๐ฆโ2))))) |
193 | 192 | 2rexbidv 3212 |
. . . . . . . 8
โข (๐ง = ((๐ธโ2) + (๐นโ2)) โ (โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ๐ง = ((๐ฅโ2) + (๐ฆโ2))) โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ((๐ธโ2) + (๐นโ2)) = ((๐ฅโ2) + (๐ฆโ2))))) |
194 | 190, 193,
45 | elab2 3633 |
. . . . . . 7
โข (((๐ธโ2) + (๐นโ2)) โ ๐ โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ gcd ๐ฆ) = 1 โง ((๐ธโ2) + (๐นโ2)) = ((๐ฅโ2) + (๐ฆโ2)))) |
195 | 189, 194 | sylibr 233 |
. . . . . 6
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โ ๐) |
196 | 164, 195 | sselid 3941 |
. . . . 5
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โ โ) |
197 | 196 | nngt0d 12136 |
. . . 4
โข (๐ โ 0 < ((๐ธโ2) + (๐นโ2))) |
198 | 5 | nngt0d 12136 |
. . . 4
โข (๐ โ 0 < ๐) |
199 | 160, 161,
197, 198 | divgt0d 12024 |
. . 3
โข (๐ โ 0 < (((๐ธโ2) + (๐นโ2)) / ๐)) |
200 | | elnnz 12443 |
. . 3
โข ((((๐ธโ2) + (๐นโ2)) / ๐) โ โ โ ((((๐ธโ2) + (๐นโ2)) / ๐) โ โค โง 0 < (((๐ธโ2) + (๐นโ2)) / ๐))) |
201 | 157, 199,
200 | sylanbrc 584 |
. 2
โข (๐ โ (((๐ธโ2) + (๐นโ2)) / ๐) โ โ) |
202 | | prmnn 16485 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
203 | 202 | ad2antrl 727 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ ๐ โ โ) |
204 | 203 | nnred 12102 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ ๐ โ โ) |
205 | 157 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ (((๐ธโ2) + (๐นโ2)) / ๐) โ โค) |
206 | 205 | zred 12540 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ (((๐ธโ2) + (๐นโ2)) / ๐) โ โ) |
207 | | peano2zm 12477 |
. . . . . . . . . . 11
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
208 | 8, 207 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ โ 1) โ โค) |
209 | 208 | zred 12540 |
. . . . . . . . 9
โข (๐ โ (๐ โ 1) โ โ) |
210 | 209 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ (๐ โ 1) โ โ) |
211 | | simprr 772 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐)) |
212 | | prmz 16486 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โค) |
213 | 212 | ad2antrl 727 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ ๐ โ โค) |
214 | 201 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ (((๐ธโ2) + (๐นโ2)) / ๐) โ โ) |
215 | | dvdsle 16127 |
. . . . . . . . . 10
โข ((๐ โ โค โง (((๐ธโ2) + (๐นโ2)) / ๐) โ โ) โ (๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐) โ ๐ โค (((๐ธโ2) + (๐นโ2)) / ๐))) |
216 | 213, 214,
215 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ (๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐) โ ๐ โค (((๐ธโ2) + (๐นโ2)) / ๐))) |
217 | 211, 216 | mpd 15 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ ๐ โค (((๐ธโ2) + (๐นโ2)) / ๐)) |
218 | | zsqcl 13962 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ (๐โ2) โ
โค) |
219 | 8, 218 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐โ2) โ โค) |
220 | 219 | zred 12540 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐โ2) โ โ) |
221 | 220 | rehalfcld 12334 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐โ2) / 2) โ
โ) |
222 | 16 | zred 12540 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ถโ2) โ โ) |
223 | 22 | zred 12540 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ทโ2) โ โ) |
224 | 222, 223 | readdcld 11118 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ถโ2) + (๐ทโ2)) โ โ) |
225 | | 1red 11090 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 1 โ
โ) |
226 | 48 | nnsqcld 14073 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ถ gcd ๐ท)โ2) โ โ) |
227 | 226 | nnred 12102 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ถ gcd ๐ท)โ2) โ โ) |
228 | 150 | nn0ge0d 12410 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 โค ((๐ธโ2) + (๐นโ2))) |
229 | 226 | nnge1d 12135 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 1 โค ((๐ถ gcd ๐ท)โ2)) |
230 | 225, 227,
160, 228, 229 | lemul1ad 12028 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1 ยท ((๐ธโ2) + (๐นโ2))) โค (((๐ถ gcd ๐ท)โ2) ยท ((๐ธโ2) + (๐นโ2)))) |
231 | 150 | nn0cnd 12409 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โ โ) |
232 | 231 | mulid2d 11107 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1 ยท ((๐ธโ2) + (๐นโ2))) = ((๐ธโ2) + (๐นโ2))) |
233 | 230, 232,
93 | 3brtr3d 5135 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โค ((๐ถโ2) + (๐ทโ2))) |
234 | 221 | rehalfcld 12334 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((๐โ2) / 2) / 2) โ
โ) |
235 | 11, 5, 12 | 4sqlem7 16751 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ถโ2) โค (((๐โ2) / 2) / 2)) |
236 | 17, 5, 18 | 4sqlem7 16751 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ทโ2) โค (((๐โ2) / 2) / 2)) |
237 | 222, 223,
234, 234, 235, 236 | le2addd 11708 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ถโ2) + (๐ทโ2)) โค ((((๐โ2) / 2) / 2) + (((๐โ2) / 2) / 2))) |
238 | 221 | recnd 11117 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐โ2) / 2) โ
โ) |
239 | 238 | 2halvesd 12333 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((((๐โ2) / 2) / 2) + (((๐โ2) / 2) / 2)) = ((๐โ2) / 2)) |
240 | 237, 239 | breqtrd 5130 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ถโ2) + (๐ทโ2)) โค ((๐โ2) / 2)) |
241 | 160, 224,
221, 233, 240 | letrd 11246 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โค ((๐โ2) / 2)) |
242 | 5 | nnsqcld 14073 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐โ2) โ โ) |
243 | 242 | nnrpd 12884 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐โ2) โ
โ+) |
244 | | rphalflt 12873 |
. . . . . . . . . . . . . 14
โข ((๐โ2) โ
โ+ โ ((๐โ2) / 2) < (๐โ2)) |
245 | 243, 244 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐โ2) / 2) < (๐โ2)) |
246 | 160, 221,
220, 241, 245 | lelttrd 11247 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ธโ2) + (๐นโ2)) < (๐โ2)) |
247 | 8 | zcnd 12541 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
248 | 247 | sqvald 13975 |
. . . . . . . . . . . 12
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
249 | 246, 248 | breqtrd 5130 |
. . . . . . . . . . 11
โข (๐ โ ((๐ธโ2) + (๐นโ2)) < (๐ ยท ๐)) |
250 | | ltdivmul 11964 |
. . . . . . . . . . . 12
โข ((((๐ธโ2) + (๐นโ2)) โ โ โง ๐ โ โ โง (๐ โ โ โง 0 <
๐)) โ ((((๐ธโ2) + (๐นโ2)) / ๐) < ๐ โ ((๐ธโ2) + (๐นโ2)) < (๐ ยท ๐))) |
251 | 160, 161,
161, 198, 250 | syl112anc 1375 |
. . . . . . . . . . 11
โข (๐ โ ((((๐ธโ2) + (๐นโ2)) / ๐) < ๐ โ ((๐ธโ2) + (๐นโ2)) < (๐ ยท ๐))) |
252 | 249, 251 | mpbird 257 |
. . . . . . . . . 10
โข (๐ โ (((๐ธโ2) + (๐นโ2)) / ๐) < ๐) |
253 | | zltlem1 12487 |
. . . . . . . . . . 11
โข
(((((๐ธโ2) +
(๐นโ2)) / ๐) โ โค โง ๐ โ โค) โ
((((๐ธโ2) + (๐นโ2)) / ๐) < ๐ โ (((๐ธโ2) + (๐นโ2)) / ๐) โค (๐ โ 1))) |
254 | 157, 8, 253 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ ((((๐ธโ2) + (๐นโ2)) / ๐) < ๐ โ (((๐ธโ2) + (๐นโ2)) / ๐) โค (๐ โ 1))) |
255 | 252, 254 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ (((๐ธโ2) + (๐นโ2)) / ๐) โค (๐ โ 1)) |
256 | 255 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ (((๐ธโ2) + (๐นโ2)) / ๐) โค (๐ โ 1)) |
257 | 204, 206,
210, 217, 256 | letrd 11246 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ ๐ โค (๐ โ 1)) |
258 | 208 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ (๐ โ 1) โ โค) |
259 | | fznn 13438 |
. . . . . . . 8
โข ((๐ โ 1) โ โค
โ (๐ โ
(1...(๐ โ 1)) โ
(๐ โ โ โง
๐ โค (๐ โ 1)))) |
260 | 258, 259 | syl 17 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ (๐ โ (1...(๐ โ 1)) โ (๐ โ โ โง ๐ โค (๐ โ 1)))) |
261 | 203, 257,
260 | mpbir2and 712 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ ๐ โ (1...(๐ โ 1))) |
262 | 195 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ ((๐ธโ2) + (๐นโ2)) โ ๐) |
263 | 261, 262 | jca 513 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ (๐ โ (1...(๐ โ 1)) โง ((๐ธโ2) + (๐นโ2)) โ ๐)) |
264 | 46 | adantr 482 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ โ๐ โ (1...(๐ โ 1))โ๐ โ ๐ (๐ โฅ ๐ โ ๐ โ ๐)) |
265 | 151 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ ((๐ธโ2) + (๐นโ2)) โ โค) |
266 | | dvdsmul2 16096 |
. . . . . . . . 9
โข ((๐ โ โค โง (((๐ธโ2) + (๐นโ2)) / ๐) โ โค) โ (((๐ธโ2) + (๐นโ2)) / ๐) โฅ (๐ ยท (((๐ธโ2) + (๐นโ2)) / ๐))) |
267 | 8, 157, 266 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ (((๐ธโ2) + (๐นโ2)) / ๐) โฅ (๐ ยท (((๐ธโ2) + (๐นโ2)) / ๐))) |
268 | 231, 247,
107 | divcan2d 11867 |
. . . . . . . 8
โข (๐ โ (๐ ยท (((๐ธโ2) + (๐นโ2)) / ๐)) = ((๐ธโ2) + (๐นโ2))) |
269 | 267, 268 | breqtrd 5130 |
. . . . . . 7
โข (๐ โ (((๐ธโ2) + (๐นโ2)) / ๐) โฅ ((๐ธโ2) + (๐นโ2))) |
270 | 269 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ (((๐ธโ2) + (๐นโ2)) / ๐) โฅ ((๐ธโ2) + (๐นโ2))) |
271 | 213, 205,
265, 211, 270 | dvdstrd 16112 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ ๐ โฅ ((๐ธโ2) + (๐นโ2))) |
272 | | breq1 5107 |
. . . . . . 7
โข (๐ = ๐ โ (๐ โฅ ๐ โ ๐ โฅ ๐)) |
273 | | eleq1w 2821 |
. . . . . . 7
โข (๐ = ๐ โ (๐ โ ๐ โ ๐ โ ๐)) |
274 | 272, 273 | imbi12d 345 |
. . . . . 6
โข (๐ = ๐ โ ((๐ โฅ ๐ โ ๐ โ ๐) โ (๐ โฅ ๐ โ ๐ โ ๐))) |
275 | | breq2 5108 |
. . . . . . 7
โข (๐ = ((๐ธโ2) + (๐นโ2)) โ (๐ โฅ ๐ โ ๐ โฅ ((๐ธโ2) + (๐นโ2)))) |
276 | 275 | imbi1d 342 |
. . . . . 6
โข (๐ = ((๐ธโ2) + (๐นโ2)) โ ((๐ โฅ ๐ โ ๐ โ ๐) โ (๐ โฅ ((๐ธโ2) + (๐นโ2)) โ ๐ โ ๐))) |
277 | 274, 276 | rspc2v 3589 |
. . . . 5
โข ((๐ โ (1...(๐ โ 1)) โง ((๐ธโ2) + (๐นโ2)) โ ๐) โ (โ๐ โ (1...(๐ โ 1))โ๐ โ ๐ (๐ โฅ ๐ โ ๐ โ ๐) โ (๐ โฅ ((๐ธโ2) + (๐นโ2)) โ ๐ โ ๐))) |
278 | 263, 264,
271, 277 | syl3c 66 |
. . . 4
โข ((๐ โง (๐ โ โ โง ๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐))) โ ๐ โ ๐) |
279 | 278 | expr 458 |
. . 3
โข ((๐ โง ๐ โ โ) โ (๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐) โ ๐ โ ๐)) |
280 | 279 | ralrimiva 3142 |
. 2
โข (๐ โ โ๐ โ โ (๐ โฅ (((๐ธโ2) + (๐นโ2)) / ๐) โ ๐ โ ๐)) |
281 | | inss1 4187 |
. . . . 5
โข (๐ โฉ โ) โ ๐ |
282 | 162, 281 | sstri 3952 |
. . . 4
โข ๐ โ ๐ |
283 | 282, 195 | sselid 3941 |
. . 3
โข (๐ โ ((๐ธโ2) + (๐นโ2)) โ ๐) |
284 | 268, 283 | eqeltrd 2839 |
. 2
โข (๐ โ (๐ ยท (((๐ธโ2) + (๐นโ2)) / ๐)) โ ๐) |
285 | 1, 5, 201, 280, 284 | 2sqlem6 26693 |
1
โข (๐ โ ๐ โ ๐) |