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