Are there any statements considered a proof for any of these conditional statements?

Question

The following conditional statements are some of building blocks of a proof I've written: $$\forall\alpha,A\in\mathbb Z^*,\forall B\in\mathbb Z^+\left(\frac{A}{GCD\left(A,B\right)}=\alpha\rightarrow A=\alpha\times{GCD\left(A,B\right)}\right)$$

$$\forall A,E\in\mathbb Z^*,\forall B,F\in\mathbb Z^+\left(\frac{E}{F}\times\frac{A}{B}=\frac{E\times A}{F\times B}\rightarrow\forall\alpha\in\mathbb Z^*,\forall\beta\in\mathbb Z^+\left(\left(A=\alpha\times GCD\left(A,B\right)\wedge B=\beta\times GCD\left(A,B\right)\right)\rightarrow \frac{E}{F}\times\frac{A}{B}=\frac{E\times\alpha\times GCD\left(A,B\right)}{B\times\beta\times GCD\left(A,B\right)}\right)\right)$$

$$\forall\alpha,A,E\in\mathbb Z^*,\forall\beta,B,F\in\mathbb Z^+\left(\frac{E}{F}\times\frac{A}{B}=\frac{E\times\alpha\times{GCD\left(A,B\right)}}{F\times\beta\times{GCD\left(A,B\right)}}=\frac{E\times\alpha}{F\times\beta}\rightarrow\frac{E}{F}\times\frac{A}{B}=\frac{E\times\alpha}{F\times\beta}\right)$$

$$\forall\alpha,A,C,E\in\mathbb Z^*,\forall\beta,B,D,F\in\mathbb Z^+\left(\frac{E}{F}\times\frac{A}{B}=\frac{E\times\alpha}{F\times\beta}=\frac{E}{F}\times\frac{C}{D}\rightarrow\frac{E}{F}\times\frac{A}{B}=\frac{E}{F}\times\frac{C}{D}\right)$$ Now I need to make sure that none of these statements need to be proved(which seems to me they don't need to), or more accurately there are no statements that can be provided as a proof for any of these, so any tip is appreciated.

Answer 1

For the first one, you would need an axiom that relates division and multiplication, because such mathematical operators are not built into logic. So, for example, you could use as an axiom:

$$\forall z \in \mathbb Z^* \forall x,y \in \mathbb Z^+ (\frac{x}{z}=y \leftrightarrow x = y \times z)$$

Also, you need to rewrite an expression like $x=y=z$ (like you have in the third and fourth statements) using a conjunction: $x = y \land y = z$.

Otherwise, the last three statements can all be proven using pure logic ... and with that additional axiom, the first statement can be proven as well ... and the crucial logical inference in all cases is $= Elim$, which states that for any terms $t_1$ and $t_2$, and any formula $\varphi(x)$: if you have a statement $\varphi(t_1)$, as well as a statement $t_1 = t_2$, then you can infer statement $\varphi(t_2)$, where $\varphi(t_2)$ is the result of replacing some or all occurrences of $t_1$ in $\varphi(t_1)$ with $t_2$.

Below, for example, would be the formal proof for the last statement:

1. Assume $$\alpha,A,C,E\in\mathbb Z^*,\beta,B,D,F\in\mathbb Z^+$$

2. Assume $$\frac{E}{F}\times\frac{A}{B}=\frac{E\times\alpha}{F\times\beta} \land \frac{E\times\alpha}{F\times\beta}=\frac{E}{F}\times\frac{C}{D}$$

3.$$\frac{E}{F}\times\frac{A}{B}=\frac{E\times\alpha}{F\times\beta} \qquad(\land \: Elim \: 2) $$

4. $$\frac{E\times\alpha}{F\times\beta}=\frac{E}{F}\times\frac{C}{D}\qquad(\land \: Elim \: 2) $$

5. $$\frac{E}{F}\times\frac{A}{B}=\frac{E}{F}\times\frac{C}{D} \qquad(= \: Elim \: 3,4) $$

6. $$\left(\frac{E}{F}\times\frac{A}{B}=\frac{E\times\alpha}{F\times\beta} \land \frac{E\times\alpha}{F\times\beta}=\frac{E}{F}\times\frac{C}{D}\right)\rightarrow\frac{E}{F}\times\frac{A}{B}=\frac{E}{F}\times\frac{C}{D}\qquad(\rightarrow \: Intro \: 2-5) $$

7. $$\forall\alpha,A,C,E\in\mathbb Z^*,\forall\beta,B,D,F\in\mathbb Z^+\left(\left(\frac{E}{F}\times\frac{A}{B}=\frac{E\times\alpha}{F\times\beta} \land \frac{E\times\alpha}{F\times\beta}=\frac{E}{F}\times\frac{C}{D}\right)\rightarrow\frac{E}{F}\times\frac{A}{B}=\frac{E}{F}\times\frac{C}{D}\right)\qquad(\forall \: Intro \: 1-6) $$