1789 subsection{*Products and 1, by T. M. Rasmussen*} |
1789 subsection{*Products and 1, by T. M. Rasmussen*} |
1790 |
1790 |
1791 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))" |
1791 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))" |
1792 by arith |
1792 by arith |
1793 |
1793 |
1794 lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)" |
1794 lemma abs_zmult_eq_1: |
1795 apply (cases "\<bar>n\<bar>=1") |
1795 assumes mn: "\<bar>m * n\<bar> = 1" |
1796 apply (simp add: abs_mult) |
1796 shows "\<bar>m\<bar> = (1::int)" |
1797 apply (rule ccontr) |
1797 proof - |
1798 apply (auto simp add: linorder_neq_iff abs_mult) |
1798 have 0: "m \<noteq> 0 & n \<noteq> 0" using mn |
1799 apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>") |
1799 by auto |
1800 prefer 2 apply arith |
1800 have "~ (2 \<le> \<bar>m\<bar>)" |
1801 apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp) |
1801 proof |
1802 apply (rule mult_mono, auto) |
1802 assume "2 \<le> \<bar>m\<bar>" |
1803 done |
1803 hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>" |
|
1804 by (simp add: mult_mono 0) |
|
1805 also have "... = \<bar>m*n\<bar>" |
|
1806 by (simp add: abs_mult) |
|
1807 also have "... = 1" |
|
1808 by (simp add: mn) |
|
1809 finally have "2*\<bar>n\<bar> \<le> 1" . |
|
1810 thus "False" using 0 |
|
1811 by auto |
|
1812 qed |
|
1813 thus ?thesis using 0 |
|
1814 by auto |
|
1815 qed |
1804 |
1816 |
1805 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1" |
1817 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1" |
1806 by (insert abs_zmult_eq_1 [of m n], arith) |
1818 by (insert abs_zmult_eq_1 [of m n], arith) |
1807 |
1819 |
1808 lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)" |
1820 lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)" |