:: RADIX_1 semantic presentation

theorem Th1: :: RADIX_1:1

canceled;

theorem Th2: :: RADIX_1:2

for b₁, b₂ being Nat st b₁ mod b₂ = b₂ - 1 holds
(b₁ + 1) mod b₂ = 0

proof end;

theorem Th3: :: RADIX_1:3

for b₁, b₂ being Nat st b₁ <> 0 & b₂ mod b₁ < b₁ - 1 holds
(b₂ + 1) mod b₁ = (b₂ mod b₁) + 1

proof end;

theorem Th4: :: RADIX_1:4

for b₁, b₂, b₃ being Nat st b₁ <> 0 holds
(b₂ mod (b₁ * b₃)) mod b₃ = b₂ mod b₃

proof end;

theorem Th5: :: RADIX_1:5

for b₁, b₂ being Nat holds
( not b₁ <> 0 or (b₂ + 1) mod b₁ = 0 or (b₂ + 1) mod b₁ = (b₂ mod b₁) + 1 )

proof end;

theorem Th6: :: RADIX_1:6

for b₁, b₂, b₃ being Nat st b₁ <> 0 & b₂ <> 0 holds
(b₃ mod (b₁ |^ b₂)) div (b₁ |^ (b₂ -' 1)) < b₁

proof end;

theorem Th7: :: RADIX_1:7

for b₁, b₂, b₃ being Nat st b₁ <= b₂ holds
b₃ |^ b₁ divides b₃ |^ b₂

proof end;

theorem Th8: :: RADIX_1:8

for b₁, b₂, b₃ being Integer st b₁ > 0 & b₂ >= 0 holds
(b₃ mod (b₁ * b₂)) mod b₂ = b₃ mod b₂

proof end;

definition

let c₁ be Nat;
func Radix c₁ -> Nat equals :: RADIX_1:def 1
2 to_power a₁;
correctness

proof end;

end;

:: deftheorem Def1 defines Radix RADIX_1:def 1 :

definition

let c₁ be Nat;
func c₁ -SD -> set equals :: RADIX_1:def 2
{ b₁ where B is Element of INT : ( b₁ <= (Radix a₁) - 1 & b₁ >= (- (Radix a₁)) + 1 ) } ;
correctness ;

end;

:: deftheorem Def2 defines -SD RADIX_1:def 2 :

theorem Th9: :: RADIX_1:9

for b₁ being Nat holds Radix b₁ <> 0 by POWER:39;

Lemma7: for b₁ being Nat st b₁ >= 2 holds
Radix b₁ >= 2 + 2

proof end;

theorem Th10: :: RADIX_1:10

for b₁ being set holds
( b₁ in 0 -SD iff b₁ = 0 )

proof end;

theorem Th11: :: RADIX_1:11

0 -SD = {0} by Th10, TARSKI:def 1;

theorem Th12: :: RADIX_1:12

for b₁ being Nat holds b₁ -SD c= (b₁ + 1) -SD

proof end;

theorem Th13: :: RADIX_1:13

for b₁ being Nat
for b₂ being set st b₂ in b₁ -SD holds
b₂ is Integer

proof end;

theorem Th14: :: RADIX_1:14

for b₁ being Nat holds b₁ -SD c= INT

proof end;

theorem Th15: :: RADIX_1:15

for b₁ being Nat
for b₂ being Integer st b₂ in b₁ -SD holds
( b₂ <= (Radix b₁) - 1 & b₂ >= (- (Radix b₁)) + 1 )

proof end;

theorem Th16: :: RADIX_1:16

for b₁ being Nat holds 0 in b₁ -SD

proof end;

registration

let c₁ be Nat;
cluster a₁ -SD -> non empty ;
coherence by Th16;

end;

definition

let c₁ be Nat;
redefine func -SD as c₁ -SD -> non empty Subset of INT ;
coherence by Th14;

end;

theorem Th17: :: RADIX_1:17

canceled;

theorem Th18: :: RADIX_1:18

for b₁, b₂, b₃ being Nat
for b₄ being Tuple of b₂,(b₃ -SD ) st b₁ in Seg b₂ holds
b₄ . b₁ is Element of b₃ -SD

proof end;

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of c₃,(c₂ -SD );
func DigA c₄,c₁ -> Integer equals :Def3: :: RADIX_1:def 3
a₄ . a₁ if a₁ in Seg a₃
0 if a₁ = 0
;
coherence

proof end;

consistency by FINSEQ_1:3;

end;

:: deftheorem Def3 defines DigA RADIX_1:def 3 :

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of c₃,(c₂ -SD );
func DigB c₄,c₁ -> Element of INT equals :: RADIX_1:def 4
DigA a₄,a₁;
coherence by INT_1:def 2;

end;

:: deftheorem Def4 defines DigB RADIX_1:def 4 :

theorem Th19: :: RADIX_1:19

for b₁, b₂, b₃ being Nat
for b₄ being Tuple of b₂,(b₃ -SD ) st b₁ in Seg b₂ holds
DigA b₄,b₁ is Element of b₃ -SD

proof end;

theorem Th20: :: RADIX_1:20

for b₁ being Nat
for b₂ being Tuple of 1,INT st b₂ /. 1 = b₁ holds
b₂ = <*b₁*>

proof end;

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of c₃,(c₂ -SD );
func SubDigit c₄,c₁,c₂ -> Element of INT equals :: RADIX_1:def 5
((Radix a₂) |^ (a₁ -' 1)) * (DigB a₄,a₁);
coherence by INT_1:def 2;

end;

:: deftheorem Def5 defines SubDigit RADIX_1:def 5 :

definition

let c₁, c₂ be Nat;
let c₃ be Tuple of c₁,(c₂ -SD );
func DigitSD c₃ -> Tuple of a₁,INT means :Def6: :: RADIX_1:def 6
for b₁ being Nat st b₁ in Seg a₁ holds
a₄ /. b₁ = SubDigit a₃,b₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines DigitSD RADIX_1:def 6 :

definition

let c₁, c₂ be Nat;
let c₃ be Tuple of c₁,(c₂ -SD );
func SDDec c₃ -> Integer equals :: RADIX_1:def 7
Sum (DigitSD a₃);
coherence ;

end;

:: deftheorem Def7 defines SDDec RADIX_1:def 7 :

definition

let c₁, c₂, c₃ be Nat;
func DigitDC c₃,c₁,c₂ -> Element of a₂ -SD equals :: RADIX_1:def 8
(a₃ mod ((Radix a₂) |^ a₁)) div ((Radix a₂) |^ (a₁ -' 1));
coherence

proof end;

end;

:: deftheorem Def8 defines DigitDC RADIX_1:def 8 :

definition

let c₁, c₂, c₃ be Nat;
func DecSD c₃,c₂,c₁ -> Tuple of a₂,(a₁ -SD ) means :Def9: :: RADIX_1:def 9
for b₁ being Nat st b₁ in Seg a₂ holds
DigA a₄,b₁ = DigitDC a₃,b₁,a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines DecSD RADIX_1:def 9 :

definition

let c₁ be Integer;
func SD_Add_Carry c₁ -> Integer equals :Def10: :: RADIX_1:def 10
1 if a₁ > 2
- 1 if a₁ < - 2
otherwise 0;
coherence ;
consistency ;

end;

:: deftheorem Def10 defines SD_Add_Carry RADIX_1:def 10 :

theorem Th21: :: RADIX_1:21

SD_Add_Carry 0 = 0 by Def10;

Lemma22: for b₁ being Integer holds
( - 1 <= SD_Add_Carry b₁ & SD_Add_Carry b₁ <= 1 )

proof end;

definition

let c₁ be Integer;
let c₂ be Nat;
func SD_Add_Data c₁,c₂ -> Integer equals :: RADIX_1:def 11
a₁ - ((SD_Add_Carry a₁) * (Radix a₂));
coherence ;

end;

:: deftheorem Def11 defines SD_Add_Data RADIX_1:def 11 :

theorem Th22: :: RADIX_1:22

for b₁ being Nat holds SD_Add_Data 0,b₁ = 0 by Th21;

theorem Th23: :: RADIX_1:23

for b₁ being Nat
for b₂, b₃ being Integer st b₁ >= 2 & b₂ in b₁ -SD & b₃ in b₁ -SD holds
( (- (Radix b₁)) + 2 <= SD_Add_Data (b₂ + b₃),b₁ & SD_Add_Data (b₂ + b₃),b₁ <= (Radix b₁) - 2 )

proof end;

definition

let c₁, c₂, c₃ be Nat;
pred c₂ is_represented_by c₁,c₃ means :Def12: :: RADIX_1:def 12
a₂ < (Radix a₃) |^ a₁;

end;

:: deftheorem Def12 defines is_represented_by RADIX_1:def 12 :

theorem Th24: :: RADIX_1:24

for b₁, b₂ being Nat st b₁ is_represented_by 1,b₂ holds
DigA (DecSD b₁,1,b₂),1 = b₁

proof end;

theorem Th25: :: RADIX_1:25

for b₁, b₂ being Nat st b₂ >= 1 holds
for b₃ being Nat st b₃ is_represented_by b₂,b₁ holds
b₃ = SDDec (DecSD b₃,b₂,b₁)

proof end;

theorem Th26: :: RADIX_1:26

for b₁, b₂, b₃ being Nat st b₁ >= 2 & b₂ is_represented_by 1,b₁ & b₃ is_represented_by 1,b₁ holds
SD_Add_Carry ((DigA (DecSD b₂,1,b₁),1) + (DigA (DecSD b₃,1,b₁),1)) = SD_Add_Carry (b₂ + b₃)

proof end;

Lemma27: for b₁, b₂, b₃, b₄ being Nat st b₄ in Seg b₁ holds
DigA (DecSD b₂,(b₁ + 1),b₃),b₄ = DigA (DecSD (b₂ mod ((Radix b₃) |^ b₁)),b₁,b₃),b₄

proof end;

theorem Th27: :: RADIX_1:27

for b₁, b₂, b₃ being Nat st b₁ is_represented_by b₂ + 1,b₃ holds
DigA (DecSD b₁,(b₂ + 1),b₃),(b₂ + 1) = b₁ div ((Radix b₃) |^ b₂)

proof end;

definition

let c₁, c₂, c₃ be Nat;
let c₄, c₅ be Tuple of c₃,(c₁ -SD );
assume E29: ( c₂ in Seg c₃ & c₁ >= 2 ) ;
func Add c₄,c₅,c₂,c₁ -> Element of a₁ -SD equals :Def13: :: RADIX_1:def 13
(SD_Add_Data ((DigA a₄,a₂) + (DigA a₅,a₂)),a₁) + (SD_Add_Carry ((DigA a₄,(a₂ -' 1)) + (DigA a₅,(a₂ -' 1))));
coherence

proof end;

end;

:: deftheorem Def13 defines Add RADIX_1:def 13 :

definition

let c₁, c₂ be Nat;
let c₃, c₄ be Tuple of c₁,(c₂ -SD );
func c₃ '+' c₄ -> Tuple of a₁,(a₂ -SD ) means :Def14: :: RADIX_1:def 14
for b₁ being Nat st b₁ in Seg a₁ holds
DigA a₅,b₁ = Add a₃,a₄,b₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines '+' RADIX_1:def 14 :

theorem Th28: :: RADIX_1:28

for b₁, b₂, b₃ being Nat st b₁ >= 2 & b₂ is_represented_by 1,b₁ & b₃ is_represented_by 1,b₁ holds
SDDec ((DecSD b₂,1,b₁) '+' (DecSD b₃,1,b₁)) = SD_Add_Data (b₂ + b₃),b₁

proof end;

theorem Th29: :: RADIX_1:29

for b₁ being Nat st b₁ >= 1 holds
for b₂, b₃, b₄ being Nat st b₂ >= 2 & b₃ is_represented_by b₁,b₂ & b₄ is_represented_by b₁,b₂ holds
b₃ + b₄ = (SDDec ((DecSD b₃,b₁,b₂) '+' (DecSD b₄,b₁,b₂))) + (((Radix b₂) |^ b₁) * (SD_Add_Carry ((DigA (DecSD b₃,b₁,b₂),b₁) + (DigA (DecSD b₄,b₁,b₂),b₁))))

proof end;