Metamath Proof Explorer

Theorem fourierdlem39

Description: Integration by parts of S. ( A (,) B ) ( ( Fx ) x. ( sin( R x. x ) ) ) _d x (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem39.a 
|- ( ph -> A e. RR )
fourierdlem39.b 
|- ( ph -> B e. RR )
fourierdlem39.aleb 
|- ( ph -> A <_ B )
fourierdlem39.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
fourierdlem39.g 
|- G = ( RR _D F )
fourierdlem39.gcn 
|- ( ph -> G e. ( ( A (,) B ) -cn-> CC ) )
fourierdlem39.gbd 
|- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y )
fourierdlem39.r 
|- ( ph -> R e. RR+ )
Assertion fourierdlem39 
|- ( ph -> S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) _d x = ( ( ( ( F ` B ) x. -u ( ( cos ` ( R x. B ) ) / R ) ) - ( ( F ` A ) x. -u ( ( cos ` ( R x. A ) ) / R ) ) ) - S. ( A (,) B ) ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) _d x ) )

Proof

Step Hyp Ref Expression
1 fourierdlem39.a 
 |-  ( ph -> A e. RR )
2 fourierdlem39.b 
 |-  ( ph -> B e. RR )
3 fourierdlem39.aleb 
 |-  ( ph -> A <_ B )
4 fourierdlem39.f 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
5 fourierdlem39.g 
 |-  G = ( RR _D F )
6 fourierdlem39.gcn 
 |-  ( ph -> G e. ( ( A (,) B ) -cn-> CC ) )
7 fourierdlem39.gbd 
 |-  ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y )
8 fourierdlem39.r 
 |-  ( ph -> R e. RR+ )
9 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC )
10 4 9 syl 
 |-  ( ph -> F : ( A [,] B ) --> CC )
11 10 feqmptd 
 |-  ( ph -> F = ( x e. ( A [,] B ) |-> ( F ` x ) ) )
12 11 eqcomd 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( F ` x ) ) = F )
13 12 4 eqeltrd 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( F ` x ) ) e. ( ( A [,] B ) -cn-> CC ) )
14 coscn 
 |-  cos e. ( CC -cn-> CC )
15 14 a1i 
 |-  ( ph -> cos e. ( CC -cn-> CC ) )
16 1 2 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
17 ax-resscn 
 |-  RR C_ CC
18 16 17 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
19 8 rpred 
 |-  ( ph -> R e. RR )
20 19 recnd 
 |-  ( ph -> R e. CC )
21 ssid 
 |-  CC C_ CC
22 21 a1i 
 |-  ( ph -> CC C_ CC )
23 18 20 22 constcncfg 
 |-  ( ph -> ( x e. ( A [,] B ) |-> R ) e. ( ( A [,] B ) -cn-> CC ) )
24 18 22 idcncfg 
 |-  ( ph -> ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) )
25 23 24 mulcncf 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( R x. x ) ) e. ( ( A [,] B ) -cn-> CC ) )
26 15 25 cncfmpt1f 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( cos ` ( R x. x ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
27 8 rpcnne0d 
 |-  ( ph -> ( R e. CC /\ R =/= 0 ) )
28 eldifsn 
 |-  ( R e. ( CC \ { 0 } ) <-> ( R e. CC /\ R =/= 0 ) )
29 27 28 sylibr 
 |-  ( ph -> R e. ( CC \ { 0 } ) )
30 difssd 
 |-  ( ph -> ( CC \ { 0 } ) C_ CC )
31 18 29 30 constcncfg 
 |-  ( ph -> ( x e. ( A [,] B ) |-> R ) e. ( ( A [,] B ) -cn-> ( CC \ { 0 } ) ) )
32 26 31 divcncf 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( ( cos ` ( R x. x ) ) / R ) ) e. ( ( A [,] B ) -cn-> CC ) )
33 32 negcncfg 
 |-  ( ph -> ( x e. ( A [,] B ) |-> -u ( ( cos ` ( R x. x ) ) / R ) ) e. ( ( A [,] B ) -cn-> CC ) )
34 cncff 
 |-  ( G e. ( ( A (,) B ) -cn-> CC ) -> G : ( A (,) B ) --> CC )
35 6 34 syl 
 |-  ( ph -> G : ( A (,) B ) --> CC )
