defpred S_{1}[ Nat] means for i being Nat st i in dom (Sgm0 ($1 /\ OddNAT)) holds

(Sgm0 ($1 /\ OddNAT)) . i = (2 * i) + 1;

A1: S_{1}[ 0 ]
_{1}[N]
from NAT_1:sch 2(A1, A2);

hence for N, i being Nat st i in dom (Sgm0 (N /\ OddNAT)) holds

(Sgm0 (N /\ OddNAT)) . i = (2 * i) + 1 ; :: thesis: verum

(Sgm0 ($1 /\ OddNAT)) . i = (2 * i) + 1;

A1: S

proof

let i be Nat; :: thesis: ( i in dom (Sgm0 (0 /\ OddNAT)) implies (Sgm0 (0 /\ OddNAT)) . i = (2 * i) + 1 )

assume i in dom (Sgm0 (0 /\ OddNAT)) ; :: thesis: (Sgm0 (0 /\ OddNAT)) . i = (2 * i) + 1

then i in len (Sgm0 {}) ;

then i in card {} by AFINSQ_2:20;

hence (Sgm0 (0 /\ OddNAT)) . i = (2 * i) + 1 ; :: thesis: verum

end;assume i in dom (Sgm0 (0 /\ OddNAT)) ; :: thesis: (Sgm0 (0 /\ OddNAT)) . i = (2 * i) + 1

then i in len (Sgm0 {}) ;

then i in card {} by AFINSQ_2:20;

hence (Sgm0 (0 /\ OddNAT)) . i = (2 * i) + 1 ; :: thesis: verum

A2: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

for N being Nat holds SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

thus S_{1}[n + 1]
:: thesis: verum

end;assume A3: S

thus S

proof

let i be Nat; :: thesis: ( i in dom (Sgm0 ((n + 1) /\ OddNAT)) implies (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1 )

assume A4: i in dom (Sgm0 ((n + 1) /\ OddNAT)) ; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

end;assume A4: i in dom (Sgm0 ((n + 1) /\ OddNAT)) ; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

per cases
( n is odd or n is even )
;

end;

suppose A5:
n is odd
; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

A6:
(n + 1) /\ OddNAT = (n /\ OddNAT) \/ {n}

reconsider Y = {n} as finite natural-membered set ;

A10: X <N< Y

then not n in n /\ OddNAT by XBOOLE_0:def 4;

then A11: card ((n + 1) /\ OddNAT) = (card (n /\ OddNAT)) + 1 by A6, CARD_2:41;

A12: i in Segm (dom (Sgm0 ((n + 1) /\ OddNAT))) by A4;

then i < len (Sgm0 ((n + 1) /\ OddNAT)) by NAT_1:44;

then i < (card (n /\ OddNAT)) + 1 by A11, AFINSQ_2:20;

then i < (len (Sgm0 X)) + 1 by AFINSQ_2:20;

end;proof

reconsider X = n /\ OddNAT as finite natural-membered set ;
thus
(n + 1) /\ OddNAT c= (n /\ OddNAT) \/ {n}
:: according to XBOOLE_0:def 10 :: thesis: (n /\ OddNAT) \/ {n} c= (n + 1) /\ OddNAT

assume x in (n /\ OddNAT) \/ {n} ; :: thesis: x in (n + 1) /\ OddNAT

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (n /\ OddNAT) \/ {n} or x in (n + 1) /\ OddNAT )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (n + 1) /\ OddNAT or x in (n /\ OddNAT) \/ {n} )

assume A7: x in (n + 1) /\ OddNAT ; :: thesis: x in (n /\ OddNAT) \/ {n}

then ( x in n + 1 & x in OddNAT ) by XBOOLE_0:def 4;

then consider y being Nat such that

A8: ( y = x & y is odd ) ;

( y in Segm (n + 1) & y in OddNAT ) by A7, XBOOLE_0:def 4, A8;

then ( ( y < n or y = n ) & y in OddNAT ) by NAT_1:44, NAT_1:22;

then ( ( y in Segm n & y in OddNAT ) or y = n ) by NAT_1:44;

