Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lincmb01cmp Structured version   Visualization version   Unicode version

Theorem lincmb01cmp 11775
 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

Proof of Theorem lincmb01cmp
StepHypRef Expression
1 simpr 463 . . . . 5
2 0re 9643 . . . . . . 7
32a1i 11 . . . . . 6
4 1re 9642 . . . . . . 7
54a1i 11 . . . . . 6
62, 4elicc2i 11700 . . . . . . . 8
76simp1bi 1023 . . . . . . 7
87adantl 468 . . . . . 6
9 difrp 11337 . . . . . . . 8
109biimp3a 1369 . . . . . . 7
1110adantr 467 . . . . . 6
12 eqid 2451 . . . . . . 7
13 eqid 2451 . . . . . . 7
1412, 13iccdil 11770 . . . . . 6
153, 5, 8, 11, 14syl22anc 1269 . . . . 5
161, 15mpbid 214 . . . 4
17 simpl2 1012 . . . . . . . 8
18 simpl1 1011 . . . . . . . 8
1917, 18resubcld 10047 . . . . . . 7
2019recnd 9669 . . . . . 6
2120mul02d 9831 . . . . 5
2220mulid2d 9661 . . . . 5
2321, 22oveq12d 6308 . . . 4
2416, 23eleqtrd 2531 . . 3
258, 19remulcld 9671 . . . 4
26 eqid 2451 . . . . 5
27 eqid 2451 . . . . 5
2826, 27iccshftr 11766 . . . 4
293, 19, 25, 18, 28syl22anc 1269 . . 3
3024, 29mpbid 214 . 2
318recnd 9669 . . . . 5
3217recnd 9669 . . . . 5
3331, 32mulcld 9663 . . . 4
3418recnd 9669 . . . . 5
3531, 34mulcld 9663 . . . 4
3633, 35, 34subadd23d 10008 . . 3
3731, 32, 34subdid 10074 . . . 4
3837oveq1d 6305 . . 3
39 resubcl 9938 . . . . . . . 8
404, 8, 39sylancr 669 . . . . . . 7
4140, 18remulcld 9671 . . . . . 6
4241recnd 9669 . . . . 5
4342, 33addcomd 9835 . . . 4
44 1cnd 9659 . . . . . . 7
4544, 31, 34subdird 10075 . . . . . 6
4634mulid2d 9661 . . . . . . 7
4746oveq1d 6305 . . . . . 6
4845, 47eqtrd 2485 . . . . 5
4948oveq2d 6306 . . . 4
5043, 49eqtrd 2485 . . 3
5136, 38, 503eqtr4d 2495 . 2