:: INT_3 semantic presentation

begin

definition
redefine func multint means :: INT_3:def 1
 for a, b being ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) holds it : ( ( ) ( ) 1-sorted ) . (a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) ,b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) = multreal : ( ( Function-like V29(K7(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ,REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( V50() V51() V52() ) set ) , REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) ) ( Relation-like K7(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ,REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( V50() V51() V52() ) set ) -defined REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) -valued Function-like V29(K7(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ,REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( V50() V51() V52() ) set ) , REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) V50() V51() V52() ) Element of K6(K7(K7(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ,REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( V50() V51() V52() ) set ) ,REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( V50() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) ,b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) ) : ( ( ) ( ) set ) ;
end;

definition
redefine func compint means :: INT_3:def 2
 for a being ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) holds it : ( ( ) ( ) 1-sorted ) . a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) = compreal : ( ( Function-like V29( REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) , REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) -defined REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) -valued Function-like V29( REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) , REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) V50() V51() V52() ) Element of K6(K7(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ,REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( V50() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) . a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) : ( ( ) ( V11() V12() ext-real ) set ) ;
end;

definition
func INT.Ring -> ( ( ) ( ) doubleLoopStr ) equals :: INT_3:def 3
 doubleLoopStr(# INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ,addint : ( ( Function-like V29(K7(INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ,INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() ) set ) , INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) ) ( Relation-like K7(INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ,INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() ) set ) -defined INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued Function-like V29(K7(INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ,INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() ) set ) , INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) V50() V51() V52() ) Element of K6(K7(K7(INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ,INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() ) set ) ,INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,multint : ( ( Function-like V29(K7(INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ,INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() ) set ) , INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) ) ( Relation-like K7(INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ,INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() ) set ) -defined INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued Function-like V29(K7(INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ,INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() ) set ) , INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) V50() V51() V52() ) Element of K6(K7(K7(INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ,INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() ) set ) ,INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,(In (1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) )) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) ,(In (0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) )) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) #) : ( ( strict ) ( strict ) doubleLoopStr ) ;
end;

registration
cluster INT.Ring : ( ( ) ( ) doubleLoopStr ) -> non empty strict ;
end;

registration
cluster the carrier of INT.Ring : ( ( ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non zero ) set ) -> integer-membered ;
end;

registration
let a, b be ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ;
let c, d be ( ( integer ) ( V11() V12() integer ext-real ) Integer) ;
identify ;
identify ;
end;

registration
cluster INT.Ring : ( ( ) ( non empty strict ) doubleLoopStr ) -> well-unital ;
end;

registration
cluster INT.Ring : ( ( ) ( non empty strict unital right_unital well-unital left_unital ) doubleLoopStr ) -> non degenerated right_complementable associative commutative Abelian add-associative right_zeroed distributive domRing-like ;
end;

registration
let a be ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ;
let b be ( ( integer ) ( V11() V12() integer ext-real ) Integer) ;
identify ;
end;

definition
let a be ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ;
:: original: |.
redefine func abs a -> ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) equals :: INT_3:def 4
a : ( ( ) ( ) set ) if a : ( ( ) ( ) set ) >= 0. INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( V11() V12() integer V32() ext-real zero ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) )
otherwise - a : ( ( ) ( ) set ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ;
end;

definition
func absint -> ( ( Function-like V29( the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) -defined NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Function of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) means :: INT_3:def 5
 for a being ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) holds it : ( ( ) ( ) set ) . a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) = absreal : ( ( Function-like V29( REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) , REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) -defined REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) -valued Function-like V29( REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) , REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) V50() V51() V52() ) Element of K6(K7(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ,REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( V50() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) . a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) : ( ( ) ( V11() V12() ext-real ) set ) ;
end;

theorem :: INT_3:1
for a being ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) holds absint : ( ( Function-like V29( the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) -defined NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Function of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) . a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) = abs a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ;

theorem :: INT_3:2
for a, b, q1, q2, r1, r2 being ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) st b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) <> 0. INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( V11() V12() integer V32() ext-real zero ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) & a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) = (q1 : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) * b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) + r1 : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) & 0. INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( V11() V12() integer V32() ext-real zero ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) <= r1 : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) & r1 : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) < abs b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) & a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) = (q2 : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) * b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) + r2 : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) & 0. INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( V11() V12() integer V32() ext-real zero ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) <= r2 : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) & r2 : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) < abs b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) holds
( q1 : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) = q2 : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) & r1 : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) = r2 : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ) ;

