Step | Hyp | Ref
| Expression |
1 | | fourierdlem68.f |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
2 | | fourierdlem68.xre |
. . . . . 6
β’ (π β π β β) |
3 | | fourierdlem68.a |
. . . . . 6
β’ (π β π΄ β β) |
4 | | fourierdlem68.b |
. . . . . 6
β’ (π β π΅ β β) |
5 | | fourierdlem68.fdv |
. . . . . 6
β’ (π β (β D (πΉ βΎ ((π + π΄)(,)(π + π΅)))):((π + π΄)(,)(π + π΅))βΆβ) |
6 | | ioossicc 13356 |
. . . . . . 7
β’ (π΄(,)π΅) β (π΄[,]π΅) |
7 | | fourierdlem68.ab |
. . . . . . 7
β’ (π β (π΄[,]π΅) β (-Ο[,]Ο)) |
8 | 6, 7 | sstrid 3956 |
. . . . . 6
β’ (π β (π΄(,)π΅) β (-Ο[,]Ο)) |
9 | | fourierdlem68.n0 |
. . . . . . 7
β’ (π β Β¬ 0 β (π΄[,]π΅)) |
10 | 6 | sseli 3941 |
. . . . . . 7
β’ (0 β
(π΄(,)π΅) β 0 β (π΄[,]π΅)) |
11 | 9, 10 | nsyl 140 |
. . . . . 6
β’ (π β Β¬ 0 β (π΄(,)π΅)) |
12 | | fourierdlem68.c |
. . . . . 6
β’ (π β πΆ β β) |
13 | | fourierdlem68.o |
. . . . . 6
β’ π = (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))) |
14 | 1, 2, 3, 4, 5, 8, 11, 12, 13 | fourierdlem57 44490 |
. . . . 5
β’ ((π β ((β D π):(π΄(,)π΅)βΆβ β§ (β D π) = (π β (π΄(,)π΅) β¦ (((((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )) Β· (2 Β· (sinβ(π / 2)))) β
((cosβ(π / 2))
Β· ((πΉβ(π + π )) β πΆ))) / ((2 Β· (sinβ(π / 2)))β2))))) β§
(β D (π β (π΄(,)π΅) β¦ (2 Β· (sinβ(π / 2))))) = (π β (π΄(,)π΅) β¦ (cosβ(π / 2)))) |
15 | 14 | simpli 485 |
. . . 4
β’ (π β ((β D π):(π΄(,)π΅)βΆβ β§ (β D π) = (π β (π΄(,)π΅) β¦ (((((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )) Β· (2 Β· (sinβ(π / 2)))) β
((cosβ(π / 2))
Β· ((πΉβ(π + π )) β πΆ))) / ((2 Β· (sinβ(π /
2)))β2))))) |
16 | 15 | simpld 496 |
. . 3
β’ (π β (β D π):(π΄(,)π΅)βΆβ) |
17 | 16 | fdmd 6680 |
. 2
β’ (π β dom (β D π) = (π΄(,)π΅)) |
18 | | eqid 2733 |
. . . . . 6
β’ (π‘ β (π΄[,]π΅) β¦ (2 Β· (sinβ(π‘ / 2)))) = (π‘ β (π΄[,]π΅) β¦ (2 Β· (sinβ(π‘ / 2)))) |
19 | | fourierdlem68.altb |
. . . . . . 7
β’ (π β π΄ < π΅) |
20 | 3, 4, 19 | ltled 11308 |
. . . . . 6
β’ (π β π΄ β€ π΅) |
21 | | 2re 12232 |
. . . . . . . . . . 11
β’ 2 β
β |
22 | 21 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π‘ β (π΄[,]π΅)) β 2 β β) |
23 | 3, 4 | iccssred 13357 |
. . . . . . . . . . . . 13
β’ (π β (π΄[,]π΅) β β) |
24 | 23 | sselda 3945 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β (π΄[,]π΅)) β π‘ β β) |
25 | 24 | rehalfcld 12405 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β (π΄[,]π΅)) β (π‘ / 2) β β) |
26 | 25 | resincld 16030 |
. . . . . . . . . 10
β’ ((π β§ π‘ β (π΄[,]π΅)) β (sinβ(π‘ / 2)) β β) |
27 | 22, 26 | remulcld 11190 |
. . . . . . . . 9
β’ ((π β§ π‘ β (π΄[,]π΅)) β (2 Β· (sinβ(π‘ / 2))) β
β) |
28 | | 2cnd 12236 |
. . . . . . . . . 10
β’ ((π β§ π‘ β (π΄[,]π΅)) β 2 β β) |
29 | 26 | recnd 11188 |
. . . . . . . . . 10
β’ ((π β§ π‘ β (π΄[,]π΅)) β (sinβ(π‘ / 2)) β β) |
30 | | 2ne0 12262 |
. . . . . . . . . . 11
β’ 2 β
0 |
31 | 30 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π‘ β (π΄[,]π΅)) β 2 β 0) |
32 | 7 | sselda 3945 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β (π΄[,]π΅)) β π‘ β (-Ο[,]Ο)) |
33 | | eqcom 2740 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ = 0 β 0 = π‘) |
34 | 33 | biimpi 215 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = 0 β 0 = π‘) |
35 | 34 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π‘ β (π΄[,]π΅) β§ π‘ = 0) β 0 = π‘) |
36 | | simpl 484 |
. . . . . . . . . . . . . . 15
β’ ((π‘ β (π΄[,]π΅) β§ π‘ = 0) β π‘ β (π΄[,]π΅)) |
37 | 35, 36 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ ((π‘ β (π΄[,]π΅) β§ π‘ = 0) β 0 β (π΄[,]π΅)) |
38 | 37 | adantll 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π‘ β (π΄[,]π΅)) β§ π‘ = 0) β 0 β (π΄[,]π΅)) |
39 | 9 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π‘ β (π΄[,]π΅)) β§ π‘ = 0) β Β¬ 0 β (π΄[,]π΅)) |
40 | 38, 39 | pm2.65da 816 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β (π΄[,]π΅)) β Β¬ π‘ = 0) |
41 | 40 | neqned 2947 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β (π΄[,]π΅)) β π‘ β 0) |
42 | | fourierdlem44 44478 |
. . . . . . . . . . 11
β’ ((π‘ β (-Ο[,]Ο) β§
π‘ β 0) β
(sinβ(π‘ / 2)) β
0) |
43 | 32, 41, 42 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π‘ β (π΄[,]π΅)) β (sinβ(π‘ / 2)) β 0) |
44 | 28, 29, 31, 43 | mulne0d 11812 |
. . . . . . . . 9
β’ ((π β§ π‘ β (π΄[,]π΅)) β (2 Β· (sinβ(π‘ / 2))) β 0) |
45 | | eldifsn 4748 |
. . . . . . . . 9
β’ ((2
Β· (sinβ(π‘ /
2))) β (β β {0}) β ((2 Β· (sinβ(π‘ / 2))) β β β§ (2
Β· (sinβ(π‘ /
2))) β 0)) |
46 | 27, 44, 45 | sylanbrc 584 |
. . . . . . . 8
β’ ((π β§ π‘ β (π΄[,]π΅)) β (2 Β· (sinβ(π‘ / 2))) β (β β
{0})) |
47 | 46, 18 | fmptd 7063 |
. . . . . . 7
β’ (π β (π‘ β (π΄[,]π΅) β¦ (2 Β· (sinβ(π‘ / 2)))):(π΄[,]π΅)βΆ(β β
{0})) |
48 | | difss 4092 |
. . . . . . . . . 10
β’ (β
β {0}) β β |
49 | | ax-resscn 11113 |
. . . . . . . . . 10
β’ β
β β |
50 | 48, 49 | sstri 3954 |
. . . . . . . . 9
β’ (β
β {0}) β β |
51 | 50 | a1i 11 |
. . . . . . . 8
β’ (π β (β β {0})
β β) |
52 | 23, 49 | sstrdi 3957 |
. . . . . . . . . 10
β’ (π β (π΄[,]π΅) β β) |
53 | | 2cnd 12236 |
. . . . . . . . . 10
β’ (π β 2 β
β) |
54 | | ssid 3967 |
. . . . . . . . . . 11
β’ β
β β |
55 | 54 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β
β) |
56 | 52, 53, 55 | constcncfg 44199 |
. . . . . . . . 9
β’ (π β (π‘ β (π΄[,]π΅) β¦ 2) β ((π΄[,]π΅)βcnββ)) |
57 | | sincn 25819 |
. . . . . . . . . . 11
β’ sin
β (ββcnββ) |
58 | 57 | a1i 11 |
. . . . . . . . . 10
β’ (π β sin β
(ββcnββ)) |
59 | 52, 55 | idcncfg 44200 |
. . . . . . . . . . 11
β’ (π β (π‘ β (π΄[,]π΅) β¦ π‘) β ((π΄[,]π΅)βcnββ)) |
60 | | eldifsn 4748 |
. . . . . . . . . . . . . 14
β’ (2 β
(β β {0}) β (2 β β β§ 2 β
0)) |
61 | 28, 31, 60 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β (π΄[,]π΅)) β 2 β (β β
{0})) |
62 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π‘ β (π΄[,]π΅) β¦ 2) = (π‘ β (π΄[,]π΅) β¦ 2) |
63 | 61, 62 | fmptd 7063 |
. . . . . . . . . . . 12
β’ (π β (π‘ β (π΄[,]π΅) β¦ 2):(π΄[,]π΅)βΆ(β β
{0})) |
64 | | difssd 4093 |
. . . . . . . . . . . . 13
β’ (π β (β β {0})
β β) |
65 | | cncfcdm 24277 |
. . . . . . . . . . . . 13
β’
(((β β {0}) β β β§ (π‘ β (π΄[,]π΅) β¦ 2) β ((π΄[,]π΅)βcnββ)) β ((π‘ β (π΄[,]π΅) β¦ 2) β ((π΄[,]π΅)βcnβ(β β {0})) β (π‘ β (π΄[,]π΅) β¦ 2):(π΄[,]π΅)βΆ(β β
{0}))) |
66 | 64, 56, 65 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ((π‘ β (π΄[,]π΅) β¦ 2) β ((π΄[,]π΅)βcnβ(β β {0})) β (π‘ β (π΄[,]π΅) β¦ 2):(π΄[,]π΅)βΆ(β β
{0}))) |
67 | 63, 66 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β (π‘ β (π΄[,]π΅) β¦ 2) β ((π΄[,]π΅)βcnβ(β β {0}))) |
68 | 59, 67 | divcncf 24827 |
. . . . . . . . . 10
β’ (π β (π‘ β (π΄[,]π΅) β¦ (π‘ / 2)) β ((π΄[,]π΅)βcnββ)) |
69 | 58, 68 | cncfmpt1f 24293 |
. . . . . . . . 9
β’ (π β (π‘ β (π΄[,]π΅) β¦ (sinβ(π‘ / 2))) β ((π΄[,]π΅)βcnββ)) |
70 | 56, 69 | mulcncf 24826 |
. . . . . . . 8
β’ (π β (π‘ β (π΄[,]π΅) β¦ (2 Β· (sinβ(π‘ / 2)))) β ((π΄[,]π΅)βcnββ)) |
71 | | cncfcdm 24277 |
. . . . . . . 8
β’
(((β β {0}) β β β§ (π‘ β (π΄[,]π΅) β¦ (2 Β· (sinβ(π‘ / 2)))) β ((π΄[,]π΅)βcnββ)) β ((π‘ β (π΄[,]π΅) β¦ (2 Β· (sinβ(π‘ / 2)))) β ((π΄[,]π΅)βcnβ(β β {0})) β (π‘ β (π΄[,]π΅) β¦ (2 Β· (sinβ(π‘ / 2)))):(π΄[,]π΅)βΆ(β β
{0}))) |
72 | 51, 70, 71 | syl2anc 585 |
. . . . . . 7
β’ (π β ((π‘ β (π΄[,]π΅) β¦ (2 Β· (sinβ(π‘ / 2)))) β ((π΄[,]π΅)βcnβ(β β {0})) β (π‘ β (π΄[,]π΅) β¦ (2 Β· (sinβ(π‘ / 2)))):(π΄[,]π΅)βΆ(β β
{0}))) |
73 | 47, 72 | mpbird 257 |
. . . . . 6
β’ (π β (π‘ β (π΄[,]π΅) β¦ (2 Β· (sinβ(π‘ / 2)))) β ((π΄[,]π΅)βcnβ(β β {0}))) |
74 | 18, 3, 4, 20, 73 | cncficcgt0 44215 |
. . . . 5
β’ (π β βπ β β+ βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ /
2))))) |
75 | | reelprrecn 11148 |
. . . . . . . 8
β’ β
β {β, β} |
76 | 75 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β β β {β, β}) |
77 | 1 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β πΉ:ββΆβ) |
78 | 2 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
79 | | elioore 13300 |
. . . . . . . . . . . . 13
β’ (π β (π΄(,)π΅) β π β β) |
80 | 79 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
81 | 78, 80 | readdcld 11189 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) β β) |
82 | 77, 81 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (πΉβ(π + π )) β β) |
83 | 12 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β πΆ β β) |
84 | 82, 83 | resubcld 11588 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β ((πΉβ(π + π )) β πΆ) β β) |
85 | 84 | recnd 11188 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β ((πΉβ(π + π )) β πΆ) β β) |
86 | 85 | 3ad2antl1 1186 |
. . . . . . 7
β’ (((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β§ π β (π΄(,)π΅)) β ((πΉβ(π + π )) β πΆ) β β) |
87 | 75 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β {β,
β}) |
88 | 82 | recnd 11188 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (πΉβ(π + π )) β β) |
89 | 5 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β (β D (πΉ βΎ ((π + π΄)(,)(π + π΅)))):((π + π΄)(,)(π + π΅))βΆβ) |
90 | 2, 3 | readdcld 11189 |
. . . . . . . . . . . . . 14
β’ (π β (π + π΄) β β) |
91 | 90 | rexrd 11210 |
. . . . . . . . . . . . 13
β’ (π β (π + π΄) β
β*) |
92 | 91 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(,)π΅)) β (π + π΄) β
β*) |
93 | 2, 4 | readdcld 11189 |
. . . . . . . . . . . . . 14
β’ (π β (π + π΅) β β) |
94 | 93 | rexrd 11210 |
. . . . . . . . . . . . 13
β’ (π β (π + π΅) β
β*) |
95 | 94 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(,)π΅)) β (π + π΅) β
β*) |
96 | 3 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β π΄ β β) |
97 | 96 | rexrd 11210 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄(,)π΅)) β π΄ β
β*) |
98 | 4 | rexrd 11210 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β
β*) |
99 | 98 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄(,)π΅)) β π΅ β
β*) |
100 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄(,)π΅)) β π β (π΄(,)π΅)) |
101 | | ioogtlb 43819 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β*
β§ π΅ β
β* β§ π
β (π΄(,)π΅)) β π΄ < π ) |
102 | 97, 99, 100, 101 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β π΄ < π ) |
103 | 96, 80, 78, 102 | ltadd2dd 11319 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(,)π΅)) β (π + π΄) < (π + π )) |
104 | 4 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β π΅ β β) |
105 | | iooltub 43834 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β*
β§ π΅ β
β* β§ π
β (π΄(,)π΅)) β π < π΅) |
106 | 97, 99, 100, 105 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β π < π΅) |
107 | 80, 104, 78, 106 | ltadd2dd 11319 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) < (π + π΅)) |
108 | 92, 95, 81, 103, 107 | eliood 43822 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) β ((π + π΄)(,)(π + π΅))) |
109 | 89, 108 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )) β β) |
110 | | eqid 2733 |
. . . . . . . . . . 11
β’ (β
D (πΉ βΎ ((π + π΄)(,)(π + π΅)))) = (β D (πΉ βΎ ((π + π΄)(,)(π + π΅)))) |
111 | 1, 2, 3, 4, 110, 5 | fourierdlem28 44462 |
. . . . . . . . . 10
β’ (π β (β D (π β (π΄(,)π΅) β¦ (πΉβ(π + π )))) = (π β (π΄(,)π΅) β¦ ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )))) |
112 | 83 | recnd 11188 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β πΆ β β) |
113 | | 0red 11163 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β 0 β β) |
114 | | iooretop 24145 |
. . . . . . . . . . . . 13
β’ (π΄(,)π΅) β (topGenβran
(,)) |
115 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(TopOpenββfld) =
(TopOpenββfld) |
116 | 115 | tgioo2 24182 |
. . . . . . . . . . . . 13
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
117 | 114, 116 | eleqtri 2832 |
. . . . . . . . . . . 12
β’ (π΄(,)π΅) β
((TopOpenββfld) βΎt
β) |
118 | 117 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π΄(,)π΅) β
((TopOpenββfld) βΎt
β)) |
119 | 12 | recnd 11188 |
. . . . . . . . . . 11
β’ (π β πΆ β β) |
120 | 87, 118, 119 | dvmptconst 44242 |
. . . . . . . . . 10
β’ (π β (β D (π β (π΄(,)π΅) β¦ πΆ)) = (π β (π΄(,)π΅) β¦ 0)) |
121 | 87, 88, 109, 111, 112, 113, 120 | dvmptsub 25347 |
. . . . . . . . 9
β’ (π β (β D (π β (π΄(,)π΅) β¦ ((πΉβ(π + π )) β πΆ))) = (π β (π΄(,)π΅) β¦ (((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )) β 0))) |
122 | 109 | recnd 11188 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )) β β) |
123 | 122 | subid1d 11506 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )) β 0) = ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π ))) |
124 | 123 | mpteq2dva 5206 |
. . . . . . . . 9
β’ (π β (π β (π΄(,)π΅) β¦ (((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )) β 0)) = (π β (π΄(,)π΅) β¦ ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )))) |
125 | 121, 124 | eqtrd 2773 |
. . . . . . . 8
β’ (π β (β D (π β (π΄(,)π΅) β¦ ((πΉβ(π + π )) β πΆ))) = (π β (π΄(,)π΅) β¦ ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )))) |
126 | 125 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β (β D (π β
(π΄(,)π΅) β¦ ((πΉβ(π + π )) β πΆ))) = (π β (π΄(,)π΅) β¦ ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )))) |
127 | 122 | 3ad2antl1 1186 |
. . . . . . 7
β’ (((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β§ π β (π΄(,)π΅)) β ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )) β β) |
128 | | 2cnd 12236 |
. . . . . . . . 9
β’ (π β (π΄(,)π΅) β 2 β β) |
129 | 79 | recnd 11188 |
. . . . . . . . . . 11
β’ (π β (π΄(,)π΅) β π β β) |
130 | 129 | halfcld 12403 |
. . . . . . . . . 10
β’ (π β (π΄(,)π΅) β (π / 2) β β) |
131 | 130 | sincld 16017 |
. . . . . . . . 9
β’ (π β (π΄(,)π΅) β (sinβ(π / 2)) β β) |
132 | 128, 131 | mulcld 11180 |
. . . . . . . 8
β’ (π β (π΄(,)π΅) β (2 Β· (sinβ(π / 2))) β
β) |
133 | 132 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β§ π β (π΄(,)π΅)) β (2 Β· (sinβ(π / 2))) β
β) |
134 | | fourierdlem68.e |
. . . . . . . 8
β’ (π β πΈ β β) |
135 | 134 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β πΈ β
β) |
136 | | 1re 11160 |
. . . . . . . . 9
β’ 1 β
β |
137 | 21, 136 | remulcli 11176 |
. . . . . . . 8
β’ (2
Β· 1) β β |
138 | 137 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β (2 Β· 1) β β) |
139 | | 1red 11161 |
. . . . . . 7
β’ ((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β 1 β β) |
140 | | fourierdlem68.d |
. . . . . . . . 9
β’ (π β π· β β) |
141 | 119 | abscld 15327 |
. . . . . . . . 9
β’ (π β (absβπΆ) β
β) |
142 | 140, 141 | readdcld 11189 |
. . . . . . . 8
β’ (π β (π· + (absβπΆ)) β β) |
143 | 142 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β (π· +
(absβπΆ)) β
β) |
144 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β π) |
145 | 144, 108 | jca 513 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β (π β§ (π + π ) β ((π + π΄)(,)(π + π΅)))) |
146 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π‘ = (π + π ) β (π‘ β ((π + π΄)(,)(π + π΅)) β (π + π ) β ((π + π΄)(,)(π + π΅)))) |
147 | 146 | anbi2d 630 |
. . . . . . . . . . 11
β’ (π‘ = (π + π ) β ((π β§ π‘ β ((π + π΄)(,)(π + π΅))) β (π β§ (π + π ) β ((π + π΄)(,)(π + π΅))))) |
148 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π‘ = (π + π ) β ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))βπ‘) = ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π ))) |
149 | 148 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π‘ = (π + π ) β (absβ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))βπ‘)) = (absβ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )))) |
150 | 149 | breq1d 5116 |
. . . . . . . . . . 11
β’ (π‘ = (π + π ) β ((absβ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))βπ‘)) β€ πΈ β (absβ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π ))) β€ πΈ)) |
151 | 147, 150 | imbi12d 345 |
. . . . . . . . . 10
β’ (π‘ = (π + π ) β (((π β§ π‘ β ((π + π΄)(,)(π + π΅))) β (absβ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))βπ‘)) β€ πΈ) β ((π β§ (π + π ) β ((π + π΄)(,)(π + π΅))) β (absβ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π ))) β€ πΈ))) |
152 | | fourierdlem68.fdvbd |
. . . . . . . . . 10
β’ ((π β§ π‘ β ((π + π΄)(,)(π + π΅))) β (absβ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))βπ‘)) β€ πΈ) |
153 | 151, 152 | vtoclg 3524 |
. . . . . . . . 9
β’ ((π + π ) β β β ((π β§ (π + π ) β ((π + π΄)(,)(π + π΅))) β (absβ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π ))) β€ πΈ)) |
154 | 81, 145, 153 | sylc 65 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β (absβ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π ))) β€ πΈ) |
155 | 154 | 3ad2antl1 1186 |
. . . . . . 7
β’ (((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β§ π β (π΄(,)π΅)) β (absβ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π ))) β€ πΈ) |
156 | 128, 131 | absmuld 15345 |
. . . . . . . . 9
β’ (π β (π΄(,)π΅) β (absβ(2 Β·
(sinβ(π / 2)))) =
((absβ2) Β· (absβ(sinβ(π / 2))))) |
157 | | 0le2 12260 |
. . . . . . . . . . . 12
β’ 0 β€
2 |
158 | | absid 15187 |
. . . . . . . . . . . 12
β’ ((2
β β β§ 0 β€ 2) β (absβ2) = 2) |
159 | 21, 157, 158 | mp2an 691 |
. . . . . . . . . . 11
β’
(absβ2) = 2 |
160 | 159 | oveq1i 7368 |
. . . . . . . . . 10
β’
((absβ2) Β· (absβ(sinβ(π / 2)))) = (2 Β·
(absβ(sinβ(π /
2)))) |
161 | 131 | abscld 15327 |
. . . . . . . . . . 11
β’ (π β (π΄(,)π΅) β (absβ(sinβ(π / 2))) β
β) |
162 | | 1red 11161 |
. . . . . . . . . . 11
β’ (π β (π΄(,)π΅) β 1 β β) |
163 | 21 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π΄(,)π΅) β 2 β β) |
164 | 157 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π΄(,)π΅) β 0 β€ 2) |
165 | 79 | rehalfcld 12405 |
. . . . . . . . . . . 12
β’ (π β (π΄(,)π΅) β (π / 2) β β) |
166 | | abssinbd 43616 |
. . . . . . . . . . . 12
β’ ((π / 2) β β β
(absβ(sinβ(π /
2))) β€ 1) |
167 | 165, 166 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π΄(,)π΅) β (absβ(sinβ(π / 2))) β€ 1) |
168 | 161, 162,
163, 164, 167 | lemul2ad 12100 |
. . . . . . . . . 10
β’ (π β (π΄(,)π΅) β (2 Β·
(absβ(sinβ(π /
2)))) β€ (2 Β· 1)) |
169 | 160, 168 | eqbrtrid 5141 |
. . . . . . . . 9
β’ (π β (π΄(,)π΅) β ((absβ2) Β·
(absβ(sinβ(π /
2)))) β€ (2 Β· 1)) |
170 | 156, 169 | eqbrtrd 5128 |
. . . . . . . 8
β’ (π β (π΄(,)π΅) β (absβ(2 Β·
(sinβ(π / 2)))) β€
(2 Β· 1)) |
171 | 170 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β§ π β (π΄(,)π΅)) β (absβ(2 Β·
(sinβ(π / 2)))) β€
(2 Β· 1)) |
172 | | abscosbd 43599 |
. . . . . . . . 9
β’ ((π / 2) β β β
(absβ(cosβ(π /
2))) β€ 1) |
173 | 100, 165,
172 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β (absβ(cosβ(π / 2))) β€ 1) |
174 | 173 | 3ad2antl1 1186 |
. . . . . . 7
β’ (((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β§ π β (π΄(,)π΅)) β (absβ(cosβ(π / 2))) β€ 1) |
175 | 85 | abscld 15327 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β (absβ((πΉβ(π + π )) β πΆ)) β β) |
176 | 88 | abscld 15327 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (absβ(πΉβ(π + π ))) β β) |
177 | 112 | abscld 15327 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (absβπΆ) β β) |
178 | 176, 177 | readdcld 11189 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β ((absβ(πΉβ(π + π ))) + (absβπΆ)) β β) |
179 | 140 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β π· β β) |
180 | 179, 177 | readdcld 11189 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β (π· + (absβπΆ)) β β) |
181 | 88, 112 | abs2dif2d 15349 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β (absβ((πΉβ(π + π )) β πΆ)) β€ ((absβ(πΉβ(π + π ))) + (absβπΆ))) |
182 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
β’ (π‘ = (π + π ) β (πΉβπ‘) = (πΉβ(π + π ))) |
183 | 182 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ (π‘ = (π + π ) β (absβ(πΉβπ‘)) = (absβ(πΉβ(π + π )))) |
184 | 183 | breq1d 5116 |
. . . . . . . . . . . . 13
β’ (π‘ = (π + π ) β ((absβ(πΉβπ‘)) β€ π· β (absβ(πΉβ(π + π ))) β€ π·)) |
185 | 147, 184 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π‘ = (π + π ) β (((π β§ π‘ β ((π + π΄)(,)(π + π΅))) β (absβ(πΉβπ‘)) β€ π·) β ((π β§ (π + π ) β ((π + π΄)(,)(π + π΅))) β (absβ(πΉβ(π + π ))) β€ π·))) |
186 | | fourierdlem68.fbd |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β ((π + π΄)(,)(π + π΅))) β (absβ(πΉβπ‘)) β€ π·) |
187 | 185, 186 | vtoclg 3524 |
. . . . . . . . . . 11
β’ ((π + π ) β ((π + π΄)(,)(π + π΅)) β ((π β§ (π + π ) β ((π + π΄)(,)(π + π΅))) β (absβ(πΉβ(π + π ))) β€ π·)) |
188 | 108, 145,
187 | sylc 65 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (absβ(πΉβ(π + π ))) β€ π·) |
189 | 176, 179,
177, 188 | leadd1dd 11774 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β ((absβ(πΉβ(π + π ))) + (absβπΆ)) β€ (π· + (absβπΆ))) |
190 | 175, 178,
180, 181, 189 | letrd 11317 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β (absβ((πΉβ(π + π )) β πΆ)) β€ (π· + (absβπΆ))) |
191 | 190 | 3ad2antl1 1186 |
. . . . . . 7
β’ (((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β§ π β (π΄(,)π΅)) β (absβ((πΉβ(π + π )) β πΆ)) β€ (π· + (absβπΆ))) |
192 | 14 | simpri 487 |
. . . . . . . 8
β’ (β
D (π β (π΄(,)π΅) β¦ (2 Β· (sinβ(π / 2))))) = (π β (π΄(,)π΅) β¦ (cosβ(π / 2))) |
193 | 192 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β (β D (π β
(π΄(,)π΅) β¦ (2 Β· (sinβ(π / 2))))) = (π β (π΄(,)π΅) β¦ (cosβ(π / 2)))) |
194 | 130 | coscld 16018 |
. . . . . . . 8
β’ (π β (π΄(,)π΅) β (cosβ(π / 2)) β β) |
195 | 194 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β§ π β (π΄(,)π΅)) β (cosβ(π / 2)) β β) |
196 | | simp2 1138 |
. . . . . . 7
β’ ((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β π β
β+) |
197 | | oveq1 7365 |
. . . . . . . . . . . . . 14
β’ (π‘ = π β (π‘ / 2) = (π / 2)) |
198 | 197 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (sinβ(π‘ / 2)) = (sinβ(π / 2))) |
199 | 198 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π‘ = π β (2 Β· (sinβ(π‘ / 2))) = (2 Β·
(sinβ(π /
2)))) |
200 | 199 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π‘ = π β (absβ(2 Β·
(sinβ(π‘ / 2)))) =
(absβ(2 Β· (sinβ(π / 2))))) |
201 | 200 | breq2d 5118 |
. . . . . . . . . 10
β’ (π‘ = π β (π β€ (absβ(2 Β·
(sinβ(π‘ / 2))))
β π β€ (absβ(2
Β· (sinβ(π /
2)))))) |
202 | 201 | cbvralvw 3224 |
. . . . . . . . 9
β’
(βπ‘ β
(π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2))))
β βπ β
(π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π /
2))))) |
203 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π π |
204 | | nfra1 3266 |
. . . . . . . . . . 11
β’
β²π βπ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π /
2)))) |
205 | 203, 204 | nfan 1903 |
. . . . . . . . . 10
β’
β²π (π β§ βπ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π /
2))))) |
206 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ βπ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π / 2)))))
β§ π β (π΄(,)π΅)) β βπ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π /
2))))) |
207 | 6, 100 | sselid 3943 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β π β (π΄[,]π΅)) |
208 | 207 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ βπ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π / 2)))))
β§ π β (π΄(,)π΅)) β π β (π΄[,]π΅)) |
209 | | rspa 3230 |
. . . . . . . . . . . 12
β’
((βπ β
(π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π / 2)))) β§
π β (π΄[,]π΅)) β π β€ (absβ(2 Β·
(sinβ(π /
2))))) |
210 | 206, 208,
209 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ βπ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π / 2)))))
β§ π β (π΄(,)π΅)) β π β€ (absβ(2 Β·
(sinβ(π /
2))))) |
211 | 210 | ex 414 |
. . . . . . . . . 10
β’ ((π β§ βπ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π / 2)))))
β (π β (π΄(,)π΅) β π β€ (absβ(2 Β·
(sinβ(π /
2)))))) |
212 | 205, 211 | ralrimi 3239 |
. . . . . . . . 9
β’ ((π β§ βπ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π / 2)))))
β βπ β
(π΄(,)π΅)π β€ (absβ(2 Β·
(sinβ(π /
2))))) |
213 | 202, 212 | sylan2b 595 |
. . . . . . . 8
β’ ((π β§ βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β βπ β
(π΄(,)π΅)π β€ (absβ(2 Β·
(sinβ(π /
2))))) |
214 | 213 | 3adant2 1132 |
. . . . . . 7
β’ ((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β βπ β
(π΄(,)π΅)π β€ (absβ(2 Β·
(sinβ(π /
2))))) |
215 | | eqid 2733 |
. . . . . . 7
β’ (β
D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2)))))) = (β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2)))))) |
216 | 76, 86, 126, 127, 133, 135, 138, 139, 143, 155, 171, 174, 191, 193, 195, 196, 214, 215 | dvdivbd 44250 |
. . . . . 6
β’ ((π β§ π β β+ β§
βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2)))))
β βπ β
β βπ β
(π΄(,)π΅)(absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) β€ π) |
217 | 216 | rexlimdv3a 3153 |
. . . . 5
β’ (π β (βπ β β+ βπ‘ β (π΄[,]π΅)π β€ (absβ(2 Β·
(sinβ(π‘ / 2))))
β βπ β
β βπ β
(π΄(,)π΅)(absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) β€ π)) |
218 | 74, 217 | mpd 15 |
. . . 4
β’ (π β βπ β β βπ β (π΄(,)π΅)(absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) β€ π) |
219 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π β |
220 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π
D |
221 | | nfmpt1 5214 |
. . . . . . . . . 10
β’
β²π (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))) |
222 | 13, 221 | nfcxfr 2902 |
. . . . . . . . 9
β’
β²π π |
223 | 219, 220,
222 | nfov 7388 |
. . . . . . . 8
β’
β²π (β D π) |
224 | 223 | nfdm 5907 |
. . . . . . 7
β’
β²π dom
(β D π) |
225 | | nfcv 2904 |
. . . . . . 7
β’
β²π (π΄(,)π΅) |
226 | 224, 225 | raleqf 3327 |
. . . . . 6
β’ (dom
(β D π) = (π΄(,)π΅) β (βπ β dom (β D π)(absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) β€ π β βπ β (π΄(,)π΅)(absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) β€ π)) |
227 | 17, 226 | syl 17 |
. . . . 5
β’ (π β (βπ β dom (β D π)(absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) β€ π β βπ β (π΄(,)π΅)(absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) β€ π)) |
228 | 227 | rexbidv 3172 |
. . . 4
β’ (π β (βπ β β βπ β dom (β D π)(absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) β€ π β βπ β β βπ β (π΄(,)π΅)(absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) β€ π)) |
229 | 218, 228 | mpbird 257 |
. . 3
β’ (π β βπ β β βπ β dom (β D π)(absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) β€ π) |
230 | 13 | a1i 11 |
. . . . . . . 8
β’ (π β π = (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2)))))) |
231 | 230 | oveq2d 7374 |
. . . . . . 7
β’ (π β (β D π) = (β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))) |
232 | 231 | fveq1d 6845 |
. . . . . 6
β’ (π β ((β D π)βπ ) = ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) |
233 | 232 | fveq2d 6847 |
. . . . 5
β’ (π β (absβ((β D
π)βπ )) = (absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ ))) |
234 | 233 | breq1d 5116 |
. . . 4
β’ (π β ((absβ((β D
π)βπ )) β€ π β (absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) β€ π)) |
235 | 234 | rexralbidv 3211 |
. . 3
β’ (π β (βπ β β βπ β dom (β D π)(absβ((β D π)βπ )) β€ π β βπ β β βπ β dom (β D π)(absβ((β D (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))))βπ )) β€ π)) |
236 | 229, 235 | mpbird 257 |
. 2
β’ (π β βπ β β βπ β dom (β D π)(absβ((β D π)βπ )) β€ π) |
237 | 17, 236 | jca 513 |
1
β’ (π β (dom (β D π) = (π΄(,)π΅) β§ βπ β β βπ β dom (β D π)(absβ((β D π)βπ )) β€ π)) |