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