Theorem ruclem13 7473

Description: Lemma for ruc 7500. A helper lemma showing the recursive 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	|- (D seq1 C):NN-->(RR X. RR)

Distinct variable group:   x,y,z

Proof of Theorem ruclem13

Step	Hyp	Ref	Expression
1		df-f 3189	. 2 |- ((D seq1 C):NN-->(RR X. RR) <-> ((D seq1 C) Fn NN /\ ran ( D seq1 C) (_ (RR X. RR)))
2		ruclem13.2	. . . 4 |- 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 7469	. . 3 |- D e. V
4		ruclem13.0	. . . 4 |- F:NN-->RR
5		ruclem13.1	. . . 4 |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))
6	4, 5	ruclem5 7465	. . 3 |- C e. V
7	3, 6	seq1fn 6265	. 2 |- (D seq1 C) Fn NN
8	4, 5	ruclem7 7467	. . . 4 |- (C` 1) = <.((F` 1) + 1), ((F` 1) + 2)>.
9		oprex 3974	. . . . . 6 |- ((F` 1) + 2) e. V
10	9	opelxp 3209	. . . . 5 |- (<.((F` 1) + 1), ((F` 1) + 2)>. e. (RR X. RR) <-> (((F` 1) + 1) e. RR /\ ((F` 1) + 2) e. RR))
11		1nn 5890	. . . . . . 7 |- 1 e. NN
12		ffvelrn 3805	. . . . . . 7 |- ((F:NN-->RR /\ 1 e. NN) -> (F` 1) e. RR)
13	4, 11, 12	mp2an 696	. . . . . 6 |- (F` 1) e. RR
14		1re 5415	. . . . . 6 |- 1 e. RR
15	13, 14	readdcl 5314	. . . . 5 |- ((F` 1) + 1) e. RR
16		2re 5934	. . . . . 6 |- 2 e. RR
17	13, 16	readdcl 5314	. . . . 5 |- ((F` 1) + 2) e. RR
18	10, 15, 17	mpbir2an 729	. . . 4 |- <.((F` 1) + 1), ((F` 1) + 2)>. e. (RR X. RR)
19	8, 18	eqeltr 1541	. . 3 |- (C` 1) e. (RR X. RR)
20		difss 2163	. . . . 5 |- (NN \ {1}) (_ NN
21		fssres 3634	. . . . 5 |- ((F:NN-->RR /\ (NN \ {1}) (_ NN) -> (F |` (NN \ {1})):(NN \ {1})-->RR)
22	4, 20, 21	mp2an 696	. . . 4 |- (F |` (NN \ {1})):(NN \ {1})-->RR
23	4, 5	ruclem6 7466	. . . . 5 |- (C |` (NN \ {1})) = (F |` (NN \ {1}))
24		feq1 3612	. . . . 5 |- ((C |` (NN \ {1})) = (F |` (NN \ {1})) -> ((C |` (NN \ {1})):(NN \ {1})-->RR <-> (F |` (NN \ {1})):(NN \ {1})-->RR))
25	23, 24	ax-mp 7	. . . 4 |- ((C |` (NN \ {1})):(NN \ {1})-->RR <-> (F |` (NN \ {1})):(NN \ {1})-->RR)
26	22, 25	mpbir 190	. . 3 |- (C |` (NN \ {1})):(NN \ {1})-->RR
27		iftrue 2362	. . . . . . . . 9 |- (((1st` x) < y /\ y < (2nd` x)) -> 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 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>.)
28	27	eleq1d 1537	. . . . . . . 8 |- (((1st` x) < y /\ y < (2nd` x)) -> (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)>.) e. (RR X. RR) <-> <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>. e. (RR X. RR)))
29		opelxpi 3212	. . . . . . . . . . 11 |- (((((2 x. y) + (2nd` x)) / 3) e. RR /\ ((y + (2 x. (2nd` x))) / 3) e. RR) -> <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>. e. (RR X. RR))
30		axaddrcl 5252	. . . . . . . . . . . . 13 |- (((2 x. y) e. RR /\ (2nd` x) e. RR) -> ((2 x. y) + (2nd` x)) e. RR)
31		axmulrcl 5254	. . . . . . . . . . . . . 14 |- ((2 e. RR /\ y e. RR) -> (2 x. y) e. RR)
32	16, 31	mpan 694	. . . . . . . . . . . . 13 |- (y e. RR -> (2 x. y) e. RR)
33	30, 32	sylan 448	. . . . . . . . . . . 12 |- ((y e. RR /\ (2nd` x) e. RR) -> ((2 x. y) + (2nd` x)) e. RR)
34		3re 5936	. . . . . . . . . . . . 13 |- 3 e. RR
35		3pos 5946	. . . . . . . . . . . . . 14 |- 0 < 3
36	34, 35	gt0ne0i 5599	. . . . . . . . . . . . 13 |- 3 =/= 0
37		redivclt 5764	. . . . . . . . . . . . 13 |- ((((2 x. y) + (2nd` x)) e. RR /\ 3 e. RR /\ 3 =/= 0) -> (((2 x. y) + (2nd` x)) / 3) e. RR)
38	34, 36, 37	mp3an23 906	. . . . . . . . . . . 12 |- (((2 x. y) + (2nd` x)) e. RR -> (((2 x. y) + (2nd` x)) / 3) e. RR)
39	33, 38	syl 10	. . . . . . . . . . 11 |- ((y e. RR /\ (2nd` x) e. RR) -> (((2 x. y) + (2nd` x)) / 3) e. RR)
40		axaddrcl 5252	. . . . . . . . . . . . 13 |- ((y e. RR /\ (2 x. (2nd` x)) e. RR) -> (y + (2 x. (2nd` x))) e. RR)
41		axmulrcl 5254	. . . . . . . . . . . . . 14 |- ((2 e. RR /\ (2nd` x) e. RR) -> (2 x. (2nd` x)) e. RR)
42	16, 41	mpan 694	. . . . . . . . . . . . 13 |- ((2nd` x) e. RR -> (2 x. (2nd` x)) e. RR)
43	40, 42	sylan2 451	. . . . . . . . . . . 12 |- ((y e. RR /\ (2nd` x) e. RR) -> (y + (2 x. (2nd` x))) e. RR)
44		redivclt 5764	. . . . . . . . . . . . 13 |- (((y + (2 x. (2nd` x))) e. RR /\ 3 e. RR /\ 3 =/= 0) -> ((y + (2 x. (2nd` x))) / 3) e. RR)
45	34, 36, 44	mp3an23 906	. . . . . . . . . . . 12 |- ((y + (2 x. (2nd` x))) e. RR -> ((y + (2 x. (2nd` x))) / 3) e. RR)
46	43, 45	syl 10	. . . . . . . . . . 11 |- ((y e. RR /\ (2nd` x) e. RR) -> ((y + (2 x. (2nd` x))) / 3) e. RR)
47	29, 39, 46	sylanc 471	. . . . . . . . . 10 |- ((y e. RR /\ (2nd` x) e. RR) -> <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>. e. (RR X. RR))
48	47	ancoms 436	. . . . . . . . 9 |- (((2nd` x) e. RR /\ y e. RR) -> <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>. e. (RR X. RR))
49	48	adantll 392	. . . . . . . 8 |- ((((1st` x) e. RR /\ (2nd` x) e. RR) /\ y e. RR) -> <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>. e. (RR X. RR))
50	28, 49	syl5bir 210	. . . . . . 7 |- (((1st` x) < y /\ y < (2nd` x)) -> ((((1st` x) e. RR /\ (2nd` x) e. RR) /\ y e. RR) -> if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x.