then ( y in n /\ OddNAT or y in {n} ) by XBOOLE_0:def 4, TARSKI:def 1;

hence x in (n /\ OddNAT) \/ {n} by A8, XBOOLE_0:def 3; :: thesis: verum

end;assume A7: x in (n + 1) /\ OddNAT ; :: thesis: x in (n /\ OddNAT) \/ {n}

then ( x in n + 1 & x in OddNAT ) by XBOOLE_0:def 4;

then consider y being Nat such that

A8: ( y = x & y is odd ) ;

( y in Segm (n + 1) & y in OddNAT ) by A7, XBOOLE_0:def 4, A8;

then ( ( y < n or y = n ) & y in OddNAT ) by NAT_1:44, NAT_1:22;

then ( ( y in Segm n & y in OddNAT ) or y = n ) by NAT_1:44;

then ( y in n /\ OddNAT or y in {n} ) by XBOOLE_0:def 4, TARSKI:def 1;

hence x in (n /\ OddNAT) \/ {n} by A8, XBOOLE_0:def 3; :: thesis: verum

assume x in (n /\ OddNAT) \/ {n} ; :: thesis: x in (n + 1) /\ OddNAT

reconsider Y = {n} as finite natural-membered set ;

A10: X <N< Y

proof

not n in n
;
let a, b be Nat; :: according to AFINSQ_2:def 5 :: thesis: ( not a in X or not b in Y or not b <= a )

assume ( a in X & b in Y ) ; :: thesis: not b <= a

then ( a in Segm n & b = n ) by XBOOLE_0:def 4, TARSKI:def 1;

hence a < b by NAT_1:44; :: thesis: verum

end;assume ( a in X & b in Y ) ; :: thesis: not b <= a

then ( a in Segm n & b = n ) by XBOOLE_0:def 4, TARSKI:def 1;

hence a < b by NAT_1:44; :: thesis: verum

then not n in n /\ OddNAT by XBOOLE_0:def 4;

then A11: card ((n + 1) /\ OddNAT) = (card (n /\ OddNAT)) + 1 by A6, CARD_2:41;

A12: i in Segm (dom (Sgm0 ((n + 1) /\ OddNAT))) by A4;

then i < len (Sgm0 ((n + 1) /\ OddNAT)) by NAT_1:44;

then i < (card (n /\ OddNAT)) + 1 by A11, AFINSQ_2:20;

then i < (len (Sgm0 X)) + 1 by AFINSQ_2:20;

per cases then
( i < len (Sgm0 X) or i = len (Sgm0 X) )
by NAT_1:22;

end;

suppose A13:
i < len (Sgm0 X)
; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

then A14:
i < Segm (card (Sgm0 (n /\ OddNAT)))
;

thus (Sgm0 ((n + 1) /\ OddNAT)) . i = (Sgm0 (n /\ OddNAT)) . i by A10, A13, AFINSQ_2:29, A6

.= (2 * i) + 1 by A14, NAT_1:44, A3 ; :: thesis: verum

end;thus (Sgm0 ((n + 1) /\ OddNAT)) . i = (Sgm0 (n /\ OddNAT)) . i by A10, A13, AFINSQ_2:29, A6

.= (2 * i) + 1 by A14, NAT_1:44, A3 ; :: thesis: verum

suppose A15:
i = len (Sgm0 X)
; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

then A16: (Sgm0 ((n + 1) /\ OddNAT)) . i =
(Sgm0 Y) . 0
by AFINSQ_2:32, A10, A6

.= n by AFINSQ_2:22 ;

(Sgm0 ((n + 1) /\ OddNAT)) . i in rng (Sgm0 ((n + 1) /\ OddNAT)) by FUNCT_1:3, A4;

then (Sgm0 ((n + 1) /\ OddNAT)) . i in (n + 1) /\ OddNAT by AFINSQ_2:def 4;

then (Sgm0 ((n + 1) /\ OddNAT)) . i in OddNAT by XBOOLE_0:def 4;

then consider r being Nat such that