definition
let a, b be ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ;
assume b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) <> 0. INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( V11() V12() integer V32() ext-real zero ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ;
func a div b -> ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) means :: INT_3:def 6
 ex r being ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) st
( a : ( ( ) ( ) set ) = (it : ( ( ) ( ) BiModStr over a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) * b : ( ( ) ( ) set ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) + r : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) & 0. INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( V11() V12() integer V32() ext-real zero ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) <= r : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) & r : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) < abs b : ( ( ) ( ) set ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) );
end;

definition
let a, b be ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ;
assume b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) <> 0. INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( V11() V12() integer V32() ext-real zero ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ;
func a mod b -> ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) means :: INT_3:def 7
 ex q being ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) st
( a : ( ( ) ( ) set ) = (q : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) * b : ( ( ) ( ) set ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) + it : ( ( ) ( ) BiModStr over a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) & 0. INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( V11() V12() integer V32() ext-real zero ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) <= it : ( ( ) ( ) BiModStr over a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) & it : ( ( ) ( ) BiModStr over a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) < abs b : ( ( ) ( ) set ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) );
end;

theorem :: INT_3:3
for a, b being ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) st b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) <> 0. INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( V11() V12() integer V32() ext-real zero ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) holds
a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) = ((a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) div b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) * b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) + (a : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) mod b : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) ;

begin

definition
let I be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
attr I is Euclidian means :: INT_3:def 8
 ex f being ( ( Function-like V29( the carrier of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like the carrier of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( the carrier of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Function of the carrier of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) st
for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st b : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) <> 0. I : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
ex q, r being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) = (q : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) ) : ( ( ) ( ) Element of the carrier of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) + r : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) : ( ( ) ( ) Element of the carrier of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) & ( r : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) = 0. I : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of I : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) or f : ( ( Function-like V29( the carrier of I : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like the carrier of I : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non zero ) set ) -defined NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( the carrier of I : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Function of the carrier of I : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) . r : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) < f : ( ( Function-like V29( the carrier of I : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like the carrier of I : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non zero ) set ) -defined NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( the carrier of I : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Function of the carrier of I : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) . b : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) );
end;

registration
cluster INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like ) doubleLoopStr ) -> Euclidian ;
end;

registration
cluster non empty non degenerated right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like Euclidian for ( ( ) ( ) doubleLoopStr ) ;
end;

definition
mode EuclidianRing is ( ( non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive domRing-like Euclidian ) ( non empty non degenerated V77() right_complementable unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like Euclidian ) Ring) ;
end;

registration
cluster non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like Euclidian for ( ( ) ( ) doubleLoopStr ) ;
end;

definition
let E be ( ( non empty Euclidian ) ( non empty Euclidian ) doubleLoopStr ) ;
mode DegreeFunction of E -> ( ( Function-like V29( the carrier of E : ( ( ) ( ) set ) : ( ( ) ( ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like the carrier of E : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( the carrier of E : ( ( ) ( ) set ) : ( ( ) ( ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Function of the carrier of E : ( ( ) ( ) set ) : ( ( ) ( ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) means :: INT_3:def 9
 for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st b : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) <> 0. E : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of E : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
ex q, r being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) = (q : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) ) : ( ( ) ( ) Element of the carrier of E : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) + r : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) : ( ( ) ( ) Element of the carrier of E : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) & ( r : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) = 0. E : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of E : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) or it : ( ( ) ( ) set ) . r : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) < it : ( ( ) ( ) set ) . b : ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) );
end;

theorem :: INT_3:4
for E being ( ( non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive domRing-like Euclidian ) ( non empty non degenerated V77() right_complementable unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like Euclidian ) EuclidianRing) holds E : ( ( non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive domRing-like Euclidian ) ( non empty non degenerated V77() right_complementable unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like Euclidian ) EuclidianRing) is ( ( non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive domRing-like gcd-like ) ( non empty non degenerated V77() right_complementable unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like gcd-like ) gcdDomain) ;

registration
cluster non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like Euclidian -> non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like gcd-like for ( ( ) ( ) doubleLoopStr ) ;
end;

definition
:: original: absint
redefine func absint -> ( ( ) ( Relation-like the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like gcd-like Euclidian ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) -defined NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like gcd-like Euclidian ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) DegreeFunction of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like gcd-like Euclidian ) doubleLoopStr ) ) ;
end;

