EDB — 1ZV

[1ZV]Prerequisites:[29D]↺↻,[1ZS]↺↻,[1ZT]↺↻. Prove ¹ than in an ordered ring \(F\):

1. for each \(x ∈ F, x^ 2 ≥ 0\) , in particular \(1 = 1^ 2{\gt}0\);

2. \(x {\gt} 0 ⇒ -x {\lt} 0\)

3. \(y {\gt} x ⇒ -y {\lt} -x \) ;

4. \(x ≤ y \land a ≤ 0 ⇒ a · x ≥ a · y\) ;

5. \(x \ge a \land y\ge b ⇒ x + y ≥ a + b\) ;

6. \(x {\gt} a \land y\ge b ⇒ x + y {\gt} a + b\) ;

7. \(x \ge a \ge 0 \land y\ge b\ge 0 ⇒ x · y ≥ a · b\) ;

Prove than in an ordered field \(F\):

1. \(x {\gt} a {\gt} 0 \land y{\gt} b\ge 0 ⇒ x · y {\gt} a · b\) ;

2. \(x {\gt} 0 ⇒ x ^{−1} {\gt} 0\) ;

3. \(y {\gt} x {\gt} 0 ⇒ x ^{−1} {\gt} y ^{−1} {\gt} 0\) ;

4. \(x · y {\gt} 0\) if and only if \(x\) and \(y\) agree on sign (i.e. either both > 0 or both < 0);