---

Step * of Lemma cube-mod-9

∀n:ℤ. ((n^3 ≡ 0 mod 9) ∨ (n^3 ≡ 1 mod 9) ∨ (n^3 ≡ (-1) mod 9))
BY
{ ((D 0 THENA Auto)
   THEN (InstLemma `rem-eqmod` [⌜n⌝;⌜9⌝]⋅ THENA Auto)
   THEN (InstLemma `exp_functionality_wrt_eqmod` [⌜9⌝;⌜n rem 9⌝;⌜n⌝;⌜3⌝]⋅ THENA Auto)
   THEN (RWO "-1<" 0 THENA Auto)) }

1
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)

---

Latex:

---

Latex:
\mforall{}n:\mBbbZ{}.  ((n\^{}3  \mequiv{}  0  mod  9)  \mvee{}  (n\^{}3  \mequiv{}  1  mod  9)  \mvee{}  (n\^{}3  \mequiv{}  (-1)  mod  9))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma  `rem-eqmod`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}9\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `exp\_functionality\_wrt\_eqmod`  [\mkleeneopen{}9\mkleeneclose{};\mkleeneopen{}n  rem  9\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}3\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1<"  0  THENA  Auto))

---

Home Index