---

Step * of Lemma divisor-in-range

∀n:{2...}
  ∀[k:ℕ]
    ∀i:{1...}. ∀j:{i..i + k-}.
      (∃m:ℤ [(m < n ∧ (2 ≤ m) ∧ (m | n))]) ∨ (¬(∃m:ℤ [((2 ≤ m) ∧ (i ≤ m) ∧ (m ≤ j) ∧ (m | n))])) supposing j < n
BY
{ TACTIC:((D 0 THENA Auto)
          THEN InstLemma `uniform-comp-nat-induction` [⌜λ2k.∀i:{1...}. ∀j:{i..i + k-}.
                                                              (∃m:ℤ [(m < n ∧ (2 ≤ m) ∧ (m | n))])
                                                              ∨ (¬(∃m:ℤ [((2 ≤ m) ∧ (i ≤ m) ∧ (m ≤ j) ∧ (m | n))])) 
                                                              supposing j < n⌝]⋅
          THEN Auto
          THEN (Evaluate ⌜p = iseg_product_rem(i;j;n) ∈ ℤ⌝⋅ THENA Auto)
          THEN (Evaluate ⌜g = better-gcd(n;p) ∈ ℤ⌝⋅ THENA Auto)
          THEN Subst' better-gcd(n;p) = gcd(n;iseg_product(i;j)) ∈ ℤ -1) }

1
.....equality..... 
1. n : {2...}
2. n@0 : ℕ
3. ∀[m:ℕn@0]
     ∀i:{1...}. ∀j:{i..i + m-}.
       (∃m:ℤ [(m < n ∧ (2 ≤ m) ∧ (m | n))]) ∨ (¬(∃m:ℤ [((2 ≤ m) ∧ (i ≤ m) ∧ (m ≤ j) ∧ (m | n))])) supposing j < n
4. i : {1...}
5. j : {i..i + n@0-}
6. j < n
7. p : ℤ
8. p = iseg_product_rem(i;j;n) ∈ ℤ
9. g : ℤ
10. g = better-gcd(n;p) ∈ ℤ
⊢ better-gcd(n;p) = gcd(n;iseg_product(i;j)) ∈ ℤ

2
1. n : {2...}
2. [n@0] : ℕ
3. ∀[m:ℕn@0]
     ∀i:{1...}. ∀j:{i..i + m-}.
       (∃m:ℤ [(m < n ∧ (2 ≤ m) ∧ (m | n))]) ∨ (¬(∃m:ℤ [((2 ≤ m) ∧ (i ≤ m) ∧ (m ≤ j) ∧ (m | n))])) supposing j < n
4. i : {1...}
5. j : {i..i + n@0-}
6. j < n
7. p : ℤ
8. p = iseg_product_rem(i;j;n) ∈ ℤ
9. g : ℤ
10. g = gcd(n;iseg_product(i;j)) ∈ ℤ
⊢ (∃m:ℤ [(m < n ∧ (2 ≤ m) ∧ (m | n))]) ∨ (¬(∃m:ℤ [((2 ≤ m) ∧ (i ≤ m) ∧ (m ≤ j) ∧ (m | n))]))

---

Latex:

---

Latex:
\mforall{}n:\{2...\}
    \mforall{}[k:\mBbbN{}]
        \mforall{}i:\{1...\}.  \mforall{}j:\{i..i  +  k\msupminus{}\}.
            (\mexists{}m:\mBbbZ{}  [(m  <  n  \mwedge{}  (2  \mleq{}  m)  \mwedge{}  (m  |  n))])  \mvee{}  (\mneg{}(\mexists{}m:\mBbbZ{}  [((2  \mleq{}  m)  \mwedge{}  (i  \mleq{}  m)  \mwedge{}  (m  \mleq{}  j)  \mwedge{}  (m  |  n))])) 
            supposing  j  <  n


By

---

Latex:
TACTIC:((D  0  THENA  Auto)
                THEN  InstLemma  `uniform-comp-nat-induction`  [\mkleeneopen{}\mlambda{}\msubtwo{}k.\mforall{}i:\{1...\}.  \mforall{}j:\{i..i  +  k\msupminus{}\}.
                                                                                                                        (\mexists{}m:\mBbbZ{}  [(m  <  n  \mwedge{}  (2  \mleq{}  m)  \mwedge{}  (m  |  n))])
                                                                                                                        \mvee{}  (\mneg{}(\mexists{}m:\mBbbZ{}  [((2  \mleq{}  m)
                                                                                                                                            \mwedge{}  (i  \mleq{}  m)
                                                                                                                                            \mwedge{}  (m  \mleq{}  j)
                                                                                                                                            \mwedge{}  (m  |  n))])) 
                                                                                                                        supposing  j  <  n\mkleeneclose{}]\mcdot{}
                THEN  Auto
                THEN  (Evaluate  \mkleeneopen{}p  =  iseg\_product\_rem(i;j;n)\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (Evaluate  \mkleeneopen{}g  =  better-gcd(n;p)\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  Subst'  better-gcd(n;p)  =  gcd(n;iseg\_product(i;j))  -1)

---

Home Index