let n be non zero Nat; for l, m being Nat st l + m <= (2 to_power (n -' 1)) - 1 holds
(carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE
let l, m be Nat; ( l + m <= (2 to_power (n -' 1)) - 1 implies (carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE )
set L = n -BinarySequence l;
set M = n -BinarySequence m;
set F = FALSE ;
set T = TRUE ;
assume A1:
l + m <= (2 to_power (n -' 1)) - 1
; (carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE
then A2:
l < 2 to_power (n -' 1)
by Th8;
n >= 1
by NAT_1:14;
then
n - 1 >= 1 - 1
by XREAL_1:9;
then
n -' 1 = n - 1
by XREAL_0:def 2;
then
2 to_power (n -' 1) < 2 to_power n
by POWER:39, XREAL_1:146;
then A3:
(2 to_power (n -' 1)) - 1 < (2 to_power n) - 1
by XREAL_1:14;
assume
not (carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE
; contradiction
then A4:
(carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = TRUE
by XBOOLEAN:def 3;
A5:
m < 2 to_power (n -' 1)
by A1, Th8;
1 <= n
by NAT_1:14;
then A6:
n in Seg n
by FINSEQ_1:1;
then A7: (n -BinarySequence m) /. n =
IFEQ (((m div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE)
by BINARI_3:def 1
.=
IFEQ ((0 mod 2),0,FALSE,TRUE)
by A5, NAT_D:27
.=
IFEQ (0,0,FALSE,TRUE)
by NAT_D:26
.=
FALSE
by FUNCOP_1:def 8
;
(n -BinarySequence l) /. n =
IFEQ (((l div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE)
by A6, BINARI_3:def 1
.=
IFEQ ((0 mod 2),0,FALSE,TRUE)
by A2, NAT_D:27
.=
IFEQ (0,0,FALSE,TRUE)
by NAT_D:26
.=
FALSE
by FUNCOP_1:def 8
;
then ((n -BinarySequence l) + (n -BinarySequence m)) /. n =
(FALSE 'xor' FALSE) 'xor' TRUE
by A4, A6, A7, BINARITH:def 5
.=
TRUE
;
then A8:
Absval ((n -BinarySequence l) + (n -BinarySequence m)) >= 2 to_power (n -' 1)
by Th12;
l + m < 2 to_power (n -' 1)
by A1, XREAL_1:146, XXREAL_0:2;
hence
contradiction
by A1, A3, A8, Th11, XXREAL_0:2; verum