let a be real number ; :: thesis: for p, q being Rational st a > 0 holds
(a #Q p) #Q q = a #Q (p * q)
let p, q be Rational; :: thesis: ( a > 0 implies (a #Q p) #Q q = a #Q (p * q) )
assume A1: a > 0 ; :: thesis: (a #Q p) #Q q = a #Q (p * q)
then A2: a #Z (numerator p) > 0 by Th49;
A3: denominator p >= 1 by RAT_1:29;
A4: denominator q >= 1 by RAT_1:29;
A5: a #Z ((numerator p) * (numerator q)) >= 0 by A1, Th49;
A6: denominator p <> 0 by RAT_1:def 3;
denominator q <> 0 by RAT_1:def 3;
then A7: (denominator p) * (denominator q) <> 0 by A6, XCMPLX_1:6;
then A8: (denominator p) * (denominator q) > 0 ;
A9: denominator (p * q) > 0 by RAT_1:27;
p = (numerator p) / (denominator p) by RAT_1:37;
then p * q = ((numerator p) / (denominator p)) * ((numerator q) / (denominator q)) by RAT_1:37
.= (((numerator p) / (denominator p)) * (numerator q)) / (denominator q)
.= ((numerator p) * (numerator q)) / ((denominator p) * (denominator q)) by XCMPLX_1:84 ;
then consider n being Element of NAT such that
A11: ( (numerator p) * (numerator q) = (numerator (p * q)) * n & (denominator p) * (denominator q) = (denominator (p * q)) * n ) by A7, RAT_1:60;
((denominator (p * q)) * n) / (denominator (p * q)) > 0 by A8, A9, A11, XREAL_1:141;
then n > 0 ;
then A12: n >= 0 + 1 by NAT_1:13;
A13: denominator (p * q) >= 1 by RAT_1:29;
reconsider k = n as Integer ;
A14: a #Z (numerator (p * q)) > 0 by A1, Th49;
A15: (denominator (p * q)) * n >= 0 + 1 by A8, A11, NAT_1:13;
A16: a #Q (p * q) > 0 by A1, Th63;
thus (a #Q p) #Q q = (denominator q) -Root ((denominator p) -Root ((a #Z (numerator p)) #Z (numerator q))) by A2, Th56, RAT_1:29
.= (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 A3, A4, A5, A11, 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, A15, Th56
.= ((n * (denominator (p * q))) -Root (a #Z (numerator (p * q)))) |^ n by Th46
.= (n -Root (a #Q (p * q))) |^ n by A12, A13, A14, Th34
.= a #Q (p * q) by A12, A16, Lm2 ; :: thesis: verum