36 35 feqmptd 
 |-  ( ph -> G = ( x e. ( A (,) B ) |-> ( G ` x ) ) )
37 36 eqcomd 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( G ` x ) ) = G )
38 37 6 eqeltrd 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( G ` x ) ) e. ( ( A (,) B ) -cn-> CC ) )
39 sincn 
 |-  sin e. ( CC -cn-> CC )
40 39 a1i 
 |-  ( ph -> sin e. ( CC -cn-> CC ) )
41 ioosscn 
 |-  ( A (,) B ) C_ CC
42 41 a1i 
 |-  ( ph -> ( A (,) B ) C_ CC )
43 42 20 22 constcncfg 
 |-  ( ph -> ( x e. ( A (,) B ) |-> R ) e. ( ( A (,) B ) -cn-> CC ) )
44 42 22 idcncfg 
 |-  ( ph -> ( x e. ( A (,) B ) |-> x ) e. ( ( A (,) B ) -cn-> CC ) )
45 43 44 mulcncf 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( R x. x ) ) e. ( ( A (,) B ) -cn-> CC ) )
46 40 45 cncfmpt1f 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( sin ` ( R x. x ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
47 ioombl 
 |-  ( A (,) B ) e. dom vol
48 47 a1i 
 |-  ( ph -> ( A (,) B ) e. dom vol )
49 volioo 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
50 1 2 3 49 syl3anc 
 |-  ( ph -> ( vol ` ( A (,) B ) ) = ( B - A ) )
51 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
52 50 51 eqeltrd 
 |-  ( ph -> ( vol ` ( A (,) B ) ) e. RR )
53 eqid 
 |-  ( x e. ( A [,] B ) |-> ( F ` x ) ) = ( x e. ( A [,] B ) |-> ( F ` x ) )
54 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
55 54 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
56 10 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> F : ( A [,] B ) --> CC )
57 55 sselda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A [,] B ) )
58 56 57 ffvelcdmd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
59 53 13 55 22 58 cncfmptssg 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) e. ( ( A (,) B ) -cn-> CC ) )
60 59 46 mulcncf 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
61 cniccbdd 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> E. y e. RR A. z e. ( A [,] B ) ( abs ` ( F ` z ) ) <_ y )
62 1 2 4 61 syl3anc 
 |-  ( ph -> E. y e. RR A. z e. ( A [,] B ) ( abs ` ( F ` z ) ) <_ y )
63 nfra1 
 |-  F/ z A. z e. ( A [,] B ) ( abs ` ( F ` z ) ) <_ y
64 54 sseli 
 |-  ( z e. ( A (,) B ) -> z e. ( A [,] B ) )
65 rspa 
 |-  ( ( A. z e. ( A [,] B ) ( abs ` ( F ` z ) ) <_ y /\ z e. ( A [,] B ) ) -> ( abs ` ( F ` z ) ) <_ y )
66 64 65 sylan2 
 |-  ( ( A. z e. ( A [,] B ) ( abs ` ( F ` z ) ) <_ y /\ z e. ( A (,) B ) ) -> ( abs ` ( F ` z ) ) <_ y )
67 66 ex 
 |-  ( A. z e. ( A [,] B ) ( abs ` ( F ` z ) ) <_ y -> ( z e. ( A (,) B ) -> ( abs ` ( F ` z ) ) <_ y ) )
68 63 67 ralrimi 
 |-  ( A. z e. ( A [,] B ) ( abs ` ( F ` z ) ) <_ y -> A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y )
69 68 a1i 
 |-  ( ( ph /\ y e. RR ) -> ( A. z e. ( A [,] B ) ( abs ` ( F ` z ) ) <_ y -> A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y ) )
70 69 reximdva 
 |-  ( ph -> ( E. y e. RR A. z e. ( A [,] B ) ( abs ` ( F ` z ) ) <_ y -> E. y e. RR A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y ) )
71 62 70 mpd 
 |-  ( ph -> E. y e. RR A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y )
72 nfv 
 |-  F/ z ( ph /\ y e. RR )
73 nfra1 
 |-  F/ z A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y
74 72 73 nfan 
 |-  F/ z ( ( ph /\ y e. RR ) /\ A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y )
75 simpll 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y ) /\ z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ) -> ( ph /\ y e. RR ) )
76 simpr 
 |-  ( ( ph /\ z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ) -> z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) )
77 19 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> R e. RR )
78 elioore 
 |-  ( x e. ( A (,) B ) -> x e. RR )
79 78 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. RR )
80 77 79 remulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( R x. x ) e. RR )
81 80 resincld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( sin ` ( R x. x ) ) e. RR )
82 81 recnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( sin ` ( R x. x ) ) e. CC )
83 58 82 mulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) e. CC )
84 83 ralrimiva 
 |-  ( ph -> A. x e. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) e. CC )
85 dmmptg 
 |-  ( A. x e. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) e. CC -> dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) = ( A (,) B ) )
86 84 85 syl 
 |-  ( ph -> dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) = ( A (,) B ) )
87 86 adantr 
 |-  ( ( ph /\ z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ) -> dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) = ( A (,) B ) )
