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 ffvelrnd
 |-  ( ( 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 sseldi
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> z e. ( A [,] B ) )
104 102 103 ffvelrnd
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( F ` z ) e. CC )
105 20 adantr
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> R e. CC )
106 41 101 sseldi
 |-  ( ( 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 sseldi
 |-  ( ( ( ( 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 mulid1d
 |-  ( ( ( ( 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 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( ( ( 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 mulid1d
 |-  ( ( 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 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
295 294 tgioo2
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
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 295 294 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 ) )