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

Theorem lincmb01cmp 11043
 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 449 . . . . 5
2 0re 9096 . . . . . . 7
32a1i 11 . . . . . 6
4 1re 9095 . . . . . . 7
54a1i 11 . . . . . 6
62, 4elicc2i 10981 . . . . . . . 8
76simp1bi 973 . . . . . . 7
87adantl 454 . . . . . 6
9 difrp 10650 . . . . . . . 8
109biimp3a 1284 . . . . . . 7
1110adantr 453 . . . . . 6
12 eqid 2438 . . . . . . 7
13 eqid 2438 . . . . . . 7
1412, 13iccdil 11039 . . . . . 6
153, 5, 8, 11, 14syl22anc 1186 . . . . 5
161, 15mpbid 203 . . . 4
17 simpl2 962 . . . . . . . 8
18 simpl1 961 . . . . . . . 8
1917, 18resubcld 9470 . . . . . . 7
2019recnd 9119 . . . . . 6
2120mul02d 9269 . . . . 5
2220mulid2d 9111 . . . . 5
2321, 22oveq12d 6102 . . . 4
2416, 23eleqtrd 2514 . . 3
258, 19remulcld 9121 . . . 4
26 eqid 2438 . . . . 5
27 eqid 2438 . . . . 5
2826, 27iccshftr 11035 . . . 4
293, 19, 25, 18, 28syl22anc 1186 . . 3
3024, 29mpbid 203 . 2
318recnd 9119 . . . . 5
3217recnd 9119 . . . . 5
3331, 32mulcld 9113 . . . 4
3418recnd 9119 . . . . 5
3531, 34mulcld 9113 . . . 4
3633, 35, 34subadd23d 9438 . . 3
3731, 32, 34subdid 9494 . . . 4
3837oveq1d 6099 . . 3
39 resubcl 9370 . . . . . . . 8
404, 8, 39sylancr 646 . . . . . . 7
4140, 18remulcld 9121 . . . . . 6
4241recnd 9119 . . . . 5
4342, 33addcomd 9273 . . . 4
44 ax-1cn 9053 . . . . . . . 8
4544a1i 11 . . . . . . 7
4645, 31, 34subdird 9495 . . . . . 6
4734mulid2d 9111 . . . . . . 7
4847oveq1d 6099 . . . . . 6
4946, 48eqtrd 2470 . . . . 5
5049oveq2d 6100 . . . 4
5143, 50eqtrd 2470 . . 3
5236, 38, 513eqtr4d 2480 . 2