---

Step * 1 1 of Lemma cube-mod-9


1. r : {-8..9-}
⊢ (r^3 ≡ 0 mod 9) ∨ (r^3 ≡ 1 mod 9) ∨ (r^3 ≡ (-1) mod 9)
BY
{ ((RWO "modulus-equal-iff-eqmod<" 0 THENA Auto)
   THEN (Subst' 0 mod 9 ~ 0 0 THENA Computation)
   THEN (Subst' 1 mod 9 ~ 1 0 THENA Computation)
   THEN (Subst' (-1) mod 9 ~ 8 0 THENA Computation)) }

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

---

Latex:

---

Latex:

1.  r  :  \{-8..9\msupminus{}\}
\mvdash{}  (r\^{}3  \mequiv{}  0  mod  9)  \mvee{}  (r\^{}3  \mequiv{}  1  mod  9)  \mvee{}  (r\^{}3  \mequiv{}  (-1)  mod  9)


By

---

Latex:
((RWO  "modulus-equal-iff-eqmod<"  0  THENA  Auto)
  THEN  (Subst'  0  mod  9  \msim{}  0  0  THENA  Computation)
  THEN  (Subst'  1  mod  9  \msim{}  1  0  THENA  Computation)
  THEN  (Subst'  (-1)  mod  9  \msim{}  8  0  THENA  Computation))

---

Home Index