Theorem ruclem29 7538

Description: Lemma for ruc 7549. At any index A, the interval between our constructed functions G and H does not include the corresponding value of input function F. In other words, our constructed functions define, by ruclem26 7535 and ruclem27 7536, an ever-shrinking interval that eventually squeezes out all values of F.

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))
ruclem28.a	|- A e. NN

Assertion

Ref	Expression
ruclem29	|- -. ((G` A) < (F` A) /\ (F` A) < (H` A))

Distinct variable groups:   x,y,z   z,F

Proof of Theorem ruclem29

Step	Hyp	Ref	Expression
1		ruclem28.a	. 2 |- A e. NN
2		fveq2 3724	. . . . . 6 |- (w = 1 -> (G` w) = (G` 1))
3		fveq2 3724	. . . . . 6 |- (w = 1 -> (F` w) = (F` 1))
4	2, 3	breq12d 2631	. . . . 5 |- (w = 1 -> ((G` w) < (F` w) <-> (G` 1) < (F` 1)))
5		fveq2 3724	. . . . . 6 |- (w = 1 -> (H` w) = (H` 1))
6	3, 5	breq12d 2631	. . . . 5 |- (w = 1 -> ((F` w) < (H` w) <-> (F` 1) < (H` 1)))
7	4, 6	anbi12d 628	. . . 4 |- (w = 1 -> (((G` w) < (F` w) /\ (F` w) < (H` w)) <-> ((G` 1) < (F` 1) /\ (F` 1) < (H` 1))))
8	7	negbid 611	. . 3 |- (w = 1 -> (-. ((G` w) < (F` w) /\ (F` w) < (H` w)) <-> -. ((G` 1) < (F` 1) /\ (F` 1) < (H` 1))))
9		fveq2 3724	. . . . . 6 |- (w = (v + 1) -> (G` w) = (G` (v + 1)))
10		fveq2 3724	. . . . . 6 |- (w = (v + 1) -> (F` w) = (F` (v + 1)))
11	9, 10	breq12d 2631	. . . . 5 |- (w = (v + 1) -> ((G` w) < (F` w) <-> (G` (v + 1)) < (F` (v + 1))))
12		fveq2 3724	. . . . . 6 |- (w = (v + 1) -> (H` w) = (H` (v + 1)))
13	10, 12	breq12d 2631	. . . . 5 |- (w = (v + 1) -> ((F` w) < (H` w) <-> (F` (v + 1)) < (H` (v + 1))))
14	11, 13	anbi12d 628	. . . 4 |- (w = (v + 1) -> (((G` w) < (F` w) /\ (F` w) < (H` w)) <-> ((G` (v + 1)) < (F` (v + 1)) /\ (F` (v + 1)) < (H` (v + 1)))))
15	14	negbid 611	. . 3 |- (w = (v + 1) -> (-. ((G` w) < (F` w) /\ (F` w) < (H` w)) <-> -. ((G` (v + 1)) < (F` (v + 1)) /\ (F` (v + 1)) < (H` (v + 1)))))
16		fveq2 3724	. . . . . 6 |- (w = A -> (G` w) = (G` A))
17		fveq2 3724	. . . . . 6 |- (w = A -> (F` w) = (F` A))
18	16, 17	breq12d 2631	. . . . 5 |- (w = A -> ((G` w) < (F` w) <-> (G` A) < (F` A)))
19		fveq2 3724	. . . . . 6 |- (w = A -> (H` w) = (H` A))
20	17, 19	breq12d 2631	. . . . 5 |- (w = A -> ((F` w) < (H` w) <-> (F` A) < (H` A)))
21	18, 20	anbi12d 628	. . . 4 |- (w = A -> (((G` w) < (F` w) /\ (F` w) < (H` w)) <-> ((G` A) < (F` A) /\ (F` A) < (H` A))))
22	21	negbid 611	. . 3 |- (w = A -> (-. ((G` w) < (F` w) /\ (F` w) < (H` w)) <-> -. ((G` A) < (F` A) /\ (F` A) < (H` A))))
23		ruclem.0	. . . . . . . 8 |- F:NN-->RR
24		1nn 5934	. . . . . . . 8 |- 1 e. NN
25		ffvelrn 3814	. . . . . . . 8 |- ((F:NN-->RR /\ 1 e. NN) -> (F` 1) e. RR)
26	23, 24, 25	mp2an 697	. . . . . . 7 |- (F` 1) e. RR
27	26	ltp1 5813	. . . . . 6 |- (F` 1) < ((F` 1) + 1)
28		ruclem.1	. . . . . . 7 |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))
29		ruclem.2	. . . . . . 7 |- 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)>.))}
30		ruclem.3	. . . . . . 7 |- G = (1st o. (D seq1 C))
31		ruclem.4	. . . . . . 7 |- H = (2nd o. (D seq1 C))
32	23, 28, 29, 30, 31	ruclem16 7525	. . . . . 6 |- (G` 1) = ((F` 1) + 1)
33	27, 32	breqtrr 2640	. . . . 5 |- (F` 1) < (G` 1)
34	23, 28, 29, 30, 31, 24	ruclem22 7531	. . . . . 6 |- (G` 1) e. RR
35	26, 34	ltnsym 5577	. . . . 5 |- ((F` 1) < (G` 1) -> -. (G` 1) < (F` 1))
36	33, 35	ax-mp 7	. . . 4 |- -. (G` 1) < (F` 1)
37	36	intnanr 692	. . 3 |- -. ((G` 1) < (F` 1) /\ (F` 1) < (H` 1))
38		opreq1 3968	. . . . . . . 8 |- (v = if(v e. NN, v, 1) -> (v + 1) = (if(v e. NN, v, 1) + 1))
39	38	fveq2d 3728	. . . . . . 7 |- (v = if(v e. NN, v, 1) -> (G` (v + 1)) = (G` (if(v e. NN, v, 1) + 1)))
40	38	fveq2d 3728	. . . . . . 7 |- (v = if(v e. NN, v, 1) -> (F` (v + 1)) = (F` (if(v e. NN, v, 1) + 1)))
41	39, 40	breq12d 2631	. . . . . 6 |- (v = if(v e. NN, v, 1) -> ((G` (v + 1)) < (F` (v + 1)) <-> (G` (if(v e. NN, v, 1) + 1)) < (F` (if(v e. NN, v, 1) + 1))))
42	38	fveq2d 3728	. . . . . . 7 |- (v = if(v e. NN, v, 1) -> (H` (v + 1)) = (H` (if(v e. NN, v, 1) + 1)))
43	40, 42	breq12d 2631	. . . . . 6 |- (v = if(v e. NN, v, 1) -> ((F` (v + 1)) < (H` (v + 1)) <-> (F` (if(v e. NN, v, 1) + 1)) < (H` (if(v e. NN, v, 1) + 1))))
44	41, 43	anbi12d 628	. . . . 5 |- (v = if(v e. NN, v, 1) -> (((G` (v + 1)) < (F` (v + 1)) /\ (F` (v + 1)) < (H` (v + 1))) <-> ((G` (if(v e. NN, v, 1) + 1)) < (F` (if(v e. NN, v, 1) + 1)) /\ (F` (if(v e. NN, v, 1) + 1)) < (H` (if(v e. NN, v, 1) + 1)))))
45	44	negbid 611	. . . 4 |- (v = if(v e. NN, v, 1) -> (-. ((G` (v + 1)) < (F` (v + 1)) /\ (F` (v + 1)) < (H` (v + 1))) <-> -. ((G` (if(v e. NN, v, 1) + 1)) < (F` (if(v e. NN, v, 1) + 1)) /\ (F` (if(v e. NN, v, 1) + 1)) < (H` (if(v e. NN, v, 1) + 1)))))
46	24	elimel 2394	. . . . 5 |- if(v e. NN, v, 1) e. NN
47	23, 28, 29, 30, 31, 46	ruclem28 7537	. . . 4 |- -. ((G` (if(v e. NN, v, 1) + 1)) < (F` (if(v e. NN, v, 1) + 1)) /\ (F