---

Step * 1 of Lemma cube-mod-9


1. n : ℤ
2. (n rem 9) ≡ n mod 9
3. (n rem 9)^3 ≡ n^3 mod 9
⊢ ((n rem 9)^3 ≡ 0 mod 9) ∨ ((n rem 9)^3 ≡ 1 mod 9) ∨ ((n rem 9)^3 ≡ (-1) mod 9)
BY
{ ((GenConcl ⌜(n rem 9) = r ∈ {-8..9-}⌝⋅
    THENA (Auto
           THEN (InstLemma `rem_bounds_absval` [⌜9⌝;⌜n⌝]⋅ THENA Auto)
           THEN (Subst' |9| ~ 9 -1 THENA Auto)
           THEN RWO "absval_strict_ubound" (-1)
           THEN Auto)
    )
   THEN All Thin
   ) }

1
1. r : {-8..9-}
⊢ (r^3 ≡ 0 mod 9) ∨ (r^3 ≡ 1 mod 9) ∨ (r^3 ≡ (-1) mod 9)

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  (n  rem  9)  \mequiv{}  n  mod  9
3.  (n  rem  9)\^{}3  \mequiv{}  n\^{}3  mod  9
\mvdash{}  ((n  rem  9)\^{}3  \mequiv{}  0  mod  9)  \mvee{}  ((n  rem  9)\^{}3  \mequiv{}  1  mod  9)  \mvee{}  ((n  rem  9)\^{}3  \mequiv{}  (-1)  mod  9)


By

---

Latex:
((GenConcl  \mkleeneopen{}(n  rem  9)  =  r\mkleeneclose{}\mcdot{}
    THENA  (Auto
                  THEN  (InstLemma  `rem\_bounds\_absval`  [\mkleeneopen{}9\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
                  THEN  (Subst'  |9|  \msim{}  9  -1  THENA  Auto)
                  THEN  RWO  "absval\_strict\_ubound"  (-1)
                  THEN  Auto)
    )
  THEN  All  Thin
  )

---

Home Index