1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
(* Evgeny Makarov, INRIA, 2007 *)
9
(************************************************************************)
11
(*i $Id: ZMulOrder.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
13
Require Export ZAddOrder.
15
Module ZMulOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
16
Module Export ZAddOrderPropMod := ZAddOrderPropFunct ZAxiomsMod.
17
Open Local Scope IntScope.
19
Theorem Zmul_lt_pred :
20
forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
23
Theorem Zmul_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m).
24
Proof NZmul_lt_mono_pos_l.
26
Theorem Zmul_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p).
27
Proof NZmul_lt_mono_pos_r.
29
Theorem Zmul_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n).
30
Proof NZmul_lt_mono_neg_l.
32
Theorem Zmul_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p).
33
Proof NZmul_lt_mono_neg_r.
35
Theorem Zmul_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m.
36
Proof NZmul_le_mono_nonneg_l.
38
Theorem Zmul_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n.
39
Proof NZmul_le_mono_nonpos_l.
41
Theorem Zmul_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p.
42
Proof NZmul_le_mono_nonneg_r.
44
Theorem Zmul_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p.
45
Proof NZmul_le_mono_nonpos_r.
47
Theorem Zmul_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m).
50
Theorem Zmul_cancel_r : forall n m p : Z, p ~= 0 -> (n * p == m * p <-> n == m).
53
Theorem Zmul_id_l : forall n m : Z, m ~= 0 -> (n * m == m <-> n == 1).
56
Theorem Zmul_id_r : forall n m : Z, n ~= 0 -> (n * m == n <-> m == 1).
59
Theorem Zmul_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
60
Proof NZmul_le_mono_pos_l.
62
Theorem Zmul_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p).
63
Proof NZmul_le_mono_pos_r.
65
Theorem Zmul_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n).
66
Proof NZmul_le_mono_neg_l.
68
Theorem Zmul_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p).
69
Proof NZmul_le_mono_neg_r.
71
Theorem Zmul_lt_mono_nonneg :
72
forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
73
Proof NZmul_lt_mono_nonneg.
75
Theorem Zmul_lt_mono_nonpos :
76
forall n m p q : Z, m <= 0 -> n < m -> q <= 0 -> p < q -> m * q < n * p.
78
intros n m p q H1 H2 H3 H4.
79
apply Zle_lt_trans with (m * p).
80
apply Zmul_le_mono_nonpos_l; [assumption | now apply Zlt_le_incl].
81
apply -> Zmul_lt_mono_neg_r; [assumption | now apply Zlt_le_trans with q].
84
Theorem Zmul_le_mono_nonneg :
85
forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
86
Proof NZmul_le_mono_nonneg.
88
Theorem Zmul_le_mono_nonpos :
89
forall n m p q : Z, m <= 0 -> n <= m -> q <= 0 -> p <= q -> m * q <= n * p.
91
intros n m p q H1 H2 H3 H4.
92
apply Zle_trans with (m * p).
93
now apply Zmul_le_mono_nonpos_l.
94
apply Zmul_le_mono_nonpos_r; [now apply Zle_trans with q | assumption].
97
Theorem Zmul_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m.
100
Theorem Zmul_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m.
103
Theorem Zmul_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0.
106
Theorem Zmul_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0.
109
Theorem Zmul_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m.
112
rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonneg_r.
115
Theorem Zmul_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m.
118
rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonpos_r.
121
Theorem Zmul_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0.
124
rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonpos_r.
127
Theorem Zmul_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0.
129
intros; rewrite Zmul_comm; now apply Zmul_nonneg_nonpos.
132
Theorem Zlt_1_mul_pos : forall n m : Z, 1 < n -> 0 < m -> 1 < n * m.
133
Proof NZlt_1_mul_pos.
135
Theorem Zeq_mul_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0.
138
Theorem Zneq_mul_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
141
Theorem Zeq_square_0 : forall n : Z, n * n == 0 <-> n == 0.
144
Theorem Zeq_mul_0_l : forall n m : Z, n * m == 0 -> m ~= 0 -> n == 0.
147
Theorem Zeq_mul_0_r : forall n m : Z, n * m == 0 -> n ~= 0 -> m == 0.
150
Theorem Zlt_0_mul : forall n m : Z, 0 < n * m <-> 0 < n /\ 0 < m \/ m < 0 /\ n < 0.
153
Notation Zmul_pos := Zlt_0_mul (only parsing).
156
forall n m : Z, n * m < 0 <-> n < 0 /\ m > 0 \/ n > 0 /\ m < 0.
158
intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]].
159
destruct (Zlt_trichotomy n 0) as [H1 | [H1 | H1]];
160
[| rewrite H1 in H; rewrite Zmul_0_l in H; false_hyp H Zlt_irrefl |];
161
(destruct (Zlt_trichotomy m 0) as [H2 | [H2 | H2]];
162
[| rewrite H2 in H; rewrite Zmul_0_r in H; false_hyp H Zlt_irrefl |]);
163
try (left; now split); try (right; now split).
164
assert (H3 : n * m > 0) by now apply Zmul_neg_neg.
165
elimtype False; now apply (Zlt_asymm (n * m) 0).
166
assert (H3 : n * m > 0) by now apply Zmul_pos_pos.
167
elimtype False; now apply (Zlt_asymm (n * m) 0).
168
now apply Zmul_neg_pos. now apply Zmul_pos_neg.
171
Notation Zmul_neg := Zlt_mul_0 (only parsing).
174
forall n m : Z, 0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0.
176
assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_sym).
177
intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R.
178
rewrite Zlt_0_mul, Zeq_mul_0.
179
pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto.
182
Notation Zmul_nonneg := Zle_0_mul (only parsing).
185
forall n m : Z, n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 /\ 0 <= m.
187
assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_sym).
188
intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R.
189
rewrite Zlt_mul_0, Zeq_mul_0.
190
pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto.
193
Notation Zmul_nonpos := Zle_mul_0 (only parsing).
195
Theorem Zle_0_square : forall n : Z, 0 <= n * n.
197
intro n; destruct (Zneg_nonneg_cases n).
198
apply Zlt_le_incl; now apply Zmul_neg_neg.
199
now apply Zmul_nonneg_nonneg.
202
Notation Zsquare_nonneg := Zle_0_square (only parsing).
204
Theorem Znlt_square_0 : forall n : Z, ~ n * n < 0.
206
intros n H. apply -> Zlt_nge in H. apply H. apply Zsquare_nonneg.
209
Theorem Zsquare_lt_mono_nonneg : forall n m : Z, 0 <= n -> n < m -> n * n < m * m.
210
Proof NZsquare_lt_mono_nonneg.
212
Theorem Zsquare_lt_mono_nonpos : forall n m : Z, n <= 0 -> m < n -> n * n < m * m.
214
intros n m H1 H2. now apply Zmul_lt_mono_nonpos.
217
Theorem Zsquare_le_mono_nonneg : forall n m : Z, 0 <= n -> n <= m -> n * n <= m * m.
218
Proof NZsquare_le_mono_nonneg.
220
Theorem Zsquare_le_mono_nonpos : forall n m : Z, n <= 0 -> m <= n -> n * n <= m * m.
222
intros n m H1 H2. now apply Zmul_le_mono_nonpos.
225
Theorem Zsquare_lt_simpl_nonneg : forall n m : Z, 0 <= m -> n * n < m * m -> n < m.
226
Proof NZsquare_lt_simpl_nonneg.
228
Theorem Zsquare_le_simpl_nonneg : forall n m : Z, 0 <= m -> n * n <= m * m -> n <= m.
229
Proof NZsquare_le_simpl_nonneg.
231
Theorem Zsquare_lt_simpl_nonpos : forall n m : Z, m <= 0 -> n * n < m * m -> m < n.
233
intros n m H1 H2. destruct (Zle_gt_cases n 0).
234
destruct (NZlt_ge_cases m n).
235
assumption. assert (F : m * m <= n * n) by now apply Zsquare_le_mono_nonpos.
236
apply -> NZle_ngt in F. false_hyp H2 F.
237
now apply Zle_lt_trans with 0.
240
Theorem Zsquare_le_simpl_nonpos : forall n m : NZ, m <= 0 -> n * n <= m * m -> m <= n.
242
intros n m H1 H2. destruct (NZle_gt_cases n 0).
243
destruct (NZle_gt_cases m n).
244
assumption. assert (F : m * m < n * n) by now apply Zsquare_lt_mono_nonpos.
245
apply -> NZlt_nge in F. false_hyp H2 F.
246
apply Zlt_le_incl; now apply NZle_lt_trans with 0.
249
Theorem Zmul_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
250
Proof NZmul_2_mono_l.
252
Theorem Zlt_1_mul_neg : forall n m : Z, n < -1 -> m < 0 -> 1 < n * m.
254
intros n m H1 H2. apply -> (NZmul_lt_mono_neg_r m) in H1.
255
apply <- Zopp_pos_neg in H2. rewrite Zmul_opp_l, Zmul_1_l in H1.
256
now apply Zlt_1_l with (- m).
260
Theorem Zlt_mul_n1_neg : forall n m : Z, 1 < n -> m < 0 -> n * m < -1.
262
intros n m H1 H2. apply -> (NZmul_lt_mono_neg_r m) in H1.
263
rewrite Zmul_1_l in H1. now apply Zlt_n1_r with m.
267
Theorem Zlt_mul_n1_pos : forall n m : Z, n < -1 -> 0 < m -> n * m < -1.
269
intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1.
270
rewrite Zmul_opp_l, Zmul_1_l in H1.
271
apply <- Zopp_neg_pos in H2. now apply Zlt_n1_r with (- m).
275
Theorem Zlt_1_mul_l : forall n m : Z, 1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
277
intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]].
278
left. now apply Zlt_mul_n1_neg.
279
right; left; now rewrite H1, Zmul_0_r.
280
right; right; now apply Zlt_1_mul_pos.
283
Theorem Zlt_n1_mul_r : forall n m : Z, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
285
intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]].
286
right; right. now apply Zlt_1_mul_neg.
287
right; left; now rewrite H1, Zmul_0_r.
288
left. now apply Zlt_mul_n1_pos.
291
Theorem Zeq_mul_1 : forall n m : Z, n * m == 1 -> n == 1 \/ n == -1.
293
assert (F : ~ 1 < -1).
295
assert (H1 : -1 < 0). apply <- Zopp_neg_pos. apply Zlt_succ_diag_r.
296
assert (H2 : 1 < 0) by now apply Zlt_trans with (-1). false_hyp H2 Znlt_succ_diag_l.
298
intros m H; rewrite Zmul_0_l in H; false_hyp H Zneq_succ_diag_r.
299
intros n H; split; apply <- Zle_succ_l in H; le_elim H.
300
intros m H1; apply (Zlt_1_mul_l n m) in H.
301
rewrite H1 in H; destruct H as [H | [H | H]].
302
false_hyp H F. false_hyp H Zneq_succ_diag_l. false_hyp H Zlt_irrefl.
304
intros m H1; apply (Zlt_1_mul_l n m) in H. rewrite Zmul_opp_l in H1;
305
apply -> Zeq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]].
306
false_hyp H Zlt_irrefl. apply -> Zeq_opp_l in H. rewrite Zopp_0 in H.
307
false_hyp H Zneq_succ_diag_l. false_hyp H F.
308
intros; right; symmetry; now apply Zopp_wd.
311
Theorem Zlt_mul_diag_l : forall n m : Z, n < 0 -> (1 < m <-> n * m < n).
313
intros n m H. stepr (n * m < n * 1) by now rewrite Zmul_1_r.
314
now apply Zmul_lt_mono_neg_l.
317
Theorem Zlt_mul_diag_r : forall n m : Z, 0 < n -> (1 < m <-> n < n * m).
319
intros n m H. stepr (n * 1 < n * m) by now rewrite Zmul_1_r.
320
now apply Zmul_lt_mono_pos_l.
323
Theorem Zle_mul_diag_l : forall n m : Z, n < 0 -> (1 <= m <-> n * m <= n).
325
intros n m H. stepr (n * m <= n * 1) by now rewrite Zmul_1_r.
326
now apply Zmul_le_mono_neg_l.
329
Theorem Zle_mul_diag_r : forall n m : Z, 0 < n -> (1 <= m <-> n <= n * m).
331
intros n m H. stepr (n * 1 <= n * m) by now rewrite Zmul_1_r.
332
now apply Zmul_le_mono_pos_l.
335
Theorem Zlt_mul_r : forall n m p : Z, 0 < n -> 1 < p -> n < m -> n < m * p.
337
intros. stepl (n * 1) by now rewrite Zmul_1_r.
338
apply Zmul_lt_mono_nonneg.
339
now apply Zlt_le_incl. assumption. apply Zle_0_1. assumption.
342
End ZMulOrderPropFunct.
added
removed
theories/Numbers/Integer/Abstract/ZMulOrder.v
