Metamath Proof Explorer


Theorem dvdsext

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

Ref Expression
Assertion dvdsext A0B0A=Bx0AxBx

Proof

Step Hyp Ref Expression
1 breq1 A=BAxBx
2 1 ralrimivw A=Bx0AxBx
3 simpll A0B0x0AxBxA0
4 simplr A0B0x0AxBxB0
5 nn0z B0B
6 iddvds BBB
7 5 6 syl B0BB
8 7 ad2antlr A0B0x0AxBxBB
9 breq2 x=BAxAB
10 breq2 x=BBxBB
11 9 10 bibi12d x=BAxBxABBB
12 11 rspcva B0x0AxBxABBB
13 12 adantll A0B0x0AxBxABBB
14 8 13 mpbird A0B0x0AxBxAB
15 nn0z A0A
16 iddvds AAA
17 15 16 syl A0AA
18 17 ad2antrr A0B0x0AxBxAA
19 breq2 x=AAxAA
20 breq2 x=ABxBA
21 19 20 bibi12d x=AAxBxAABA
22 21 rspcva A0x0AxBxAABA
23 22 adantlr A0B0x0AxBxAABA
24 18 23 mpbid A0B0x0AxBxBA
25 dvdseq A0B0ABBAA=B
26 3 4 14 24 25 syl22anc A0B0x0AxBxA=B
27 26 ex A0B0x0AxBxA=B
28 2 27 impbid2 A0B0A=Bx0AxBx