Step | Hyp | Ref
| Expression |
1 | | 2cnd 12238 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โ) |
2 | 1 | sqsqrtd 15331 |
. . . . . . . . . . 11
โข (๐ โ ((โโ2)โ2)
= 2) |
3 | | sqrt2irrlem.3 |
. . . . . . . . . . . 12
โข (๐ โ (โโ2) = (๐ด / ๐ต)) |
4 | 3 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ โ ((โโ2)โ2)
= ((๐ด / ๐ต)โ2)) |
5 | 2, 4 | eqtr3d 2779 |
. . . . . . . . . 10
โข (๐ โ 2 = ((๐ด / ๐ต)โ2)) |
6 | | sqrt2irrlem.1 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โค) |
7 | 6 | zcnd 12615 |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ โ) |
8 | | sqrt2irrlem.2 |
. . . . . . . . . . . 12
โข (๐ โ ๐ต โ โ) |
9 | 8 | nncnd 12176 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ โ) |
10 | 8 | nnne0d 12210 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ 0) |
11 | 7, 9, 10 | sqdivd 14071 |
. . . . . . . . . 10
โข (๐ โ ((๐ด / ๐ต)โ2) = ((๐ดโ2) / (๐ตโ2))) |
12 | 5, 11 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ 2 = ((๐ดโ2) / (๐ตโ2))) |
13 | 12 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ (2 ยท (๐ตโ2)) = (((๐ดโ2) / (๐ตโ2)) ยท (๐ตโ2))) |
14 | 7 | sqcld 14056 |
. . . . . . . . 9
โข (๐ โ (๐ดโ2) โ โ) |
15 | 8 | nnsqcld 14154 |
. . . . . . . . . 10
โข (๐ โ (๐ตโ2) โ โ) |
16 | 15 | nncnd 12176 |
. . . . . . . . 9
โข (๐ โ (๐ตโ2) โ โ) |
17 | 15 | nnne0d 12210 |
. . . . . . . . 9
โข (๐ โ (๐ตโ2) โ 0) |
18 | 14, 16, 17 | divcan1d 11939 |
. . . . . . . 8
โข (๐ โ (((๐ดโ2) / (๐ตโ2)) ยท (๐ตโ2)) = (๐ดโ2)) |
19 | 13, 18 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ (2 ยท (๐ตโ2)) = (๐ดโ2)) |
20 | 19 | oveq1d 7377 |
. . . . . 6
โข (๐ โ ((2 ยท (๐ตโ2)) / 2) = ((๐ดโ2) / 2)) |
21 | | 2ne0 12264 |
. . . . . . . 8
โข 2 โ
0 |
22 | 21 | a1i 11 |
. . . . . . 7
โข (๐ โ 2 โ 0) |
23 | 16, 1, 22 | divcan3d 11943 |
. . . . . 6
โข (๐ โ ((2 ยท (๐ตโ2)) / 2) = (๐ตโ2)) |
24 | 20, 23 | eqtr3d 2779 |
. . . . 5
โข (๐ โ ((๐ดโ2) / 2) = (๐ตโ2)) |
25 | 24, 15 | eqeltrd 2838 |
. . . 4
โข (๐ โ ((๐ดโ2) / 2) โ
โ) |
26 | 25 | nnzd 12533 |
. . 3
โข (๐ โ ((๐ดโ2) / 2) โ
โค) |
27 | | zesq 14136 |
. . . 4
โข (๐ด โ โค โ ((๐ด / 2) โ โค โ
((๐ดโ2) / 2) โ
โค)) |
28 | 6, 27 | syl 17 |
. . 3
โข (๐ โ ((๐ด / 2) โ โค โ ((๐ดโ2) / 2) โ
โค)) |
29 | 26, 28 | mpbird 257 |
. 2
โข (๐ โ (๐ด / 2) โ โค) |
30 | 1 | sqvald 14055 |
. . . . . . . 8
โข (๐ โ (2โ2) = (2 ยท
2)) |
31 | 30 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ ((๐ดโ2) / (2โ2)) = ((๐ดโ2) / (2 ยท 2))) |
32 | 7, 1, 22 | sqdivd 14071 |
. . . . . . 7
โข (๐ โ ((๐ด / 2)โ2) = ((๐ดโ2) / (2โ2))) |
33 | 14, 1, 1, 22, 22 | divdiv1d 11969 |
. . . . . . 7
โข (๐ โ (((๐ดโ2) / 2) / 2) = ((๐ดโ2) / (2 ยท 2))) |
34 | 31, 32, 33 | 3eqtr4d 2787 |
. . . . . 6
โข (๐ โ ((๐ด / 2)โ2) = (((๐ดโ2) / 2) / 2)) |
35 | 24 | oveq1d 7377 |
. . . . . 6
โข (๐ โ (((๐ดโ2) / 2) / 2) = ((๐ตโ2) / 2)) |
36 | 34, 35 | eqtrd 2777 |
. . . . 5
โข (๐ โ ((๐ด / 2)โ2) = ((๐ตโ2) / 2)) |
37 | | zsqcl 14041 |
. . . . . 6
โข ((๐ด / 2) โ โค โ
((๐ด / 2)โ2) โ
โค) |
38 | 29, 37 | syl 17 |
. . . . 5
โข (๐ โ ((๐ด / 2)โ2) โ
โค) |
39 | 36, 38 | eqeltrrd 2839 |
. . . 4
โข (๐ โ ((๐ตโ2) / 2) โ
โค) |
40 | 15 | nnrpd 12962 |
. . . . . 6
โข (๐ โ (๐ตโ2) โ
โ+) |
41 | 40 | rphalfcld 12976 |
. . . . 5
โข (๐ โ ((๐ตโ2) / 2) โ
โ+) |
42 | 41 | rpgt0d 12967 |
. . . 4
โข (๐ โ 0 < ((๐ตโ2) / 2)) |
43 | | elnnz 12516 |
. . . 4
โข (((๐ตโ2) / 2) โ โ
โ (((๐ตโ2) / 2)
โ โค โง 0 < ((๐ตโ2) / 2))) |
44 | 39, 42, 43 | sylanbrc 584 |
. . 3
โข (๐ โ ((๐ตโ2) / 2) โ
โ) |
45 | | nnesq 14137 |
. . . 4
โข (๐ต โ โ โ ((๐ต / 2) โ โ โ
((๐ตโ2) / 2) โ
โ)) |
46 | 8, 45 | syl 17 |
. . 3
โข (๐ โ ((๐ต / 2) โ โ โ ((๐ตโ2) / 2) โ
โ)) |
47 | 44, 46 | mpbird 257 |
. 2
โข (๐ โ (๐ต / 2) โ โ) |
48 | 29, 47 | jca 513 |
1
โข (๐ โ ((๐ด / 2) โ โค โง (๐ต / 2) โ
โ)) |