Is this a perfectly rigorous proof for "if and only if"? Any missing bits to achieve perfect rigor?

Note: my goal is maximum mathematical rigor.

The toy problem here is (from [{Spivak's Calculus book}'s 1st chapter]'s problems):

• Prove that, if $$b,d\ne 0$$, then $$\frac{a}{b} = \frac{c}{d}$$ if and only if $$ad = bc$$.
• Allowed axioms are only: additive association/inverse/identity, multiplicative association/inverse/identity, and distributive property of addition and multiplication.

Now, what puzzles me is: how would my proof be different if there was no "if and only if" phrase?

Below is my proving attempt:

First let's rewrite the problem in a language closer to the axioms:

• Prove $$ab^{-1} = cd^{-1}$$ if and only if $$ad = bc$$ (of course, $$b,d\ne 0$$).

Proof--- By multiplying both sides by $$bd$$:

$$ab^{-1}bd = cd^{-1}bd$$

By [axiom mul assotition]

$$a(b^{-1}b)d = c(d^{-1}d)b$$

By [axiom mul inverse]:

$$a(1)d = c(1)b$$

By [axiom mul identity]:

$$ad = cb$$

$$\blacksquare$$

My questions

Is my proof above adequate to show "if" (way forward) and "and only if" (way back) properties?

If maximum rigor is to sought for my proof, should I add any extra wordings there to signify that my proof is actually proving the "iff" (both ways) and not only "if" (forward)? E.g. should I reverse the proof backwards to show that it's both ways?

Your proof assumes, from the start, that, given three real numbers $$a$$, $$b$$, and $$c$$, with $$c\neq0$$,$$a=b\iff ac=bc.$$Perhaps that you could prove it.
Besides, after multiplying both sides by $$bd$$, what you should get is $$(ab^{-1})(bd)=(cd^{-1})(bd)$$. Only then can you use associativity to prove what you want to prove. And note that you have used the commutativity of the multiplication, when you went from $$cd^{-1}bd$$ to $$c(d^{-1}d)b$$ .
• At the first step, when you claim that $ab^{-1}=cd^{-1}\iff ab^{-1}bd=cd^{-1}bd$. May 19 '19 at 22:00
• Almost. You should prove that $a=b\iff ac=bc$. May 21 '19 at 13:50
• Substituting $a$ into $b$ only proves that $a=b\implies ac=bc$. In order to prove that $ac=bc\implies a=b$, you should do$$ac=bc\implies(ac)c^{-1}=(bc)c^{-1}\iff a(cc^{-1})=b(cc^{-1})\iff a=b.$$ May 21 '19 at 14:16