let a be Real; for p, q being Rational st a > 0 holds
(a #Q p) * (a #Q q) = a #Q (p + q)
let p, q be Rational; ( a > 0 implies (a #Q p) * (a #Q q) = a #Q (p + q) )
set dp = denominator p;
set dq = denominator q;
set np = numerator p;
set nq = numerator q;
A1:
denominator p >= 1
by RAT_1:11;
reconsider ddq = denominator q as Integer ;
reconsider ddp = denominator p as Integer ;
A2:
denominator (p + q) >= 1
by RAT_1:11;
A3:
denominator q >= 1
by RAT_1:11;
then A4:
(denominator p) * (denominator q) >= 1
by A1, XREAL_1:159;
p + q =
((numerator p) / (denominator p)) + q
by RAT_1:15
.=
((numerator p) / (denominator p)) + ((numerator q) / (denominator q))
by RAT_1:15
.=
(((numerator p) * (denominator q)) + ((numerator q) * (denominator p))) / ((denominator p) * (denominator q))
by XCMPLX_1:116
;
then consider n being Nat such that
A5:
((numerator p) * (denominator q)) + ((numerator q) * (denominator p)) = (numerator (p + q)) * n
and
A6:
(denominator p) * (denominator q) = (denominator (p + q)) * n
by RAT_1:27;
reconsider k = n as Integer ;
assume A7:
a > 0
; (a #Q p) * (a #Q q) = a #Q (p + q)
then A8:
a #Z ((numerator q) - (numerator p)) >= 0
by Th39;
n > 0
by A6;
then A9:
n >= 0 + 1
by NAT_1:13;
A10:
a #Z (numerator p) > 0
by A7, Th39;
then A11:
(a #Z (numerator p)) |^ ((denominator p) + (denominator q)) >= 0
by Th6;
A12:
a #Z ((numerator q) - (numerator p)) > 0
by A7, Th39;
then A13:
(a #Z ((numerator q) - (numerator p))) |^ (denominator p) >= 0
by Th6;
A14:
a #Q (p + q) > 0
by A7, Th52;
A15:
a #Z (numerator (p + q)) > 0
by A7, Th39;
thus (a #Q p) * (a #Q q) =
((denominator p) -Root (a #Z (numerator p))) * ((denominator q) -Root (a #Z ((numerator p) + ((numerator q) - (numerator p)))))
.=
((denominator p) -Root (a #Z (numerator p))) * ((denominator q) -Root ((a #Z (numerator p)) * (a #Z ((numerator q) - (numerator p)))))
by A7, Th44
.=
((denominator p) -Root (a #Z (numerator p))) * (((denominator q) -Root (a #Z (numerator p))) * ((denominator q) -Root (a #Z ((numerator q) - (numerator p)))))
by A10, A8, Th22, RAT_1:11
.=
(((denominator p) -Root (a #Z (numerator p))) * ((denominator q) -Root (a #Z (numerator p)))) * ((denominator q) -Root (a #Z ((numerator q) - (numerator p))))
.=
(((denominator p) * (denominator q)) -Root ((a #Z (numerator p)) |^ ((denominator p) + (denominator q)))) * ((denominator q) -Root (a #Z ((numerator q) - (numerator p))))
by A10, A3, A1, Th26
.=
(((denominator p) * (denominator q)) -Root ((a #Z (numerator p)) |^ ((denominator p) + (denominator q)))) * ((denominator q) -Root ((denominator p) -Root ((a #Z ((numerator q) - (numerator p))) |^ (denominator p))))
by A12, A1, Lm2
.=
(((denominator p) * (denominator q)) -Root ((a #Z (numerator p)) |^ ((denominator p) + (denominator q)))) * (((denominator p) * (denominator q)) -Root ((a #Z ((numerator q) - (numerator p))) |^ (denominator p)))
by A3, A1, A13, Th25
.=
((denominator p) * (denominator q)) -Root (((a #Z (numerator p)) |^ ((denominator p) + (denominator q))) * ((a #Z ((numerator q) - (numerator p))) |^ (denominator p)))
by A3, A1, A13, A11, Th22, XREAL_1:159
.=
((denominator p) * (denominator q)) -Root (((a #Z (numerator p)) #Z (ddp + ddq)) * ((a #Z ((numerator q) - (numerator p))) |^ (denominator p)))
by Th36
.=
((denominator p) * (denominator q)) -Root (((a #Z (numerator p)) #Z (ddp + ddq)) * ((a #Z ((numerator q) - (numerator p))) #Z ddp))
by Th36
.=
((denominator p) * (denominator q)) -Root ((a #Z ((numerator p) * (ddp + ddq))) * ((a #Z ((numerator q) - (numerator p))) #Z ddp))
by Th45
.=
((denominator p) * (denominator q)) -Root ((a #Z ((numerator p) * (ddp + ddq))) * (a #Z (((numerator q) - (numerator p)) * ddp)))
by Th45
.=
((denominator p) * (denominator q)) -Root (a #Z ((((numerator p) * ddp) + ((numerator p) * ddq)) + (((numerator q) - (numerator p)) * ddp)))
by A7, Th44
.=
((denominator (p + q)) * n) -Root ((a #Z (numerator (p + q))) #Z k)
by A5, A6, Th45
.=
(((denominator (p + q)) * n) -Root (a #Z (numerator (p + q)))) #Z k
by A4, A6, A15, Th46
.=
((n * (denominator (p + q))) -Root (a #Z (numerator (p + q)))) |^ n
by Th36
.=
(n -Root (a #Q (p + q))) |^ n
by A9, A2, A15, Th25
.=
a #Q (p + q)
by A9, A14, Lm2
; verum