( [0,0] `2 = 0 & [0,1] `2 = 1 & [0,2] `2 = 2 & [0,3] `2 = 3 & [0,4] `2 = 4 ) ;
hence for b₁ being Integer holds
( ( o = [0,0] & o = [0,1] implies ( b₁ = i + j iff b₁ = i - j ) ) & ( o = [0,0] & o = [0,2] implies ( b₁ = i + j iff b₁ = i * j ) ) & ( o = [0,0] & o = [0,3] implies ( b₁ = i + j iff b₁ = i div j ) ) & ( o = [0,0] & o = [0,4] implies ( b₁ = i + j iff b₁ = i mod j ) ) & ( o = [0,1] & o = [0,2] implies ( b₁ = i - j iff b₁ = i * j ) ) & ( o = [0,1] & o = [0,3] implies ( b₁ = i - j iff b₁ = i div j ) ) & ( o = [0,1] & o = [0,4] implies ( b₁ = i - j iff b₁ = i mod j ) ) & ( o = [0,2] & o = [0,3] implies ( b₁ = i * j iff b₁ = i div j ) ) & ( o = [0,2] & o = [0,4] implies ( b₁ = i * j iff b₁ = i mod j ) ) & ( o = [0,3] & o = [0,4] implies ( b₁ = i div j iff b₁ = i mod j ) ) ) ; :: thesis: verum