Theorem ruclem13 4897

Description: Lemma for ruc 4924. A helper lemma showing the sequence builder used for our construction maps natural numbers to pairs of reals.

Hypotheses

Ref	Expression
ruclem13.0	|- F:NN-->RR
ruclem13.1	|- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))
ruclem13.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)>.))}

Assertion

Ref	Expression
ruclem13	|- (DseqC):NN-->(RR X. RR)

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

Proof of Theorem ruclem13

Step	Hyp	Ref	Expression
1		ruclem13.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)>.))}
2	1	ruclem9 4893	. . . 4 |- D e. V
3		ruclem13.0	. . . . 5 |- F:NN-->RR
4		ruclem13.1	. . . . 5 |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))
5	3, 4	ruclem5 4889	. . . 4 |- C e. V
6	2, 5	seqfn 4672	. . 3 |- (DseqC) Fn NN
7	3, 4	ruclem7 4891	. . . . 5 |- (C` 1) = <.((F` 1) + 1), ((F` 1) + 2)>.
8		1nn 4432	. . . . . . . . 9 |- 1 e. NN
9		ffvrn 2890	. . . . . . . . 9 |- ((F:NN-->RR /\ 1 e. NN) -> (F` 1) e. RR)
10	3, 8, 9	mp2an 520	. . . . . . . 8 |- (F` 1) e. RR
11		ax1re 4064	. . . . . . . 8 |- 1 e. RR
12	10, 11	readdcl 4118	. . . . . . 7 |- ((F` 1) + 1) e. RR
13		2re 4470	. . . . . . . 8 |- 2 e. RR
14	10, 13	readdcl 4118	. . . . . . 7 |- ((F` 1) + 2) e. RR
15	12, 14	pm3.2i 234	. . . . . 6 |- (((F` 1) + 1) e. RR /\ ((F` 1) + 2) e. RR)
16		oprex 3018	. . . . . . 7 |- ((F` 1) + 2) e. V
17	16	opelxp 2452	. . . . . 6 |- (<.((F` 1) + 1), ((F` 1) + 2)>. e. (RR X. RR) <-> (((F` 1) + 1) e. RR /\ ((F` 1) + 2) e. RR))
18	15, 17	mpbir 165	. . . . 5 |- <.((F` 1) + 1), ((F` 1) + 2)>. e. (RR X. RR)
19	7, 18	eqeltr 1159	. . . 4 |- (C` 1) e. (RR X. RR)
20		difss 1596	. . . . . 6 |- (NN \ {1}) (_ NN
21		fssres 2764	. . . . . 6 |- ((F:NN-->RR /\ (NN \ {1}) (_ NN) -> (F |` (NN \ {1})):(NN \ {1})-->RR)
22	3, 20, 21	mp2an 520	. . . . 5 |- (F |` (NN \ {1})):(NN \ {1})-->RR
23	3, 4	ruclem6 4890	. . . . . 6 |- (C |` (NN \ {1})) = (F |` (NN \ {1}))
24		feq1 2748	. . . . . 6 |- ((C |` (NN \ {1})) = (F |` (NN \ {1})) -> ((C |` (NN \ {1})):(NN \ {1})-->RR <-> (F |` (NN \ {1})):(NN \ {1})-->RR))
25	23, 24	ax-mp 6	. . . . 5 |- ((C |` (NN \ {1})):(NN \ {1})-->RR <-> (F |` (NN \ {1})):(NN \ {1})-->RR)
26	22, 25	mpbir 165	. . . 4 |- (C |` (NN \ {1})):(NN \ {1})-->RR
27	1	ruclem12 4896	. . . . . . 7 |- D = {<.<.w, v>., u>. | ((w e. (RR X. RR) /\ v e. RR) /\ u = 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)>.))}
28		opex 1893	. . . . . . . . . . . 12 |- <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>. e. V
29		opex 1893	. . . . . . . . . . . 12 |- <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>. e. V
30	28, 29	ifex 1797	. . . . . . . . . . 11 |- 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)>.) e. V
31	27	oprabval4g 3053	. . . . . . . . . . 11 |- ((w e. (RR X. RR) /\ v e. RR /\ 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)>.) e. V) -> (wDv) = 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)>.))
32	30, 31	mp3an3 641	. . . . . . . . . 10 |- ((w e. (RR X. RR) /\ v e. RR) -> (wDv) = 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)>.))
33	32	cleq2d 1112	. . . . . . . . 9 |- ((w e. (RR X. RR) /\ v e. RR) -> (u = (wDv) <-> u = 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)>.)))
34	33	pm5.32i 489	. . . . . . . 8 |- (((w e. (RR X. RR) /\ v e. RR) /\ u = (wDv)) <-> ((w e. (RR X. RR) /\ v e. RR) /\ u = 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)>.)))
35	34	bioprabi 3027	. . . . . . 7 |- {<.<.w, v>., u>. | ((w e. (RR X. RR) /\ v e. RR) /\ u = (wDv))} = {<.<.w, v>., u>. | ((w e. (RR X. RR) /\ v e. RR) /\ u = 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)>.))}
36	27, 35	eqtr4 1122	. . . . . 6 |- D = {<.<.w, v>., u>. | ((w e. (RR X. RR) /\ v e. RR) /\ u = (wDv))}
37		iftrue 1780	. . . . . . . . . . . . 13 |- (((1st` w) < v /\ v < (2nd` w)) -> if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) +