let a, b, n be Nat; :: thesis: for p being prime Nat st a * b = p |^ n holds
ex k, l being Nat st
( a = p |^ k & b = p |^ l & k + l = n )
let p be prime Nat; :: thesis: ( a * b = p |^ n implies ex k, l being Nat st
( a = p |^ k & b = p |^ l & k + l = n ) )
assume A1: a * b = p |^ n ; :: thesis: ex k, l being Nat st
( a = p |^ k & b = p |^ l & k + l = n )
then a divides p |^ n ;
then consider k being Nat such that
A2: ( a = p |^ k & k <= n ) by GROUPP_1:2;
b divides p |^ n by A1;
then consider l being Nat such that
A3: ( b = p |^ l & l <= n ) by GROUPP_1:2;
p |^ n = p |^ (k + l) by NEWTON:8, A1, A2, A3;
then n = k + l by PEPIN:30, Def0;
hence ex k, l being Nat st
( a = p |^ k & b = p |^ l & k + l = n ) by A2, A3; :: thesis: verum