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 
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A = B <-> A. x e. NN0 ( A || x <-> B || x ) ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( A = B -> ( A || x <-> B || x ) )
2 1 ralrimivw 
 |-  ( A = B -> A. x e. NN0 ( A || x <-> B || x ) )
3 simpll 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ A. x e. NN0 ( A || x <-> B || x ) ) -> A e. NN0 )
4 simplr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ A. x e. NN0 ( A || x <-> B || x ) ) -> B e. NN0 )
5 nn0z 
 |-  ( B e. NN0 -> B e. ZZ )
6 iddvds 
 |-  ( B e. ZZ -> B || B )
7 5 6 syl 
 |-  ( B e. NN0 -> B || B )
8 7 ad2antlr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ A. x e. NN0 ( A || x <-> B || x ) ) -> B || B )
9 breq2 
 |-  ( x = B -> ( A || x <-> A || B ) )
10 breq2 
 |-  ( x = B -> ( B || x <-> B || B ) )
11 9 10 bibi12d 
 |-  ( x = B -> ( ( A || x <-> B || x ) <-> ( A || B <-> B || B ) ) )
12 11 rspcva 
 |-  ( ( B e. NN0 /\ A. x e. NN0 ( A || x <-> B || x ) ) -> ( A || B <-> B || B ) )
13 12 adantll 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ A. x e. NN0 ( A || x <-> B || x ) ) -> ( A || B <-> B || B ) )
14 8 13 mpbird 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ A. x e. NN0 ( A || x <-> B || x ) ) -> A || B )
15 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
16 iddvds 
 |-  ( A e. ZZ -> A || A )
17 15 16 syl 
 |-  ( A e. NN0 -> A || A )
18 17 ad2antrr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ A. x e. NN0 ( A || x <-> B || x ) ) -> A || A )
19 breq2 
 |-  ( x = A -> ( A || x <-> A || A ) )
20 breq2 
 |-  ( x = A -> ( B || x <-> B || A ) )
21 19 20 bibi12d 
 |-  ( x = A -> ( ( A || x <-> B || x ) <-> ( A || A <-> B || A ) ) )
22 21 rspcva 
 |-  ( ( A e. NN0 /\ A. x e. NN0 ( A || x <-> B || x ) ) -> ( A || A <-> B || A ) )
23 22 adantlr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ A. x e. NN0 ( A || x <-> B || x ) ) -> ( A || A <-> B || A ) )
24 18 23 mpbid 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ A. x e. NN0 ( A || x <-> B || x ) ) -> B || A )
25 dvdseq 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( A || B /\ B || A ) ) -> A = B )
26 3 4 14 24 25 syl22anc 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ A. x e. NN0 ( A || x <-> B || x ) ) -> A = B )
27 26 ex 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A. x e. NN0 ( A || x <-> B || x ) -> A = B ) )
28 2 27 impbid2 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A = B <-> A. x e. NN0 ( A || x <-> B || x ) ) )