ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltsonq Unicode version

Theorem ltsonq 7372
Description: 'Less than' is a strict ordering on positive fractions. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 4-May-2013.)
Assertion
Ref Expression
ltsonq  |-  <Q  Or  Q.

Proof of Theorem ltsonq
Dummy variables  a  b  c  d  e  f  x  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nqqs 7322 . . . . . 6  |-  Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
2 id 19 . . . . . . . 8  |-  ( [
<. z ,  w >. ]  ~Q  =  x  ->  [ <. z ,  w >. ]  ~Q  =  x )
32, 2breq12d 4011 . . . . . . 7  |-  ( [
<. z ,  w >. ]  ~Q  =  x  -> 
( [ <. z ,  w >. ]  ~Q  <Q  [
<. z ,  w >. ]  ~Q  <->  x  <Q  x ) )
43notbid 667 . . . . . 6  |-  ( [
<. z ,  w >. ]  ~Q  =  x  -> 
( -.  [ <. z ,  w >. ]  ~Q  <Q  [ <. z ,  w >. ]  ~Q  <->  -.  x  <Q  x ) )
5 ltsopi 7294 . . . . . . . 8  |-  <N  Or  N.
6 ltrelpi 7298 . . . . . . . 8  |-  <N  C_  ( N.  X.  N. )
75, 6soirri 5015 . . . . . . 7  |-  -.  (
w  .N  z ) 
<N  ( w  .N  z
)
8 ordpipqqs 7348 . . . . . . . . 9  |-  ( ( ( z  e.  N.  /\  w  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )
)  ->  ( [ <. z ,  w >. ]  ~Q  <Q  [ <. z ,  w >. ]  ~Q  <->  ( z  .N  w )  <N  (
w  .N  z ) ) )
98anidms 397 . . . . . . . 8  |-  ( ( z  e.  N.  /\  w  e.  N. )  ->  ( [ <. z ,  w >. ]  ~Q  <Q  [
<. z ,  w >. ]  ~Q  <->  ( z  .N  w )  <N  (
w  .N  z ) ) )
10 mulcompig 7305 . . . . . . . . 9  |-  ( ( z  e.  N.  /\  w  e.  N. )  ->  ( z  .N  w
)  =  ( w  .N  z ) )
1110breq1d 4008 . . . . . . . 8  |-  ( ( z  e.  N.  /\  w  e.  N. )  ->  ( ( z  .N  w )  <N  (
w  .N  z )  <-> 
( w  .N  z
)  <N  ( w  .N  z ) ) )
129, 11bitrd 188 . . . . . . 7  |-  ( ( z  e.  N.  /\  w  e.  N. )  ->  ( [ <. z ,  w >. ]  ~Q  <Q  [
<. z ,  w >. ]  ~Q  <->  ( w  .N  z )  <N  (
w  .N  z ) ) )
137, 12mtbiri 675 . . . . . 6  |-  ( ( z  e.  N.  /\  w  e.  N. )  ->  -.  [ <. z ,  w >. ]  ~Q  <Q  [
<. z ,  w >. ]  ~Q  )
141, 4, 13ecoptocl 6612 . . . . 5  |-  ( x  e.  Q.  ->  -.  x  <Q  x )
1514adantl 277 . . . 4  |-  ( ( T.  /\  x  e. 
Q. )  ->  -.  x  <Q  x )
16 breq1 4001 . . . . . . . 8  |-  ( [
<. a ,  b >. ]  ~Q  =  x  -> 
( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d
>. ]  ~Q  <->  x  <Q  [
<. c ,  d >. ]  ~Q  ) )
1716anbi1d 465 . . . . . . 7  |-  ( [
<. a ,  b >. ]  ~Q  =  x  -> 
( ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d
>. ]  ~Q  /\  [ <. c ,  d >. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) 
<->  ( x  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) ) )
18 breq1 4001 . . . . . . 7  |-  ( [
<. a ,  b >. ]  ~Q  =  x  -> 
( [ <. a ,  b >. ]  ~Q  <Q  [ <. e ,  f
>. ]  ~Q  <->  x  <Q  [
<. e ,  f >. ]  ~Q  ) )
1917, 18imbi12d 234 . . . . . 6  |-  ( [
<. a ,  b >. ]  ~Q  =  x  -> 
( ( ( [
<. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  )  ->  [ <. a ,  b >. ]  ~Q  <Q  [ <. e ,  f
>. ]  ~Q  )  <->  ( (
x  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  )  ->  x  <Q  [ <. e ,  f >. ]  ~Q  ) ) )
20 breq2 4002 . . . . . . . 8  |-  ( [
<. c ,  d >. ]  ~Q  =  y  -> 
( x  <Q  [ <. c ,  d >. ]  ~Q  <->  x 
<Q  y ) )
21 breq1 4001 . . . . . . . 8  |-  ( [
<. c ,  d >. ]  ~Q  =  y  -> 
( [ <. c ,  d >. ]  ~Q  <Q  [ <. e ,  f
>. ]  ~Q  <->  y  <Q  [
<. e ,  f >. ]  ~Q  ) )
2220, 21anbi12d 473 . . . . . . 7  |-  ( [
<. c ,  d >. ]  ~Q  =  y  -> 
( ( x  <Q  [
<. c ,  d >. ]  ~Q  /\  [ <. c ,  d >. ]  ~Q  <Q  [ <. e ,  f
>. ]  ~Q  )  <->  ( x  <Q  y  /\  y  <Q  [ <. e ,  f
>. ]  ~Q  ) ) )
2322imbi1d 231 . . . . . 6  |-  ( [
<. c ,  d >. ]  ~Q  =  y  -> 
( ( ( x 
<Q  [ <. c ,  d
>. ]  ~Q  /\  [ <. c ,  d >. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  )  ->  x  <Q  [ <. e ,  f >. ]  ~Q  ) 
<->  ( ( x  <Q  y  /\  y  <Q  [ <. e ,  f >. ]  ~Q  )  ->  x  <Q  [ <. e ,  f >. ]  ~Q  ) ) )
24 breq2 4002 . . . . . . . 8  |-  ( [
<. e ,  f >. ]  ~Q  =  z  -> 
( y  <Q  [ <. e ,  f >. ]  ~Q  <->  y 
<Q  z ) )
2524anbi2d 464 . . . . . . 7  |-  ( [
<. e ,  f >. ]  ~Q  =  z  -> 
( ( x  <Q  y  /\  y  <Q  [ <. e ,  f >. ]  ~Q  ) 
<->  ( x  <Q  y  /\  y  <Q  z ) ) )
26 breq2 4002 . . . . . . 7  |-  ( [
<. e ,  f >. ]  ~Q  =  z  -> 
( x  <Q  [ <. e ,  f >. ]  ~Q  <->  x 
<Q  z ) )
2725, 26imbi12d 234 . . . . . 6  |-  ( [
<. e ,  f >. ]  ~Q  =  z  -> 
( ( ( x 
<Q  y  /\  y  <Q  [ <. e ,  f
>. ]  ~Q  )  ->  x  <Q  [ <. e ,  f >. ]  ~Q  ) 
<->  ( ( x  <Q  y  /\  y  <Q  z
)  ->  x  <Q  z ) ) )
28 ordpipqqs 7348 . . . . . . . . . . . . . . . 16  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )
)  ->  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  <->  ( a  .N  d ) 
<N  ( b  .N  c
) ) )
29283adant3 1017 . . . . . . . . . . . . . . 15  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  <->  ( a  .N  d ) 
<N  ( b  .N  c
) ) )
30 simp1l 1021 . . . . . . . . . . . . . . . . 17  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  a  e.  N. )
31 simp2r 1024 . . . . . . . . . . . . . . . . 17  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  d  e.  N. )
32 mulclpi 7302 . . . . . . . . . . . . . . . . 17  |-  ( ( a  e.  N.  /\  d  e.  N. )  ->  ( a  .N  d
)  e.  N. )
3330, 31, 32syl2anc 411 . . . . . . . . . . . . . . . 16  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( a  .N  d )  e.  N. )
34 simp1r 1022 . . . . . . . . . . . . . . . . 17  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  b  e.  N. )
35 simp2l 1023 . . . . . . . . . . . . . . . . 17  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  c  e.  N. )
36 mulclpi 7302 . . . . . . . . . . . . . . . . 17  |-  ( ( b  e.  N.  /\  c  e.  N. )  ->  ( b  .N  c
)  e.  N. )
3734, 35, 36syl2anc 411 . . . . . . . . . . . . . . . 16  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( b  .N  c )  e.  N. )
38 simp3r 1026 . . . . . . . . . . . . . . . . 17  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  f  e.  N. )
39 mulclpi 7302 . . . . . . . . . . . . . . . . 17  |-  ( ( c  e.  N.  /\  f  e.  N. )  ->  ( c  .N  f
)  e.  N. )
4035, 38, 39syl2anc 411 . . . . . . . . . . . . . . . 16  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( c  .N  f )  e.  N. )
41 ltmpig 7313 . . . . . . . . . . . . . . . 16  |-  ( ( ( a  .N  d
)  e.  N.  /\  ( b  .N  c
)  e.  N.  /\  ( c  .N  f
)  e.  N. )  ->  ( ( a  .N  d )  <N  (
b  .N  c )  <-> 
( ( c  .N  f )  .N  (
a  .N  d ) )  <N  ( (
c  .N  f )  .N  ( b  .N  c ) ) ) )
4233, 37, 40, 41syl3anc 1238 . . . . . . . . . . . . . . 15  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( (
a  .N  d ) 
<N  ( b  .N  c
)  <->  ( ( c  .N  f )  .N  ( a  .N  d
) )  <N  (
( c  .N  f
)  .N  ( b  .N  c ) ) ) )
4329, 42bitrd 188 . . . . . . . . . . . . . 14  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  <->  ( ( c  .N  f
)  .N  ( a  .N  d ) ) 
<N  ( ( c  .N  f )  .N  (
b  .N  c ) ) ) )
4443biimpa 296 . . . . . . . . . . . . 13  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d
>. ]  ~Q  )  -> 
( ( c  .N  f )  .N  (
a  .N  d ) )  <N  ( (
c  .N  f )  .N  ( b  .N  c ) ) )
4544adantrr 479 . . . . . . . . . . . 12  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) )  ->  (
( c  .N  f
)  .N  ( a  .N  d ) ) 
<N  ( ( c  .N  f )  .N  (
b  .N  c ) ) )
46 mulcompig 7305 . . . . . . . . . . . . . 14  |-  ( ( ( c  .N  f
)  e.  N.  /\  ( b  .N  c
)  e.  N. )  ->  ( ( c  .N  f )  .N  (
b  .N  c ) )  =  ( ( b  .N  c )  .N  ( c  .N  f ) ) )
4740, 37, 46syl2anc 411 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( (
c  .N  f )  .N  ( b  .N  c ) )  =  ( ( b  .N  c )  .N  (
c  .N  f ) ) )
4847adantr 276 . . . . . . . . . . . 12  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) )  ->  (
( c  .N  f
)  .N  ( b  .N  c ) )  =  ( ( b  .N  c )  .N  ( c  .N  f
) ) )
4945, 48breqtrd 4024 . . . . . . . . . . 11  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) )  ->  (
( c  .N  f
)  .N  ( a  .N  d ) ) 
<N  ( ( b  .N  c )  .N  (
c  .N  f ) ) )
50 ordpipqqs 7348 . . . . . . . . . . . . . . 15  |-  ( ( ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( [ <. c ,  d >. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  <->  ( c  .N  f ) 
<N  ( d  .N  e
) ) )
51503adant1 1015 . . . . . . . . . . . . . 14  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( [ <. c ,  d >. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  <->  ( c  .N  f ) 
<N  ( d  .N  e
) ) )
52 simp3l 1025 . . . . . . . . . . . . . . . 16  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  e  e.  N. )
53 mulclpi 7302 . . . . . . . . . . . . . . . 16  |-  ( ( d  e.  N.  /\  e  e.  N. )  ->  ( d  .N  e
)  e.  N. )
5431, 52, 53syl2anc 411 . . . . . . . . . . . . . . 15  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( d  .N  e )  e.  N. )
55 ltmpig 7313 . . . . . . . . . . . . . . 15  |-  ( ( ( c  .N  f
)  e.  N.  /\  ( d  .N  e
)  e.  N.  /\  ( b  .N  c
)  e.  N. )  ->  ( ( c  .N  f )  <N  (
d  .N  e )  <-> 
( ( b  .N  c )  .N  (
c  .N  f ) )  <N  ( (
b  .N  c )  .N  ( d  .N  e ) ) ) )
5640, 54, 37, 55syl3anc 1238 . . . . . . . . . . . . . 14  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( (
c  .N  f ) 
<N  ( d  .N  e
)  <->  ( ( b  .N  c )  .N  ( c  .N  f
) )  <N  (
( b  .N  c
)  .N  ( d  .N  e ) ) ) )
5751, 56bitrd 188 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( [ <. c ,  d >. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  <->  ( ( b  .N  c
)  .N  ( c  .N  f ) ) 
<N  ( ( b  .N  c )  .N  (
d  .N  e ) ) ) )
5857biimpa 296 . . . . . . . . . . . 12  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  [ <. c ,  d >. ]  ~Q  <Q  [ <. e ,  f
>. ]  ~Q  )  -> 
( ( b  .N  c )  .N  (
c  .N  f ) )  <N  ( (
b  .N  c )  .N  ( d  .N  e ) ) )
5958adantrl 478 . . . . . . . . . . 11  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) )  ->  (
( b  .N  c
)  .N  ( c  .N  f ) ) 
<N  ( ( b  .N  c )  .N  (
d  .N  e ) ) )
605, 6sotri 5016 . . . . . . . . . . 11  |-  ( ( ( ( c  .N  f )  .N  (
a  .N  d ) )  <N  ( (
b  .N  c )  .N  ( c  .N  f ) )  /\  ( ( b  .N  c )  .N  (
c  .N  f ) )  <N  ( (
b  .N  c )  .N  ( d  .N  e ) ) )  ->  ( ( c  .N  f )  .N  ( a  .N  d
) )  <N  (
( b  .N  c
)  .N  ( d  .N  e ) ) )
6149, 59, 60syl2anc 411 . . . . . . . . . 10  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) )  ->  (
( c  .N  f
)  .N  ( a  .N  d ) ) 
<N  ( ( b  .N  c )  .N  (
d  .N  e ) ) )
62 mulcompig 7305 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  N.  /\  y  e.  N. )  ->  ( x  .N  y
)  =  ( y  .N  x ) )
6362adantl 277 . . . . . . . . . . . . . 14  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( x  e.  N.  /\  y  e. 
N. ) )  -> 
( x  .N  y
)  =  ( y  .N  x ) )
64 mulasspig 7306 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  N.  /\  y  e.  N.  /\  z  e.  N. )  ->  (
( x  .N  y
)  .N  z )  =  ( x  .N  ( y  .N  z
) ) )
6564adantl 277 . . . . . . . . . . . . . 14  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( x  e.  N.  /\  y  e. 
N.  /\  z  e.  N. ) )  ->  (
( x  .N  y
)  .N  z )  =  ( x  .N  ( y  .N  z
) ) )
66 mulclpi 7302 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  N.  /\  y  e.  N. )  ->  ( x  .N  y
)  e.  N. )
6766adantl 277 . . . . . . . . . . . . . 14  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( x  e.  N.  /\  y  e. 
N. ) )  -> 
( x  .N  y
)  e.  N. )
6835, 31, 30, 63, 65, 38, 67caov411d 6050 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( (
c  .N  d )  .N  ( a  .N  f ) )  =  ( ( a  .N  d )  .N  (
c  .N  f ) ) )
6963, 33, 40caovcomd 6021 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( (
a  .N  d )  .N  ( c  .N  f ) )  =  ( ( c  .N  f )  .N  (
a  .N  d ) ) )
7068, 69eqtrd 2208 . . . . . . . . . . . 12  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( (
c  .N  d )  .N  ( a  .N  f ) )  =  ( ( c  .N  f )  .N  (
a  .N  d ) ) )
7135, 31, 34, 63, 65, 52, 67caov4d 6049 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( (
c  .N  d )  .N  ( b  .N  e ) )  =  ( ( c  .N  b )  .N  (
d  .N  e ) ) )
7263, 35, 34caovcomd 6021 . . . . . . . . . . . . . 14  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( c  .N  b )  =  ( b  .N  c ) )
7372oveq1d 5880 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( (
c  .N  b )  .N  ( d  .N  e ) )  =  ( ( b  .N  c )  .N  (
d  .N  e ) ) )
7471, 73eqtrd 2208 . . . . . . . . . . . 12  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( (
c  .N  d )  .N  ( b  .N  e ) )  =  ( ( b  .N  c )  .N  (
d  .N  e ) ) )
7570, 74breq12d 4011 . . . . . . . . . . 11  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( (
( c  .N  d
)  .N  ( a  .N  f ) ) 
<N  ( ( c  .N  d )  .N  (
b  .N  e ) )  <->  ( ( c  .N  f )  .N  ( a  .N  d
) )  <N  (
( b  .N  c
)  .N  ( d  .N  e ) ) ) )
7675adantr 276 . . . . . . . . . 10  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) )  ->  (
( ( c  .N  d )  .N  (
a  .N  f ) )  <N  ( (
c  .N  d )  .N  ( b  .N  e ) )  <->  ( (
c  .N  f )  .N  ( a  .N  d ) )  <N 
( ( b  .N  c )  .N  (
d  .N  e ) ) ) )
7761, 76mpbird 167 . . . . . . . . 9  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) )  ->  (
( c  .N  d
)  .N  ( a  .N  f ) ) 
<N  ( ( c  .N  d )  .N  (
b  .N  e ) ) )
78 mulclpi 7302 . . . . . . . . . . . 12  |-  ( ( a  e.  N.  /\  f  e.  N. )  ->  ( a  .N  f
)  e.  N. )
7930, 38, 78syl2anc 411 . . . . . . . . . . 11  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( a  .N  f )  e.  N. )
80 mulclpi 7302 . . . . . . . . . . . 12  |-  ( ( b  e.  N.  /\  e  e.  N. )  ->  ( b  .N  e
)  e.  N. )
8134, 52, 80syl2anc 411 . . . . . . . . . . 11  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( b  .N  e )  e.  N. )
82 mulclpi 7302 . . . . . . . . . . . 12  |-  ( ( c  e.  N.  /\  d  e.  N. )  ->  ( c  .N  d
)  e.  N. )
8335, 31, 82syl2anc 411 . . . . . . . . . . 11  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( c  .N  d )  e.  N. )
84 ltmpig 7313 . . . . . . . . . . 11  |-  ( ( ( a  .N  f
)  e.  N.  /\  ( b  .N  e
)  e.  N.  /\  ( c  .N  d
)  e.  N. )  ->  ( ( a  .N  f )  <N  (
b  .N  e )  <-> 
( ( c  .N  d )  .N  (
a  .N  f ) )  <N  ( (
c  .N  d )  .N  ( b  .N  e ) ) ) )
8579, 81, 83, 84syl3anc 1238 . . . . . . . . . 10  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( (
a  .N  f ) 
<N  ( b  .N  e
)  <->  ( ( c  .N  d )  .N  ( a  .N  f
) )  <N  (
( c  .N  d
)  .N  ( b  .N  e ) ) ) )
8685adantr 276 . . . . . . . . 9  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) )  ->  (
( a  .N  f
)  <N  ( b  .N  e )  <->  ( (
c  .N  d )  .N  ( a  .N  f ) )  <N 
( ( c  .N  d )  .N  (
b  .N  e ) ) ) )
8777, 86mpbird 167 . . . . . . . 8  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) )  ->  (
a  .N  f ) 
<N  ( b  .N  e
) )
88 ordpipqqs 7348 . . . . . . . . . 10  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  <->  ( a  .N  f ) 
<N  ( b  .N  e
) ) )
89883adant2 1016 . . . . . . . . 9  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  <->  ( a  .N  f ) 
<N  ( b  .N  e
) ) )
9089adantr 276 . . . . . . . 8  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) )  ->  ( [ <. a ,  b
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  <->  ( a  .N  f ) 
<N  ( b  .N  e
) ) )
9187, 90mpbird 167 . . . . . . 7  |-  ( ( ( ( a  e. 
N.  /\  b  e.  N. )  /\  (
c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  /\  ( [ <. a ,  b >. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  ) )  ->  [ <. a ,  b >. ]  ~Q  <Q  [ <. e ,  f
>. ]  ~Q  )
9291ex 115 . . . . . 6  |-  ( ( ( a  e.  N.  /\  b  e.  N. )  /\  ( c  e.  N.  /\  d  e.  N. )  /\  ( e  e.  N.  /\  f  e.  N. )
)  ->  ( ( [ <. a ,  b
>. ]  ~Q  <Q  [ <. c ,  d >. ]  ~Q  /\ 
[ <. c ,  d
>. ]  ~Q  <Q  [ <. e ,  f >. ]  ~Q  )  ->  [ <. a ,  b >. ]  ~Q  <Q  [ <. e ,  f
>. ]  ~Q  ) )
931, 19, 23, 27, 923ecoptocl 6614 . . . . 5  |-  ( ( x  e.  Q.  /\  y  e.  Q.  /\  z  e.  Q. )  ->  (
( x  <Q  y  /\  y  <Q  z )  ->  x  <Q  z
) )
9493adantl 277 . . . 4  |-  ( ( T.  /\  ( x  e.  Q.  /\  y  e.  Q.  /\  z  e. 
Q. ) )  -> 
( ( x  <Q  y  /\  y  <Q  z
)  ->  x  <Q  z ) )
9515, 94ispod 4298 . . 3  |-  ( T. 
->  <Q  Po  Q. )
96 nqtri3or 7370 . . . 4  |-  ( ( x  e.  Q.  /\  y  e.  Q. )  ->  ( x  <Q  y  \/  x  =  y  \/  y  <Q  x ) )
9796adantl 277 . . 3  |-  ( ( T.  /\  ( x  e.  Q.  /\  y  e.  Q. ) )  -> 
( x  <Q  y  \/  x  =  y  \/  y  <Q  x ) )
9895, 97issod 4313 . 2  |-  ( T. 
->  <Q  Or  Q. )
9998mptru 1362 1  |-  <Q  Or  Q.
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ w3o 977    /\ w3a 978    = wceq 1353   T. wtru 1354    e. wcel 2146   <.cop 3592   class class class wbr 3998    Or wor 4289  (class class class)co 5865   [cec 6523   N.cnpi 7246    .N cmi 7248    <N clti 7249    ~Q ceq 7253   Q.cnq 7254    <Q cltq 7259
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-coll 4113  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-iinf 4581
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-reu 2460  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-iun 3884  df-br 3999  df-opab 4060  df-mpt 4061  df-tr 4097  df-eprel 4283  df-id 4287  df-po 4290  df-iso 4291  df-iord 4360  df-on 4362  df-suc 4365  df-iom 4584  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-ov 5868  df-oprab 5869  df-mpo 5870  df-1st 6131  df-2nd 6132  df-recs 6296  df-irdg 6361  df-oadd 6411  df-omul 6412  df-er 6525  df-ec 6527  df-qs 6531  df-ni 7278  df-mi 7280  df-lti 7281  df-enq 7321  df-nqqs 7322  df-ltnqqs 7327
This theorem is referenced by:  nqtric  7373  lt2addnq  7378  lt2mulnq  7379  ltbtwnnqq  7389  prarloclemarch2  7393  genplt2i  7484  genpdisj  7497  addlocprlemgt  7508  nqprdisj  7518  nqprloc  7519  addnqprlemfl  7533  addnqprlemfu  7534  prmuloclemcalc  7539  mulnqprlemfl  7549  mulnqprlemfu  7550  distrlem4prl  7558  distrlem4pru  7559  ltsopr  7570  ltexprlemopl  7575  ltexprlemopu  7577  ltexprlemdisj  7580  ltexprlemru  7586  recexprlemlol  7600  recexprlemupu  7602  recexprlemdisj  7604  recexprlemss1l  7609  recexprlemss1u  7610  cauappcvgprlemopl  7620  cauappcvgprlemlol  7621  cauappcvgprlemupu  7623  cauappcvgprlemdisj  7625  cauappcvgprlemloc  7626  cauappcvgprlemladdfu  7628  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  caucvgprlemk  7639  caucvgprlemnkj  7640  caucvgprlemnbj  7641  caucvgprlemm  7642  caucvgprlemopl  7643  caucvgprlemlol  7644  caucvgprlemupu  7646  caucvgprlemloc  7649  caucvgprlemladdfu  7651  caucvgprprlemloccalc  7658  caucvgprprlemml  7668  caucvgprprlemopl  7671  suplocexprlemru  7693
  Copyright terms: Public domain W3C validator