let a be Real; for p, q being Rational st a > 0 holds
(a #Q p) #Q q = a #Q (p * q)
let p, q be Rational; ( a > 0 implies (a #Q p) #Q q = a #Q (p * q) )
A1:
denominator p >= 1
by RAT_1:11;
p = (numerator p) / (denominator p)
by RAT_1:15;
then p * q =
((numerator p) / (denominator p)) * ((numerator q) / (denominator q))
by RAT_1:15
.=
(((numerator p) / (denominator p)) * (numerator q)) / (denominator q)
.=
((numerator p) * (numerator q)) / ((denominator p) * (denominator q))
by XCMPLX_1:83
;
then consider n being Nat such that
A2:
(numerator p) * (numerator q) = (numerator (p * q)) * n
and
A3:
(denominator p) * (denominator q) = (denominator (p * q)) * n
by RAT_1:27;
A4:
(denominator (p * q)) * n >= 0 + 1
by A3, NAT_1:13;
n > 0
by A3;
then A5:
n >= 0 + 1
by NAT_1:13;
reconsider k = n as Integer ;
A6:
denominator q >= 1
by RAT_1:11;
A7:
denominator (p * q) >= 1
by RAT_1:11;
assume A8:
a > 0
; (a #Q p) #Q q = a #Q (p * q)
then A9:
a #Z ((numerator p) * (numerator q)) >= 0
by Th39;
A10:
a #Q (p * q) > 0
by A8, Th52;
A11:
a #Z (numerator (p * q)) > 0
by A8, Th39;
a #Z (numerator p) > 0
by A8, Th39;
hence (a #Q p) #Q q =
(denominator q) -Root ((denominator p) -Root ((a #Z (numerator p)) #Z (numerator q)))
by Th46, RAT_1:11
.=
(denominator q) -Root ((denominator p) -Root (a #Z ((numerator p) * (numerator q))))
by Th45
.=
((denominator (p * q)) * n) -Root (a #Z ((numerator (p * q)) * k))
by A1, A6, A9, A2, A3, Th25
.=
((denominator (p * q)) * n) -Root ((a #Z (numerator (p * q))) #Z k)
by Th45
.=
(((denominator (p * q)) * n) -Root (a #Z (numerator (p * q)))) #Z k
by A11, A4, Th46
.=
((n * (denominator (p * q))) -Root (a #Z (numerator (p * q)))) |^ n
by Th36
.=
(n -Root (a #Q (p * q))) |^ n
by A5, A7, A11, Th25
.=
a #Q (p * q)
by A5, A10, Lm2
;
verum