let m be Nat; :: thesis: for d, e being Element of NAT st d in dom (Sgm (RelPrimes m)) & e in dom (Sgm (RelPrimes m)) & d <> e holds
not (Sgm (RelPrimes m)) . d,(Sgm (RelPrimes m)) . e are_congruent_mod m
let d, e be Element of NAT ; :: thesis: ( d in dom (Sgm (RelPrimes m)) & e in dom (Sgm (RelPrimes m)) & d <> e implies not (Sgm (RelPrimes m)) . d,(Sgm (RelPrimes m)) . e are_congruent_mod m )
assume A1: ( d in dom (Sgm (RelPrimes m)) & e in dom (Sgm (RelPrimes m)) & d <> e ) ; :: thesis: not (Sgm (RelPrimes m)) . d,(Sgm (RelPrimes m)) . e are_congruent_mod m
A2: RelPrimes m c= Seg m by Th1;
rng (Sgm (RelPrimes m)) = RelPrimes m by A2, FINSEQ_1:def 13;
then A3: ( (Sgm (RelPrimes m)) . d in RelPrimes m & (Sgm (RelPrimes m)) . e in RelPrimes m ) by A1, FUNCT_1:def 3;
then consider k1 being Element of NAT such that
A4: ( k1 = (Sgm (RelPrimes m)) . d & m,k1 are_coprime & k1 >= 1 & k1 <= m ) ;
consider k2 being Element of NAT such that
A5: ( k2 = (Sgm (RelPrimes m)) . e & m,k2 are_coprime & k2 >= 1 & k2 <= m ) by A3;
A6: ( ((Sgm (RelPrimes m)) . d) - ((Sgm (RelPrimes m)) . e) <= m - 1 & 1 - m <= ((Sgm (RelPrimes m)) . d) - ((Sgm (RelPrimes m)) . e) ) by A4, A5, XREAL_1:13;
A7: m - 1 < m by XREAL_1:146;
A8: ((Sgm (RelPrimes m)) . d) - ((Sgm (RelPrimes m)) . e) < m by A6, XXREAL_0:2, XREAL_1:146;
- m < - (m - 1) by A7, XREAL_1:24;
then - m < ((Sgm (RelPrimes m)) . d) - ((Sgm (RelPrimes m)) . e) by A6, XXREAL_0:2;
then A9: |.(((Sgm (RelPrimes m)) . d) - ((Sgm (RelPrimes m)) . e)).| < m by A8, SEQ_2:1;
now :: thesis: not (Sgm (RelPrimes m)) . d,(Sgm (RelPrimes m)) . e are_congruent_mod m
assume (Sgm (RelPrimes m)) . d,(Sgm (RelPrimes m)) . e are_congruent_mod m ; :: thesis: contradiction
then A10: m divides ((Sgm (RelPrimes m)) . d) - ((Sgm (RelPrimes m)) . e) by INT_2:15;
Sgm (RelPrimes m) is one-to-one by A2, FINSEQ_3:92;
then ((Sgm (RelPrimes m)) . d) - ((Sgm (RelPrimes m)) . e) <> 0 by A1, FUNCT_1:def 4;
then |.m.| <= |.(((Sgm (RelPrimes m)) . d) - ((Sgm (RelPrimes m)) . e)).| by A10, INT_4:6;
hence contradiction by A9, ABSVALUE:def 1; :: thesis: verum
end;
hence not (Sgm (RelPrimes m)) . d,(Sgm (RelPrimes m)) . e are_congruent_mod m ; :: thesis: verum