let k, n be Nat; :: thesis: ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } iff ( n is prime & k in Segm n & not k in {0} ) )

set X = { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ;

thus ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } implies ( n is prime & k in Segm n & not k in {0} ) ) :: thesis: ( n is prime & k in Segm n & not k in {0} implies ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ) )

A4: n is prime and

A5: k in Segm n and

A6: not k in {0} ; :: thesis: ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } )

A7: k <> 0 by A6, TARSKI:def 1;

then A8: k >= 1 by NAT_1:14;

A9: k < n by A5, NAT_1:44;

then ( k in NAT & k,n are_coprime ) by A4, A7, Th2, ORDINAL1:def 12;

hence ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ) by A4, A9, A8; :: thesis: verum

set X = { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ;

thus ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } implies ( n is prime & k in Segm n & not k in {0} ) ) :: thesis: ( n is prime & k in Segm n & not k in {0} implies ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ) )

proof

assume that
assume that

A1: n is prime and

A2: k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ; :: thesis: ( n is prime & k in Segm n & not k in {0} )

A3: ex kk being Element of NAT st

( kk = k & n,kk are_coprime & kk >= 1 & kk <= n ) by A2;

then k <> n by A1, Lm2, Th1;

then k < n by A3, XXREAL_0:1;

hence ( n is prime & k in Segm n & not k in {0} ) by A1, A3, NAT_1:44, TARSKI:def 1; :: thesis: verum

end;A1: n is prime and

A2: k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ; :: thesis: ( n is prime & k in Segm n & not k in {0} )

A3: ex kk being Element of NAT st

( kk = k & n,kk are_coprime & kk >= 1 & kk <= n ) by A2;

then k <> n by A1, Lm2, Th1;

then k < n by A3, XXREAL_0:1;

hence ( n is prime & k in Segm n & not k in {0} ) by A1, A3, NAT_1:44, TARSKI:def 1; :: thesis: verum

A4: n is prime and

A5: k in Segm n and

A6: not k in {0} ; :: thesis: ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } )

A7: k <> 0 by A6, TARSKI:def 1;

then A8: k >= 1 by NAT_1:14;

A9: k < n by A5, NAT_1:44;

then ( k in NAT & k,n are_coprime ) by A4, A7, Th2, ORDINAL1:def 12;

hence ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ) by A4, A9, A8; :: thesis: verum