:: by Robert Milewski

::

:: Received February 23, 1998

:: Copyright (c) 1998-2021 Association of Mizar Users

scheme :: NAT_2:sch 1

NonUniqPiFinRecExD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Nat, P_{1}[ set , set , set ] } :

NonUniqPiFinRecExD{ F

ex p being FinSequence of F_{1}() st

( len p = F_{3}() & ( p /. 1 = F_{2}() or F_{3}() = 0 ) & ( for n being Nat st 1 <= n & n < F_{3}() holds

P_{1}[n,p /. n,p /. (n + 1)] ) )

provided( len p = F

P

A1:
for n being Nat st 1 <= n & n < F_{3}() holds

for x being Element of F_{1}() ex y being Element of F_{1}() st P_{1}[n,x,y]

for x being Element of F

proof end;

theorem :: NAT_2:15

for i, k, n being Nat st k divides n & 1 <= n & 1 <= i & i <= k holds

(n -' i) div k = (n div k) - 1

(n -' i) div k = (n div k) - 1

proof end;

theorem :: NAT_2:23

for k, n, t being Nat st 1 <= t & k <= n & 2 * t divides k holds

( n div t is even iff (n -' k) div t is even )

( n div t is even iff (n -' k) div t is even )

proof end;

:: deftheorem Def1 defines trivial NAT_2:def 1 :

for n being Nat holds

( n is trivial iff ( n = 0 or n = 1 ) );

for n being Nat holds

( n is trivial iff ( n = 0 or n = 1 ) );

registration

not for b_{1} being Nat holds b_{1} is trivial
end;

cluster ext-real non negative non trivial V12() V13() V14() V18() complex V38() integer dim-like for set ;

existence not for b

proof end;

:: from POLYNOM1, 2007.03.18, A.T.