theorem :: INT_3:5
for F being ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital ) doubleLoopStr ) holds F : ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital ) doubleLoopStr ) is Euclidian ;

registration
cluster non empty almost_left_invertible associative commutative right_zeroed well-unital -> non empty Euclidian for ( ( ) ( ) doubleLoopStr ) ;
end;

theorem :: INT_3:6
for F being ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital Euclidian ) doubleLoopStr )
for f being ( ( Function-like V29( the carrier of b1 : ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital Euclidian ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like the carrier of b1 : ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital Euclidian ) doubleLoopStr ) : ( ( ) ( non zero ) set ) -defined NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( the carrier of b1 : ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital Euclidian ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Function of the carrier of F : ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital Euclidian ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) holds f : ( ( Function-like V29( the carrier of b1 : ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital Euclidian ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like the carrier of b1 : ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital Euclidian ) doubleLoopStr ) : ( ( ) ( non zero ) set ) -defined NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( the carrier of b1 : ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital Euclidian ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Function of the carrier of b1 : ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital Euclidian ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) is ( ( ) ( Relation-like the carrier of b1 : ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital Euclidian ) doubleLoopStr ) : ( ( ) ( non zero ) set ) -defined NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( the carrier of b1 : ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital Euclidian ) doubleLoopStr ) : ( ( ) ( non zero ) set ) , NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) DegreeFunction of F : ( ( non empty almost_left_invertible associative commutative right_zeroed well-unital ) ( non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital Euclidian ) doubleLoopStr ) ) ;

begin

definition
let n be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
assume n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) > 0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func multint n -> ( ( Function-like V29(K7((Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like K7((Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) -defined Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29(K7((Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) BinOp of Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) means :: INT_3:def 10
 for k, l being ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) holds it : ( ( ) ( ) set ) . (k : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,l : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) = (k : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) * l : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) mod n : ( ( ) ( ) set ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

definition
let n be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
assume n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) > 0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func compint n -> ( ( Function-like V29( Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) , Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -defined Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) , Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) UnOp of Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) means :: INT_3:def 11
 for k being ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) holds it : ( ( ) ( ) set ) . k : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = (n : ( ( ) ( ) set ) - k : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) mod n : ( ( ) ( ) set ) : ( ( integer ) ( V11() V12() integer ext-real ) set ) ;
end;

theorem :: INT_3:7
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) > 0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for a, b being ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ( a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) + b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) < n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) implies (addint n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( Function-like V29(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) -defined INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Element of K6(K7(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) = a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) + b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( (addint n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( Function-like V29(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) -defined INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Element of K6(K7(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) = a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) + b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) implies a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) + b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) < n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) & ( a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) + b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) >= n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) implies (addint n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( Function-like V29(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) -defined INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Element of K6(K7(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) = (a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) + b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) - n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) ) & ( (addint n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( Function-like V29(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) -defined INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Element of K6(K7(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) = (a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) + b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) - n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) implies a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) + b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) >= n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) ) ;

theorem :: INT_3:8
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) > 0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for a, b being ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
( ( k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) * n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) <= a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) * b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) * b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) < (k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) + 1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) iff (multint n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( Function-like V29(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) -defined Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29(K7((Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) BinOp of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) . (a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) = (a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) * b : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) - (k : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) * n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) ) ;

theorem :: INT_3:9
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) > 0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for a being ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ( a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) = 0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) implies (compint n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( Function-like V29( Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -defined Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) UnOp of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) . a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) = 0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( (compint n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( Function-like V29( Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -defined Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) UnOp of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) . a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) = 0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) implies a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) = 0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) <> 0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) implies (compint n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( Function-like V29( Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -defined Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) UnOp of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) . a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) = n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) - a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) ) & ( (compint n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( Function-like V29( Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -defined Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29( Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) , Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) UnOp of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) . a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) set ) = n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) - a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() V12() integer V32() ext-real ) Element of INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) ) implies a : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) <> 0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ;

