let n1, n2 be Nat; ( n1 + n2 = 1 iff ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) )
thus
( not n1 + n2 = 1 or ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) )
( ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) implies n1 + n2 = 1 )proof
assume A1:
n1 + n2 = 1
;
( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) )
now ( n1 <= 1 & n2 <= 1 & not ( n1 = 1 & n2 = 0 ) implies ( n1 = 0 & n2 = 1 ) )A2:
(
n1 = 0 implies not
n2 = 0 )
by A1;
assume A3:
(
n1 <= 1 &
n2 <= 1 )
;
( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) )
(
n1 = 1 implies not
n2 = 1 )
by A1;
hence
( (
n1 = 1 &
n2 = 0 ) or (
n1 = 0 &
n2 = 1 ) )
by A3, A2, NAT_1:25;
verum end;
hence
( (
n1 = 1 &
n2 = 0 ) or (
n1 = 0 &
n2 = 1 ) )
by A1, Th1;
verum
end;
thus
( ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) implies n1 + n2 = 1 )
; verum