88 76 87 eleqtrd 
 |-  ( ( ph /\ z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ) -> z e. ( A (,) B ) )
89 88 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y ) /\ z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ) -> z e. ( A (,) B ) )
90 simplr 
 |-  ( ( ( ph /\ A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y ) /\ z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ) -> A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y )
91 88 adantlr 
 |-  ( ( ( ph /\ A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y ) /\ z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ) -> z e. ( A (,) B ) )
92 rspa 
 |-  ( ( A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y /\ z e. ( A (,) B ) ) -> ( abs ` ( F ` z ) ) <_ y )
93 90 91 92 syl2anc 
 |-  ( ( ( ph /\ A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y ) /\ z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ) -> ( abs ` ( F ` z ) ) <_ y )
94 93 adantllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y ) /\ z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ) -> ( abs ` ( F ` z ) ) <_ y )
95 eqidd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) = ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) )
96 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
97 oveq2 
 |-  ( x = z -> ( R x. x ) = ( R x. z ) )
98 97 fveq2d 
 |-  ( x = z -> ( sin ` ( R x. x ) ) = ( sin ` ( R x. z ) ) )
99 96 98 oveq12d 
 |-  ( x = z -> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) = ( ( F ` z ) x. ( sin ` ( R x. z ) ) ) )
100 99 adantl 
 |-  ( ( ( ph /\ z e. ( A (,) B ) ) /\ x = z ) -> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) = ( ( F ` z ) x. ( sin ` ( R x. z ) ) ) )
101 simpr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> z e. ( A (,) B ) )
102 10 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> F : ( A [,] B ) --> CC )
103 54 101 sselid 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> z e. ( A [,] B ) )
104 102 103 ffvelcdmd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( F ` z ) e. CC )
105 20 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> R e. CC )
106 41 101 sselid 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> z e. CC )
107 105 106 mulcld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( R x. z ) e. CC )
108 107 sincld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( sin ` ( R x. z ) ) e. CC )
109 104 108 mulcld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( F ` z ) x. ( sin ` ( R x. z ) ) ) e. CC )
110 95 100 101 109 fvmptd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) = ( ( F ` z ) x. ( sin ` ( R x. z ) ) ) )
111 110 fveq2d 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) ) = ( abs ` ( ( F ` z ) x. ( sin ` ( R x. z ) ) ) ) )
112 104 108 absmuld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` ( ( F ` z ) x. ( sin ` ( R x. z ) ) ) ) = ( ( abs ` ( F ` z ) ) x. ( abs ` ( sin ` ( R x. z ) ) ) ) )
113 111 112 eqtrd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) ) = ( ( abs ` ( F ` z ) ) x. ( abs ` ( sin ` ( R x. z ) ) ) ) )
114 113 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) -> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) ) = ( ( abs ` ( F ` z ) ) x. ( abs ` ( sin ` ( R x. z ) ) ) ) )
115 114 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) ) = ( ( abs ` ( F ` z ) ) x. ( abs ` ( sin ` ( R x. z ) ) ) ) )
116 simplll 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ph )
117 simplr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> z e. ( A (,) B ) )
118 116 117 104 syl2anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( F ` z ) e. CC )
119 118 abscld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( abs ` ( F ` z ) ) e. RR )
120 20 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> R e. CC )
121 41 117 sselid 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> z e. CC )
122 120 121 mulcld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( R x. z ) e. CC )
123 122 sincld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( sin ` ( R x. z ) ) e. CC )
124 123 abscld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( abs ` ( sin ` ( R x. z ) ) ) e. RR )
125 119 124 remulcld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( ( abs ` ( F ` z ) ) x. ( abs ` ( sin ` ( R x. z ) ) ) ) e. RR )
126 1red 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> 1 e. RR )
127 119 126 remulcld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( ( abs ` ( F ` z ) ) x. 1 ) e. RR )
128 simpllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> y e. RR )
129 128 126 remulcld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( y x. 1 ) e. RR )
130 108 abscld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` ( sin ` ( R x. z ) ) ) e. RR )
131 1red 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> 1 e. RR )
132 104 abscld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` ( F ` z ) ) e. RR )
133 104 absge0d 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> 0 <_ ( abs ` ( F ` z ) ) )
134 19 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> R e. RR )
135 elioore 
 |-  ( z e. ( A (,) B ) -> z e. RR )
136 135 adantl 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> z e. RR )
137 134 136 remulcld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( R x. z ) e. RR )
138 abssinbd 
 |-  ( ( R x. z ) e. RR -> ( abs ` ( sin ` ( R x. z ) ) ) <_ 1 )
