let O be Ordering of F_Rat; O = Positives(F_Rat)
defpred S1[ Nat] means $1 in O;
A:
( 0. F_Rat = 0 & 1. F_Rat = 1 )
by GAUSSINT:def 14;
B:
( 1. F_Rat in O & 0. F_Rat in O )
by ord3;
IA:
S1[ 0 ]
by A, ord3;
E:
( O + O c= O & O * O c= O )
by defpc;
IS:
now for k being Nat st S1[k] holds
S1[k + 1]end;
I:
for k being Nat holds S1[k]
from NAT_1:sch 2(IA, IS);
Positives(F_Rat) c= O
proof
let o be
object ;
TARSKI:def 3 ( not o in Positives(F_Rat) or o in O )
assume
o in Positives(F_Rat)
;
o in O
then consider r being
Element of
RAT such that A1:
(
o = r &
0 <= r )
;
consider m,
n being
Integer such that B1:
(
n <> 0 &
r = m / n )
by RAT_1:1;
reconsider a =
n,
b =
m as
Element of
F_Rat by RAT_1:def 2, GAUSSINT:def 14;
per cases
( m = 0 or 0 < m or m < 0 )
;
suppose C1:
m < 0
;
o in Othen
0 >= n
by A1, B1;
then reconsider n1 =
- n,
m1 =
- m as
Element of
NAT by C1, INT_1:3;
C:
(
m1 in O &
n1 in O )
by I;
K:
- a <> 0. F_Rat
by B1, GAUSSINT:def 14;
not
- a is
zero
by B1, GAUSSINT:def 14;
then
(- a) " in O
by C, ord5;
then F:
(- b) * ((- a) ") in O * O
by C;
H:
- (n ") = - (a ")
by B1, GAUSSINT:def 14, GAUSSINT:15;
a <> 0. F_Rat
by B1, GAUSSINT:def 14;
then 1. F_Rat =
a * (a ")
by VECTSP_1:def 10
.=
(- (a ")) * (- a)
;
then
(- a) " = - (a ")
by VECTSP_1:def 10, K;
hence
o in O
by A1, B1, F, E, H;
verum end; end;
end;
hence
O = Positives(F_Rat)
by ordsub; verum