replacing variables in a conditional statement by functions

Question

Considering following conditional statement as an example: $$\forall A,C,E\in\mathbb Z^*,\forall B,D,F\in\mathbb Z^+\left(\frac{A}{B}=\frac{C}{D}\rightarrow\frac{E}{F}\times\frac{A}{B}=\frac{E}{F}\times\frac{C}{D}\right)$$ I want to prove that a statement like below which states you can replace variables of above statement by functions is true: $$\left(\forall x\in\mathbb Z^*,\forall y\in\mathbb Z^+\left(\frac{x}{GCD\left(x,y\right)}\in\mathbb Z^*\right)\wedge\forall g,i\in\mathbb Z^+,\forall h\in\mathbb Z^*\left(\frac{g\times i}{GCD\left(g,h\right)\times GCD\left(h,i\right)}\in\mathbb Z^+\right)\wedge\forall A,C,E\in\mathbb Z^*,\forall B,D,F\in\mathbb Z^+\left(\frac{A}{B}=\frac{C}{D}\rightarrow\frac{E}{F}\times\frac{A}{B}=\frac{E}{F}\times\frac{C}{D}\right)\right)\rightarrow\forall x,A,C,h\in\mathbb Z^*,\forall y,B,D,g,i\in\mathbb Z^+\left(\frac{A}{B}=\frac{C}{D}\rightarrow\frac{\frac{x}{GCD\left(x,y\right)}}{\frac{g\times i}{GCD\left(g,h\right)\times GCD\left(h,i\right)}}\times\frac{A}{B}=\frac{\frac{x}{GCD\left(x,y\right)}}{\frac{g\times i}{GCD\left(g,h\right)\times GCD\left(h,i\right)}}\times\frac{C}{D}\right)$$ Now any tip on how I should approach this is greatly appreciated.

Answer 1

You don't need to do any special work, since the $=$ rules in logic take care of all this automatically.

For example, $= Intro$ is defined as follows:

$t=t$ with $t$ any term. Thus, the following are all good applications of this rule:

I.

$a=a$ ('typical' use of $= Intro$)

II.

$a * b = a * b$ (you can use complex terms as well)

Likewise, $=Elim$ is defined as follows:

$\varphi(t_1)$

$t_1 = t_2$

$\therefore \varphi(t_2)$ where $\varphi(t_2)$ is the result of substituting some or all of the terms $t_1$ occurring in $\varphi(t_1)$ with $t_2$

Thus, below are some perfectly acceptable applications of $= Elim$:

III.

$P(a)$

$a=b$

$\therefore P(b)$ ('typical'use of $= Elim$)

IV.

$P(a,a)$

$a = b$

$\therefore P(a,b)$ (you don't have to replace all $a$'s with $b$'s)

V.

$P(a*b)$

$a * b = c * d$

$\therefore P(c*d)$ (you can substitute complex terms involving functions)

So, your statement is easily provable using this rule, since the consequent is already a logical necessity:

1. $$\frac{A}{B} = \frac{C}{D} \qquad Assumption$$

2. $$\frac{\frac{x}{GCD\left(x,y\right)}}{\frac{g\times i}{GCD\left(g,h\right)\times GCD\left(h,i\right)}}\times\frac{A}{B}=\frac{\frac{x}{GCD\left(x,y\right)}}{\frac{g\times i}{GCD\left(g,h\right)\times GCD\left(h,i\right)}}\times\frac{A}{B} \qquad = Intro$$

3.$$\frac{\frac{x}{GCD\left(x,y\right)}}{\frac{g\times i}{GCD\left(g,h\right)\times GCD\left(h,i\right)}}\times\frac{A}{B}=\frac{\frac{x}{GCD\left(x,y\right)}}{\frac{g\times i}{GCD\left(g,h\right)\times GCD\left(h,i\right)}}\times\frac{C}{B} \qquad = Elim \: 1,2$$

4. $$\frac{A}{B}=\frac{C}{D}\rightarrow\frac{\frac{x}{GCD\left(x,y\right)}}{\frac{g\times i}{GCD\left(g,h\right)\times GCD\left(h,i\right)}}\times\frac{A}{B}=\frac{\frac{x}{GCD\left(x,y\right)}}{\frac{g\times i}{GCD\left(g,h\right)\times GCD\left(h,i\right)}}\times\frac{C}{D} \qquad \rightarrow Intro \: 1-3$$