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