let x, y be Nat; :: thesis: ( y = x ! iff ex n, y1, y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] ) )
thus ( y = x ! implies ex n, y1, y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] ) ) :: thesis: ( ex n, y1, y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] ) implies y = x ! )
proof
assume A1: y = x ! ; :: thesis: ex n, y1, y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] )
per cases ( x = 0 or x > 0 ) ;
suppose A2: x = 0 ; :: thesis: ex n, y1, y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] )
take n = 1; :: thesis: ex y1, y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] )
take y1 = 0 ; :: thesis: ex y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] )
take y2 = 1; :: thesis: ex y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] )
take y3 = 1; :: thesis: ( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] )
thus ( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 ) by A2, NEWTON:19; :: thesis: y = [\(y2 / y3)/]
thus y = [\(y2 / y3)/] by NEWTON:12, A2, A1; :: thesis: verum
end;
suppose A3: x > 0 ; :: thesis: ex n, y1, y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] )
take n = ((2 * x) |^ (x + 1)) + 1; :: thesis: ex y1, y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] )
take y1 = (2 * x) |^ (x + 1); :: thesis: ex y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] )
take y2 = n |^ x; :: thesis: ex y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] )
take y3 = n choose x; :: thesis: ( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] )
n > y1 by NAT_1:13;
hence ( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] ) by A1, A3, Th17; :: thesis: verum
end;
end;
end;
given n, y1, y2, y3 being Nat such that A4: ( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 ) and
A5: y = [\(y2 / y3)/] ; :: thesis: y = x !
per cases ( x = 0 or x > 0 ) ;
suppose A6: x = 0 ; :: thesis: y = x !
then ( y1 = 0 & y2 = 1 & y3 = 1 ) by A4, NEWTON:4, NEWTON:19;
hence y = x ! by NEWTON:12, A6, A5; :: thesis: verum
end;
suppose x > 0 ; :: thesis: y = x !
hence y = x ! by A4, A5, Th17; :: thesis: verum
end;
end;