A17: ( r = (Sgm0 ((n + 1) /\ OddNAT)) . i & r is odd ) ;

consider j being Nat such that

A18: r = (2 * j) + 1 by A17, ABIAN:9;

end;.= n by AFINSQ_2:22 ;

(Sgm0 ((n + 1) /\ OddNAT)) . i in rng (Sgm0 ((n + 1) /\ OddNAT)) by FUNCT_1:3, A4;

then (Sgm0 ((n + 1) /\ OddNAT)) . i in (n + 1) /\ OddNAT by AFINSQ_2:def 4;

then (Sgm0 ((n + 1) /\ OddNAT)) . i in OddNAT by XBOOLE_0:def 4;

then consider r being Nat such that

A17: ( r = (Sgm0 ((n + 1) /\ OddNAT)) . i & r is odd ) ;

consider j being Nat such that

A18: r = (2 * j) + 1 by A17, ABIAN:9;

per cases
( j < i or j = i or j > i )
by XXREAL_0:1;

end;

suppose A19:
j < i
; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

then A20:
j < Segm (card (Sgm0 (n /\ OddNAT)))
by A15;

j < card (Sgm0 ((n + 1) /\ OddNAT)) by A19, A12, NAT_1:44, XXREAL_0:2;

then A21: j in Segm (dom (Sgm0 ((n + 1) /\ OddNAT))) by NAT_1:44;

(Sgm0 ((n + 1) /\ OddNAT)) . j = (Sgm0 (n /\ OddNAT)) . j by A10, A19, A15, AFINSQ_2:29, A6

.= (Sgm0 ((n + 1) /\ OddNAT)) . i by A20, NAT_1:44, A3, A17, A18 ;

