Theorem dvdsext

Description: Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Assertion	dvdsext	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(A=B\leftrightarrow \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢A=B\to \left(A\parallel x\leftrightarrow B\parallel x\right)$$
2	1	ralrimivw	$$⊢A=B\to \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)$$
3		simpll	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)\to A\in {\mathbb{N}}_0$$
4		simplr	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)\to B\in {\mathbb{N}}_0$$
5		nn0z	$$⊢B\in {\mathbb{N}}_0\to B\in \mathbb{Z}$$
6		iddvds	$$⊢B\in \mathbb{Z}\to B\parallel B$$
7	5 6	syl	$$⊢B\in {\mathbb{N}}_0\to B\parallel B$$
8	7	ad2antlr	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)\to B\parallel B$$
9		breq2	$$⊢x=B\to \left(A\parallel x\leftrightarrow A\parallel B\right)$$
10		breq2	$$⊢x=B\to \left(B\parallel x\leftrightarrow B\parallel B\right)$$
11	9 10	bibi12d	$$⊢x=B\to \left(\left(A\parallel x\leftrightarrow B\parallel x\right)\leftrightarrow \left(A\parallel B\leftrightarrow B\parallel B\right)\right)$$
12	11	rspcva	$$⊢\left(B\in {\mathbb{N}}_0\wedge \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)\to \left(A\parallel B\leftrightarrow B\parallel B\right)$$
13	12	adantll	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)\to \left(A\parallel B\leftrightarrow B\parallel B\right)$$
14	8 13	mpbird	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)\to A\parallel B$$
15		nn0z	$$⊢A\in {\mathbb{N}}_0\to A\in \mathbb{Z}$$
16		iddvds	$$⊢A\in \mathbb{Z}\to A\parallel A$$
17	15 16	syl	$$⊢A\in {\mathbb{N}}_0\to A\parallel A$$
18	17	ad2antrr	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)\to A\parallel A$$
19		breq2	$$⊢x=A\to \left(A\parallel x\leftrightarrow A\parallel A\right)$$
20		breq2	$$⊢x=A\to \left(B\parallel x\leftrightarrow B\parallel A\right)$$
21	19 20	bibi12d	$$⊢x=A\to \left(\left(A\parallel x\leftrightarrow B\parallel x\right)\leftrightarrow \left(A\parallel A\leftrightarrow B\parallel A\right)\right)$$
22	21	rspcva	$$⊢\left(A\in {\mathbb{N}}_0\wedge \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)\to \left(A\parallel A\leftrightarrow B\parallel A\right)$$
23	22	adantlr	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)\to \left(A\parallel A\leftrightarrow B\parallel A\right)$$
24	18 23	mpbid	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)\to B\parallel A$$
25		dvdseq	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge \left(A\parallel B\wedge B\parallel A\right)\right)\to A=B$$
26	3 4 14 24 25	syl22anc	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)\to A=B$$
27	26	ex	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(\forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\to A=B\right)$$
28	2 27	impbid2	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(A=B\leftrightarrow \forall x\in {\mathbb{N}}_0\left(A\parallel x\leftrightarrow B\parallel x\right)\right)$$