definition
let n be ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ;
func INT.Ring n -> ( ( ) ( ) doubleLoopStr ) equals :: INT_3:def 12
 doubleLoopStr(# (Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(addint n : ( ( ) ( ) set ) ) : ( ( Function-like V29(K7((Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like K7((Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) -defined INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29(K7((Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) Element of K6(K7(K7((Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) ) : ( ( ) ( ) set ) ) ,(multint n : ( ( ) ( ) set ) ) : ( ( Function-like V29(K7((Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like K7((Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) -defined Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V29(K7((Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( RAT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() ) set ) -valued INT : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() ) set ) -valued V50() V51() V52() V53() ) set ) , Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) V50() V51() V52() V53() ) BinOp of Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,(In (1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,(In (0 : ( ( ) ( zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,(Segm n : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( ) ( V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative ) Element of Segm n : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of K6(NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) #) : ( ( strict ) ( strict ) doubleLoopStr ) ;
end;

registration
let n be ( ( non zero V10() ) ( non zero V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) Nat) ;
cluster INT.Ring n : ( ( non zero V10() ) ( non zero V4() V5() V6() V10() V11() V12() integer ext-real positive non negative ) set ) : ( ( ) ( ) doubleLoopStr ) -> non empty strict ;
end;

theorem :: INT_3:10
( INT.Ring 1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty strict ) doubleLoopStr ) is degenerated & INT.Ring 1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty strict ) doubleLoopStr ) is ( ( non empty right_complementable associative Abelian add-associative right_zeroed well-unital distributive ) ( non empty right_complementable unital associative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) & INT.Ring 1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty strict ) doubleLoopStr ) is almost_left_invertible & INT.Ring 1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty strict ) doubleLoopStr ) is unital & INT.Ring 1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty strict ) doubleLoopStr ) is distributive & INT.Ring 1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty strict ) doubleLoopStr ) is commutative ) ;

registration
cluster non empty degenerated right_complementable almost_left_invertible strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital for ( ( ) ( ) doubleLoopStr ) ;
end;

theorem :: INT_3:11
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) > 1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( not INT.Ring n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( ) doubleLoopStr ) is degenerated & INT.Ring n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( ) doubleLoopStr ) is ( ( non empty right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive ) ( non empty right_complementable unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital ) Ring) ) ;

theorem :: INT_3:12
for p being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st p : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) > 1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( INT.Ring p : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) : ( ( ) ( ) doubleLoopStr ) is ( ( non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive ) ( non empty non degenerated V77() right_complementable almost_left_invertible unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital gcd-like Euclidian ) doubleLoopStr ) iff p : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) is ( ( V10() prime ) ( V4() V5() V6() V10() V11() V12() integer prime ext-real non negative ) Prime) ) ;

registration
cluster V10() prime -> non zero V10() prime for ( ( ) ( ) set ) ;
end;

registration
let p be ( ( V10() prime ) ( non zero V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative ) Prime) ;
cluster INT.Ring p : ( ( V10() prime ) ( non zero V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative ) set ) : ( ( ) ( non empty strict ) doubleLoopStr ) -> non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive ;
end;

theorem :: INT_3:13
1. INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like gcd-like Euclidian ) doubleLoopStr ) : ( ( ) ( V11() V12() integer V32() ext-real non zero ) Element of the carrier of INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like gcd-like Euclidian ) doubleLoopStr ) : ( ( ) ( non zero V2() complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ) = 1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: INT_3:14
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) st 1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) < n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) holds
1. (INT.Ring n : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) Element of the carrier of (INT.Ring b1 : ( ( V10() ) ( V4() V5() V6() V10() V11() V12() integer ext-real non negative ) Nat) ) : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) ) = 1 : ( ( ) ( non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() ) Element of K6(REAL : ( ( ) ( non zero V33() complex-membered ext-real-membered real-membered V66() ) set ) ) : ( ( ) ( ) set ) ) ) ;

begin

registration
cluster INT.Ring : ( ( ) ( non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like gcd-like Euclidian ) doubleLoopStr ) -> infinite ;
end;

registration
cluster non empty infinite right_complementable strict unital associative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital for ( ( ) ( ) doubleLoopStr ) ;
end;