param (PROP prop.ghi () "") param (PREDICATE predicate_eq.ghi (PROP) "") param (NATURALS ../naturals/common.ghi (PROP PREDICATE) "") param (NEGATIVE negative.ghi (PROP PREDICATE NATURALS) "") tvar (wff ph ps ch th ta) tvar (nat A B C D) var (nat x) term (nat (/ A B)) ## redirect division_min.ghi stmt (diveq12 () () (-> (/\ (= A B) (= C D)) (= (/ A C) (/ B D)))) stmt (divcan () () (-> (-. (= B (0))) (= (* B (/ A B)) A))) ## redirect division.gh ## Divide a number on both sides of an equation ## ## (-> (= A B) (= (/ A C) (/ B C))) ##
stmt (diveq1 () () (-> (= A B) (= (/ A C) (/ B C)))) ## Divide a number on both sides ## ## (= A ] ] [ B ] ) ## (= (/ A ] C) ] (/ [ B ] C)) ##
stmt (diveq1i () ((= A B)) (= (/ A C) (/ B C))) ## Equality over Division stmt (diveq1d () ((-> ph (= A B))) (-> ph (= (/ A C) (/ B C)))) ## Divide a number on both sides of an equation stmt (diveq2 () () (-> (= A B) (= (/ C A) (/ C B)))) ## Divide a number on both sides ## ## (= [ A ] [ [ B ) ## (= (/ C [ A ] ) [ (/ C [ B)) ##
stmt (diveq2i () ((= A B)) (= (/ C A) (/ C B))) ## Equality over Division stmt (diveq2d () ((-> ph (= A B))) (-> ph (= (/ C A) (/ C B)))) ## Equality over Division ## ## (= A ] ] ] [ B ] ] ) ## (= [ [ C ] [ [ [ D) ## (= (/ A ] [ C ] ) (/ [ B ] [ D)) ##
stmt (diveq12i () ((= A B) (= C D)) (= (/ A C) (/ B D))) ## Equality over Division stmt (diveq12d () ((-> ph (= A B)) (-> ph (= C D))) (-> ph (= (/ A C) (/ B D)))) ## Cancel with Division stmt (divcani () ((-. (= A (0)))) (= (* A (/ B A)) B)) ## Cancel with Division stmt (reciprocalcan () () (-> (-. (= A (0))) (= (* A (/ (1) A)) (1)))) ## Cancel with Division stmt (reciprocalcani () ((-. (= A (0)))) (= (* A (/ (1) A)) (1))) ## Cancel With Division stmt (divcan2 () () (-> (-. (= A (0))) (= (/ (* A B) A) B))) ## Cancel with Division ## ## (-. (= A (0))) ## (= (/ (* A B) A) B) ##
stmt (divcan2i () ((-. (= A (0)))) (= (/ (* A B) A) B)) ## Cancel with Division stmt (divcan3 () () (-> (-. (= A (0))) (= (/ (* B A) A) B))) ## 0 divided by anything is 0 stmt (0div () () (-> (-. (= A (0))) (= (/ (0) A) (0)))) ## 0 divided by anything is 0 stmt (0divi () ((-. (= A (0)))) (= (/ (0) A) (0))) ## Divide by 1 stmt (divid () () (= (/ A (1)) A)) ## Expand Fraction stmt (expandFrac () () (-> (-. (= B (0))) (= (/ A B) (* A (/ (1) B))))) ## Expand Fraction stmt (expandFraci () ((-. (= B (0)))) (= (/ A B) (* A (/ (1) B)))) ## Cancel using Division stmt (frac1 () () (-> (-. (= A (0))) (= (/ A A) (1)))) ## Cancel using Division stmt (frac1i () ((-. (= A (0)))) (= (/ A A) (1))) ## Division & Multiplication Ass. stmt (divmulass () () (-> (-. (= C (0))) (= (* A (/ B C)) (/ (* A B) C)))) ## Division & Multiplication Ass. stmt (divmulassi () ((-. (= C (0)))) (= (* A (/ B C)) (/ (* A B) C))) ## Division & Multiplication Ass. stmt (divmulass2i () ((-. (= C (0)))) (= (* (/ B C) A) (/ (* B A) C))) ## Zero Product Property ## ## (-. (= A ] ] ] (0))) ## (-. (= [ [ B ] (0))) ## (-. (= (* A ] [ B ] ) (0))) ##
stmt (zeroProducti () ((-. (= A (0))) (-. (= B (0)))) (-. (= (* A B) (0)))) ## Multiply Fractions stmt (fracmul () () (-> (/\ (-. (= B (0))) (-. (= D (0)))) (= (* (/ A B) (/ C D)) (/ (* A C) (* B D))))) ## Multiply Fractions stmt (fracmuli () ((-. (= B (0))) (-. (= D (0)))) (= (* (/ A B) (/ C D)) (/ (* A C) (* B D)))) ## Fraction with common factor ## Numerators and Denominators with common factors can be simplified. stmt (fracFactors () () (-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ (* A C) (* B C)) (/ A B)))) ## Fraction with common factor ## Numerators and Denominators with common factors can be simplified. ## ## (-. (= B (0)) ## (-. (= C (0))) ## (= (/ (* A C) (* B C)) (/ A B)) ##
stmt (fracFactorsi () ((-. (= B (0))) (-. (= C (0)))) (= (/ (* A C) (* B C)) (/ A B))) ## Distribute Division over Addition stmt (divdistr () () (-> (-. (= C (0))) (= (+ (/ A C) (/ B C)) (/ (+ A B) C)))) ## Distribute Division over Addition stmt (divdistri () ((-. (= C (0)))) (= (+ (/ A C) (/ B C)) (/ (+ A B) C))) ## Add Fractions stmt (addfrac () () (-> (/\ (-. (= B (0))) (-. (= D (0)))) (= (+ (/ A B) (/ C D)) (/ (+ (* A D) (* B C)) (* B D))))) ## Add Fractions stmt (addfraci () ((-. (= B (0))) (-. (= D (0)))) (= (+ (/ A B) (/ C D)) (/ (+ (* A D) (* B C)) (* B D)))) ## Negative Numerator ## A negative numerator is equivalent to a negative fraction. stmt (negNumerator () () (-> (-. (= B (0))) (= (/ (-n A) B) (-n (/ A B))))) ## Negative Numerator stmt (negNumeratori () ((-. (= B (0)))) (= (/ (-n A) B) (-n (/ A B)))) ## Negative Denominator stmt (negDenominatori () ((-. (= B (0)))) (= (/ A (-n B)) (-n (/ A B)))) stmt (negDenominator () () (-> (-. (= B (0))) (= (-n (/ A B)) (/ A (-n B))))) ## Double Negative Fraction stmt (doublenegfrac () () (-> (-. (= B (0))) (= (/ (-n A) (-n B)) (/ A B)))) ## Double Negative Fraction stmt (doublenegfraci () ((-. (= B (0)))) (= (/ (-n A) (-n B)) (/ A B))) ## Common Division in Fraction stmt (fracFactors2 () () (-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ (/ A C) (/ B C)) (/ A B)))) ## Common Division in Fraction stmt (fracFactors2i () ((-. (= B (0))) (-. (= C (0)))) (= (/ (/ A C) (/ B C)) (/ A B))) ## Commute Division stmt (divcom () () (-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ (/ A B) C) (/ (/ A C) B)))) ## Distribute Division Over Subtraction stmt (divminusdistr () () (-> (-. (= C (0))) (= (- (/ A C) (/ B C)) (/ (- A B) C)))) ## Distribute Division Over Subtraction stmt (divminusdistri () ((-. (= C (0)))) (= (- (/ A C) (/ B C)) (/ (- A B) C))) ## Multiply Two Denominators stmt (doublediv () () (-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ (/ A B) C) (/ A (* B C))))) ## Multiply Two Denominators stmt (doubledivi () ((-. (= B (0))) (-. (= C (0)))) (= (/ (/ A B) C) (/ A (* B C)))) ## A positive number has a positive reciprocal stmt (posReciprocal () () (-> (> A (0)) (> (/ (1) A) (0)))) stmt (posReciprocal2 () () (-> (-. (= A (0))) (<-> (> A (0)) (> (/ (1) A) (0))))) ## A number is its reciprocal's reciprocal stmt (doubleReciprocal () () (-> (-. (= A (0))) (= (/ (1) (/ (1) A)) A))) stmt (divDouble () () (-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ A (/ B C)) (/ (* A C) B)))) stmt (divNotZeroi () ((-. (= A (0))) (-. (= B (0)))) (-. (= (/ A B) (0)))) stmt (divNotZero () () (-> (/\ (-. (= A (0))) (-. (= B (0)))) (-. (= (/ A B) (0)))))