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

Theorem ltanqg 6652
Description: Ordering property of addition for positive fractions. Proposition 9-2.6(ii) of [Gleason] p. 120. (Contributed by Jim Kingdon, 22-Sep-2019.)
Assertion
Ref Expression
ltanqg  |-  ( ( A  e.  Q.  /\  B  e.  Q.  /\  C  e.  Q. )  ->  ( A  <Q  B  <->  ( C  +Q  A )  <Q  ( C  +Q  B ) ) )

Proof of Theorem ltanqg
Dummy variables  x  y  z  w  v  u  f  g  h are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nqqs 6600 . 2  |-  Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
2 breq1 3796 . . 3  |-  ( [
<. x ,  y >. ]  ~Q  =  A  -> 
( [ <. x ,  y >. ]  ~Q  <Q  [ <. z ,  w >. ]  ~Q  <->  A  <Q  [
<. z ,  w >. ]  ~Q  ) )
3 oveq2 5551 . . . 4  |-  ( [
<. x ,  y >. ]  ~Q  =  A  -> 
( [ <. v ,  u >. ]  ~Q  +Q  [
<. x ,  y >. ]  ~Q  )  =  ( [ <. v ,  u >. ]  ~Q  +Q  A
) )
43breq1d 3803 . . 3  |-  ( [
<. x ,  y >. ]  ~Q  =  A  -> 
( ( [ <. v ,  u >. ]  ~Q  +Q  [ <. x ,  y
>. ]  ~Q  )  <Q 
( [ <. v ,  u >. ]  ~Q  +Q  [
<. z ,  w >. ]  ~Q  )  <->  ( [ <. v ,  u >. ]  ~Q  +Q  A ) 
<Q  ( [ <. v ,  u >. ]  ~Q  +Q  [
<. z ,  w >. ]  ~Q  ) ) )
52, 4bibi12d 233 . 2  |-  ( [
<. x ,  y >. ]  ~Q  =  A  -> 
( ( [ <. x ,  y >. ]  ~Q  <Q  [ <. z ,  w >. ]  ~Q  <->  ( [ <. v ,  u >. ]  ~Q  +Q  [ <. x ,  y >. ]  ~Q  )  <Q  ( [ <. v ,  u >. ]  ~Q  +Q  [ <. z ,  w >. ]  ~Q  ) )  <-> 
( A  <Q  [ <. z ,  w >. ]  ~Q  <->  ( [ <. v ,  u >. ]  ~Q  +Q  A
)  <Q  ( [ <. v ,  u >. ]  ~Q  +Q  [ <. z ,  w >. ]  ~Q  ) ) ) )
6 breq2 3797 . . 3  |-  ( [
<. z ,  w >. ]  ~Q  =  B  -> 
( A  <Q  [ <. z ,  w >. ]  ~Q  <->  A 
<Q  B ) )
7 oveq2 5551 . . . 4  |-  ( [
<. z ,  w >. ]  ~Q  =  B  -> 
( [ <. v ,  u >. ]  ~Q  +Q  [
<. z ,  w >. ]  ~Q  )  =  ( [ <. v ,  u >. ]  ~Q  +Q  B
) )
87breq2d 3805 . . 3  |-  ( [
<. z ,  w >. ]  ~Q  =  B  -> 
( ( [ <. v ,  u >. ]  ~Q  +Q  A )  <Q  ( [ <. v ,  u >. ]  ~Q  +Q  [ <. z ,  w >. ]  ~Q  )  <->  ( [ <. v ,  u >. ]  ~Q  +Q  A ) 
<Q  ( [ <. v ,  u >. ]  ~Q  +Q  B ) ) )
96, 8bibi12d 233 . 2  |-  ( [
<. z ,  w >. ]  ~Q  =  B  -> 
( ( A  <Q  [
<. z ,  w >. ]  ~Q  <->  ( [ <. v ,  u >. ]  ~Q  +Q  A )  <Q  ( [ <. v ,  u >. ]  ~Q  +Q  [ <. z ,  w >. ]  ~Q  ) )  <->  ( A  <Q  B  <->  ( [ <. v ,  u >. ]  ~Q  +Q  A )  <Q  ( [ <. v ,  u >. ]  ~Q  +Q  B
) ) ) )
10 oveq1 5550 . . . 4  |-  ( [
<. v ,  u >. ]  ~Q  =  C  -> 
( [ <. v ,  u >. ]  ~Q  +Q  A )  =  ( C  +Q  A ) )
11 oveq1 5550 . . . 4  |-  ( [
<. v ,  u >. ]  ~Q  =  C  -> 
( [ <. v ,  u >. ]  ~Q  +Q  B )  =  ( C  +Q  B ) )
1210, 11breq12d 3806 . . 3  |-  ( [
<. v ,  u >. ]  ~Q  =  C  -> 
( ( [ <. v ,  u >. ]  ~Q  +Q  A )  <Q  ( [ <. v ,  u >. ]  ~Q  +Q  B
)  <->  ( C  +Q  A )  <Q  ( C  +Q  B ) ) )
1312bibi2d 230 . 2  |-  ( [
<. v ,  u >. ]  ~Q  =  C  -> 
( ( A  <Q  B  <-> 
( [ <. v ,  u >. ]  ~Q  +Q  A )  <Q  ( [ <. v ,  u >. ]  ~Q  +Q  B
) )  <->  ( A  <Q  B  <->  ( C  +Q  A )  <Q  ( C  +Q  B ) ) ) )
14 addclpi 6579 . . . . . 6  |-  ( ( f  e.  N.  /\  g  e.  N. )  ->  ( f  +N  g
)  e.  N. )
1514adantl 271 . . . . 5  |-  ( ( ( ( x  e. 
N.  /\  y  e.  N. )  /\  (
z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  /\  ( f  e.  N.  /\  g  e. 
N. ) )  -> 
( f  +N  g
)  e.  N. )
16 simp3l 967 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  v  e.  N. )
17 simp1r 964 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  y  e.  N. )
18 mulclpi 6580 . . . . . 6  |-  ( ( v  e.  N.  /\  y  e.  N. )  ->  ( v  .N  y
)  e.  N. )
1916, 17, 18syl2anc 403 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( v  .N  y )  e.  N. )
20 simp3r 968 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  u  e.  N. )
21 simp1l 963 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  x  e.  N. )
22 mulclpi 6580 . . . . . 6  |-  ( ( u  e.  N.  /\  x  e.  N. )  ->  ( u  .N  x
)  e.  N. )
2320, 21, 22syl2anc 403 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( u  .N  x )  e.  N. )
2415, 19, 23caovcld 5685 . . . 4  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
v  .N  y )  +N  ( u  .N  x ) )  e. 
N. )
25 mulclpi 6580 . . . . 5  |-  ( ( u  e.  N.  /\  y  e.  N. )  ->  ( u  .N  y
)  e.  N. )
2620, 17, 25syl2anc 403 . . . 4  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( u  .N  y )  e.  N. )
27 mulclpi 6580 . . . . . . 7  |-  ( ( f  e.  N.  /\  g  e.  N. )  ->  ( f  .N  g
)  e.  N. )
2827adantl 271 . . . . . 6  |-  ( ( ( ( x  e. 
N.  /\  y  e.  N. )  /\  (
z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  /\  ( f  e.  N.  /\  g  e. 
N. ) )  -> 
( f  .N  g
)  e.  N. )
29 simp2r 966 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  w  e.  N. )
3028, 16, 29caovcld 5685 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( v  .N  w )  e.  N. )
31 simp2l 965 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  z  e.  N. )
32 mulclpi 6580 . . . . . 6  |-  ( ( u  e.  N.  /\  z  e.  N. )  ->  ( u  .N  z
)  e.  N. )
3320, 31, 32syl2anc 403 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( u  .N  z )  e.  N. )
3415, 30, 33caovcld 5685 . . . 4  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
v  .N  w )  +N  ( u  .N  z ) )  e. 
N. )
35 mulclpi 6580 . . . . 5  |-  ( ( u  e.  N.  /\  w  e.  N. )  ->  ( u  .N  w
)  e.  N. )
3620, 29, 35syl2anc 403 . . . 4  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( u  .N  w )  e.  N. )
37 ordpipqqs 6626 . . . 4  |-  ( ( ( ( ( v  .N  y )  +N  ( u  .N  x
) )  e.  N.  /\  ( u  .N  y
)  e.  N. )  /\  ( ( ( v  .N  w )  +N  ( u  .N  z
) )  e.  N.  /\  ( u  .N  w
)  e.  N. )
)  ->  ( [ <. ( ( v  .N  y )  +N  (
u  .N  x ) ) ,  ( u  .N  y ) >. ]  ~Q  <Q  [ <. (
( v  .N  w
)  +N  ( u  .N  z ) ) ,  ( u  .N  w ) >. ]  ~Q  <->  ( ( ( v  .N  y )  +N  (
u  .N  x ) )  .N  ( u  .N  w ) ) 
<N  ( ( u  .N  y )  .N  (
( v  .N  w
)  +N  ( u  .N  z ) ) ) ) )
3824, 26, 34, 36, 37syl22anc 1171 . . 3  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( [ <. ( ( v  .N  y )  +N  (
u  .N  x ) ) ,  ( u  .N  y ) >. ]  ~Q  <Q  [ <. (
( v  .N  w
)  +N  ( u  .N  z ) ) ,  ( u  .N  w ) >. ]  ~Q  <->  ( ( ( v  .N  y )  +N  (
u  .N  x ) )  .N  ( u  .N  w ) ) 
<N  ( ( u  .N  y )  .N  (
( v  .N  w
)  +N  ( u  .N  z ) ) ) ) )
39 simp3 941 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( v  e.  N.  /\  u  e. 
N. ) )
40 simp1 939 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( x  e.  N.  /\  y  e. 
N. ) )
41 addpipqqs 6622 . . . . 5  |-  ( ( ( v  e.  N.  /\  u  e.  N. )  /\  ( x  e.  N.  /\  y  e.  N. )
)  ->  ( [ <. v ,  u >. ]  ~Q  +Q  [ <. x ,  y >. ]  ~Q  )  =  [ <. (
( v  .N  y
)  +N  ( u  .N  x ) ) ,  ( u  .N  y ) >. ]  ~Q  )
4239, 40, 41syl2anc 403 . . . 4  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( [ <. v ,  u >. ]  ~Q  +Q  [ <. x ,  y >. ]  ~Q  )  =  [ <. (
( v  .N  y
)  +N  ( u  .N  x ) ) ,  ( u  .N  y ) >. ]  ~Q  )
43 simp2 940 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( z  e.  N.  /\  w  e. 
N. ) )
44 addpipqqs 6622 . . . . 5  |-  ( ( ( v  e.  N.  /\  u  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )
)  ->  ( [ <. v ,  u >. ]  ~Q  +Q  [ <. z ,  w >. ]  ~Q  )  =  [ <. (
( v  .N  w
)  +N  ( u  .N  z ) ) ,  ( u  .N  w ) >. ]  ~Q  )
4539, 43, 44syl2anc 403 . . . 4  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( [ <. v ,  u >. ]  ~Q  +Q  [ <. z ,  w >. ]  ~Q  )  =  [ <. (
( v  .N  w
)  +N  ( u  .N  z ) ) ,  ( u  .N  w ) >. ]  ~Q  )
4642, 45breq12d 3806 . . 3  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( ( [ <. v ,  u >. ]  ~Q  +Q  [ <. x ,  y >. ]  ~Q  )  <Q  ( [ <. v ,  u >. ]  ~Q  +Q  [ <. z ,  w >. ]  ~Q  )  <->  [ <. (
( v  .N  y
)  +N  ( u  .N  x ) ) ,  ( u  .N  y ) >. ]  ~Q  <Q  [ <. ( ( v  .N  w )  +N  ( u  .N  z
) ) ,  ( u  .N  w )
>. ]  ~Q  ) )
47 ordpipqqs 6626 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )
)  ->  ( [ <. x ,  y >. ]  ~Q  <Q  [ <. z ,  w >. ]  ~Q  <->  ( x  .N  w )  <N  (
y  .N  z ) ) )
48473adant3 959 . . . 4  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( [ <. x ,  y >. ]  ~Q  <Q  [ <. z ,  w >. ]  ~Q  <->  ( x  .N  w )  <N  (
y  .N  z ) ) )
49 mulclpi 6580 . . . . . 6  |-  ( ( x  e.  N.  /\  w  e.  N. )  ->  ( x  .N  w
)  e.  N. )
5021, 29, 49syl2anc 403 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( x  .N  w )  e.  N. )
51 mulclpi 6580 . . . . . 6  |-  ( ( y  e.  N.  /\  z  e.  N. )  ->  ( y  .N  z
)  e.  N. )
5217, 31, 51syl2anc 403 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( y  .N  z )  e.  N. )
53 mulclpi 6580 . . . . . 6  |-  ( ( u  e.  N.  /\  u  e.  N. )  ->  ( u  .N  u
)  e.  N. )
5420, 20, 53syl2anc 403 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( u  .N  u )  e.  N. )
55 ltmpig 6591 . . . . 5  |-  ( ( ( x  .N  w
)  e.  N.  /\  ( y  .N  z
)  e.  N.  /\  ( u  .N  u
)  e.  N. )  ->  ( ( x  .N  w )  <N  (
y  .N  z )  <-> 
( ( u  .N  u )  .N  (
x  .N  w ) )  <N  ( (
u  .N  u )  .N  ( y  .N  z ) ) ) )
5650, 52, 54, 55syl3anc 1170 . . . 4  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
x  .N  w ) 
<N  ( y  .N  z
)  <->  ( ( u  .N  u )  .N  ( x  .N  w
) )  <N  (
( u  .N  u
)  .N  ( y  .N  z ) ) ) )
57 mulclpi 6580 . . . . . . 7  |-  ( ( ( u  .N  x
)  e.  N.  /\  ( u  .N  w
)  e.  N. )  ->  ( ( u  .N  x )  .N  (
u  .N  w ) )  e.  N. )
5823, 36, 57syl2anc 403 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
u  .N  x )  .N  ( u  .N  w ) )  e. 
N. )
59 mulclpi 6580 . . . . . . 7  |-  ( ( ( u  .N  y
)  e.  N.  /\  ( u  .N  z
)  e.  N. )  ->  ( ( u  .N  y )  .N  (
u  .N  z ) )  e.  N. )
6026, 33, 59syl2anc 403 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
u  .N  y )  .N  ( u  .N  z ) )  e. 
N. )
61 mulclpi 6580 . . . . . . 7  |-  ( ( ( v  .N  y
)  e.  N.  /\  ( u  .N  w
)  e.  N. )  ->  ( ( v  .N  y )  .N  (
u  .N  w ) )  e.  N. )
6219, 36, 61syl2anc 403 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
v  .N  y )  .N  ( u  .N  w ) )  e. 
N. )
63 ltapig 6590 . . . . . 6  |-  ( ( ( ( u  .N  x )  .N  (
u  .N  w ) )  e.  N.  /\  ( ( u  .N  y )  .N  (
u  .N  z ) )  e.  N.  /\  ( ( v  .N  y )  .N  (
u  .N  w ) )  e.  N. )  ->  ( ( ( u  .N  x )  .N  ( u  .N  w
) )  <N  (
( u  .N  y
)  .N  ( u  .N  z ) )  <-> 
( ( ( v  .N  y )  .N  ( u  .N  w
) )  +N  (
( u  .N  x
)  .N  ( u  .N  w ) ) )  <N  ( (
( v  .N  y
)  .N  ( u  .N  w ) )  +N  ( ( u  .N  y )  .N  ( u  .N  z
) ) ) ) )
6458, 60, 62, 63syl3anc 1170 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
( u  .N  x
)  .N  ( u  .N  w ) ) 
<N  ( ( u  .N  y )  .N  (
u  .N  z ) )  <->  ( ( ( v  .N  y )  .N  ( u  .N  w ) )  +N  ( ( u  .N  x )  .N  (
u  .N  w ) ) )  <N  (
( ( v  .N  y )  .N  (
u  .N  w ) )  +N  ( ( u  .N  y )  .N  ( u  .N  z ) ) ) ) )
65 mulcompig 6583 . . . . . . . 8  |-  ( ( f  e.  N.  /\  g  e.  N. )  ->  ( f  .N  g
)  =  ( g  .N  f ) )
6665adantl 271 . . . . . . 7  |-  ( ( ( ( x  e. 
N.  /\  y  e.  N. )  /\  (
z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  /\  ( f  e.  N.  /\  g  e. 
N. ) )  -> 
( f  .N  g
)  =  ( g  .N  f ) )
67 mulasspig 6584 . . . . . . . 8  |-  ( ( f  e.  N.  /\  g  e.  N.  /\  h  e.  N. )  ->  (
( f  .N  g
)  .N  h )  =  ( f  .N  ( g  .N  h
) ) )
6867adantl 271 . . . . . . 7  |-  ( ( ( ( x  e. 
N.  /\  y  e.  N. )  /\  (
z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  /\  ( f  e.  N.  /\  g  e. 
N.  /\  h  e.  N. ) )  ->  (
( f  .N  g
)  .N  h )  =  ( f  .N  ( g  .N  h
) ) )
6920, 20, 21, 66, 68, 29, 28caov4d 5716 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
u  .N  u )  .N  ( x  .N  w ) )  =  ( ( u  .N  x )  .N  (
u  .N  w ) ) )
7020, 20, 17, 66, 68, 31, 28caov4d 5716 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
u  .N  u )  .N  ( y  .N  z ) )  =  ( ( u  .N  y )  .N  (
u  .N  z ) ) )
7169, 70breq12d 3806 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
( u  .N  u
)  .N  ( x  .N  w ) ) 
<N  ( ( u  .N  u )  .N  (
y  .N  z ) )  <->  ( ( u  .N  x )  .N  ( u  .N  w
) )  <N  (
( u  .N  y
)  .N  ( u  .N  z ) ) ) )
72 distrpig 6585 . . . . . . . 8  |-  ( ( f  e.  N.  /\  g  e.  N.  /\  h  e.  N. )  ->  (
f  .N  ( g  +N  h ) )  =  ( ( f  .N  g )  +N  ( f  .N  h
) ) )
7372adantl 271 . . . . . . 7  |-  ( ( ( ( x  e. 
N.  /\  y  e.  N. )  /\  (
z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  /\  ( f  e.  N.  /\  g  e. 
N.  /\  h  e.  N. ) )  ->  (
f  .N  ( g  +N  h ) )  =  ( ( f  .N  g )  +N  ( f  .N  h
) ) )
7473, 19, 23, 36, 15, 66caovdir2d 5708 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
( v  .N  y
)  +N  ( u  .N  x ) )  .N  ( u  .N  w ) )  =  ( ( ( v  .N  y )  .N  ( u  .N  w
) )  +N  (
( u  .N  x
)  .N  ( u  .N  w ) ) ) )
7573, 26, 30, 33caovdid 5707 . . . . . . 7  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
u  .N  y )  .N  ( ( v  .N  w )  +N  ( u  .N  z
) ) )  =  ( ( ( u  .N  y )  .N  ( v  .N  w
) )  +N  (
( u  .N  y
)  .N  ( u  .N  z ) ) ) )
7620, 17, 16, 66, 68, 29, 28caov411d 5717 . . . . . . . 8  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
u  .N  y )  .N  ( v  .N  w ) )  =  ( ( v  .N  y )  .N  (
u  .N  w ) ) )
7776oveq1d 5558 . . . . . . 7  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
( u  .N  y
)  .N  ( v  .N  w ) )  +N  ( ( u  .N  y )  .N  ( u  .N  z
) ) )  =  ( ( ( v  .N  y )  .N  ( u  .N  w
) )  +N  (
( u  .N  y
)  .N  ( u  .N  z ) ) ) )
7875, 77eqtrd 2114 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
u  .N  y )  .N  ( ( v  .N  w )  +N  ( u  .N  z
) ) )  =  ( ( ( v  .N  y )  .N  ( u  .N  w
) )  +N  (
( u  .N  y
)  .N  ( u  .N  z ) ) ) )
7974, 78breq12d 3806 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
( ( v  .N  y )  +N  (
u  .N  x ) )  .N  ( u  .N  w ) ) 
<N  ( ( u  .N  y )  .N  (
( v  .N  w
)  +N  ( u  .N  z ) ) )  <->  ( ( ( v  .N  y )  .N  ( u  .N  w ) )  +N  ( ( u  .N  x )  .N  (
u  .N  w ) ) )  <N  (
( ( v  .N  y )  .N  (
u  .N  w ) )  +N  ( ( u  .N  y )  .N  ( u  .N  z ) ) ) ) )
8064, 71, 793bitr4d 218 . . . 4  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
( u  .N  u
)  .N  ( x  .N  w ) ) 
<N  ( ( u  .N  u )  .N  (
y  .N  z ) )  <->  ( ( ( v  .N  y )  +N  ( u  .N  x ) )  .N  ( u  .N  w
) )  <N  (
( u  .N  y
)  .N  ( ( v  .N  w )  +N  ( u  .N  z ) ) ) ) )
8148, 56, 803bitrd 212 . . 3  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( [ <. x ,  y >. ]  ~Q  <Q  [ <. z ,  w >. ]  ~Q  <->  ( (
( v  .N  y
)  +N  ( u  .N  x ) )  .N  ( u  .N  w ) )  <N 
( ( u  .N  y )  .N  (
( v  .N  w
)  +N  ( u  .N  z ) ) ) ) )
8238, 46, 813bitr4rd 219 . 2  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( [ <. x ,  y >. ]  ~Q  <Q  [ <. z ,  w >. ]  ~Q  <->  ( [ <. v ,  u >. ]  ~Q  +Q  [ <. x ,  y >. ]  ~Q  )  <Q  ( [ <. v ,  u >. ]  ~Q  +Q  [ <. z ,  w >. ]  ~Q  ) ) )
831, 5, 9, 13, 823ecoptocl 6261 1  |-  ( ( A  e.  Q.  /\  B  e.  Q.  /\  C  e.  Q. )  ->  ( A  <Q  B  <->  ( C  +Q  A )  <Q  ( C  +Q  B ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    /\ w3a 920    = wceq 1285    e. wcel 1434   <.cop 3409   class class class wbr 3793  (class class class)co 5543   [cec 6170   N.cnpi 6524    +N cpli 6525    .N cmi 6526    <N clti 6527    ~Q ceq 6531   Q.cnq 6532    +Q cplq 6534    <Q cltq 6537
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-coll 3901  ax-sep 3904  ax-nul 3912  ax-pow 3956  ax-pr 3972  ax-un 4196  ax-setind 4288  ax-iinf 4337
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1687  df-eu 1945  df-mo 1946  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ne 2247  df-ral 2354  df-rex 2355  df-reu 2356  df-rab 2358  df-v 2604  df-sbc 2817  df-csb 2910  df-dif 2976  df-un 2978  df-in 2980  df-ss 2987  df-nul 3259  df-pw 3392  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-int 3645  df-iun 3688  df-br 3794  df-opab 3848  df-mpt 3849  df-tr 3884  df-eprel 4052  df-id 4056  df-iord 4129  df-on 4131  df-suc 4134  df-iom 4340  df-xp 4377  df-rel 4378  df-cnv 4379  df-co 4380  df-dm 4381  df-rn 4382  df-res 4383  df-ima 4384  df-iota 4897  df-fun 4934  df-fn 4935  df-f 4936  df-f1 4937  df-fo 4938  df-f1o 4939  df-fv 4940  df-ov 5546  df-oprab 5547  df-mpt2 5548  df-1st 5798  df-2nd 5799  df-recs 5954  df-irdg 6019  df-oadd 6069  df-omul 6070  df-er 6172  df-ec 6174  df-qs 6178  df-ni 6556  df-pli 6557  df-mi 6558  df-lti 6559  df-plpq 6596  df-enq 6599  df-nqqs 6600  df-plqqs 6601  df-ltnqqs 6605
This theorem is referenced by:  ltanqi  6654  lt2addnq  6656  ltaddnq  6659  prarloclemlt  6745  prarloclemcalc  6754  addlocprlemgt  6786  addclpr  6789  prmuloclemcalc  6817  distrlem4prl  6836  distrlem4pru  6837  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemdisj  6858  ltexprlemloc  6859  ltexprlemfl  6861  ltexprlemfu  6863  aptiprleml  6891  aptiprlemu  6892  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemloc  6927  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprprlemml  6946  caucvgprprlemopl  6949  caucvgprprlemlol  6950
  Copyright terms: Public domain W3C validator