let A, B, C, d, e, c be Real; for u being Function of (REAL 2),REAL st ( for x, t being Real holds u /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))) ) holds
( u is_partial_differentiable_on [#] (REAL 2),<*1*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = ((- ((A * e) * (sin . (e * x)))) + ((B * e) * (cos . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((- ((C * (e * c)) * (sin . ((e * c) * t)))) + ((d * (e * c)) * (cos . ((e * c) * t)))) ) & u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real holds
( (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = - (((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = - ((((e * c) ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) ) ) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )
let u be Function of (REAL 2),REAL; ( ( for x, t being Real holds u /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))) ) implies ( u is_partial_differentiable_on [#] (REAL 2),<*1*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = ((- ((A * e) * (sin . (e * x)))) + ((B * e) * (cos . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((- ((C * (e * c)) * (sin . ((e * c) * t)))) + ((d * (e * c)) * (cos . ((e * c) * t)))) ) & u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real holds
( (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = - (((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = - ((((e * c) ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) ) ) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) ) )
assume AS:
for x, t being Real holds u /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))
; ( u is_partial_differentiable_on [#] (REAL 2),<*1*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = ((- ((A * e) * (sin . (e * x)))) + ((B * e) * (cos . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((- ((C * (e * c)) * (sin . ((e * c) * t)))) + ((d * (e * c)) * (cos . ((e * c) * t)))) ) & u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real holds
( (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = - (((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = - ((((e * c) ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) ) ) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )
consider f being Function of REAL,REAL such that
A1:
for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x)))
by LM42;
consider g being Function of REAL,REAL such that
A2:
for t being Real holds g . t = (C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))
by LM42;
D0:
( dom f = REAL & dom g = REAL )
by FUNCT_2:def 1;
A3:
for x, t being Real holds u /. <*x,t*> = (f /. x) * (g /. t)
X1:
f is_differentiable_on 2, [#] REAL
by LM41, A1;
X2:
g is_differentiable_on 2, [#] REAL
by LM41, A2;
X3:
for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t)
by LM43, A1, A2;
Y1:
for x, t being Real holds (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = ((- ((A * e) * (sin . (e * x)))) + ((B * e) * (cos . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))
proof
let x,
t be
Real;
(u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = ((- ((A * e) * (sin . (e * x)))) + ((B * e) * (cos . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))
Y11:
(u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = (diff (f,x)) * (g /. t)
by X1, X2, X3, LM50, A3;
Y12:
(f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x)))))
by LM41, A1;
Y13:
f is_differentiable_on [#] REAL
by D0, X1, DIFF2;
Y14:
x in [#] REAL
by XREAL_0:def 1;
g /. t =
g . t
by PARTFUN1:def 6, D0, XREAL_0:def 1
.=
(C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))
by A2
;
hence
(u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = ((- ((A * e) * (sin . (e * x)))) + ((B * e) * (cos . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))
by Y11, Y12, Y13, Y14, FDIFF_1:def 7;
verum
end;
Y2:
for x, t being Real holds (u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((- ((C * (e * c)) * (sin . ((e * c) * t)))) + ((d * (e * c)) * (cos . ((e * c) * t))))
proof
let x,
t be
Real;
(u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((- ((C * (e * c)) * (sin . ((e * c) * t)))) + ((d * (e * c)) * (cos . ((e * c) * t))))
Y12:
(g `| ([#] REAL)) . t = - ((e * c) * ((C * (sin . ((e * c) * t))) - (d * (cos . ((e * c) * t)))))
by LM41, A2;
Y13:
g is_differentiable_on [#] REAL
by D0, X2, DIFF2;
t in [#] REAL
by XREAL_0:def 1;
then Y14:
diff (
g,
t)
= (g `| ([#] REAL)) . t
by Y13, FDIFF_1:def 7;
f /. x =
f . x
by PARTFUN1:def 6, D0, XREAL_0:def 1
.=
(A * (cos . (e * x))) + (B * (sin . (e * x)))
by A1
;
hence
(u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((- ((C * (e * c)) * (sin . ((e * c) * t)))) + ((d * (e * c)) * (cos . ((e * c) * t))))
by X1, X2, X3, LM50, A3, Y12, Y14;
verum
end;
Y3:
for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = - (((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))))
proof
let x,
t be
Real;
(u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = - (((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))))
Y11:
(u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t)
by X1, X2, X3, LM50, A3;
R1:
[#] REAL = dom f
by FUNCT_2:def 1;
R2:
f `| ([#] REAL) is_differentiable_on [#] REAL
by R1, X1, DIFF2;
x in [#] REAL
by XREAL_0:def 1;
then Y13:
x in dom ((f `| ([#] REAL)) `| ([#] REAL))
by R2, FDIFF_1:def 7;
Y15:
((diff (f,([#] REAL))) . 2) /. x =
((f `| ([#] REAL)) `| ([#] REAL)) /. x
by D0, X1, DIFF2
.=
((f `| ([#] REAL)) `| ([#] REAL)) . x
by Y13, PARTFUN1:def 6
.=
- ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x)))))
by LM41, A1
;
g /. t =
g . t
by PARTFUN1:def 6, D0, XREAL_0:def 1
.=
(C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))
by A2
;
hence
(u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = - (((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))))
by Y11, Y15;
verum
end;
for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = - ((((e * c) ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))))
proof
let x,
t be
Real;
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = - ((((e * c) ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))))
Y11:
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,([#] REAL))) . 2) /. t)
by X1, X2, X3, LM50, A3;
R1:
[#] REAL = dom g
by FUNCT_2:def 1;
R2:
g `| ([#] REAL) is_differentiable_on [#] REAL
by R1, X2, DIFF2;
t in [#] REAL
by XREAL_0:def 1;
then Y13:
t in dom ((g `| ([#] REAL)) `| ([#] REAL))
by R2, FDIFF_1:def 7;
Y15:
((diff (g,([#] REAL))) . 2) /. t =
((g `| ([#] REAL)) `| ([#] REAL)) /. t
by D0, X2, DIFF2
.=
((g `| ([#] REAL)) `| ([#] REAL)) . t
by Y13, PARTFUN1:def 6
.=
- (((e * c) ^2) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))))
by LM41, A2
;
f /. x =
f . x
by PARTFUN1:def 6, D0, XREAL_0:def 1
.=
(A * (cos . (e * x))) + (B * (sin . (e * x)))
by A1
;
hence
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = - ((((e * c) ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))))
by Y11, Y15;
verum
end;
hence
( u is_partial_differentiable_on [#] (REAL 2),<*1*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = ((- ((A * e) * (sin . (e * x)))) + ((B * e) * (cos . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((- ((C * (e * c)) * (sin . ((e * c) * t)))) + ((d * (e * c)) * (cos . ((e * c) * t)))) ) & u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real holds
( (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = - (((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = - ((((e * c) ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) ) ) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )
by X1, X2, X3, LM50, A3, Y1, Y2, Y3; verum