reconsider d1 = d as Element of NAT by ORDINAL1:def 12;
let a, b be Nat; :: thesis: ( d |^ a divides n & not d |^ (a + 1) divides n & d |^ b divides n & not d |^ (b + 1) divides n implies a = b )
assume that
A9: d |^ a divides n and
A10: ( not d |^ (a + 1) divides n & d |^ b divides n ) and
A11: not d |^ (b + 1) divides n and
A12: a <> b ; :: thesis: contradiction
reconsider a = a, b = b as Element of NAT by ORDINAL1:def 12;
per cases ( a < b or b < a ) by A12, XXREAL_0:1;
suppose A13: a < b ; :: thesis: contradiction
then consider x being Nat such that
A14: a + x = b by NAT_1:10;
reconsider x = x as Element of NAT by ORDINAL1:def 12;
now :: thesis: not 0 + 1 > x
assume 0 + 1 > x ; :: thesis: contradiction
then x = 0 by NAT_1:13;
hence contradiction by A13, A14; :: thesis: verum
end;
then a + 1 <= a + x by XREAL_1:6;
then d1 |^ (a + 1) divides d1 |^ (a + x) by NEWTON:89;
hence contradiction by A10, A14, NAT_D:4; :: thesis: verum
end;
suppose A15: b < a ; :: thesis: contradiction
then consider x being Nat such that
A16: b + x = a by NAT_1:10;
reconsider x = x as Element of NAT by ORDINAL1:def 12;
now :: thesis: not 0 + 1 > x
assume 0 + 1 > x ; :: thesis: contradiction
then x = 0 by NAT_1:13;
hence contradiction by A15, A16; :: thesis: verum
end;
then b + 1 <= b + x by XREAL_1:6;
then d1 |^ (b + 1) divides d1 |^ (b + x) by NEWTON:89;
hence contradiction by A9, A11, A16, NAT_D:4; :: thesis: verum
end;
end;