defpred S1[ Nat] means for i being Nat st i in dom (Sgm0 ($1 /\ EvenNAT)) holds
(Sgm0 ($1 /\ EvenNAT)) . i = 2 * i;
A1:
S1[ 0 ]
A2:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A3:
S1[
n]
;
S1[n + 1]thus
S1[
n + 1]
verumproof
let i be
Nat;
( i in dom (Sgm0 ((n + 1) /\ EvenNAT)) implies (Sgm0 ((n + 1) /\ EvenNAT)) . i = 2 * i )
assume A4:
i in dom (Sgm0 ((n + 1) /\ EvenNAT))
;
(Sgm0 ((n + 1) /\ EvenNAT)) . i = 2 * i
per cases
( n is even or n is odd )
;
suppose A5:
n is
even
;
(Sgm0 ((n + 1) /\ EvenNAT)) . i = 2 * iA6:
(n + 1) /\ EvenNAT = (n /\ EvenNAT) \/ {n}
reconsider X =
n /\ EvenNAT as
finite natural-membered set ;
reconsider Y =
{n} as
finite natural-membered set ;
A10:
X <N< Y
not
n in n
;
then
not
n in n /\ EvenNAT
by XBOOLE_0:def 4;
then A11:
card ((n + 1) /\ EvenNAT) = (card (n /\ EvenNAT)) + 1
by A6, CARD_2:41;
A12:
i in Segm (dom (Sgm0 ((n + 1) /\ EvenNAT)))
by A4;
then
i < len (Sgm0 ((n + 1) /\ EvenNAT))
by NAT_1:44;
then
i < (card (n /\ EvenNAT)) + 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;
suppose A15:
i = len (Sgm0 X)
;
(Sgm0 ((n + 1) /\ EvenNAT)) . i = 2 * ithen A16:
(Sgm0 ((n + 1) /\ EvenNAT)) . i =
(Sgm0 Y) . 0
by AFINSQ_2:32, A10, A6
.=
n
by AFINSQ_2:22
;
(Sgm0 ((n + 1) /\ EvenNAT)) . i in rng (Sgm0 ((n + 1) /\ EvenNAT))
by FUNCT_1:3, A4;
then
(Sgm0 ((n + 1) /\ EvenNAT)) . i in (n + 1) /\ EvenNAT
by AFINSQ_2:def 4;
then
(Sgm0 ((n + 1) /\ EvenNAT)) . i in EvenNAT
by XBOOLE_0:def 4;
then consider r being
Nat such that A17:
(
r = (Sgm0 ((n + 1) /\ EvenNAT)) . i &
r is
even )
;
consider j being
Nat such that A18:
r = 2
* j
by A17, ABIAN:def 2;
per cases
( j < i or j = i or j > i )
by XXREAL_0:1;
suppose A19:
j < i
;
(Sgm0 ((n + 1) /\ EvenNAT)) . i = 2 * ithen A20:
j < Segm (card (Sgm0 (n /\ EvenNAT)))
by A15;
j < card (Sgm0 ((n + 1) /\ EvenNAT))
by A19, A12, NAT_1:44, XXREAL_0:2;
then A21:
j in Segm (dom (Sgm0 ((n + 1) /\ EvenNAT)))
by NAT_1:44;
(Sgm0 ((n + 1) /\ EvenNAT)) . j =
(Sgm0 (n /\ EvenNAT)) . j
by A10, A19, A15, AFINSQ_2:29, A6
.=
(Sgm0 ((n + 1) /\ EvenNAT)) . i
by A20, NAT_1:44, A3, A17, A18
;
hence
(Sgm0 ((n + 1) /\ EvenNAT)) . i = 2
* i
by A21, A4, FUNCT_1:def 4, A19;
verum end; end; end; end; end; end;
end; end;
for N being Nat holds S1[N]
from NAT_1:sch 2(A1, A2);
hence
for N, i being Nat st i in dom (Sgm0 (N /\ EvenNAT)) holds
(Sgm0 (N /\ EvenNAT)) . i = 2 * i
; verum