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 ! )

A5: y = [\(y2 / y3)/] ; :: thesis: y = x !

( 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

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
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)/] )

end;( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] )

per cases
( x = 0 or x > 0 )
;

end;

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)/] )

( 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 INT_1:25, NEWTON:12, A2, A1; :: thesis: verum

end;( 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 INT_1:25, NEWTON:12, A2, A1; :: thesis: verum

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)/] )

( 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;( 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

A5: y = [\(y2 / y3)/] ; :: thesis: y = x !