Theorem ruclem15 7467

Description: Lemma for ruc 7492. A helper lemma showing the successor value of the recursive 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. (D seq1 C))
ruclem.4	|- H = (2nd o. (D seq1 C))
ruclem15.a	|- A e. NN

Assertion

Ref	Expression
ruclem15	|- ((D seq1 C)` (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 groups:   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 7461	. . . 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 7457	. . . 4 |- C e. V
7	3, 6	seq1p1 6255	. . 3 |- (A e. NN -> ((D seq1 C)` (A + 1)) = (((D seq1 C)` A)D(C` (A + 1))))
8	1, 7	ax-mp 7	. 2 |- ((D seq1 C)` (A + 1)) = (((D seq1 C)` A)D(C` (A + 1)))
9	4, 5, 2	ruclem13 7465	. . . 4 |- (D seq1 C):NN-->(RR X. RR)
10		ffvelrn 3799	. . . 4 |- (((D seq1 C):NN-->(RR X. RR) /\ A e. NN) -> ((D seq1 C)` A) e. (RR X. RR))
11	9, 1, 10	mp2an 695	. . 3 |- ((D seq1 C)` A) e. (RR X. RR)
12	4, 5, 1	ruclem8 7460	. . . 4 |- (C` (A + 1)) = (F` (A + 1))
13		peano2nn 5883	. . . . . 6 |- (A e. NN -> (A + 1) e. NN)
14	1, 13	ax-mp 7	. . . . 5 |- (A + 1) e. NN
15		ffvelrn 3799	. . . . 5 |- ((F:NN-->RR /\ (A + 1) e. NN) -> (F` (A + 1)) e. RR)
16	4, 14, 15	mp2an 695	. . . 4 |- (F` (A + 1)) e. RR
17	12, 16	eqeltr 1536	. . 3 |- (C` (A + 1)) e. RR
18		opex 2772	. . . . 5 |- <.(((2 x. (C` (A + 1))) + (2nd` ((D seq1 C)` A))) / 3), (((C` (A + 1)) + (2 x. (2nd` ((D seq1 C)` A)))) / 3)>. e. V
19		opex 2772	. . . . 5 |- <.(((2 x. (1st` ((D seq1 C)` A))) + (2nd` ((D seq1 C)` A))) / 3), (((1st` ((D seq1 C)` A)) + (2 x. (2nd` ((D seq1 C)` A)))) / 3)>. e. V
20	18, 19	ifex 2390	. . . 4 |- if(((1st` ((D seq1 C)` A)) < (C` (A + 1)) /\ (C` (A + 1)) < (2nd` ((D seq1 C)` A))), <.(((2 x. (C` (A + 1))) + (2nd` ((D seq1 C)` A))) / 3), (((C` (A + 1)) + (2 x. (2nd` ((D seq1 C)` A)))) / 3)>., <.(((2 x. (1st` ((D seq1 C)` A))) + (2nd` ((D seq1 C)` A))) / 3), (((1st` ((D seq1 C)` A)) + (2 x. (2nd` ((D seq1 C)` A)))) / 3)>.) e. V
21		eqid 1468	. . . . 5 |- v = v
22		ruclem4 7456	. . . . 5 |- ((w = ((D seq1 C)` 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` ((D seq1 C)` A)) < v /\ v < (2nd` ((D seq1 C)` A))), <.(((2 x. v) + (2nd` ((D seq1 C)` A))) / 3), ((v + (2 x. (2nd` ((D seq1 C)` A)))) / 3)>., <.(((2 x. (1st` ((D seq1 C)` A))) + (2nd` ((D seq1 C)` A))) / 3), (((1st` ((D seq1 C)` A)) + (2 x. (2nd` ((D seq1 C)` A)))) / 3)>.))
23	21, 22	mpan2 694	. . . 4 |- (w = ((D seq1 C)` 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` ((D seq1 C)` A)) < v /\ v < (2nd` ((D seq1 C)` A))), <.(((2 x. v) + (2nd` ((D seq1 C)` A))) / 3), ((v + (2 x. (2nd` ((D seq1 C)` A)))) / 3)>., <.(((2 x. (1st` ((D seq1 C)` A))) + (2nd` ((D seq1 C)` A))) / 3), (((1st` ((D seq1 C)` A)) + (2 x. (2nd` ((D seq1 C)` A)))) / 3)>.))
24		eqid 1468	. . . . 5 |- ((D seq1 C)` A) = ((D seq1 C)` A)
25		ruclem4 7456	. . . . 5 |- ((((D seq1 C)` A) = ((D seq1 C)` A) /\ v = (C` (A + 1))) -> if(((1st` ((D seq1 C)` A)) < v /\ v < (2nd` ((D seq1 C)` A))), <.(((2 x. v) + (2nd` ((D seq1 C)` A))) / 3), ((v + (2 x. (2nd` ((D seq1 C)` A)))) / 3)>., <.(((2 x. (1st` ((D seq1 C)` A))) + (2nd` ((D seq1 C)` A))) / 3), (((1st` ((D seq1 C)` A)) + (2 x. (2nd` ((D seq1 C)` A)))) / 3)>.) = if(((1st` ((D seq1 C)` A)) < (C` (A + 1)) /\ (C` (A + 1)) < (2nd` ((D seq1 C)` A))), <.(((2 x. (C` (A + 1))) + (2nd` ((D seq1 C)` A))) / 3), (((C` (A + 1)) + (2 x. (2nd` ((D seq1 C)` A)))) / 3)>., <.(((2 x. (1st` ((D seq1 C)` A))) + (2nd` ((D seq1 C)` A))) / 3), (((1st` ((D seq1 C)` A)) + (2 x. (2nd` ((D seq1 C