let f be Function of [:NAT,NAT:],ExtREAL; ( f is P-convergent_to_-infty implies ( not f is P-convergent_to_+infty & not f is P-convergent_to_finite_number ) )
assume A1:
f is P-convergent_to_-infty
; ( not f is P-convergent_to_+infty & not f is P-convergent_to_finite_number )
hereby not f is P-convergent_to_finite_number
assume
f is
P-convergent_to_+infty
;
contradictionthen consider N1 being
Nat such that A3:
for
n,
m being
Nat st
n >= N1 &
m >= N1 holds
f . (
n,
m)
>= 1
;
consider N2 being
Nat such that A4:
for
n,
m being
Nat st
n >= N2 &
m >= N2 holds
- 1
>= f . (
n,
m)
by A1;
reconsider N1 =
N1,
N2 =
N2 as
Element of
NAT by ORDINAL1:def 12;
set N =
max (
N1,
N2);
A5:
(
max (
N1,
N2)
>= N1 &
max (
N1,
N2)
>= N2 )
by XXREAL_0:25;
then
f . (
(max (N1,N2)),
(max (N1,N2)))
>= 1
by A3;
hence
contradiction
by A4, A5;
verum
end;
assume
f is P-convergent_to_finite_number
; contradiction
then consider p being Real such that
A6:
for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - p).| < e
;
reconsider p1 = p as ExtReal ;
per cases
( p > 0 or p = 0 or p < 0 )
;
suppose A9:
p > 0
;
contradictionthen consider N1 being
Nat such that A7:
for
n,
m being
Nat st
n >= N1 &
m >= N1 holds
|.((f . (n,m)) - p1).| < p
by A6;
A8:
now for n, m being Nat st n >= N1 & m >= N1 holds
0 < f . (n,m)end; consider N2 being
Nat such that A10:
for
n,
m being
Nat st
n >= N2 &
m >= N2 holds
- (2 * p) >= f . (
n,
m)
by A1, A9;
reconsider N1 =
N1,
N2 =
N2 as
Element of
NAT by ORDINAL1:def 12;
set N =
max (
N1,
N2);
A11:
(
max (
N1,
N2)
>= N1 &
max (
N1,
N2)
>= N2 )
by XXREAL_0:25;
then
0 < f . (
(max (N1,N2)),
(max (N1,N2)))
by A8;
hence
contradiction
by A9, A11, A10;
verum end; suppose A12:
p = 0
;
contradictionconsider N1 being
Nat such that A13:
for
n,
m being
Nat st
n >= N1 &
m >= N1 holds
|.((f . (n,m)) - p).| < 1
by A6;
consider N2 being
Nat such that A14:
for
n,
m being
Nat st
n >= N2 &
m >= N2 holds
- 1
>= f . (
n,
m)
by A1;
reconsider N1 =
N1,
N2 =
N2 as
Element of
NAT by ORDINAL1:def 12;
reconsider jj = 1 as
ExtReal ;
set N =
max (
N1,
N2);
A15:
(
max (
N1,
N2)
>= N1 &
max (
N1,
N2)
>= N2 )
by XXREAL_0:25;
then
|.((f . ((max (N1,N2)),(max (N1,N2)))) - p1).| < jj
by A13;
then
- jj < (f . ((max (N1,N2)),(max (N1,N2)))) - p1
by EXTREAL1:21;
then
(- jj) + p < f . (
(max (N1,N2)),
(max (N1,N2)))
by XXREAL_3:53;
then
- jj < f . (
(max (N1,N2)),
(max (N1,N2)))
by A12, XXREAL_3:4;
then
- 1
< f . (
(max (N1,N2)),
(max (N1,N2)))
by XXREAL_3:def 3;
hence
contradiction
by A14, A15;
verum end; suppose A16:
p < 0
;
contradictionthen consider N1 being
Nat such that A17:
for
n,
m being
Nat st
n >= N1 &
m >= N1 holds
|.((f . (n,m)) - p).| < - p
by A6;
A18:
now for n, m being Nat st n >= N1 & m >= N1 holds
2 * p < f . (n,m)end; consider N2 being
Nat such that A19:
for
n,
m being
Nat st
n >= N2 &
m >= N2 holds
f . (
n,
m)
<= 2
* p
by A1, A16;
reconsider N1 =
N1,
N2 =
N2 as
Element of
NAT by ORDINAL1:def 12;
set N =
max (
N1,
N2);
A20:
(
max (
N1,
N2)
>= N1 &
max (
N1,
N2)
>= N2 )
by XXREAL_0:25;
then
2
* p < f . (
(max (N1,N2)),
(max (N1,N2)))
by A18;
hence
contradiction
by A19, A20;
verum end; end;