This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥 ) ) )