let n be Nat; :: thesis: for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } is diophantine Subset of ()
let i1, i2, i3 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } is diophantine Subset of ()
set n7 = n + 7;
set WW = { p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } ;
{ p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } c= n -xtuples_of NAT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } or y in n -xtuples_of NAT )
assume y in { p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } ; :: thesis:
then ex p being n -element XFinSequence of NAT st
( y = p & p . i2 = (p . i1) |^ (p . i3) ) ;
hence y in n -xtuples_of NAT by HILB10_2:def 5; :: thesis: verum
end;
then reconsider WW = { p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } as Subset of () ;
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } is diophantine Subset of ()
end;
suppose A1: n <> 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } is diophantine Subset of ()
n = n + 0 ;
then reconsider N = n, I1 = i1, I2 = i2, I3 = i3, N1 = n + 1, N2 = n + 2, N3 = n + 3, N4 = n + 4, N5 = n + 5, N6 = n + 6 as Element of n + 7 by ;
defpred S1[ XFinSequence of NAT ] means \$1 . I1 = 0 ;
A2: { p where p is n + 7 -element XFinSequence of NAT : S1[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th14;
defpred S2[ XFinSequence of NAT ] means \$1 . I1 = 1;
A3: { p where p is n + 7 -element XFinSequence of NAT : S2[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th14;
defpred S3[ XFinSequence of NAT ] means 1 * (\$1 . I1) > (0 * (\$1 . I2)) + 1;
A4: { p where p is n + 7 -element XFinSequence of NAT : S3[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th7;
defpred S4[ XFinSequence of NAT ] means \$1 . I2 = 0 ;
A5: { p where p is n + 7 -element XFinSequence of NAT : S4[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th14;
defpred S5[ XFinSequence of NAT ] means \$1 . I2 = 1;
A6: { p where p is n + 7 -element XFinSequence of NAT : S5[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th14;
defpred S6[ XFinSequence of NAT ] means \$1 . I3 = 0 ;
A7: { p where p is n + 7 -element XFinSequence of NAT : S6[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th14;
defpred S7[ XFinSequence of NAT ] means 1 * (\$1 . I3) > (0 * (\$1 . I1)) + 0;
A8: { p where p is n + 7 -element XFinSequence of NAT : S7[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th7;
defpred S8[ XFinSequence of NAT ] means 1 * (\$1 . N4) = (1 * (\$1 . I3)) + 1;
A9: { p where p is n + 7 -element XFinSequence of NAT : S8[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th6;
defpred S9[ XFinSequence of NAT ] means 1 * (\$1 . N5) = (1 * (\$1 . N3)) * (\$1 . I1);
A10: { p where p is n + 7 -element XFinSequence of NAT : S9[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th9;
defpred S10[ XFinSequence of NAT ] means ( \$1 . N = Py ((\$1 . I1),(\$1 . N4)) & \$1 . I1 > 1 );
A11: { p where p is n + 7 -element XFinSequence of NAT : S10[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th23;
defpred S11[ XFinSequence of NAT ] means 1 * (\$1 . N3) > (2 * (\$1 . I3)) * (\$1 . N);
A12: { p where p is n + 7 -element XFinSequence of NAT : S11[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th17;
defpred S12[ XFinSequence of NAT ] means ( \$1 . N1 = Py ((\$1 . N3),(\$1 . N4)) & \$1 . N3 > 1 );
A13: { p where p is n + 7 -element XFinSequence of NAT : S12[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th23;
defpred S13[ XFinSequence of NAT ] means ( \$1 . N2 = Py ((\$1 . N5),(\$1 . N4)) & \$1 . N5 > 1 );
A14: { p where p is n + 7 -element XFinSequence of NAT : S13[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th23;
defpred S14[ XFinSequence of NAT ] means 1 * (\$1 . N6) = (1 * (\$1 . I2)) * (\$1 . N1);
A15: { p where p is n + 7 -element XFinSequence of NAT : S14[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th9;
defpred S15[ XFinSequence of NAT ] means 1 * (\$1 . N6) >= (1 * (\$1 . N2)) + 0;
A16: { p where p is n + 7 -element XFinSequence of NAT : S15[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th8;
defpred S16[ XFinSequence of NAT ] means 2 * (\$1 . N6) < (1 * (\$1 . N1)) + (2 * (\$1 . N2));
A17: { p where p is n + 7 -element XFinSequence of NAT : S16[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th18;
defpred S17[ XFinSequence of NAT ] means 1 * (\$1 . N2) >= (1 * (\$1 . N6)) + 0;
A18: { p where p is n + 7 -element XFinSequence of NAT : S17[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th8;
defpred S18[ XFinSequence of NAT ] means (- 2) * (\$1 . N6) < (1 * (\$1 . N1)) + ((- 2) * (\$1 . N2));
A19: { p where p is n + 7 -element XFinSequence of NAT : S18[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) by Th18;
defpred S19[ XFinSequence of NAT ] means ( S5[\$1] & S6[\$1] );
defpred S20[ XFinSequence of NAT ] means ( S1[\$1] & S4[\$1] );
defpred S21[ XFinSequence of NAT ] means ( S20[\$1] & S7[\$1] );
defpred S22[ XFinSequence of NAT ] means ( S2[\$1] & S5[\$1] );
defpred S23[ XFinSequence of NAT ] means ( S22[\$1] & S7[\$1] );
defpred S24[ XFinSequence of NAT ] means ( S3[\$1] & S7[\$1] );
defpred S25[ XFinSequence of NAT ] means ( S15[\$1] & S16[\$1] );
defpred S26[ XFinSequence of NAT ] means ( S17[\$1] & S18[\$1] );
{ p where p is n + 7 -element XFinSequence of NAT : ( S5[p] & S6[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A20: { p where p is n + 7 -element XFinSequence of NAT : S19[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S1[p] & S4[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A21: { p where p is n + 7 -element XFinSequence of NAT : S20[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S20[p] & S7[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A22: { p where p is n + 7 -element XFinSequence of NAT : S21[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S2[p] & S5[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A23: { p where p is n + 7 -element XFinSequence of NAT : S22[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S22[p] & S7[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A24: { p where p is n + 7 -element XFinSequence of NAT : S23[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S3[p] & S7[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A25: { p where p is n + 7 -element XFinSequence of NAT : S24[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S15[p] & S16[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A26: { p where p is n + 7 -element XFinSequence of NAT : S25[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S17[p] & S18[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A27: { p where p is n + 7 -element XFinSequence of NAT : S26[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
defpred S27[ XFinSequence of NAT ] means ( S25[\$1] or S26[\$1] );
{ p where p is n + 7 -element XFinSequence of NAT : ( S25[p] or S26[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A28: { p where p is n + 7 -element XFinSequence of NAT : S27[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
defpred S28[ XFinSequence of NAT ] means ( S19[\$1] or S21[\$1] );
{ p where p is n + 7 -element XFinSequence of NAT : ( S19[p] or S21[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A29: { p where p is n + 7 -element XFinSequence of NAT : S28[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
defpred S29[ XFinSequence of NAT ] means ( S28[\$1] or S23[\$1] );
{ p where p is n + 7 -element XFinSequence of NAT : ( S28[p] or S23[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A30: { p where p is n + 7 -element XFinSequence of NAT : S29[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
defpred S30[ XFinSequence of NAT ] means ( S8[\$1] & S9[\$1] );
defpred S31[ XFinSequence of NAT ] means ( S10[\$1] & S11[\$1] );
defpred S32[ XFinSequence of NAT ] means ( S31[\$1] & S12[\$1] );
defpred S33[ XFinSequence of NAT ] means ( S32[\$1] & S13[\$1] );
defpred S34[ XFinSequence of NAT ] means ( S33[\$1] & S27[\$1] );
defpred S35[ XFinSequence of NAT ] means ( S24[\$1] & S34[\$1] );
defpred S36[ XFinSequence of NAT ] means ( S35[\$1] & S30[\$1] );
defpred S37[ XFinSequence of NAT ] means ( S36[\$1] & S14[\$1] );
{ p where p is n + 7 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A31: { p where p is n + 7 -element XFinSequence of NAT : S30[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S10[p] & S11[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A32: { p where p is n + 7 -element XFinSequence of NAT : S31[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S31[p] & S12[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A33: { p where p is n + 7 -element XFinSequence of NAT : S32[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S32[p] & S13[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A34: { p where p is n + 7 -element XFinSequence of NAT : S33[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S33[p] & S27[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A35: { p where p is n + 7 -element XFinSequence of NAT : S34[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S24[p] & S34[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A36: { p where p is n + 7 -element XFinSequence of NAT : S35[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S35[p] & S30[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A37: { p where p is n + 7 -element XFinSequence of NAT : S36[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
{ p where p is n + 7 -element XFinSequence of NAT : ( S36[p] & S14[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from then A38: { p where p is n + 7 -element XFinSequence of NAT : S37[p] } is diophantine Subset of ((n + 7) -xtuples_of NAT) ;
defpred S38[ XFinSequence of NAT ] means ( S29[\$1] or S37[\$1] );
A39: { p where p is n + 7 -element XFinSequence of NAT : ( S29[p] or S37[p] ) } is diophantine Subset of ((n + 7) -xtuples_of NAT) from set DD = { p where p is n + 7 -element XFinSequence of NAT : S38[p] } ;
set DDR = { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } ;
A40: { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } is diophantine Subset of () by ;
A41: { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } c= WW
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } or o in WW )
assume A42: o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } ; :: thesis: o in WW
consider p being n + 7 -element XFinSequence of NAT such that
A43: ( o = p | n & p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } ) by A42;
consider q being n + 7 -element XFinSequence of NAT such that
A44: ( p = q & S38[q] ) by A43;
( len p = n + 7 & n + 7 >= n ) by ;
then len (p | n) = n by AFINSQ_1:54;
then reconsider pn = p | n as n -element XFinSequence of NAT by CARD_1:def 7;
set x = pn . i1;
set y = pn . i2;
set z = pn . i3;
set y1 = p . N;
set y2 = p . N1;
set y3 = p . N2;
set K = p . N3;
A45: ( pn . i1 = p . i1 & pn . i2 = p . i2 & pn . i3 = p . i3 ) by ;
( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) )
proof
per cases ( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( 1 * (pn . i1) > (0 * (pn . i2)) + 1 & 1 * (pn . i3) > (0 * (pn . i1)) + 0 & p . N = Py ((pn . i1),((pn . i3) + 1)) & 1 * (p . N3) > (2 * (pn . i3)) * (p . N) & p . N1 = Py ((p . N3),((pn . i3) + 1)) & 1 * (p . N2) = Py (((p . N3) * (pn . i1)),((pn . i3) + 1)) & ( ( (1 * (pn . i2)) * (p . N1) >= (1 * (p . N2)) + 0 & (2 * (pn . i2)) * (p . N1) < (1 * (p . N1)) + (2 * (p . N2)) ) or ( 1 * (p . N2) >= (pn . i2) * (p . N1) & ((- 2) * (pn . i2)) * (p . N1) < (1 * (p . N1)) + ((- 2) * (p . N2)) ) ) ) ) by ;
suppose ( pn . i2 = 1 & pn . i3 = 0 ) ; :: thesis: ( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) )

hence ( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) ) ; :: thesis: verum
end;
suppose ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) ; :: thesis: ( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) )

hence ( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) ) ; :: thesis: verum
end;
suppose ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) ; :: thesis: ( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) )

hence ( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) ) ; :: thesis: verum
end;
suppose A46: ( 1 * (pn . i1) > (0 * (pn . i2)) + 1 & 1 * (pn . i3) > (0 * (pn . i1)) + 0 & p . N = Py ((pn . i1),((pn . i3) + 1)) & 1 * (p . N3) > (2 * (pn . i3)) * (p . N) & p . N1 = Py ((p . N3),((pn . i3) + 1)) & 1 * (p . N2) = Py (((p . N3) * (pn . i1)),((pn . i3) + 1)) & ( ( (1 * (pn . i2)) * (p . N1) >= (1 * (p . N2)) + 0 & (2 * (pn . i2)) * (p . N1) < (1 * (p . N1)) + (2 * (p . N2)) ) or ( 1 * (p . N2) >= (pn . i2) * (p . N1) & ((- 2) * (pn . i2)) * (p . N1) < (1 * (p . N1)) + ((- 2) * (p . N2)) ) ) ) ; :: thesis: ( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) )

( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) )
proof
thus ( pn . i1 > 1 & pn . i3 > 0 ) by A46; :: thesis: ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) )

take p . N ; :: thesis: ex y2, y3, K being Nat st
( p . N = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * (p . N) & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) )

take p . N1 ; :: thesis: ex y3, K being Nat st
( p . N = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * (p . N) & p . N1 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / (p . N1)) & (pn . i2) - (y3 / (p . N1)) < 1 / 2 ) or ( 0 <= (y3 / (p . N1)) - (pn . i2) & (y3 / (p . N1)) - (pn . i2) < 1 / 2 ) ) )

take p . N2 ; :: thesis: ex K being Nat st
( p . N = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * (p . N) & p . N1 = Py (K,((pn . i3) + 1)) & p . N2 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - ((p . N2) / (p . N1)) & (pn . i2) - ((p . N2) / (p . N1)) < 1 / 2 ) or ( 0 <= ((p . N2) / (p . N1)) - (pn . i2) & ((p . N2) / (p . N1)) - (pn . i2) < 1 / 2 ) ) )

take p . N3 ; :: thesis: ( p . N = Py ((pn . i1),((pn . i3) + 1)) & p . N3 > (2 * (pn . i3)) * (p . N) & p . N1 = Py ((p . N3),((pn . i3) + 1)) & p . N2 = Py (((p . N3) * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - ((p . N2) / (p . N1)) & (pn . i2) - ((p . N2) / (p . N1)) < 1 / 2 ) or ( 0 <= ((p . N2) / (p . N1)) - (pn . i2) & ((p . N2) / (p . N1)) - (pn . i2) < 1 / 2 ) ) )
thus ( p . N = Py ((pn . i1),((pn . i3) + 1)) & p . N3 > (2 * (pn . i3)) * (p . N) & p . N1 = Py ((p . N3),((pn . i3) + 1)) & p . N2 = Py (((p . N3) * (pn . i1)),((pn . i3) + 1)) ) by A46; :: thesis: ( ( 0 <= (pn . i2) - ((p . N2) / (p . N1)) & (pn . i2) - ((p . N2) / (p . N1)) < 1 / 2 ) or ( 0 <= ((p . N2) / (p . N1)) - (pn . i2) & ((p . N2) / (p . N1)) - (pn . i2) < 1 / 2 ) )
not pn . i1 is trivial by ;
then ( p . N > 0 & 2 * (pn . i3) > 0 ) by ;
then (2 * (pn . i3)) * (p . N) > 0 by XREAL_1:129;
then (2 * (pn . i3)) * (p . N) >= 1 by NAT_1:14;
then p . N3 > 1 by ;
then not p . N3 is trivial by NEWTON03:def 1;
then A47: p . N1 > 0 by ;
per cases ( ( (pn . i2) * (p . N1) >= p . N2 & (2 * (pn . i2)) * (p . N1) < (1 * (p . N1)) + (2 * (p . N2)) ) or ( p . N2 >= (pn . i2) * (p . N1) & ((- 2) * (pn . i2)) * (p . N1) < (1 * (p . N1)) + ((- 2) * (p . N2)) ) ) by A46;
suppose ( (pn . i2) * (p . N1) >= p . N2 & (2 * (pn . i2)) * (p . N1) < (1 * (p . N1)) + (2 * (p . N2)) ) ; :: thesis: ( ( 0 <= (pn . i2) - ((p . N2) / (p . N1)) & (pn . i2) - ((p . N2) / (p . N1)) < 1 / 2 ) or ( 0 <= ((p . N2) / (p . N1)) - (pn . i2) & ((p . N2) / (p . N1)) - (pn . i2) < 1 / 2 ) )
then ( ((pn . i2) * (p . N1)) / (p . N1) >= (p . N2) / (p . N1) & ((2 * (pn . i2)) * (p . N1)) / (p . N1) < ((1 * (p . N1)) + (2 * (p . N2))) / (p . N1) ) by ;
then ( pn . i2 >= (p . N2) / (p . N1) & 2 * (pn . i2) < ((1 * (p . N1)) + (2 * (p . N2))) / (p . N1) ) by ;
then A48: ( (pn . i2) - ((p . N2) / (p . N1)) >= ((p . N2) / (p . N1)) - ((p . N2) / (p . N1)) & (2 * (pn . i2)) * 1 < ((1 * (p . N1)) / (p . N1)) + ((2 * (p . N2)) / (p . N1)) ) by ;
then ( (pn . i2) - ((p . N2) / (p . N1)) >= 0 & 2 * (pn . i2) < 1 + ((2 * (p . N2)) / (p . N1)) ) by ;
then (2 * (pn . i2)) / 2 < (1 + ((2 * (p . N2)) / (p . N1))) / 2 by XREAL_1:74;
then (pn . i2) / (2 / 2) < (1 / 2) + (((2 * (p . N2)) / (p . N1)) / 2) ;
then A49: pn . i2 < (1 / 2) + ((2 * (p . N2)) / ((p . N1) * 2)) by XCMPLX_1:78;
(2 * (p . N2)) / ((p . N1) * 2) = (p . N2) / (p . N1) by XCMPLX_1:91;
then (pn . i2) - ((p . N2) / (p . N1)) < ((1 / 2) + ((p . N2) / (p . N1))) - ((p . N2) / (p . N1)) by ;
hence ( ( 0 <= (pn . i2) - ((p . N2) / (p . N1)) & (pn . i2) - ((p . N2) / (p . N1)) < 1 / 2 ) or ( 0 <= ((p . N2) / (p . N1)) - (pn . i2) & ((p . N2) / (p . N1)) - (pn . i2) < 1 / 2 ) ) by A48; :: thesis: verum
end;
suppose A50: ( p . N2 >= (pn . i2) * (p . N1) & ((- 2) * (pn . i2)) * (p . N1) < (1 * (p . N1)) + ((- 2) * (p . N2)) ) ; :: thesis: ( ( 0 <= (pn . i2) - ((p . N2) / (p . N1)) & (pn . i2) - ((p . N2) / (p . N1)) < 1 / 2 ) or ( 0 <= ((p . N2) / (p . N1)) - (pn . i2) & ((p . N2) / (p . N1)) - (pn . i2) < 1 / 2 ) )
then ( (p . N2) / (p . N1) >= ((pn . i2) * (p . N1)) / (p . N1) & ((- 2) * (pn . i2)) * (p . N1) < (1 * (p . N1)) + ((- 2) * (p . N2)) ) by XREAL_1:72;
then (p . N2) / (p . N1) >= pn . i2 by ;
then A51: ((p . N2) / (p . N1)) - (pn . i2) >= (pn . i2) - (pn . i2) by XREAL_1:9;
(((- 2) * (pn . i2)) * (p . N1)) / (p . N1) < ((1 * (p . N1)) + ((- 2) * (p . N2))) / (p . N1) by ;
then (- 2) * (pn . i2) < ((1 * (p . N1)) + ((- 2) * (p . N2))) / (p . N1) by ;
then (- 2) * (pn . i2) < ((1 * (p . N1)) / (p . N1)) + (((- 2) * (p . N2)) / (p . N1)) by XCMPLX_1:62;
then (- 2) * (pn . i2) < 1 + (((- 2) * (p . N2)) / (p . N1)) by ;
then A52: (1 + (((- 2) * (p . N2)) / (p . N1))) / (- 2) < ((- 2) * (pn . i2)) / (- 2) by XREAL_1:75;
A53: (((- 2) * (p . N2)) / (p . N1)) / (- 2) = ((- 2) * (p . N2)) / ((p . N1) * (- 2)) by XCMPLX_1:78
.= (p . N2) / (p . N1) by XCMPLX_1:91 ;
(- (1 / 2)) + ((p . N2) / (p . N1)) < pn . i2 by ;
then 1 / 2 > - ((pn . i2) - ((p . N2) / (p . N1))) by ;
hence ( ( 0 <= (pn . i2) - ((p . N2) / (p . N1)) & (pn . i2) - ((p . N2) / (p . N1)) < 1 / 2 ) or ( 0 <= ((p . N2) / (p . N1)) - (pn . i2) & ((p . N2) / (p . N1)) - (pn . i2) < 1 / 2 ) ) by A51; :: thesis: verum
end;
end;
end;
hence ( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) ) ; :: thesis: verum
end;
end;
end;
then pn . i2 = (pn . i1) |^ (pn . i3) by HILB10_1:39;
hence o in WW by A43; :: thesis: verum
end;
WW c= { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } }
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in WW or o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } )
assume A54: o in WW ; :: thesis: o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } }
consider p being n -element XFinSequence of NAT such that
A55: ( o = p & p . i2 = (p . i1) |^ (p . i3) ) by A54;
set x = p . i1;
set y = p . i2;
set z = p . i3;
per cases ( ( p . i2 = 1 & p . i3 = 0 ) or ( p . i1 = 0 & p . i2 = 0 & p . i3 > 0 ) or ( p . i1 = 1 & p . i2 = 1 & p . i3 > 0 ) or ( p . i1 > 1 & p . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((p . i1),((p . i3) + 1)) & K > (2 * (p . i3)) * y1 & y2 = Py (K,((p . i3) + 1)) & y3 = Py ((K * (p . i1)),((p . i3) + 1)) & ( ( 0 <= (p . i2) - (y3 / y2) & (p . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (p . i2) & (y3 / y2) - (p . i2) < 1 / 2 ) ) ) ) )
by ;
suppose A56: ( ( p . i2 = 1 & p . i3 = 0 ) or ( p . i1 = 0 & p . i2 = 0 & p . i3 > 0 ) or ( p . i1 = 1 & p . i2 = 1 & p . i3 > 0 ) ) ; :: thesis: o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } }
reconsider Z = 0 , z1 = (p . i3) + 1 as Element of NAT ;
set Y = ((((() ^ <%Z%>) ^ <%Z%>) ^ <%z1%>) ^ <%Z%>) ^ <%Z%>;
set PY = p ^ (((((() ^ <%Z%>) ^ <%Z%>) ^ <%z1%>) ^ <%Z%>) ^ <%Z%>);
A57: ( len p = n & len (((((() ^ <%Z%>) ^ <%Z%>) ^ <%z1%>) ^ <%Z%>) ^ <%Z%>) = 7 ) by CARD_1:def 7;
A58: (p ^ (((((() ^ <%Z%>) ^ <%Z%>) ^ <%z1%>) ^ <%Z%>) ^ <%Z%>)) | n = p by ;
( S19[p ^ (((((() ^ <%Z%>) ^ <%Z%>) ^ <%z1%>) ^ <%Z%>) ^ <%Z%>)] or S21[p ^ (((((() ^ <%Z%>) ^ <%Z%>) ^ <%z1%>) ^ <%Z%>) ^ <%Z%>)] or S23[p ^ (((((() ^ <%Z%>) ^ <%Z%>) ^ <%z1%>) ^ <%Z%>) ^ <%Z%>)] ) by A56, A58, A1, Th4;
then p ^ (((((() ^ <%Z%>) ^ <%Z%>) ^ <%z1%>) ^ <%Z%>) ^ <%Z%>) in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } ;
hence o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } by ; :: thesis: verum
end;
suppose A59: ( p . i1 > 1 & p . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((p . i1),((p . i3) + 1)) & K > (2 * (p . i3)) * y1 & y2 = Py (K,((p . i3) + 1)) & y3 = Py ((K * (p . i1)),((p . i3) + 1)) & ( ( 0 <= (p . i2) - (y3 / y2) & (p . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (p . i2) & (y3 / y2) - (p . i2) < 1 / 2 ) ) ) ) ; :: thesis: o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } }
then consider y1, y2, y3, K being Nat such that
A60: ( y1 = Py ((p . i1),((p . i3) + 1)) & K > (2 * (p . i3)) * y1 & y2 = Py (K,((p . i3) + 1)) & y3 = Py ((K * (p . i1)),((p . i3) + 1)) & ( ( 0 <= (p . i2) - (y3 / y2) & (p . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (p . i2) & (y3 / y2) - (p . i2) < 1 / 2 ) ) ) ;
reconsider y1 = y1, y2 = y2, y3 = y3, K = K, z1 = (p . i3) + 1 as Element of NAT by ORDINAL1:def 12;
reconsider Kx = K * (p . i1), yy2 = (p . i2) * y2 as Element of NAT ;
set Y = (((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>;
set PY = p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>);
A61: ( len p = n & len ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) = 7 ) by CARD_1:def 7;
A62: (p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) | n = p by ;
4 in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) by ;
then A63: (p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 4) = ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 4 by
.= z1 by AFINSQ_1:48 ;
0 in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) by ;
then A64: (p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 0) = ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 0 by
.= y1 by AFINSQ_1:48 ;
3 in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) by ;
then A65: (p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 3) = ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 3 by
.= K by AFINSQ_1:48 ;
5 in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) by ;
then A66: (p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 5) = ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 5 by
.= Kx by AFINSQ_1:48 ;
not p . i1 is trivial by ;
then ( y1 > 0 & p . i3 > 0 ) by ;
then (p . i3) * y1 > 0 by XREAL_1:129;
then 2 * ((p . i3) * y1) >= 2 * 1 by ;
then A67: K >= 1 + 1 by ;
then A68: K > 1 by XXREAL_0:2;
1 in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) by ;
then A69: (p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 1) = ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 1 by
.= y2 by AFINSQ_1:48 ;
A70: K * (p . i1) > 1 * 1 by ;
2 in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) by ;
then A71: (p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 2) = ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 2 by
.= y3 by AFINSQ_1:48 ;
6 in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) by ;
then A72: (p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 6) = ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 6 by
.= yy2 by AFINSQ_1:48 ;
not p . i1 is trivial by ;
then ( y1 > 0 & 2 * (p . i3) > 0 ) by ;
then (2 * (p . i3)) * y1 > 0 by XREAL_1:129;
then (2 * (p . i3)) * y1 >= 1 by NAT_1:14;
then K > 1 by ;
then not K is trivial by NEWTON03:def 1;
then A73: y2 > 0 by ;
S27[p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)]
proof
per cases ( ( (p . i2) - (y3 / y2) >= 0 & (p . i2) - (y3 / y2) < 1 / 2 ) or ( (y3 / y2) - (p . i2) >= 0 & (y3 / y2) - (p . i2) < 1 / 2 ) ) by A60;
suppose A74: ( (p . i2) - (y3 / y2) >= 0 & (p . i2) - (y3 / y2) < 1 / 2 ) ; :: thesis: S27[p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)]
((p . i2) - (y3 / y2)) * y2 >= 0 * y2 by A74;
then ((p . i2) * y2) - ((y3 / y2) * y2) >= 0 ;
then ((p . i2) * y2) - (y3 / (y2 / y2)) >= 0 by XCMPLX_1:82;
then ((p . i2) * y2) - (y3 / 1) >= 0 by ;
then A75: (((p . i2) * y2) - y3) + y3 >= 0 + y3 by XREAL_1:6;
((p . i2) - (y3 / y2)) * y2 < (1 / 2) * y2 by ;
then ((p . i2) * y2) - ((y3 / y2) * y2) < (1 / 2) * y2 ;
then ((p . i2) * y2) - (y3 / (y2 / y2)) < (1 / 2) * y2 by XCMPLX_1:82;
then ((p . i2) * y2) - (y3 / 1) < (1 / 2) * y2 by ;
then (((p . i2) * y2) - y3) * 2 < ((1 / 2) * y2) * 2 by XREAL_1:68;
then (((2 * (p . i2)) * y2) - (2 * y3)) + (2 * y3) < (1 * y2) + (2 * y3) by XREAL_1:6;
hence S27[p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)] by A72, A71, A69, A75; :: thesis: verum
end;
suppose A76: ( (y3 / y2) - (p . i2) >= 0 & (y3 / y2) - (p . i2) < 1 / 2 ) ; :: thesis: S27[p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)]
then ((y3 / y2) - (p . i2)) + (p . i2) >= 0 + (p . i2) by XREAL_1:6;
then (y3 / y2) * y2 >= (p . i2) * y2 by XREAL_1:64;
then y3 / (y2 / y2) >= (p . i2) * y2 by XCMPLX_1:82;
then A77: y3 / 1 >= (p . i2) * y2 by ;
((y3 / y2) - (p . i2)) * y2 < (1 / 2) * y2 by ;
then ((y3 / y2) * y2) - ((p . i2) * y2) < (1 / 2) * y2 ;
then (y3 / (y2 / y2)) - ((p . i2) * y2) < (1 / 2) * y2 by XCMPLX_1:82;
then (y3 / 1) - ((p . i2) * y2) < (1 / 2) * y2 by ;
then (y3 - ((p . i2) * y2)) * 2 < ((1 / 2) * y2) * 2 by XREAL_1:68;
then ((- ((2 * (p . i2)) * y2)) + (2 * y3)) - (2 * y3) < (1 * y2) - (2 * y3) by XREAL_1:14;
hence S27[p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)] by A72, A71, A69, A77; :: thesis: verum
end;
end;
end;
then S37[p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)] by A59, A63, A67, XXREAL_0:2, A65, A71, A60, A70, A66, A64, A62, A1, Th4, A69, A72;
then p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } ;
hence o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } by ; :: thesis: verum
end;
end;
end;
hence { p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } is diophantine Subset of () by ; :: thesis: verum
end;
end;