let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for I being integer SortSymbol of S
for i, j being Integer
for a, b being Element of C,I st a = i & b = j & j <> 0 holds
a mod b = i mod j
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for I being integer SortSymbol of S
for i, j being Integer
for a, b being Element of C,I st a = i & b = j & j <> 0 holds
a mod b = i mod j
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; :: thesis: for C being bool-correct 4,1 integer image of T
for I being integer SortSymbol of S
for i, j being Integer
for a, b being Element of C,I st a = i & b = j & j <> 0 holds
a mod b = i mod j
let C be bool-correct 4,1 integer image of T; :: thesis: for I being integer SortSymbol of S
for i, j being Integer
for a, b being Element of C,I st a = i & b = j & j <> 0 holds
a mod b = i mod j
let I be integer SortSymbol of S; :: thesis: for i, j being Integer
for a, b being Element of C,I st a = i & b = j & j <> 0 holds
a mod b = i mod j
let i, j be Integer; :: thesis: for a, b being Element of C,I st a = i & b = j & j <> 0 holds
a mod b = i mod j
let a, b be Element of C,I; :: thesis: ( a = i & b = j & j <> 0 implies a mod b = i mod j )
assume A1: a = i ; :: thesis: ( not b = j or not j <> 0 or a mod b = i mod j )
assume A2: b = j ; :: thesis: ( not j <> 0 or a mod b = i mod j )
assume A3: j <> 0 ; :: thesis: a mod b = i mod j
then a div b = i div j by A1, A2, AOFA_A00:55;
then (a div b) * b = (i div j) * j by A2, AOFA_A00:55;
then a - ((a div b) * b) = i - ((i div j) * j) by A1, Th63;
hence a mod b = i mod j by A3, INT_1:def 10; :: thesis: verum