Theorem ruclem32 7492

Description: Lemma for ruc 7500. All values of function G are less than all values of function H.

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
ruclem.b	|- B e. NN

Assertion

Ref	Expression
ruclem32	|- (G` A) < (H` B)

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

Proof of Theorem ruclem32

Step	Hyp	Ref	Expression
1		ruclem.b	. . . 4 |- B e. NN
2		opreq2 3960	. . . . . . 7 |- (w = 1 -> (A + w) = (A + 1))
3	2	fveq2d 3719	. . . . . 6 |- (w = 1 -> (G` (A + w)) = (G` (A + 1)))
4	3	breq2d 2625	. . . . 5 |- (w = 1 -> ((G` A) < (G` (A + w)) <-> (G` A) < (G` (A + 1))))
5		opreq2 3960	. . . . . . 7 |- (w = v -> (A + w) = (A + v))
6	5	fveq2d 3719	. . . . . 6 |- (w = v -> (G` (A + w)) = (G` (A + v)))
7	6	breq2d 2625	. . . . 5 |- (w = v -> ((G` A) < (G` (A + w)) <-> (G` A) < (G` (A + v))))
8		opreq2 3960	. . . . . . 7 |- (w = (v + 1) -> (A + w) = (A + (v + 1)))
9	8	fveq2d 3719	. . . . . 6 |- (w = (v + 1) -> (G` (A + w)) = (G` (A + (v + 1))))
10	9	breq2d 2625	. . . . 5 |- (w = (v + 1) -> ((G` A) < (G` (A + w)) <-> (G` A) < (G` (A + (v + 1)))))
11		opreq2 3960	. . . . . . 7 |- (w = B -> (A + w) = (A + B))
12	11	fveq2d 3719	. . . . . 6 |- (w = B -> (G` (A + w)) = (G` (A + B)))
13	12	breq2d 2625	. . . . 5 |- (w = B -> ((G` A) < (G` (A + w)) <-> (G` A) < (G` (A + B))))
14		ruclem.0	. . . . . 6 |- F:NN-->RR
15		ruclem.1	. . . . . 6 |- C = ({<.1, <.((F` 1) + 1), ((F` 1) + 2)>.>.} u. (F |` (NN \ {1})))
16		ruclem.2	. . . . . 6 |- 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)>.))}
17		ruclem.3	. . . . . 6 |- G = (1st o. (D seq1 C))
18		ruclem.4	. . . . . 6 |- H = (2nd o. (D seq1 C))
19		ruclem28.a	. . . . . 6 |- A e. NN
20	14, 15, 16, 17, 18, 19	ruclem26 7486	. . . . 5 |- (G` A) < (G` (A + 1))
21		opreq2 3960	. . . . . . . . 9 |- (v = if(v e. NN, v, 1) -> (A + v) = (A + if(v e. NN, v, 1)))
22	21	fveq2d 3719	. . . . . . . 8 |- (v = if(v e. NN, v, 1) -> (G` (A + v)) = (G` (A + if(v e. NN, v, 1))))
23	22	breq2d 2625	. . . . . . 7 |- (v = if(v e. NN, v, 1) -> ((G` A) < (G` (A + v)) <-> (G` A) < (G` (A + if(v e. NN, v, 1)))))
24		opreq1 3959	. . . . . . . . . 10 |- (v = if(v e. NN, v, 1) -> (v + 1) = (if(v e. NN, v, 1) + 1))
25	24	opreq2d 3967	. . . . . . . . 9 |- (v = if(v e. NN, v, 1) -> (A + (v + 1)) = (A + (if(v e. NN, v, 1) + 1)))
26	25	fveq2d 3719	. . . . . . . 8 |- (v = if(v e. NN, v, 1) -> (G` (A + (v + 1))) = (G` (A + (if(v e. NN, v, 1) + 1))))
27	26	breq2d 2625	. . . . . . 7 |- (v = if(v e. NN, v, 1) -> ((G` A) < (G` (A + (v + 1))) <-> (G` A) < (G` (A + (if(v e. NN, v, 1) + 1)))))
28	23, 27	imbi12d 625	. . . . . 6 |- (v = if(v e. NN, v, 1) -> (((G` A) < (G` (A + v)) -> (G` A) < (G` (A + (v + 1)))) <-> ((G` A) < (G` (A + if(v e. NN, v, 1))) -> (G` A) < (G` (A + (if(v e. NN, v, 1) + 1))))))
29		1nn 5890	. . . . . . . 8 |- 1 e. NN
30	29	elimel 2390	. . . . . . 7 |- if(v e. NN, v, 1) e. NN
31	14, 15, 16, 17, 18, 19, 30	ruclem30 7490	. . . . . 6 |- ((G` A) < (G` (A + if(v e. NN, v, 1))) -> (G` A) < (G` (A + (if(v e. NN, v, 1) + 1))))
32	28, 31	dedth 2379	. . . . 5 |- (v e. NN -> ((G` A) < (G` (A + v)) -> (G` A) < (G` (A + (v + 1)))))
33	4, 7, 10, 13, 20, 32	nnind 5893	. . . 4 |- (B e. NN -> (G` A) < (G` (A + B)))
34	1, 33	ax-mp 7	. . 3 |- (G` A) < (G` (A + B))
35		nnaddclt 5896	. . . . 5 |- ((A e. NN /\ B e. NN) -> (A + B) e. NN)
36	19, 1, 35	mp2an 696	. . . 4 |- (A + B) e. NN
37	14, 15, 16, 17, 18, 36	ruclem25 7485	. . 3 |- (G` (A + B)) < (H` (A + B))
38	14, 15, 16, 17, 18, 19	ruclem22 7482	. . . 4 |- (G` A) e. RR
39	14, 15, 16, 17, 18, 36	ruclem22 7482	. . . 4 |- (G` (A + B)) e. RR
40	14, 15, 16, 17, 18, 36	ruclem23 7483	. . . 4 |- (H` (A + B)) e. RR
41	38, 39, 40	lttr 5567	. . 3 |- (((G` A) < (G` (A + B)) /\ (G` (A + B)) < (H` (A + B))) -> (G` A) < (H` (A + B)))
42	34, 37, 41	mp2an 696	. 2 |- (G` A) < (H` (A + B))
43		opreq1 3959	. . . . . 6 |- (w = 1 -> (w + B) = (1 + B))
44	43	fveq2d 3719	. . . . 5 |- (w = 1 -> (H` (w + B)) = (H` (1 + B)))
45	44	breq1d 2624	. . . 4 |- (w = 1 -> ((H` (w + B)) < (H` B) <-> (H` (1 + B)) < (H` B)))
46		opreq1 3959	. . . . . 6 |- (w = v -> (w + B) = (v + B))
47	46	fveq2d 3719	. . . . 5 |- (w = v -> (H` (w + B)) = (H` (v + B)))
48	47	breq1d 2624	. . . 4 |- (w = v -> ((H` (w + B)) < (H` B) <-> (H` (v + B)) < (H` B)))
49		opreq1 3959	. . . . . 6 |- (w = (v + 1) -> (w + B) = ((v + 1) + B))
50	49	fveq2d 3719	. . . . 5 |- (w = (v + 1) -> (H` (w + B)) = (H` ((v + 1) + B)))
51	50	breq1d 2624	. . . 4 |- (w = (v + 1) -> ((H` (w + B)) < (H` B) <-> (H` ((v + 1) + B)) < (H` B)))
52		opreq1 3959	. . . . . 6 |- (w = A -> (w + B) = (A + B))
53	52	fveq2d 3719	. . . . 5 |- (w = A -> (H` (w + B)) = (H` (A + B)))
54	53	breq1d 2624	. . . 4 |- (w = A -> ((H` (w + B)) < (H` B) <-> (H` (A + B)) < (H` B)))
55		ax1cn 5249	. . . . . . 7 |- 1 e. CC
56	1	nncn 5888	. . . . . . 7 |- B e. CC
57	55, 56	addcom 5302	. . . . . 6 |- (1 + B) = (B + 1)
58	57	fveq2i 3718	. . . . 5 |- (H` (1 + B)) = (H` (B + 1))
59	14, 15, 16, 17, 18, 1	ruclem27 7487	. . . . 5 |- (H` (B + 1)) < (H` B)
60	58, 59	eqbrtr 2629	. . . 4 |- (H` (1 + B)) < (H` B)
61		opreq1 3959	. . . . . . . 8 |- (v = if(v <