139 137 138 syl 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` ( sin ` ( R x. z ) ) ) <_ 1 )
140 130 131 132 133 139 lemul2ad 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( abs ` ( F ` z ) ) x. ( abs ` ( sin ` ( R x. z ) ) ) ) <_ ( ( abs ` ( F ` z ) ) x. 1 ) )
141 140 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) -> ( ( abs ` ( F ` z ) ) x. ( abs ` ( sin ` ( R x. z ) ) ) ) <_ ( ( abs ` ( F ` z ) ) x. 1 ) )
142 141 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( ( abs ` ( F ` z ) ) x. ( abs ` ( sin ` ( R x. z ) ) ) ) <_ ( ( abs ` ( F ` z ) ) x. 1 ) )
143 0le1 
 |-  0 <_ 1
144 143 a1i 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> 0 <_ 1 )
145 simpr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( abs ` ( F ` z ) ) <_ y )
146 119 128 126 144 145 lemul1ad 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( ( abs ` ( F ` z ) ) x. 1 ) <_ ( y x. 1 ) )
147 125 127 129 142 146 letrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( ( abs ` ( F ` z ) ) x. ( abs ` ( sin ` ( R x. z ) ) ) ) <_ ( y x. 1 ) )
148 115 147 eqbrtrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) ) <_ ( y x. 1 ) )
149 128 recnd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> y e. CC )
150 149 mulridd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( y x. 1 ) = y )
151 148 150 breqtrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( F ` z ) ) <_ y ) -> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) ) <_ y )
152 75 89 94 151 syl21anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y ) /\ z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ) -> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) ) <_ y )
153 152 ex 
 |-  ( ( ( ph /\ y e. RR ) /\ A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y ) -> ( z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) -> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) ) <_ y ) )
154 74 153 ralrimi 
 |-  ( ( ( ph /\ y e. RR ) /\ A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y ) -> A. z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ( abs ` ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) ) <_ y )
155 154 ex 
 |-  ( ( ph /\ y e. RR ) -> ( A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y -> A. z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ( abs ` ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) ) <_ y ) )
156 155 reximdva 
 |-  ( ph -> ( E. y e. RR A. z e. ( A (,) B ) ( abs ` ( F ` z ) ) <_ y -> E. y e. RR A. z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ( abs ` ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) ) <_ y ) )
157 71 156 mpd 
 |-  ( ph -> E. y e. RR A. z e. dom ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ( abs ` ( ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) ` z ) ) <_ y )