hence (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1 by A21, A4, FUNCT_1:def 4, A19; :: thesis: verum

end;j < card (Sgm0 ((n + 1) /\ OddNAT)) by A19, A12, NAT_1:44, XXREAL_0:2;

then A21: j in Segm (dom (Sgm0 ((n + 1) /\ OddNAT))) by NAT_1:44;

(Sgm0 ((n + 1) /\ OddNAT)) . j = (Sgm0 (n /\ OddNAT)) . j by A10, A19, A15, AFINSQ_2:29, A6

.= (Sgm0 ((n + 1) /\ OddNAT)) . i by A20, NAT_1:44, A3, A17, A18 ;

hence (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1 by A21, A4, FUNCT_1:def 4, A19; :: thesis: verum

suppose
j > i
; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

then A22:
2 * i < 2 * j
by XREAL_1:68;

A23: (2 * i) + 1 in OddNAT ;

( (2 * i) + 1 < n & n < n + 1 ) by A22, XREAL_1:8, A17, A18, A16, NAT_1:16;

then (2 * i) + 1 < n + 1 by XXREAL_0:2;

then (2 * i) + 1 in Segm (n + 1) by NAT_1:44;

then (2 * i) + 1 in (n + 1) /\ OddNAT by A23, XBOOLE_0:def 4;

then (2 * i) + 1 in rng (Sgm0 ((n + 1) /\ OddNAT)) by AFINSQ_2:def 4;

then consider l being object such that

A24: ( l in dom (Sgm0 ((n + 1) /\ OddNAT)) & (Sgm0 ((n + 1) /\ OddNAT)) . l = (2 * i) + 1 ) by FUNCT_1:def 3;

reconsider l = l as Element of NAT by A24;

l in Segm (dom (Sgm0 ((n + 1) /\ OddNAT))) by A24;

then l < len (Sgm0 ((n + 1) /\ OddNAT)) by NAT_1:44;

then l < (card (n /\ OddNAT)) + 1 by A11, AFINSQ_2:20;

then l < (len (Sgm0 X)) + 1 by AFINSQ_2:20;

end;A23: (2 * i) + 1 in OddNAT ;

( (2 * i) + 1 < n & n < n + 1 ) by A22, XREAL_1:8, A17, A18, A16, NAT_1:16;

then (2 * i) + 1 < n + 1 by XXREAL_0:2;

then (2 * i) + 1 in Segm (n + 1) by NAT_1:44;

then (2 * i) + 1 in (n + 1) /\ OddNAT by A23, XBOOLE_0:def 4;

then (2 * i) + 1 in rng (Sgm0 ((n + 1) /\ OddNAT)) by AFINSQ_2:def 4;

then consider l being object such that

A24: ( l in dom (Sgm0 ((n + 1) /\ OddNAT)) & (Sgm0 ((n + 1) /\ OddNAT)) . l = (2 * i) + 1 ) by FUNCT_1:def 3;

reconsider l = l as Element of NAT by A24;

l in Segm (dom (Sgm0 ((n + 1) /\ OddNAT))) by A24;

then l < len (Sgm0 ((n + 1) /\ OddNAT)) by NAT_1:44;

then l < (card (n /\ OddNAT)) + 1 by A11, AFINSQ_2:20;

then l < (len (Sgm0 X)) + 1 by AFINSQ_2:20;

per cases then
( l < len (Sgm0 X) or l = len (Sgm0 X) )
by NAT_1:22;

end;

suppose A25:
l < len (Sgm0 X)
; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

then A26:
l < Segm (card (Sgm0 (n /\ OddNAT)))
;

(Sgm0 ((n + 1) /\ OddNAT)) . l = (Sgm0 (n /\ OddNAT)) . l by A10, A25, AFINSQ_2:29, A6

.= (2 * l) + 1 by A26, NAT_1:44, A3 ;

then (2 * i) + 1 = (2 * l) + 1 by A24;

hence (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1 by A25, A15; :: thesis: verum

end;(Sgm0 ((n + 1) /\ OddNAT)) . l = (Sgm0 (n /\ OddNAT)) . l by A10, A25, AFINSQ_2:29, A6

.= (2 * l) + 1 by A26, NAT_1:44, A3 ;

then (2 * i) + 1 = (2 * l) + 1 by A24;

hence (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1 by A25, A15; :: thesis: verum

suppose A27:
n is even
; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

(n + 1) /\ OddNAT = n /\ OddNAT

end;proof

hence
(Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1
by A4, A3; :: thesis: verum
thus
(n + 1) /\ OddNAT c= n /\ OddNAT
:: according to XBOOLE_0:def 10 :: thesis: n /\ OddNAT c= (n + 1) /\ OddNAT

hence n /\ OddNAT c= (n + 1) /\ OddNAT by XBOOLE_1:26; :: thesis: verum

end;proof

Segm n c= Segm (n + 1)
by NAT_1:11, NAT_1:39;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (n + 1) /\ OddNAT or x in n /\ OddNAT )

assume x in (n + 1) /\ OddNAT ; :: thesis: x in n /\ OddNAT

then A28: ( x in Segm (n + 1) & x in OddNAT ) by XBOOLE_0:def 4;

then consider y being Nat such that

A29: ( y = x & y is odd ) ;

y < n by A28, A29, NAT_1:44, A27, NAT_1:22;

then ( y in Segm n & y in OddNAT ) by A29, NAT_1:44;

hence x in n /\ OddNAT by A29, XBOOLE_0:def 4; :: thesis: verum

end;assume x in (n + 1) /\ OddNAT ; :: thesis: x in n /\ OddNAT

then A28: ( x in Segm (n + 1) & x in OddNAT ) by XBOOLE_0:def 4;

then consider y being Nat such that

A29: ( y = x & y is odd ) ;

y < n by A28, A29, NAT_1:44, A27, NAT_1:22;

then ( y in Segm n & y in OddNAT ) by A29, NAT_1:44;

hence x in n /\ OddNAT by A29, XBOOLE_0:def 4; :: thesis: verum

hence n /\ OddNAT c= (n + 1) /\ OddNAT by XBOOLE_1:26; :: thesis: verum

hence for N, i being Nat st i in dom (Sgm0 (N /\ OddNAT)) holds

(Sgm0 (N /\ OddNAT)) . i = (2 * i) + 1 ; :: thesis: verum