let x, y, z be Nat; :: thesis: ( ( x >= z & y = x choose z ) iff ex u, v, y1, y2, y3 being Nat st
( y1 = x |^ z & y2 = (u + 1) |^ x & y3 = u |^ z & u > y1 & v = [\(y2 / y3)/] & y,v are_congruent_mod u & y < u & x >= z ) )
thus ( x >= z & y = x choose z implies ex u, v, y1, y2, y3 being Nat st
( y1 = x |^ z & y2 = (u + 1) |^ x & y3 = u |^ z & u > y1 & v = [\(y2 / y3)/] & y,v are_congruent_mod u & y < u & x >= z ) ) :: thesis: ( ex u, v, y1, y2, y3 being Nat st
( y1 = x |^ z & y2 = (u + 1) |^ x & y3 = u |^ z & u > y1 & v = [\(y2 / y3)/] & y,v are_congruent_mod u & y < u & x >= z ) implies ( x >= z & y = x choose z ) )

proof

assume A1: ( x >= z & y = x choose z ) ; :: thesis: ex u, v, y1, y2, y3 being Nat st
( y1 = x |^ z & y2 = (u + 1) |^ x & y3 = u |^ z & u > y1 & v = [\(y2 / y3)/] & y,v are_congruent_mod u & y < u & x >= z )
set y1 = x |^ z;
set u = (x |^ z) + 1;
set y2 = (((x |^ z) + 1) + 1) |^ x;
set y3 = ((x |^ z) + 1) |^ z;
set v = [\(((((x |^ z) + 1) + 1) |^ x) / (((x |^ z) + 1) |^ z))/];
reconsider v = [\(((((x |^ z) + 1) + 1) |^ x) / (((x |^ z) + 1) |^ z))/] as Element of NAT by INT_1:3, INT_1:54;
take (x |^ z) + 1 ; :: thesis: ex v, y1, y2, y3 being Nat st
( y1 = x |^ z & y2 = (((x |^ z) + 1) + 1) |^ x & y3 = ((x |^ z) + 1) |^ z & (x |^ z) + 1 > y1 & v = [\(y2 / y3)/] & y,v are_congruent_mod (x |^ z) + 1 & y < (x |^ z) + 1 & x >= z )
take v ; :: thesis: ex y1, y2, y3 being Nat st
( y1 = x |^ z & y2 = (((x |^ z) + 1) + 1) |^ x & y3 = ((x |^ z) + 1) |^ z & (x |^ z) + 1 > y1 & v = [\(y2 / y3)/] & y,v are_congruent_mod (x |^ z) + 1 & y < (x |^ z) + 1 & x >= z )
take x |^ z ; :: thesis: ex y2, y3 being Nat st
( x |^ z = x |^ z & y2 = (((x |^ z) + 1) + 1) |^ x & y3 = ((x |^ z) + 1) |^ z & (x |^ z) + 1 > x |^ z & v = [\(y2 / y3)/] & y,v are_congruent_mod (x |^ z) + 1 & y < (x |^ z) + 1 & x >= z )
take (((x |^ z) + 1) + 1) |^ x ; :: thesis: ex y3 being Nat st
( x |^ z = x |^ z & (((x |^ z) + 1) + 1) |^ x = (((x |^ z) + 1) + 1) |^ x & y3 = ((x |^ z) + 1) |^ z & (x |^ z) + 1 > x |^ z & v = [\(((((x |^ z) + 1) + 1) |^ x) / y3)/] & y,v are_congruent_mod (x |^ z) + 1 & y < (x |^ z) + 1 & x >= z )
take ((x |^ z) + 1) |^ z ; :: thesis: ( x |^ z = x |^ z & (((x |^ z) + 1) + 1) |^ x = (((x |^ z) + 1) + 1) |^ x & ((x |^ z) + 1) |^ z = ((x |^ z) + 1) |^ z & (x |^ z) + 1 > x |^ z & v = [\(((((x |^ z) + 1) + 1) |^ x) / (((x |^ z) + 1) |^ z))/] & y,v are_congruent_mod (x |^ z) + 1 & y < (x |^ z) + 1 & x >= z )
thus A2: ( x |^ z = x |^ z & (((x |^ z) + 1) + 1) |^ x = (((x |^ z) + 1) + 1) |^ x & ((x |^ z) + 1) |^ z = ((x |^ z) + 1) |^ z & (x |^ z) + 1 > x |^ z & v = [\(((((x |^ z) + 1) + 1) |^ x) / (((x |^ z) + 1) |^ z))/] ) by NAT_1:13; :: thesis: ( y,v are_congruent_mod (x |^ z) + 1 & y < (x |^ z) + 1 & x >= z )
A3: v mod ((x |^ z) + 1) = y by A2, Th15, A1;
y < (x |^ z) + 1 by A1, NAT_1:13, Th13;
then y mod ((x |^ z) + 1) = y by NAT_D:24;
then (y - v) mod ((x |^ z) + 1) = 0 by A3, INT_4:22;
then (x |^ z) + 1 divides y - v by INT_1:62;
hence ( y,v are_congruent_mod (x |^ z) + 1 & y < (x |^ z) + 1 & x >= z ) by A1, NAT_1:13, Th13, INT_1:def 4; :: thesis: verum

end;

given u, v, y1, y2, y3 being Nat such that A4: ( y1 = x |^ z & y2 = (u + 1) |^ x & y3 = u |^ z ) and
A5: ( u > y1 & v = [\(y2 / y3)/] & y,v are_congruent_mod u ) and
A6: ( y < u & x >= z ) ; :: thesis: ( x >= z & y = x choose z )
u divides y - v by A5, INT_1:def 4;
then (y - v) mod u = 0 by INT_1:62, A5;
then y mod u = v mod u by INT_4:22, A5;
then y mod u = x choose z by Th15, A4, A5, A6;
hence ( x >= z & y = x choose z ) by A6, NAT_D:24; :: thesis: verum