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
f . (n,m) < 2 * pend; 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
f . (
(max (N1,N2)),
(max (N1,N2)))
< 2
* p
by A8;
hence
contradiction
by 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
(f . ((max (N1,N2)),(max (N1,N2)))) - p1 < jj
by EXTREAL1:21;
then
f . (
(max (N1,N2)),
(max (N1,N2)))
< jj + p1
by XXREAL_3:54;
then
f . (
(max (N1,N2)),
(max (N1,N2)))
< 1
+ 0
by A12, XXREAL_3:def 2;
hence
contradiction
by A14, A15;
verum end; suppose
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
f . (n,m) < 0 end; consider N2 being
Nat such that A19:
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);
A20:
(
max (
N1,
N2)
>= N1 &
max (
N1,
N2)
>= N2 )
by XXREAL_0:25;
then
f . (
(max (N1,N2)),
(max (N1,N2)))
< 0
by A18;
hence
contradiction
by A19, A20;
verum end; end;