Metamath Proof Explorer - mmtheorems50

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 4901-5000 - Page 50 of 58

Type	Label	Description
Statement
Theorem	ruclem17 4901	Lemma for ruc 4924. A helper lemma showing our constructed function G maps NN to real numbers.
|- F:NN-->RR   &   |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))   &   |- D = {<.<.x, y>., z>. | ((x e. (RR X. RR) /\ y e. RR) /\ z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.))}   &   |- G = (1st o. (DseqC))   &   |- H = (2nd o. (DseqC))   =>   |- G:NN-->RR
Theorem	ruclem18 4902	Lemma for ruc 4924. The value of our constructed function G when the value of the input function F lies between the previous values of G and H. This assignment to G defines a new interval between G and H (see also ruclem19 4903) that avoids the value of F.
|- F:NN-->RR   &   |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))   &   |- D = {<.<.x, y>., z>. | ((x e. (RR X. RR) /\ y e. RR) /\ z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.))}   &   |- G = (1st o. (DseqC))   &   |- H = (2nd o. (DseqC))   &   |- A e. NN   =>   |- (((G` A) < (F` (A + 1)) /\ (F` (A + 1)) < (H` A)) -> (G` (A + 1)) = (((2 x. (F` (A + 1))) + (H` A)) / 3))
Theorem	ruclem19 4903	Lemma for ruc 4924. The value of our constructed function H when the value of the input function F lies between the previous values of G and H. This assignment to H defines a new interval between G and H (see also ruclem18 4902) that avoids the value of F.
|- F:NN-->RR   &   |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))   &   |- D = {<.<.x, y>., z>. | ((x e. (RR X. RR) /\ y e. RR) /\ z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.))}   &   |- G = (1st o. (DseqC))   &   |- H = (2nd o. (DseqC))   &   |- A e. NN   =>   |- (((G` A) < (F` (A + 1)) /\ (F` (A + 1)) < (H` A)) -> (H` (A + 1)) = (((F` (A + 1)) + (2 x. (H` A))) / 3))
Theorem	ruclem20 4904	Lemma for ruc 4924. The value of our constructed function G when the value of the input function F does not lie between the previous values of G and H. This assignment to G just shrinks the interval between G and H by some arbitrary amount.
|- F:NN-->RR   &   |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))   &   |- D = {<.<.x, y>., z>. | ((x e. (RR X. RR) /\ y e. RR) /\ z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.))}   &   |- G = (1st o. (DseqC))   &   |- H = (2nd o. (DseqC))   &   |- A e. NN   =>   |- (-. ((G` A) < (F` (A + 1)) /\ (F` (A + 1)) < (H` A)) -> (G` (A + 1)) = (((2 x. (G` A)) + (H` A)) / 3))
Theorem	ruclem21 4905	Lemma for ruc 4924. The value of our constructed function H when the value of the input function F does not lie between the previous values of G and H. This assignment to H just shrinks the interval between G and H by some arbitrary amount.
|- F:NN-->RR   &   |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))   &   |- D = {<.<.x, y>., z>. | ((x e. (RR X. RR) /\ y e. RR) /\ z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.))}   &   |- G = (1st o. (DseqC))   &   |- H = (2nd o. (DseqC))   &   |- A e. NN   =>   |- (-. ((G` A) < (F` (A + 1)) /\ (F` (A + 1)) < (H` A)) -> (H` (A + 1)) = (((G` A) + (2 x. (H` A))) / 3))
Theorem	ruclem22 4906	Lemma for ruc 4924. Each value of our constructed function G is a real number.
|- F:NN-->RR   &   |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))   &   |- D = {<.<.x, y>., z>. | ((x e. (RR X. RR) /\ y e. RR) /\ z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.))}   &   |- G = (1st o. (DseqC))   &   |- H = (2nd o. (DseqC))   &   |- A e. NN   =>   |- (G` A) e. RR
Theorem	ruclem23 4907	Lemma for ruc 4924. Each value of our constructed function H is a real number.
|- F:NN-->RR   &   |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))   &   |- D = {<.<.x, y>., z>. | ((x e. (RR X. RR) /\ y e. RR) /\ z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.))}   &   |- G = (1st o. (DseqC))   &   |- H = (2nd o. (DseqC))   &   |- A e. NN   =>   |- (H` A) e. RR
Theorem	ruclem24 4908	Lemma for ruc 4924. A helper lemma for the induction hypothesis in ruclem25 4909.
|- F:NN-->RR   &   |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))   &   |- D = {<.<.x, y>., z>. | ((x e. (RR X. RR) /\ y e. RR) /\ z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y)