|
57
|
1 module root2 where
|
|
|
2
|
|
141
|
3 open import Data.Nat
|
|
|
4 open import Data.Nat.Properties
|
|
57
|
5 open import Data.Empty
|
|
141
|
6 open import Data.Unit using (⊤ ; tt)
|
|
57
|
7 open import Relation.Nullary
|
|
|
8 open import Relation.Binary.PropositionalEquality
|
|
141
|
9 open import Relation.Binary.Definitions
|
|
57
|
10
|
|
148
|
11 open import gcd
|
|
159
|
12 open import even
|
|
142
|
13 open import nat
|
|
231
|
14 open import logic
|
|
141
|
15
|
|
|
16 record Rational : Set where
|
|
|
17 field
|
|
|
18 i j : ℕ
|
|
|
19 coprime : gcd i j ≡ 1
|
|
57
|
20
|
|
231
|
21 open _∧_
|
|
|
22
|
|
|
23 open import prime
|
|
|
24
|
|
|
25 -- equlid : ( n m k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * m ) → Dividable k n ∨ Dividable k m
|
|
|
26 -- equlid = {!!}
|
|
|
27
|
|
233
|
28 divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n
|
|
|
29 divdable^2 zero zero () 1<n pk dn2
|
|
|
30 divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
|
|
159
|
31 ... | yes y = y
|
|
250
|
32 ... | no non with gcd-euclid (suc k) (suc n) (suc n) 1<k (<-trans a<sa 1<n) (<-trans a<sa 1<n) (Prime.isPrime pk) dn2
|
|
233
|
33 ... | case1 dn = dn
|
|
|
34 ... | case2 dm = dm
|
|
159
|
35
|
|
199
|
36 -- gcd-div : ( i j k : ℕ ) → (if : Dividable k i) (jf : Dividable k j )
|
|
186
|
37 -- → Dividable k ( gcd i j )
|
|
|
38
|
|
253
|
39 root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime (suc p) → m > 1 → (suc p) * n * n ≡ m * m → ¬ (gcd n m ≡ 1)
|
|
|
40 root-prime-irrational n m p n>1 pn m>1 pnm = rot13 ( gcd-div n m (suc p) 1<sp dn dm ) where
|
|
|
41 1<sp : 1 < suc p
|
|
|
42 1<sp = Prime.p>1 pn
|
|
|
43 rot13 : {m : ℕ } → Dividable (suc p) m → m ≡ 1 → ⊥
|
|
185
|
44 rot13 d refl with Dividable.factor d | Dividable.is-factor d
|
|
253
|
45 ... | zero | () -- gcd 0 m ≡ 1
|
|
|
46 ... | suc n | x = ⊥-elim ( nat-≡< (sym x) rot17 ) where -- x : (suc n * suc p + 0) ≡ 1
|
|
|
47 rot17 : suc n * suc p + 0 > 1
|
|
|
48 rot17 = begin
|
|
|
49 2 ≡⟨ refl ⟩
|
|
|
50 suc (1 * 1 ) ≤⟨ {!!} ⟩
|
|
|
51 suc (1 * suc p ) <⟨ {!!} ⟩
|
|
|
52 suc (0 + n * suc p ) ≤⟨ {!!} ⟩
|
|
|
53 suc (p + n * suc p ) ≡⟨ +-comm 0 _ ⟩
|
|
|
54 suc n * suc p + 0 ∎ where open ≤-Reasoning
|
|
|
55 dm : Dividable (suc p) m
|
|
|
56 dm = divdable^2 m (suc p) 1<sp m>1 pn record { factor = n * n ; is-factor = begin
|
|
|
57 (n * n) * (suc p) + 0 ≡⟨ +-comm _ 0 ⟩
|
|
|
58 (n * n) * (suc p) ≡⟨ *-comm (n * n) (suc p) ⟩
|
|
|
59 (suc p) * (n * n) ≡⟨ sym (*-assoc (suc p) n n) ⟩
|
|
|
60 (suc p * n) * n ≡⟨ pnm ⟩
|
|
250
|
61 m * m ∎ } where open ≡-Reasoning
|
|
253
|
62 -- (suc p) * n * n = 2m' 2m'
|
|
251
|
63 -- n * n = m' 2m'
|
|
250
|
64 df = Dividable.factor dm
|
|
253
|
65 dn : Dividable (suc p) n
|
|
|
66 dn = divdable^2 n (suc p) 1<sp n>1 pn record { factor = df * df ; is-factor = begin
|
|
|
67 df * df * (suc p) + 0 ≡⟨ *-cancelʳ-≡ _ _ {p} ( begin
|
|
|
68 (df * df * (suc p) + 0) * (suc p) ≡⟨ cong (λ k → k * (suc p)) (+-comm (df * df * (suc p)) 0) ⟩
|
|
|
69 ((df * df) * (suc p)) * (suc p) ≡⟨ cong (λ k → k * (suc p)) (*-assoc df df (suc p) ) ⟩
|
|
|
70 (df * (df * (suc p))) * (suc p) ≡⟨ cong (λ k → (df * k ) * (suc p)) (*-comm df (suc p)) ⟩
|
|
|
71 (df * ((suc p) * df)) * (suc p) ≡⟨ sym ( cong (λ k → k * (suc p)) (*-assoc df (suc p) df ) ) ⟩
|
|
|
72 ((df * (suc p)) * df) * (suc p) ≡⟨ *-assoc (df * (suc p)) df (suc p) ⟩
|
|
|
73 (df * (suc p)) * (df * (suc p)) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * (suc p))) (+-comm 0 _) ⟩
|
|
|
74 (df * (suc p) + 0) * (df * (suc p) + 0) ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩
|
|
|
75 m * m ≡⟨ sym pnm ⟩
|
|
|
76 (suc p) * n * n ≡⟨ cong (λ k → k * n) (*-comm (suc p) n) ⟩
|
|
|
77 n * (suc p) * n ≡⟨ *-assoc n (suc p) n ⟩
|
|
|
78 n * (suc p * n) ≡⟨ cong (λ k → n * k) (*-comm (suc p) n) ⟩
|
|
|
79 n * (n * suc p) ≡⟨ sym (*-assoc n n (suc p)) ⟩
|
|
|
80 n * n * (suc p) ∎ ) ⟩
|
|
250
|
81 n * n ∎ } where open ≡-Reasoning
|
|
57
|
82
|
|
185
|
83
|
