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

Theorem lincmb01cmp 8621
Description: A linear combination of two reals which lies in the interval between them. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 8-Sep-2015.)
Assertion
Ref Expression
lincmb01cmp  RR  RR  <  T  0 [,] 1  1  -  T  x.  +  T  x.  [,]

Proof of Theorem lincmb01cmp
StepHypRef Expression
1 simpr 103 . . . . 5  RR  RR  <  T  0 [,] 1 
T  0 [,] 1
2 0re 6805 . . . . . . 7  0  RR
32a1i 9 . . . . . 6  RR  RR  <  T  0 [,] 1  0  RR
4 1re 6804 . . . . . . 7  1  RR
54a1i 9 . . . . . 6  RR  RR  <  T  0 [,] 1  1  RR
62, 4elicc2i 8558 . . . . . . . 8  T  0 [,] 1  T  RR  0  <_  T  T  <_ 
1
76simp1bi 918 . . . . . . 7  T  0 [,] 1  T  RR
87adantl 262 . . . . . 6  RR  RR  <  T  0 [,] 1 
T  RR
9 difrp 8374 . . . . . . . 8  RR  RR  <  -  RR+
109biimp3a 1234 . . . . . . 7  RR  RR  <  -  RR+
1110adantr 261 . . . . . 6  RR  RR  <  T  0 [,] 1  -  RR+
12 eqid 2037 . . . . . . 7  0  x.  -  0  x.  -
13 eqid 2037 . . . . . . 7  1  x.  -  1  x.  -
1412, 13iccdil 8616 . . . . . 6  0  RR  1  RR  T  RR  -  RR+  T  0 [,] 1  T  x.  -  0  x.  -  [,]
1  x.  -
153, 5, 8, 11, 14syl22anc 1135 . . . . 5  RR  RR  <  T  0 [,] 1  T 
0 [,] 1  T  x.  -  0  x.  -  [,]
1  x.  -
161, 15mpbid 135 . . . 4  RR  RR  <  T  0 [,] 1  T  x.  -  0  x.  -  [,]
1  x.  -
17 simpl2 907 . . . . . . . 8  RR  RR  <  T  0 [,] 1  RR
18 simpl1 906 . . . . . . . 8  RR  RR  <  T  0 [,] 1  RR
1917, 18resubcld 7155 . . . . . . 7  RR  RR  <  T  0 [,] 1  -  RR
2019recnd 6831 . . . . . 6  RR  RR  <  T  0 [,] 1  -  CC
2120mul02d 7165 . . . . 5  RR  RR  <  T  0 [,] 1  0  x.  -  0
2220mulid2d 6823 . . . . 5  RR  RR  <  T  0 [,] 1  1  x.  -  -
2321, 22oveq12d 5473 . . . 4  RR  RR  <  T  0 [,] 1  0  x.  -  [,] 1  x.  -  0 [,]  -
2416, 23eleqtrd 2113 . . 3  RR  RR  <  T  0 [,] 1  T  x.  -  0 [,]  -
258, 19remulcld 6833 . . . 4  RR  RR  <  T  0 [,] 1  T  x.  -  RR
26 eqid 2037 . . . . 5  0  +  0  +
27 eqid 2037 . . . . 5  -  +  -  +
2826, 27iccshftr 8612 . . . 4  0  RR  -  RR  T  x.  -  RR  RR  T  x.  -  0 [,]  -  T  x.  -  +  0  +  [,]  -  +
293, 19, 25, 18, 28syl22anc 1135 . . 3  RR  RR  <  T  0 [,] 1  T  x.  -  0 [,]  -  T  x.  -  +  0  +  [,]  -  +
3024, 29mpbid 135 . 2  RR  RR  <  T  0 [,] 1  T  x.  -  +  0  +  [,]  -  +
318recnd 6831 . . . . 5  RR  RR  <  T  0 [,] 1 
T  CC
3217recnd 6831 . . . . 5  RR  RR  <  T  0 [,] 1  CC
3331, 32mulcld 6825 . . . 4  RR  RR  <  T  0 [,] 1  T  x.  CC
3418recnd 6831 . . . . 5  RR  RR  <  T  0 [,] 1  CC
3531, 34mulcld 6825 . . . 4  RR  RR  <  T  0 [,] 1  T  x.  CC
3633, 35, 34subadd23d 7120 . . 3  RR  RR  <  T  0 [,] 1  T  x.  -  T  x.  +  T  x.  +  -  T  x.
3731, 32, 34subdid 7187 . . . 4  RR  RR  <  T  0 [,] 1  T  x.  -  T  x.  -  T  x.
3837oveq1d 5470 . . 3  RR  RR  <  T  0 [,] 1  T  x.  -  +  T  x.  -  T  x.  +
39 resubcl 7051 . . . . . . . 8  1  RR  T  RR  1  -  T  RR
404, 8, 39sylancr 393 . . . . . . 7  RR  RR  <  T  0 [,] 1  1  -  T  RR
4140, 18remulcld 6833 . . . . . 6  RR  RR  <  T  0 [,] 1  1  -  T  x.  RR
4241recnd 6831 . . . . 5  RR  RR  <  T  0 [,] 1  1  -  T  x.  CC
4342, 33addcomd 6941 . . . 4  RR  RR  <  T  0 [,] 1  1  -  T  x.  +  T  x.  T  x.  +  1  -  T  x.
44 1cnd 6821 . . . . . . 7  RR  RR  <  T  0 [,] 1  1  CC
4544, 31, 34subdird 7188 . . . . . 6  RR  RR  <  T  0 [,] 1  1  -  T  x.  1  x.  -  T  x.
4634mulid2d 6823 . . . . . . 7  RR  RR  <  T  0 [,] 1  1  x.
4746oveq1d 5470 . . . . . 6  RR  RR  <  T  0 [,] 1  1  x.  -  T  x.  -  T  x.
4845, 47eqtrd 2069 . . . . 5  RR  RR  <  T  0 [,] 1  1  -  T  x.  -  T  x.
4948oveq2d 5471 . . . 4  RR  RR  <  T  0 [,] 1  T  x.  + 
1  -  T  x.  T  x.  +  -  T  x.
5043, 49eqtrd 2069 . . 3  RR  RR  <  T  0 [,] 1  1  -  T  x.  +  T  x.  T  x.  +  -  T  x.
5136, 38, 503eqtr4d 2079 . 2  RR  RR  <  T  0 [,] 1  T  x.  -  +  1  -  T  x.  +  T  x.
5234addid2d 6940 . . 3  RR  RR  <  T  0 [,] 1  0  +
5332, 34npcand 7102 . . 3  RR  RR  <  T  0 [,] 1  -  +
5452, 53oveq12d 5473 . 2  RR  RR  <  T  0 [,] 1  0  +  [,]  -  +  [,]
5530, 51, 543eltr3d 2117 1  RR  RR  <  T  0 [,] 1  1  -  T  x.  +  T  x.  [,]
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98   w3a 884   wcel 1390   class class class wbr 3755  (class class class)co 5455   RRcr 6690   0cc0 6691   1c1 6692    + caddc 6694    x. cmul 6696    < clt 6837    <_ cle 6838    - cmin 6959   RR+crp 8338   [,]cicc 8510
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-cnex 6754  ax-resscn 6755  ax-1cn 6756  ax-1re 6757  ax-icn 6758  ax-addcl 6759  ax-addrcl 6760  ax-mulcl 6761  ax-mulrcl 6762  ax-addcom 6763  ax-mulcom 6764  ax-addass 6765  ax-mulass 6766  ax-distr 6767  ax-i2m1 6768  ax-1rid 6770  ax-0id 6771  ax-rnegex 6772  ax-precex 6773  ax-cnre 6774  ax-pre-ltirr 6775  ax-pre-ltwlin 6776  ax-pre-lttrn 6777  ax-pre-ltadd 6779  ax-pre-mulgt0 6780
This theorem depends on definitions:  df-bi 110  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-nel 2204  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-po 4024  df-iso 4025  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-iota 4810  df-fun 4847  df-fv 4853  df-riota 5411  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-pnf 6839  df-mnf 6840  df-xr 6841  df-ltxr 6842  df-le 6843  df-sub 6961  df-neg 6962  df-rp 8339  df-icc 8514
This theorem is referenced by:  iccf1o  8622
  Copyright terms: Public domain W3C validator