Step | Hyp | Ref
| Expression |
1 | | simp-4l 782 |
. . . . . 6
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ ๐ โ โ) |
2 | 1 | resqcld 14039 |
. . . . 5
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (๐โ2) โ โ) |
3 | | simpllr 775 |
. . . . . . 7
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (๐ โ โ โง 0 โค ๐)) |
4 | 3 | simpld 496 |
. . . . . 6
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ ๐ โ โ) |
5 | 4 | resqcld 14039 |
. . . . 5
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (๐โ2) โ โ) |
6 | 2, 5 | readdcld 11192 |
. . . 4
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ ((๐โ2) + (๐โ2)) โ โ) |
7 | 1 | sqge0d 14051 |
. . . . 5
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ 0 โค (๐โ2)) |
8 | 4 | sqge0d 14051 |
. . . . 5
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ 0 โค (๐โ2)) |
9 | 2, 5, 7, 8 | addge0d 11739 |
. . . 4
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ 0 โค ((๐โ2) + (๐โ2))) |
10 | 6, 9 | resqrtcld 15311 |
. . 3
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (โโ((๐โ2) + (๐โ2))) โ โ) |
11 | | simplr 768 |
. . . . . . . 8
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ ๐ท โ
โ+) |
12 | 11 | rpred 12965 |
. . . . . . 7
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ ๐ท โ โ) |
13 | 12 | rehalfcld 12408 |
. . . . . 6
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (๐ท / 2) โ โ) |
14 | 13 | resqcld 14039 |
. . . . 5
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ ((๐ท / 2)โ2) โ
โ) |
15 | 14, 14 | readdcld 11192 |
. . . 4
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (((๐ท / 2)โ2) + ((๐ท / 2)โ2)) โ
โ) |
16 | 13 | sqge0d 14051 |
. . . . 5
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ 0 โค ((๐ท / 2)โ2)) |
17 | 14, 14, 16, 16 | addge0d 11739 |
. . . 4
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ 0 โค (((๐ท / 2)โ2) + ((๐ท / 2)โ2))) |
18 | 15, 17 | resqrtcld 15311 |
. . 3
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (โโ(((๐ท / 2)โ2) + ((๐ท / 2)โ2))) โ
โ) |
19 | | simprl 770 |
. . . . . 6
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ ๐ < (๐ท / 2)) |
20 | | simp-4r 783 |
. . . . . . 7
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ 0 โค ๐) |
21 | | 2rp 12928 |
. . . . . . . . 9
โข 2 โ
โ+ |
22 | 21 | a1i 11 |
. . . . . . . 8
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ 2 โ
โ+) |
23 | 11 | rpge0d 12969 |
. . . . . . . 8
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ 0 โค ๐ท) |
24 | 12, 22, 23 | divge0d 13005 |
. . . . . . 7
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ 0 โค (๐ท / 2)) |
25 | 1, 13, 20, 24 | lt2sqd 14168 |
. . . . . 6
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (๐ < (๐ท / 2) โ (๐โ2) < ((๐ท / 2)โ2))) |
26 | 19, 25 | mpbid 231 |
. . . . 5
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (๐โ2) < ((๐ท / 2)โ2)) |
27 | | simprr 772 |
. . . . . 6
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ ๐ < (๐ท / 2)) |
28 | 3 | simprd 497 |
. . . . . . 7
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ 0 โค ๐) |
29 | 4, 13, 28, 24 | lt2sqd 14168 |
. . . . . 6
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (๐ < (๐ท / 2) โ (๐โ2) < ((๐ท / 2)โ2))) |
30 | 27, 29 | mpbid 231 |
. . . . 5
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (๐โ2) < ((๐ท / 2)โ2)) |
31 | 2, 5, 14, 14, 26, 30 | lt2addd 11786 |
. . . 4
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ ((๐โ2) + (๐โ2)) < (((๐ท / 2)โ2) + ((๐ท / 2)โ2))) |
32 | 6, 9, 15, 17 | sqrtltd 15321 |
. . . 4
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (((๐โ2) + (๐โ2)) < (((๐ท / 2)โ2) + ((๐ท / 2)โ2)) โ (โโ((๐โ2) + (๐โ2))) < (โโ(((๐ท / 2)โ2) + ((๐ท /
2)โ2))))) |
33 | 31, 32 | mpbid 231 |
. . 3
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (โโ((๐โ2) + (๐โ2))) < (โโ(((๐ท / 2)โ2) + ((๐ท /
2)โ2)))) |
34 | | rpre 12931 |
. . . . . . . . . . 11
โข (๐ท โ โ+
โ ๐ท โ
โ) |
35 | 34 | rehalfcld 12408 |
. . . . . . . . . 10
โข (๐ท โ โ+
โ (๐ท / 2) โ
โ) |
36 | 35 | resqcld 14039 |
. . . . . . . . 9
โข (๐ท โ โ+
โ ((๐ท / 2)โ2)
โ โ) |
37 | 36 | recnd 11191 |
. . . . . . . 8
โข (๐ท โ โ+
โ ((๐ท / 2)โ2)
โ โ) |
38 | 37 | 2timesd 12404 |
. . . . . . 7
โข (๐ท โ โ+
โ (2 ยท ((๐ท /
2)โ2)) = (((๐ท /
2)โ2) + ((๐ท /
2)โ2))) |
39 | 38 | fveq2d 6850 |
. . . . . 6
โข (๐ท โ โ+
โ (โโ(2 ยท ((๐ท / 2)โ2))) = (โโ(((๐ท / 2)โ2) + ((๐ท /
2)โ2)))) |
40 | 21 | a1i 11 |
. . . . . . . . . 10
โข (๐ท โ โ+
โ 2 โ โ+) |
41 | | rpge0 12936 |
. . . . . . . . . 10
โข (๐ท โ โ+
โ 0 โค ๐ท) |
42 | 34, 40, 41 | divge0d 13005 |
. . . . . . . . 9
โข (๐ท โ โ+
โ 0 โค (๐ท /
2)) |
43 | 35, 42 | sqrtsqd 15313 |
. . . . . . . 8
โข (๐ท โ โ+
โ (โโ((๐ท /
2)โ2)) = (๐ท /
2)) |
44 | 43 | oveq2d 7377 |
. . . . . . 7
โข (๐ท โ โ+
โ ((โโ2) ยท (โโ((๐ท / 2)โ2))) = ((โโ2)
ยท (๐ท /
2))) |
45 | | 2re 12235 |
. . . . . . . . 9
โข 2 โ
โ |
46 | 45 | a1i 11 |
. . . . . . . 8
โข (๐ท โ โ+
โ 2 โ โ) |
47 | | 0le2 12263 |
. . . . . . . . 9
โข 0 โค
2 |
48 | 47 | a1i 11 |
. . . . . . . 8
โข (๐ท โ โ+
โ 0 โค 2) |
49 | 35 | sqge0d 14051 |
. . . . . . . 8
โข (๐ท โ โ+
โ 0 โค ((๐ท /
2)โ2)) |
50 | 46, 48, 36, 49 | sqrtmuld 15318 |
. . . . . . 7
โข (๐ท โ โ+
โ (โโ(2 ยท ((๐ท / 2)โ2))) = ((โโ2)
ยท (โโ((๐ท
/ 2)โ2)))) |
51 | | 2cnd 12239 |
. . . . . . . . 9
โข (๐ท โ โ+
โ 2 โ โ) |
52 | 51 | sqrtcld 15331 |
. . . . . . . 8
โข (๐ท โ โ+
โ (โโ2) โ โ) |
53 | | rpcn 12933 |
. . . . . . . 8
โข (๐ท โ โ+
โ ๐ท โ
โ) |
54 | | 2ne0 12265 |
. . . . . . . . 9
โข 2 โ
0 |
55 | 54 | a1i 11 |
. . . . . . . 8
โข (๐ท โ โ+
โ 2 โ 0) |
56 | 52, 51, 53, 55 | div32d 11962 |
. . . . . . 7
โข (๐ท โ โ+
โ (((โโ2) / 2) ยท ๐ท) = ((โโ2) ยท (๐ท / 2))) |
57 | 44, 50, 56 | 3eqtr4d 2783 |
. . . . . 6
โข (๐ท โ โ+
โ (โโ(2 ยท ((๐ท / 2)โ2))) = (((โโ2) / 2)
ยท ๐ท)) |
58 | 39, 57 | eqtr3d 2775 |
. . . . 5
โข (๐ท โ โ+
โ (โโ(((๐ท
/ 2)โ2) + ((๐ท /
2)โ2))) = (((โโ2) / 2) ยท ๐ท)) |
59 | | 2lt4 12336 |
. . . . . . . . . 10
โข 2 <
4 |
60 | | 4re 12245 |
. . . . . . . . . . 11
โข 4 โ
โ |
61 | | 0re 11165 |
. . . . . . . . . . . 12
โข 0 โ
โ |
62 | | 4pos 12268 |
. . . . . . . . . . . 12
โข 0 <
4 |
63 | 61, 60, 62 | ltleii 11286 |
. . . . . . . . . . 11
โข 0 โค
4 |
64 | | sqrtlt 15155 |
. . . . . . . . . . 11
โข (((2
โ โ โง 0 โค 2) โง (4 โ โ โง 0 โค 4)) โ
(2 < 4 โ (โโ2) < (โโ4))) |
65 | 45, 47, 60, 63, 64 | mp4an 692 |
. . . . . . . . . 10
โข (2 < 4
โ (โโ2) < (โโ4)) |
66 | 59, 65 | mpbi 229 |
. . . . . . . . 9
โข
(โโ2) < (โโ4) |
67 | | 2pos 12264 |
. . . . . . . . . . 11
โข 0 <
2 |
68 | 45, 67 | sqrtpclii 15276 |
. . . . . . . . . 10
โข
(โโ2) โ โ |
69 | 60, 62 | sqrtpclii 15276 |
. . . . . . . . . 10
โข
(โโ4) โ โ |
70 | 68, 69, 45, 67 | ltdiv1ii 12092 |
. . . . . . . . 9
โข
((โโ2) < (โโ4) โ ((โโ2) / 2)
< ((โโ4) / 2)) |
71 | 66, 70 | mpbi 229 |
. . . . . . . 8
โข
((โโ2) / 2) < ((โโ4) / 2) |
72 | | sqrtsq 15163 |
. . . . . . . . . . 11
โข ((2
โ โ โง 0 โค 2) โ (โโ(2โ2)) =
2) |
73 | 45, 47, 72 | mp2an 691 |
. . . . . . . . . 10
โข
(โโ(2โ2)) = 2 |
74 | 73 | oveq1i 7371 |
. . . . . . . . 9
โข
((โโ(2โ2)) / 2) = (2 / 2) |
75 | | sq2 14110 |
. . . . . . . . . . 11
โข
(2โ2) = 4 |
76 | 75 | fveq2i 6849 |
. . . . . . . . . 10
โข
(โโ(2โ2)) = (โโ4) |
77 | 76 | oveq1i 7371 |
. . . . . . . . 9
โข
((โโ(2โ2)) / 2) = ((โโ4) /
2) |
78 | | 2div2e1 12302 |
. . . . . . . . 9
โข (2 / 2) =
1 |
79 | 74, 77, 78 | 3eqtr3i 2769 |
. . . . . . . 8
โข
((โโ4) / 2) = 1 |
80 | 71, 79 | breqtri 5134 |
. . . . . . 7
โข
((โโ2) / 2) < 1 |
81 | 46, 48 | resqrtcld 15311 |
. . . . . . . . 9
โข (๐ท โ โ+
โ (โโ2) โ โ) |
82 | 81 | rehalfcld 12408 |
. . . . . . . 8
โข (๐ท โ โ+
โ ((โโ2) / 2) โ โ) |
83 | | 1red 11164 |
. . . . . . . 8
โข (๐ท โ โ+
โ 1 โ โ) |
84 | | id 22 |
. . . . . . . 8
โข (๐ท โ โ+
โ ๐ท โ
โ+) |
85 | 82, 83, 84 | ltmul1d 13006 |
. . . . . . 7
โข (๐ท โ โ+
โ (((โโ2) / 2) < 1 โ (((โโ2) / 2) ยท
๐ท) < (1 ยท ๐ท))) |
86 | 80, 85 | mpbii 232 |
. . . . . 6
โข (๐ท โ โ+
โ (((โโ2) / 2) ยท ๐ท) < (1 ยท ๐ท)) |
87 | 53 | mullidd 11181 |
. . . . . 6
โข (๐ท โ โ+
โ (1 ยท ๐ท) =
๐ท) |
88 | 86, 87 | breqtrd 5135 |
. . . . 5
โข (๐ท โ โ+
โ (((โโ2) / 2) ยท ๐ท) < ๐ท) |
89 | 58, 88 | eqbrtrd 5131 |
. . . 4
โข (๐ท โ โ+
โ (โโ(((๐ท
/ 2)โ2) + ((๐ท /
2)โ2))) < ๐ท) |
90 | 11, 89 | syl 17 |
. . 3
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (โโ(((๐ท / 2)โ2) + ((๐ท / 2)โ2))) < ๐ท) |
91 | 10, 18, 12, 33, 90 | lttrd 11324 |
. 2
โข
(((((๐ โ
โ โง 0 โค ๐)
โง (๐ โ โ
โง 0 โค ๐)) โง
๐ท โ
โ+) โง (๐ < (๐ท / 2) โง ๐ < (๐ท / 2))) โ (โโ((๐โ2) + (๐โ2))) < ๐ท) |
92 | 91 | ex 414 |
1
โข ((((๐ โ โ โง 0 โค
๐) โง (๐ โ โ โง 0 โค ๐)) โง ๐ท โ โ+) โ ((๐ < (๐ท / 2) โง ๐ < (๐ท / 2)) โ (โโ((๐โ2) + (๐โ2))) < ๐ท)) |