Theorem ruclem15 4899

Description: Lemma for ruc 4924. A helper lemma showing the successor value of the sequence builder used for our construction.

Hypotheses

Ref	Expression
ruclem.0	|- F:NN-->RR
ruclem.1	|- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))
ruclem.2	|- 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)>.))}
ruclem.3	|- G = (1st o. (DseqC))
ruclem.4	|- H = (2nd o. (DseqC))
ruclem15.a	|- A e. NN

Assertion

Ref	Expression
ruclem15	|- ((DseqC)` (A + 1)) = if(((G` A) < (F` (A + 1)) /\ (F` (A + 1)) < (H` A)), <.(((2 x. (F` (A + 1))) + (H` A)) / 3), (((F` (A + 1)) + (2 x. (H` A))) / 3)>., <.(((2 x. (G` A)) + (H` A)) / 3), (((G` A) + (2 x. (H` A))) / 3)>.)

Distinct variable group(s):   x,y,z   z,F

Proof of Theorem ruclem15

Step	Hyp	Ref	Expression
1		ruclem15.a	. . 3 |- A e. NN
2		ruclem.2	. . . . 5 |- 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)>.))}
3	2	ruclem9 4893	. . . 4 |- D e. V
4		ruclem.0	. . . . 5 |- F:NN-->RR
5		ruclem.1	. . . . 5 |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))
6	4, 5	ruclem5 4889	. . . 4 |- C e. V
7	3, 6	seqsuc 4671	. . 3 |- (A e. NN -> ((DseqC)` (A + 1)) = (((DseqC)` A)D(C` (A + 1))))
8	1, 7	ax-mp 6	. 2 |- ((DseqC)` (A + 1)) = (((DseqC)` A)D(C` (A + 1)))
9	4, 5, 2	ruclem13 4897	. . . 4 |- (DseqC):NN-->(RR X. RR)
10		ffvrn 2890	. . . 4 |- (((DseqC):NN-->(RR X. RR) /\ A e. NN) -> ((DseqC)` A) e. (RR X. RR))
11	9, 1, 10	mp2an 520	. . 3 |- ((DseqC)` A) e. (RR X. RR)
12	4, 5, 1	ruclem8 4892	. . . 4 |- (C` (A + 1)) = (F` (A + 1))
13		peano2nn 4433	. . . . . 6 |- (A e. NN -> (A + 1) e. NN)
14	1, 13	ax-mp 6	. . . . 5 |- (A + 1) e. NN
15		ffvrn 2890	. . . . 5 |- ((F:NN-->RR /\ (A + 1) e. NN) -> (F` (A + 1)) e. RR)
16	4, 14, 15	mp2an 520	. . . 4 |- (F` (A + 1)) e. RR
17	12, 16	eqeltr 1159	. . 3 |- (C` (A + 1)) e. RR
18		opex 1893	. . . . 5 |- <.(((2 x. (C` (A + 1))) + (2nd` ((DseqC)` A))) / 3), (((C` (A + 1)) + (2 x. (2nd` ((DseqC)` A)))) / 3)>. e. V
19		opex 1893	. . . . 5 |- <.(((2 x. (1st` ((DseqC)` A))) + (2nd` ((DseqC)` A))) / 3), (((1st` ((DseqC)` A)) + (2 x. (2nd` ((DseqC)` A)))) / 3)>. e. V
20	18, 19	ifex 1797	. . . 4 |- if(((1st` ((DseqC)` A)) < (C` (A + 1)) /\ (C` (A + 1)) < (2nd` ((DseqC)` A))), <.(((2 x. (C` (A + 1))) + (2nd` ((DseqC)` A))) / 3), (((C` (A + 1)) + (2 x. (2nd` ((DseqC)` A)))) / 3)>., <.(((2 x. (1st` ((DseqC)` A))) + (2nd` ((DseqC)` A))) / 3), (((1st` ((DseqC)` A)) + (2 x. (2nd` ((DseqC)` A)))) / 3)>.) e. V
21		cleqid 1102	. . . . 5 |- v = v
22		ruclem4 4888	. . . . 5 |- ((w = ((DseqC)` A) /\ v = v) -> if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.) = if(((1st` ((DseqC)` A)) < v /\ v < (2nd` ((DseqC)` A))), <.(((2 x. v) + (2nd` ((DseqC)` A))) / 3), ((v + (2 x. (2nd` ((DseqC)` A)))) / 3)>., <.(((2 x. (1st` ((DseqC)` A))) + (2nd` ((DseqC)` A))) / 3), (((1st` ((DseqC)` A)) + (2 x. (2nd` ((DseqC)` A)))) / 3)>.))
23	21, 22	mpan2 519	. . . 4 |- (w = ((DseqC)` A) -> if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.) = if(((1st` ((DseqC)` A)) < v /\ v < (2nd` ((DseqC)` A))), <.(((2 x. v) + (2nd` ((DseqC)` A))) / 3), ((v + (2 x. (2nd` ((DseqC)` A)))) / 3)>., <.(((2 x. (1st` ((DseqC)` A))) + (2nd` ((DseqC)` A))) / 3), (((1st` ((DseqC)` A)) + (2 x. (2nd` ((DseqC)` A)))) / 3)>.))
24		cleqid 1102	. . . . 5 |- ((DseqC)` A) = ((DseqC)` A)
25		ruclem4 4888	. . . . 5 |- ((((DseqC)` A) = ((DseqC)` A) /\ v = (C` (A + 1))) -> if(((1st` ((DseqC)` A)) < v /\ v < (2nd` ((DseqC)` A))), <.(((2 x. v) + (2nd` ((DseqC)` A))) / 3), ((v + (2 x. (2nd` ((DseqC)` A)))) / 3)>., <.(((2 x. (1st` ((DseqC)` A))) + (2nd` ((DseqC)` A))) / 3), (((1st` ((DseqC)` A)) + (2 x. (2nd` ((DseqC)` A)))) / 3)>.) = if(((1st` ((DseqC)` A)) < (C` (A + 1)) /\ (C` (A + 1)) < (2nd` ((DseqC)` A))), <.(((2 x. (C` (A + 1))) + (2nd` ((DseqC)` A))) / 3), (((C` (A + 1)) + (2 x. (2nd` ((DseqC)` A)))) / 3)>., <.(((2 x. (1st` ((DseqC)` A))) + (2nd` ((DseqC)` A))) / 3), (((1st` ((DseqC)` A)) + (2 x. (2nd` ((DseqC)` A)))) / 3)>.))
26	24, 25	mpan 518	. . . 4 |- (v = (C` (A + 1)) -> if((