Step | Hyp | Ref
| Expression |
1 | | simprr 772 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ฆ โ ๐ท) |
2 | | efif1olem1.1 |
. . . . . . 7
โข ๐ท = (๐ด(,](๐ด + (2 ยท ฯ))) |
3 | 1, 2 | eleqtrdi 2844 |
. . . . . 6
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ฆ โ (๐ด(,](๐ด + (2 ยท ฯ)))) |
4 | | rexr 11206 |
. . . . . . 7
โข (๐ด โ โ โ ๐ด โ
โ*) |
5 | | simpl 484 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ด โ โ) |
6 | | 2re 12232 |
. . . . . . . . 9
โข 2 โ
โ |
7 | | pire 25831 |
. . . . . . . . 9
โข ฯ
โ โ |
8 | 6, 7 | remulcli 11176 |
. . . . . . . 8
โข (2
ยท ฯ) โ โ |
9 | | readdcl 11139 |
. . . . . . . 8
โข ((๐ด โ โ โง (2
ยท ฯ) โ โ) โ (๐ด + (2 ยท ฯ)) โ
โ) |
10 | 5, 8, 9 | sylancl 587 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ (๐ด + (2 ยท ฯ)) โ
โ) |
11 | | elioc2 13333 |
. . . . . . 7
โข ((๐ด โ โ*
โง (๐ด + (2 ยท
ฯ)) โ โ) โ (๐ฆ โ (๐ด(,](๐ด + (2 ยท ฯ))) โ (๐ฆ โ โ โง ๐ด < ๐ฆ โง ๐ฆ โค (๐ด + (2 ยท ฯ))))) |
12 | 4, 10, 11 | syl2an2r 684 |
. . . . . 6
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ (๐ฆ โ (๐ด(,](๐ด + (2 ยท ฯ))) โ (๐ฆ โ โ โง ๐ด < ๐ฆ โง ๐ฆ โค (๐ด + (2 ยท ฯ))))) |
13 | 3, 12 | mpbid 231 |
. . . . 5
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ (๐ฆ โ โ โง ๐ด < ๐ฆ โง ๐ฆ โค (๐ด + (2 ยท ฯ)))) |
14 | 13 | simp1d 1143 |
. . . 4
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ฆ โ โ) |
15 | | simprl 770 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ฅ โ ๐ท) |
16 | 15, 2 | eleqtrdi 2844 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ฅ โ (๐ด(,](๐ด + (2 ยท ฯ)))) |
17 | | elioc2 13333 |
. . . . . . . 8
โข ((๐ด โ โ*
โง (๐ด + (2 ยท
ฯ)) โ โ) โ (๐ฅ โ (๐ด(,](๐ด + (2 ยท ฯ))) โ (๐ฅ โ โ โง ๐ด < ๐ฅ โง ๐ฅ โค (๐ด + (2 ยท ฯ))))) |
18 | 4, 10, 17 | syl2an2r 684 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ (๐ฅ โ (๐ด(,](๐ด + (2 ยท ฯ))) โ (๐ฅ โ โ โง ๐ด < ๐ฅ โง ๐ฅ โค (๐ด + (2 ยท ฯ))))) |
19 | 16, 18 | mpbid 231 |
. . . . . 6
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ (๐ฅ โ โ โง ๐ด < ๐ฅ โง ๐ฅ โค (๐ด + (2 ยท ฯ)))) |
20 | 19 | simp1d 1143 |
. . . . 5
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ฅ โ โ) |
21 | | readdcl 11139 |
. . . . 5
โข ((๐ฅ โ โ โง (2
ยท ฯ) โ โ) โ (๐ฅ + (2 ยท ฯ)) โ
โ) |
22 | 20, 8, 21 | sylancl 587 |
. . . 4
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ (๐ฅ + (2 ยท ฯ)) โ
โ) |
23 | 13 | simp3d 1145 |
. . . 4
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ฆ โค (๐ด + (2 ยท ฯ))) |
24 | 8 | a1i 11 |
. . . . 5
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ (2 ยท ฯ) โ
โ) |
25 | 19 | simp2d 1144 |
. . . . 5
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ด < ๐ฅ) |
26 | 5, 20, 24, 25 | ltadd1dd 11771 |
. . . 4
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ (๐ด + (2 ยท ฯ)) < (๐ฅ + (2 ยท
ฯ))) |
27 | 14, 10, 22, 23, 26 | lelttrd 11318 |
. . 3
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ฆ < (๐ฅ + (2 ยท ฯ))) |
28 | 14, 24, 20 | ltsubaddd 11756 |
. . 3
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ((๐ฆ โ (2 ยท ฯ)) < ๐ฅ โ ๐ฆ < (๐ฅ + (2 ยท ฯ)))) |
29 | 27, 28 | mpbird 257 |
. 2
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ (๐ฆ โ (2 ยท ฯ)) < ๐ฅ) |
30 | | readdcl 11139 |
. . . 4
โข ((๐ฆ โ โ โง (2
ยท ฯ) โ โ) โ (๐ฆ + (2 ยท ฯ)) โ
โ) |
31 | 14, 8, 30 | sylancl 587 |
. . 3
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ (๐ฆ + (2 ยท ฯ)) โ
โ) |
32 | 19 | simp3d 1145 |
. . 3
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ฅ โค (๐ด + (2 ยท ฯ))) |
33 | 13 | simp2d 1144 |
. . . 4
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ด < ๐ฆ) |
34 | 5, 14, 24, 33 | ltadd1dd 11771 |
. . 3
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ (๐ด + (2 ยท ฯ)) < (๐ฆ + (2 ยท
ฯ))) |
35 | 20, 10, 31, 32, 34 | lelttrd 11318 |
. 2
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ๐ฅ < (๐ฆ + (2 ยท ฯ))) |
36 | 20, 14, 24 | absdifltd 15324 |
. 2
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ ((absโ(๐ฅ โ ๐ฆ)) < (2 ยท ฯ) โ ((๐ฆ โ (2 ยท ฯ)) <
๐ฅ โง ๐ฅ < (๐ฆ + (2 ยท ฯ))))) |
37 | 29, 35, 36 | mpbir2and 712 |
1
โข ((๐ด โ โ โง (๐ฅ โ ๐ท โง ๐ฆ โ ๐ท)) โ (absโ(๐ฅ โ ๐ฆ)) < (2 ยท ฯ)) |