let x, y, z be Nat; ( ( 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 ) )
( 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 )
;
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
;
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
;
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
;
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
;
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
;
( 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;
( 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;
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 )
; ( 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; verum