Theorem dvdsext

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

	Ref	Expression
Assertion	dvdsext	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) )
2	1	ralrimivw	⊢ ( 𝐴 = 𝐵 → ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) )
3		simpll	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) → 𝐴 ∈ ℕ0 )
4		simplr	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) → 𝐵 ∈ ℕ0 )
5		nn0z	⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℤ )
6		iddvds	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∥ 𝐵 )
7	5 6	syl	⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∥ 𝐵 )
8	7	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) → 𝐵 ∥ 𝐵 )
9		breq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∥ 𝑥 ↔ 𝐴 ∥ 𝐵 ) )
10		breq2	⊢ ( 𝑥 = 𝐵 → ( 𝐵 ∥ 𝑥 ↔ 𝐵 ∥ 𝐵 ) )
11	9 10	bibi12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ↔ ( 𝐴 ∥ 𝐵 ↔ 𝐵 ∥ 𝐵 ) ) )
12	11	rspcva	⊢ ( ( 𝐵 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) → ( 𝐴 ∥ 𝐵 ↔ 𝐵 ∥ 𝐵 ) )
13	12	adantll	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) → ( 𝐴 ∥ 𝐵 ↔ 𝐵 ∥ 𝐵 ) )
14	8 13	mpbird	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) → 𝐴 ∥ 𝐵 )
15		nn0z	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
16		iddvds	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∥ 𝐴 )
17	15 16	syl	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∥ 𝐴 )
18	17	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) → 𝐴 ∥ 𝐴 )
19		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝐴 ∥ 𝑥 ↔ 𝐴 ∥ 𝐴 ) )
20		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ∥ 𝑥 ↔ 𝐵 ∥ 𝐴 ) )
21	19 20	bibi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ↔ ( 𝐴 ∥ 𝐴 ↔ 𝐵 ∥ 𝐴 ) ) )
22	21	rspcva	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) → ( 𝐴 ∥ 𝐴 ↔ 𝐵 ∥ 𝐴 ) )
23	22	adantlr	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) → ( 𝐴 ∥ 𝐴 ↔ 𝐵 ∥ 𝐴 ) )
24	18 23	mpbid	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) → 𝐵 ∥ 𝐴 )
25		dvdseq	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( 𝐴 ∥ 𝐵 ∧ 𝐵 ∥ 𝐴 ) ) → 𝐴 = 𝐵 )
26	3 4 14 24 25	syl22anc	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) → 𝐴 = 𝐵 )
27	26	ex	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) → 𝐴 = 𝐵 ) )
28	2 27	impbid2	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∈ ℕ0 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) )