:: A Representation of Integers by Binary Arithmeticsand Addition of Integers
:: by Hisayoshi Kunimune and Yatsuka Nakamura
::
:: Received January 30, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem Th1: :: BINARI_4:1
for
m being
Nat st
m > 0 holds
m * 2
>= m + 1
theorem Th2: :: BINARI_4:2
theorem :: BINARI_4:3
theorem Th4: :: BINARI_4:4
for
k,
m,
l being
Nat st
k <= l &
l <= m & not
k = l holds
(
k + 1
<= l &
l <= m )
theorem Th5: :: BINARI_4:5
theorem :: BINARI_4:6
theorem :: BINARI_4:7
theorem Th8: :: BINARI_4:8
for
l,
m,
k being
Nat st
l + m <= k - 1 holds
(
l < k &
m < k )
theorem Th9: :: BINARI_4:9
theorem Th10: :: BINARI_4:10
theorem Th11: :: BINARI_4:11
theorem Th12: :: BINARI_4:12
theorem Th13: :: BINARI_4:13
theorem Th14: :: BINARI_4:14
theorem Th15: :: BINARI_4:15
theorem :: BINARI_4:16
theorem :: BINARI_4:17
theorem :: BINARI_4:18
theorem :: BINARI_4:19
theorem Th20: :: BINARI_4:20
:: deftheorem Def1 defines MajP BINARI_4:def 1 :
theorem :: BINARI_4:21
theorem Th22: :: BINARI_4:22
theorem :: BINARI_4:23
theorem Th24: :: BINARI_4:24
theorem :: BINARI_4:25
:: deftheorem Def2 defines 2sComplement BINARI_4:def 2 :
theorem :: BINARI_4:26
theorem :: BINARI_4:27
Lm1:
for n being non empty Nat
for k, l being Nat st k mod n = l mod n & k > l holds
ex s being Integer st k = l + (s * n)
Lm2:
for n being non empty Nat
for k, l being Nat st k mod n = l mod n holds
ex s being Integer st k = l + (s * n)
Lm3:
for n being non empty Nat
for k, l, m being Nat st m < n & k mod (2 to_power n) = l mod (2 to_power n) holds
(k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2
Lm4:
for n being non empty Nat
for h, i being Integer st h mod (2 to_power n) = i mod (2 to_power n) holds
((2 to_power (MajP n,(abs h))) + h) mod (2 to_power n) = ((2 to_power (MajP n,(abs i))) + i) mod (2 to_power n)
Lm5:
for n being non empty Nat
for h, i being Integer st h >= 0 & i >= 0 & h mod (2 to_power n) = i mod (2 to_power n) holds
2sComplement n,h = 2sComplement n,i
Lm6:
for n being non empty Nat
for h, i being Integer st h < 0 & i < 0 & h mod (2 to_power n) = i mod (2 to_power n) holds
2sComplement n,h = 2sComplement n,i
theorem :: BINARI_4:28
theorem :: BINARI_4:29
theorem Th30: :: BINARI_4:30
theorem :: BINARI_4:31
theorem Th32: :: BINARI_4:32
theorem Th33: :: BINARI_4:33
theorem :: BINARI_4:34
theorem Th35: :: BINARI_4:35
theorem :: BINARI_4:36
theorem :: BINARI_4:37
theorem :: BINARI_4:38