let a, n, m be Nat; :: thesis: ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 )
set fm = modSeq (m,n);
per cases ( a = 0 or a = 1 or a > 1 ) by NAT_1:25;
suppose A1: a = 0 ; :: thesis: ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 )
( (modSeq (m,n)) . (0 + 1) = n mod (m mod n) & (modSeq (m,n)) . 0 = m mod n ) by Def1;
hence ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 ) by A1, NAT_D:1; :: thesis: verum
end;
suppose A2: a = 1 ; :: thesis: ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 )
(modSeq (m,n)) . (0 + 2) = ((modSeq (m,n)) . 0) mod ((modSeq (m,n)) . (0 + 1)) by Def1;
hence ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 ) by A2, NAT_D:1; :: thesis: verum
end;
suppose a > 1 ; :: thesis: ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 )
then reconsider a1 = a - 1 as Nat ;
(modSeq (m,n)) . (a + 1) = (modSeq (m,n)) . (a1 + (1 + 1))
.= ((modSeq (m,n)) . a1) mod ((modSeq (m,n)) . (a1 + 1)) by Def1 ;
hence ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 ) by NAT_D:1; :: thesis: verum
end;
end;