let S be non empty non void bool-correct 4,1 integer BoolSignature ; for A being non-empty bool-correct 4,1 integer MSAlgebra over S
for I being integer SortSymbol of S holds
( the Sorts of A . I = INT & \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer
for a, b being Element of the Sorts of A . I st a = i & b = j holds
( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )
let A be non-empty bool-correct 4,1 integer MSAlgebra over S; for I being integer SortSymbol of S holds
( the Sorts of A . I = INT & \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer
for a, b being Element of the Sorts of A . I st a = i & b = j holds
( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )
let I be integer SortSymbol of S; ( the Sorts of A . I = INT & \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer
for a, b being Element of the Sorts of A . I st a = i & b = j holds
( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )
set n = 4;
consider J being SortSymbol of S such that
A1:
( J = 1 & the connectives of S . 4 is_of_type {} ,J & the Sorts of A . J = INT & (Den ((In (( the connectives of S . 4), the carrier' of S)),A)) . {} = 0 & (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) )
by Def49;
thus
the Sorts of A . I = INT
by A1, Def39; ( \0 (A,I) = 0 & \1 (A,I) = 1 & ( for i, j being Integer
for a, b being Element of the Sorts of A . I st a = i & b = j holds
( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )
thus
\0 (A,I) = 0
by A1; ( \1 (A,I) = 1 & ( for i, j being Integer
for a, b being Element of the Sorts of A . I st a = i & b = j holds
( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) ) )
thus
\1 (A,I) = 1
by A1; for i, j being Integer
for a, b being Element of the Sorts of A . I st a = i & b = j holds
( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )
let i, j be Integer; for a, b being Element of the Sorts of A . I st a = i & b = j holds
( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )
let a, b be Element of the Sorts of A . I; ( a = i & b = j implies ( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) )
assume A2:
a = i
; ( not b = j or ( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) ) )
assume A3:
b = j
; ( - a = - i & a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )
thus
- a = - i
by A1, A2; ( a + b = i + j & a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )
thus
a + b = i + j
by A1, A2, A3; ( a * b = i * j & ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )
thus
a * b = i * j
by A1, A2, A3; ( ( j <> 0 implies a div b = i div j ) & leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )
thus
( j <> 0 implies a div b = i div j )
by A1, A2, A3; ( leq (a,b) = IFGT (i,j,FALSE,TRUE) & ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )
thus A4:
leq (a,b) = IFGT (i,j,FALSE,TRUE)
by A1, A2, A3; ( ( leq (a,b) = TRUE implies i <= j ) & ( i <= j implies leq (a,b) = TRUE ) & ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )
thus
( leq (a,b) = TRUE iff i <= j )
by A4, XXREAL_0:def 11; ( ( leq (a,b) = FALSE implies i > j ) & ( i > j implies leq (a,b) = FALSE ) )
thus
( leq (a,b) = FALSE implies i > j )
by A4, XXREAL_0:def 11; ( i > j implies leq (a,b) = FALSE )
assume
i > j
; leq (a,b) = FALSE
hence
leq (a,b) = FALSE
by A4, XXREAL_0:def 11; verum