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

Metamath Proof Explorer

Theorem archiexdiv

Description: In an Archimedean group, given two positive elements, there exists a "divisor" n . (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses archiexdiv.b 
|- B = ( Base ` W )
archiexdiv.0 
|- .0. = ( 0g ` W )
archiexdiv.i 
|- .< = ( lt ` W )
archiexdiv.x 
|- .x. = ( .g ` W )
Assertion archiexdiv 
|- ( ( ( W e. oGrp /\ W e. Archi ) /\ ( X e. B /\ Y e. B ) /\ .0. .< X ) -> E. n e. NN Y .< ( n .x. X ) )

Proof

Step Hyp Ref Expression
1 archiexdiv.b 
 |-  B = ( Base ` W )
2 archiexdiv.0 
 |-  .0. = ( 0g ` W )
3 archiexdiv.i 
 |-  .< = ( lt ` W )
4 archiexdiv.x 
 |-  .x. = ( .g ` W )
5 1 2 3 4 isarchi3 
 |-  ( W e. oGrp -> ( W e. Archi <-> A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y .< ( n .x. x ) ) ) )
6 5 biimpa 
 |-  ( ( W e. oGrp /\ W e. Archi ) -> A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y .< ( n .x. x ) ) )
7 6 3ad2ant1 
 |-  ( ( ( W e. oGrp /\ W e. Archi ) /\ ( X e. B /\ Y e. B ) /\ .0. .< X ) -> A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y .< ( n .x. x ) ) )
8 simp3 
 |-  ( ( ( W e. oGrp /\ W e. Archi ) /\ ( X e. B /\ Y e. B ) /\ .0. .< X ) -> .0. .< X )
9 breq2 
 |-  ( x = X -> ( .0. .< x <-> .0. .< X ) )
10 oveq2 
 |-  ( x = X -> ( n .x. x ) = ( n .x. X ) )
11 10 breq2d 
 |-  ( x = X -> ( y .< ( n .x. x ) <-> y .< ( n .x. X ) ) )
12 11 rexbidv 
 |-  ( x = X -> ( E. n e. NN y .< ( n .x. x ) <-> E. n e. NN y .< ( n .x. X ) ) )
13 9 12 imbi12d 
 |-  ( x = X -> ( ( .0. .< x -> E. n e. NN y .< ( n .x. x ) ) <-> ( .0. .< X -> E. n e. NN y .< ( n .x. X ) ) ) )
14 breq1 
 |-  ( y = Y -> ( y .< ( n .x. X ) <-> Y .< ( n .x. X ) ) )
15 14 rexbidv 
 |-  ( y = Y -> ( E. n e. NN y .< ( n .x. X ) <-> E. n e. NN Y .< ( n .x. X ) ) )
16 15 imbi2d 
 |-  ( y = Y -> ( ( .0. .< X -> E. n e. NN y .< ( n .x. X ) ) <-> ( .0. .< X -> E. n e. NN Y .< ( n .x. X ) ) ) )
17 13 16 rspc2v 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y .< ( n .x. x ) ) -> ( .0. .< X -> E. n e. NN Y .< ( n .x. X ) ) ) )
18 17 3ad2ant2 
 |-  ( ( ( W e. oGrp /\ W e. Archi ) /\ ( X e. B /\ Y e. B ) /\ .0. .< X ) -> ( A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y .< ( n .x. x ) ) -> ( .0. .< X -> E. n e. NN Y .< ( n .x. X ) ) ) )
19 7 8 18 mp2d 
 |-  ( ( ( W e. oGrp /\ W e. Archi ) /\ ( X e. B /\ Y e. B ) /\ .0. .< X ) -> E. n e. NN Y .< ( n .x. X ) )