let a be real number ; 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;
A2:
denominator q <> 0
by RAT_1:def 3;
A3:
denominator p <> 0
by RAT_1:def 3;
then A4:
(denominator p) * (denominator q) <> 0
by A2, XCMPLX_1:6;
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 Element of NAT such that
A5:
(numerator p) * (numerator q) = (numerator (p * q)) * n
and
A6:
(denominator p) * (denominator q) = (denominator (p * q)) * n
by A3, A2, RAT_1:27, XCMPLX_1:6;
A7:
(denominator (p * q)) * n >= 0 + 1
by A4, A6, NAT_1:13;
n > 0
by A4, A6;
then A8:
n >= 0 + 1
by NAT_1:13;
reconsider k = n as Integer ;
A9:
denominator q >= 1
by RAT_1:11;
A10:
denominator (p * q) >= 1
by RAT_1:11;
assume A11:
a > 0
; (a #Q p) #Q q = a #Q (p * q)
then A12:
a #Z ((numerator p) * (numerator q)) >= 0
by Th49;
A13:
a #Q (p * q) > 0
by A11, Th63;
A14:
a #Z (numerator (p * q)) > 0
by A11, Th49;
a #Z (numerator p) > 0
by A11, Th49;
hence (a #Q p) #Q q =
(denominator q) -Root ((denominator p) -Root ((a #Z (numerator p)) #Z (numerator q)))
by Th56, RAT_1:11
.=
(denominator q) -Root ((denominator p) -Root (a #Z ((numerator p) * (numerator q))))
by Th55
.=
((denominator (p * q)) * n) -Root (a #Z ((numerator (p * q)) * k))
by A1, A9, A12, A5, A6, Th34
.=
((denominator (p * q)) * n) -Root ((a #Z (numerator (p * q))) #Z k)
by Th55
.=
(((denominator (p * q)) * n) -Root (a #Z (numerator (p * q)))) #Z k
by A14, A7, Th56
.=
((n * (denominator (p * q))) -Root (a #Z (numerator (p * q)))) |^ n
by Th46
.=
(n -Root (a #Q (p * q))) |^ n
by A8, A10, A14, Th34
.=
a #Q (p * q)
by A8, A13, Lm2
;
verum