158 48 52 60 157 cnbdibl 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) ) e. L^1 )
159 15 45 cncfmpt1f 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( cos ` ( R x. x ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
160 42 29 30 constcncfg 
 |-  ( ph -> ( x e. ( A (,) B ) |-> R ) e. ( ( A (,) B ) -cn-> ( CC \ { 0 } ) ) )
161 159 160 divcncf 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( cos ` ( R x. x ) ) / R ) ) e. ( ( A (,) B ) -cn-> CC ) )
162 161 negcncfg 
 |-  ( ph -> ( x e. ( A (,) B ) |-> -u ( ( cos ` ( R x. x ) ) / R ) ) e. ( ( A (,) B ) -cn-> CC ) )
163 38 162 mulcncf 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
164 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
165 19 adantr 
 |-  ( ( ph /\ y e. RR ) -> R e. RR )
166 8 rpne0d 
 |-  ( ph -> R =/= 0 )
167 166 adantr 
 |-  ( ( ph /\ y e. RR ) -> R =/= 0 )
168 164 165 167 redivcld 
 |-  ( ( ph /\ y e. RR ) -> ( y / R ) e. RR )
169 168 adantr 
 |-  ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) -> ( y / R ) e. RR )
170 simpr 
 |-  ( ( ph /\ z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ) -> z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) )
171 35 ffvelcdmda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( G ` x ) e. CC )
172 20 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> R e. CC )
173 78 recnd 
 |-  ( x e. ( A (,) B ) -> x e. CC )
174 173 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. CC )
175 172 174 mulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( R x. x ) e. CC )
176 175 coscld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( cos ` ( R x. x ) ) e. CC )
177 166 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> R =/= 0 )
178 176 172 177 divcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( cos ` ( R x. x ) ) / R ) e. CC )
179 178 negcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -u ( ( cos ` ( R x. x ) ) / R ) e. CC )
180 171 179 mulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) e. CC )
181 180 ralrimiva 
 |-  ( ph -> A. x e. ( A (,) B ) ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) e. CC )
182 181 adantr 
 |-  ( ( ph /\ z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ) -> A. x e. ( A (,) B ) ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) e. CC )
183 dmmptg 
 |-  ( A. x e. ( A (,) B ) ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) e. CC -> dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) = ( A (,) B ) )
184 182 183 syl 
 |-  ( ( ph /\ z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ) -> dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) = ( A (,) B ) )
185 170 184 eleqtrd 
 |-  ( ( ph /\ z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ) -> z e. ( A (,) B ) )
186 185 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ) -> z e. ( A (,) B ) )
187 eqidd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) = ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) )
188 fveq2 
 |-  ( x = z -> ( G ` x ) = ( G ` z ) )
189 97 fveq2d 
 |-  ( x = z -> ( cos ` ( R x. x ) ) = ( cos ` ( R x. z ) ) )
190 189 oveq1d 
 |-  ( x = z -> ( ( cos ` ( R x. x ) ) / R ) = ( ( cos ` ( R x. z ) ) / R ) )
191 190 negeqd 
 |-  ( x = z -> -u ( ( cos ` ( R x. x ) ) / R ) = -u ( ( cos ` ( R x. z ) ) / R ) )
192 188 191 oveq12d 
 |-  ( x = z -> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) = ( ( G ` z ) x. -u ( ( cos ` ( R x. z ) ) / R ) ) )
193 192 adantl 
 |-  ( ( ( ph /\ z e. ( A (,) B ) ) /\ x = z ) -> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) = ( ( G ` z ) x. -u ( ( cos ` ( R x. z ) ) / R ) ) )
194 35 ffvelcdmda 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( G ` z ) e. CC )
195 107 coscld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( cos ` ( R x. z ) ) e. CC )
196 166 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> R =/= 0 )
197 195 105 196 divcld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( cos ` ( R x. z ) ) / R ) e. CC )
198 197 negcld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> -u ( ( cos ` ( R x. z ) ) / R ) e. CC )
199 194 198 mulcld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( G ` z ) x. -u ( ( cos ` ( R x. z ) ) / R ) ) e. CC )
200 187 193 101 199 fvmptd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) = ( ( G ` z ) x. -u ( ( cos ` ( R x. z ) ) / R ) ) )
201 200 fveq2d 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) = ( abs ` ( ( G ` z ) x. -u ( ( cos ` ( R x. z ) ) / R ) ) ) )
202 201 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) = ( abs ` ( ( G ` z ) x. -u ( ( cos ` ( R x. z ) ) / R ) ) ) )
203 35 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) -> G : ( A (,) B ) --> CC )
204 203 ffvelcdmda 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( G ` z ) e. CC )
205 204 abscld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( abs ` ( G ` z ) ) e. RR )
206 simpllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> y e. RR )
207 20 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> R e. CC )
208 106 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> z e. CC )
209 207 208 mulcld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( R x. z ) e. CC )
210 209 coscld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( cos ` ( R x. z ) ) e. CC )
211 166 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> R =/= 0 )
212 210 207 211 divcld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( ( cos ` ( R x. z ) ) / R ) e. CC )
213 212 negcld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> -u ( ( cos ` ( R x. z ) ) / R ) e. CC )
214 213 abscld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( abs ` -u ( ( cos ` ( R x. z ) ) / R ) ) e. RR )
215 8 rprecred 
 |-  ( ph -> ( 1 / R ) e. RR )
216 215 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( 1 / R ) e. RR )
217 204 absge0d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> 0 <_ ( abs ` ( G ` z ) ) )
218 213 absge0d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> 0 <_ ( abs ` -u ( ( cos ` ( R x. z ) ) / R ) ) )
219 188 fveq2d 
 |-  ( x = z -> ( abs ` ( G ` x ) ) = ( abs ` ( G ` z ) ) )
220 219 breq1d 
 |-  ( x = z -> ( ( abs ` ( G ` x ) ) <_ y <-> ( abs ` ( G ` z ) ) <_ y ) )
221 220 rspccva 
 |-  ( ( A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y /\ z e. ( A (,) B ) ) -> ( abs ` ( G ` z ) ) <_ y )
222 221 adantll 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( abs ` ( G ` z ) ) <_ y )
223 197 absnegd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` -u ( ( cos ` ( R x. z ) ) / R ) ) = ( abs ` ( ( cos ` ( R x. z ) ) / R ) ) )
224 195 105 196 absdivd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` ( ( cos ` ( R x. z ) ) / R ) ) = ( ( abs ` ( cos ` ( R x. z ) ) ) / ( abs ` R ) ) )
225 8 rpge0d 
 |-  ( ph -> 0 <_ R )
226 19 225 absidd 
 |-  ( ph -> ( abs ` R ) = R )
227 226 oveq2d 
 |-  ( ph -> ( ( abs ` ( cos ` ( R x. z ) ) ) / ( abs ` R ) ) = ( ( abs ` ( cos ` ( R x. z ) ) ) / R ) )
228 227 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( abs ` ( cos ` ( R x. z ) ) ) / ( abs ` R ) ) = ( ( abs ` ( cos ` ( R x. z ) ) ) / R ) )
229 223 224 228 3eqtrd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` -u ( ( cos ` ( R x. z ) ) / R ) ) = ( ( abs ` ( cos ` ( R x. z ) ) ) / R ) )
230 195 abscld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` ( cos ` ( R x. z ) ) ) e. RR )
231 8 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> R e. RR+ )
232 abscosbd 
 |-  ( ( R x. z ) e. RR -> ( abs ` ( cos ` ( R x. z ) ) ) <_ 1 )
233 137 232 syl 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` ( cos ` ( R x. z ) ) ) <_ 1 )
234 230 131 231 233 lediv1dd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( abs ` ( cos ` ( R x. z ) ) ) / R ) <_ ( 1 / R ) )
235 229 234 eqbrtrd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` -u ( ( cos ` ( R x. z ) ) / R ) ) <_ ( 1 / R ) )
236 235 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( abs ` -u ( ( cos ` ( R x. z ) ) / R ) ) <_ ( 1 / R ) )
237 205 206 214 216 217 218 222 236 lemul12ad 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( ( abs ` ( G ` z ) ) x. ( abs ` -u ( ( cos ` ( R x. z ) ) / R ) ) ) <_ ( y x. ( 1 / R ) ) )
238 194 198 absmuld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( abs ` ( ( G ` z ) x. -u ( ( cos ` ( R x. z ) ) / R ) ) ) = ( ( abs ` ( G ` z ) ) x. ( abs ` -u ( ( cos ` ( R x. z ) ) / R ) ) ) )
239 238 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( abs ` ( ( G ` z ) x. -u ( ( cos ` ( R x. z ) ) / R ) ) ) = ( ( abs ` ( G ` z ) ) x. ( abs ` -u ( ( cos ` ( R x. z ) ) / R ) ) ) )
240 206 recnd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> y e. CC )
241 240 207 211 divrecd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( y / R ) = ( y x. ( 1 / R ) ) )
242 237 239 241 3brtr4d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( abs ` ( ( G ` z ) x. -u ( ( cos ` ( R x. z ) ) / R ) ) ) <_ ( y / R ) )
243 202 242 eqbrtrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. ( A (,) B ) ) -> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) <_ ( y / R ) )
244 186 243 syldan 
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) /\ z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ) -> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) <_ ( y / R ) )
245 244 ralrimiva 
 |-  ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) -> A. z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) <_ ( y / R ) )
246 breq2 
 |-  ( w = ( y / R ) -> ( ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) <_ w <-> ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) <_ ( y / R ) ) )
247 246 ralbidv 
 |-  ( w = ( y / R ) -> ( A. z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) <_ w <-> A. z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) <_ ( y / R ) ) )
248 247 rspcev 
 |-  ( ( ( y / R ) e. RR /\ A. z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) <_ ( y / R ) ) -> E. w e. RR A. z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) <_ w )
249 169 245 248 syl2anc 
 |-  ( ( ( ph /\ y e. RR ) /\ A. x e. ( A (,) B ) ( abs ` ( G ` x ) ) <_ y ) -> E. w e. RR A. z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) <_ w )
250 249 7 r19.29a 
 |-  ( ph -> E. w e. RR A. z e. dom ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ( abs ` ( ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) ` z ) ) <_ w )
251 48 52 163 250 cnbdibl 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) ) e. L^1 )
252 12 oveq2d 
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( F ` x ) ) ) = ( RR _D F ) )
253 5 eqcomi 
 |-  ( RR _D F ) = G
254 253 a1i 
 |-  ( ph -> ( RR _D F ) = G )
255 252 254 36 3eqtrd 
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( F ` x ) ) ) = ( x e. ( A (,) B ) |-> ( G ` x ) ) )
256 reelprrecn 
 |-  RR e. { RR , CC }
257 256 a1i 
 |-  ( ph -> RR e. { RR , CC } )
258 20 adantr 
 |-  ( ( ph /\ x e. RR ) -> R e. CC )
259 recn 
 |-  ( x e. RR -> x e. CC )
260 259 adantl 
 |-  ( ( ph /\ x e. RR ) -> x e. CC )
261 258 260 mulcld 
 |-  ( ( ph /\ x e. RR ) -> ( R x. x ) e. CC )
262 261 coscld 
 |-  ( ( ph /\ x e. RR ) -> ( cos ` ( R x. x ) ) e. CC )
263 166 adantr 
 |-  ( ( ph /\ x e. RR ) -> R =/= 0 )
264 262 258 263 divcld 
 |-  ( ( ph /\ x e. RR ) -> ( ( cos ` ( R x. x ) ) / R ) e. CC )
265 264 negcld 
 |-  ( ( ph /\ x e. RR ) -> -u ( ( cos ` ( R x. x ) ) / R ) e. CC )
266 19 adantr 
 |-  ( ( ph /\ x e. RR ) -> R e. RR )
267 simpr 
 |-  ( ( ph /\ x e. RR ) -> x e. RR )
268 266 267 remulcld 
 |-  ( ( ph /\ x e. RR ) -> ( R x. x ) e. RR )
269 268 resincld 
 |-  ( ( ph /\ x e. RR ) -> ( sin ` ( R x. x ) ) e. RR )
270 269 renegcld 
 |-  ( ( ph /\ x e. RR ) -> -u ( sin ` ( R x. x ) ) e. RR )
271 270 266 remulcld 
 |-  ( ( ph /\ x e. RR ) -> ( -u ( sin ` ( R x. x ) ) x. R ) e. RR )
272 271 266 263 redivcld 
 |-  ( ( ph /\ x e. RR ) -> ( ( -u ( sin ` ( R x. x ) ) x. R ) / R ) e. RR )
273 272 renegcld 
 |-  ( ( ph /\ x e. RR ) -> -u ( ( -u ( sin ` ( R x. x ) ) x. R ) / R ) e. RR )
274 recoscl 
 |-  ( y e. RR -> ( cos ` y ) e. RR )
275 274 adantl 
 |-  ( ( ph /\ y e. RR ) -> ( cos ` y ) e. RR )
276 275 recnd 
 |-  ( ( ph /\ y e. RR ) -> ( cos ` y ) e. CC )
277 resincl 
 |-  ( y e. RR -> ( sin ` y ) e. RR )
278 277 renegcld 
 |-  ( y e. RR -> -u ( sin ` y ) e. RR )
279 278 adantl 
 |-  ( ( ph /\ y e. RR ) -> -u ( sin ` y ) e. RR )
280 1red 
 |-  ( ( ph /\ x e. RR ) -> 1 e. RR )
281 257 dvmptid 
 |-  ( ph -> ( RR _D ( x e. RR |-> x ) ) = ( x e. RR |-> 1 ) )
282 257 260 280 281 20 dvmptcmul 
 |-  ( ph -> ( RR _D ( x e. RR |-> ( R x. x ) ) ) = ( x e. RR |-> ( R x. 1 ) ) )
283 258 mulridd 
 |-  ( ( ph /\ x e. RR ) -> ( R x. 1 ) = R )
284 283 mpteq2dva 
 |-  ( ph -> ( x e. RR |-> ( R x. 1 ) ) = ( x e. RR |-> R ) )
285 282 284 eqtrd 
 |-  ( ph -> ( RR _D ( x e. RR |-> ( R x. x ) ) ) = ( x e. RR |-> R ) )
286 dvcosre 
 |-  ( RR _D ( y e. RR |-> ( cos ` y ) ) ) = ( y e. RR |-> -u ( sin ` y ) )
287 286 a1i 
 |-  ( ph -> ( RR _D ( y e. RR |-> ( cos ` y ) ) ) = ( y e. RR |-> -u ( sin ` y ) ) )
288 fveq2 
 |-  ( y = ( R x. x ) -> ( cos ` y ) = ( cos ` ( R x. x ) ) )
289 fveq2 
 |-  ( y = ( R x. x ) -> ( sin ` y ) = ( sin ` ( R x. x ) ) )
290 289 negeqd 
 |-  ( y = ( R x. x ) -> -u ( sin ` y ) = -u ( sin ` ( R x. x ) ) )
291 257 257 268 266 276 279 285 287 288 290 dvmptco 
 |-  ( ph -> ( RR _D ( x e. RR |-> ( cos ` ( R x. x ) ) ) ) = ( x e. RR |-> ( -u ( sin ` ( R x. x ) ) x. R ) ) )
292 257 262 271 291 20 166 dvmptdivc 
 |-  ( ph -> ( RR _D ( x e. RR |-> ( ( cos ` ( R x. x ) ) / R ) ) ) = ( x e. RR |-> ( ( -u ( sin ` ( R x. x ) ) x. R ) / R ) ) )
293 257 264 272 292 dvmptneg 
 |-  ( ph -> ( RR _D ( x e. RR |-> -u ( ( cos ` ( R x. x ) ) / R ) ) ) = ( x e. RR |-> -u ( ( -u ( sin ` ( R x. x ) ) x. R ) / R ) ) )
294 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
295 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
296 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
297 1 2 296 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
298 257 265 273 293 16 294 295 297 dvmptres2 
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> -u ( ( cos ` ( R x. x ) ) / R ) ) ) = ( x e. ( A (,) B ) |-> -u ( ( -u ( sin ` ( R x. x ) ) x. R ) / R ) ) )
299 82 172 mulneg1d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( -u ( sin ` ( R x. x ) ) x. R ) = -u ( ( sin ` ( R x. x ) ) x. R ) )
300 299 oveq1d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( -u ( sin ` ( R x. x ) ) x. R ) / R ) = ( -u ( ( sin ` ( R x. x ) ) x. R ) / R ) )
301 82 172 mulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( sin ` ( R x. x ) ) x. R ) e. CC )
302 301 172 177 divnegd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -u ( ( ( sin ` ( R x. x ) ) x. R ) / R ) = ( -u ( ( sin ` ( R x. x ) ) x. R ) / R ) )
303 300 302 eqtr4d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( -u ( sin ` ( R x. x ) ) x. R ) / R ) = -u ( ( ( sin ` ( R x. x ) ) x. R ) / R ) )
304 303 negeqd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -u ( ( -u ( sin ` ( R x. x ) ) x. R ) / R ) = -u -u ( ( ( sin ` ( R x. x ) ) x. R ) / R ) )
305 301 172 177 divcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( sin ` ( R x. x ) ) x. R ) / R ) e. CC )
306 305 negnegd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -u -u ( ( ( sin ` ( R x. x ) ) x. R ) / R ) = ( ( ( sin ` ( R x. x ) ) x. R ) / R ) )
307 82 172 177 divcan4d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( sin ` ( R x. x ) ) x. R ) / R ) = ( sin ` ( R x. x ) ) )
308 304 306 307 3eqtrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -u ( ( -u ( sin ` ( R x. x ) ) x. R ) / R ) = ( sin ` ( R x. x ) ) )
309 308 mpteq2dva 
 |-  ( ph -> ( x e. ( A (,) B ) |-> -u ( ( -u ( sin ` ( R x. x ) ) x. R ) / R ) ) = ( x e. ( A (,) B ) |-> ( sin ` ( R x. x ) ) ) )
310 298 309 eqtrd 
 |-  ( ph -> ( RR _D ( x e. ( A [,] B ) |-> -u ( ( cos ` ( R x. x ) ) / R ) ) ) = ( x e. ( A (,) B ) |-> ( sin ` ( R x. x ) ) ) )
311 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
312 oveq2 
 |-  ( x = A -> ( R x. x ) = ( R x. A ) )
313 312 fveq2d 
 |-  ( x = A -> ( cos ` ( R x. x ) ) = ( cos ` ( R x. A ) ) )
314 313 oveq1d 
 |-  ( x = A -> ( ( cos ` ( R x. x ) ) / R ) = ( ( cos ` ( R x. A ) ) / R ) )
315 314 negeqd 
 |-  ( x = A -> -u ( ( cos ` ( R x. x ) ) / R ) = -u ( ( cos ` ( R x. A ) ) / R ) )
316 311 315 oveq12d 
 |-  ( x = A -> ( ( F ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) = ( ( F ` A ) x. -u ( ( cos ` ( R x. A ) ) / R ) ) )
317 316 adantl 
 |-  ( ( ph /\ x = A ) -> ( ( F ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) = ( ( F ` A ) x. -u ( ( cos ` ( R x. A ) ) / R ) ) )
318 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
319 oveq2 
 |-  ( x = B -> ( R x. x ) = ( R x. B ) )
320 319 fveq2d 
 |-  ( x = B -> ( cos ` ( R x. x ) ) = ( cos ` ( R x. B ) ) )
321 320 oveq1d 
 |-  ( x = B -> ( ( cos ` ( R x. x ) ) / R ) = ( ( cos ` ( R x. B ) ) / R ) )
322 321 negeqd 
 |-  ( x = B -> -u ( ( cos ` ( R x. x ) ) / R ) = -u ( ( cos ` ( R x. B ) ) / R ) )
323 318 322 oveq12d 
 |-  ( x = B -> ( ( F ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) = ( ( F ` B ) x. -u ( ( cos ` ( R x. B ) ) / R ) ) )
324 323 adantl 
 |-  ( ( ph /\ x = B ) -> ( ( F ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) = ( ( F ` B ) x. -u ( ( cos ` ( R x. B ) ) / R ) ) )
325 1 2 3 13 33 38 46 158 251 255 310 317 324 itgparts 
 |-  ( ph -> S. ( A (,) B ) ( ( F ` x ) x. ( sin ` ( R x. x ) ) ) _d x = ( ( ( ( F ` B ) x. -u ( ( cos ` ( R x. B ) ) / R ) ) - ( ( F ` A ) x. -u ( ( cos ` ( R x. A ) ) / R ) ) ) - S. ( A (,) B ) ( ( G ` x ) x. -u ( ( cos ` ( R x. x ) ) / R ) ) _d x ) )