Theorem bfplem6 12059

Description: Lemma for bfp 12065. Bound the distance between consecutive elements of the sequence G by applying bfplem5 12058 inductively.

Hypotheses

Ref	Expression
bfp.1	|- X = dom dom M
bfplem.2	|- M e. CMet
bfplem.3	|- F:X-->X
bfplem.4	|- Y e. X
bfplem.5	|- G = ({<.<.a, b>., c>. | ((a e. X /\ b e. X) /\ c = (F` a))} seq1 (NN X. {Y}))
bfplem.6	|- D = (YM(F` Y))
bfplem.7	|- K e. RR+
bfplem.8	|- K < 1
bfplem.9	|- A.x e. X A.y e. X ((F` x)M(F` y)) <_ (K x. (xMy))

Assertion

Ref	Expression
bfplem6	|- (N e. NN -> ((G` N)M(G` (N + 1))) <_ (D x. (K^(N - 1))))

Distinct variable groups:   F,a,b,c,x,y   X,a,b,c,x,y   N,a,b,c,x,y   Y,a,b,c,x,y   x,G,y   x,M,y   x,K,y

Proof of Theorem bfplem6

Step	Hyp	Ref	Expression
1		fveq2 3835	. . . 4 |- (u = 1 -> (G` u) = (G` 1))
2		opreq1 4026	. . . . 5 |- (u = 1 -> (u + 1) = (1 + 1))
3	2	fveq2d 3839	. . . 4 |- (u = 1 -> (G` (u + 1)) = (G` (1 + 1)))
4	1, 3	opreq12d 4036	. . 3 |- (u = 1 -> ((G` u)M(G` (u + 1))) = ((G` 1)M(G` (1 + 1))))
5		opreq1 4026	. . . . 5 |- (u = 1 -> (u - 1) = (1 - 1))
6	5	opreq2d 4034	. . . 4 |- (u = 1 -> (K^(u - 1)) = (K^(1 - 1)))
7	6	opreq2d 4034	. . 3 |- (u = 1 -> (D x. (K^(u - 1))) = (D x. (K^(1 - 1))))
8	4, 7	breq12d 2704	. 2 |- (u = 1 -> (((G` u)M(G` (u + 1))) <_ (D x. (K^(u - 1))) <-> ((G` 1)M(G` (1 + 1))) <_ (D x. (K^(1 - 1)))))
9		fveq2 3835	. . . 4 |- (u = v -> (G` u) = (G` v))
10		opreq1 4026	. . . . 5 |- (u = v -> (u + 1) = (v + 1))
11	10	fveq2d 3839	. . . 4 |- (u = v -> (G` (u + 1)) = (G` (v + 1)))
12	9, 11	opreq12d 4036	. . 3 |- (u = v -> ((G` u)M(G` (u + 1))) = ((G` v)M(G` (v + 1))))
13		opreq1 4026	. . . . 5 |- (u = v -> (u - 1) = (v - 1))
14	13	opreq2d 4034	. . . 4 |- (u = v -> (K^(u - 1)) = (K^(v - 1)))
15	14	opreq2d 4034	. . 3 |- (u = v -> (D x. (K^(u - 1))) = (D x. (K^(v - 1))))
16	12, 15	breq12d 2704	. 2 |- (u = v -> (((G` u)M(G` (u + 1))) <_ (D x. (K^(u - 1))) <-> ((G` v)M(G` (v + 1))) <_ (D x. (K^(v - 1)))))
17		fveq2 3835	. . . 4 |- (u = (v + 1) -> (G` u) = (G` (v + 1)))
18		opreq1 4026	. . . . 5 |- (u = (v + 1) -> (u + 1) = ((v + 1) + 1))
19	18	fveq2d 3839	. . . 4 |- (u = (v + 1) -> (G` (u + 1)) = (G` ((v + 1) + 1)))
20	17, 19	opreq12d 4036	. . 3 |- (u = (v + 1) -> ((G` u)M(G` (u + 1))) = ((G` (v + 1))M(G` ((v + 1) + 1))))
21		opreq1 4026	. . . . 5 |- (u = (v + 1) -> (u - 1) = ((v + 1) - 1))
22	21	opreq2d 4034	. . . 4 |- (u = (v + 1) -> (K^(u - 1)) = (K^((v + 1) - 1)))
23	22	opreq2d 4034	. . 3 |- (u = (v + 1) -> (D x. (K^(u - 1))) = (D x. (K^((v + 1) - 1))))
24	20, 23	breq12d 2704	. 2 |- (u = (v + 1) -> (((G` u)M(G` (u + 1))) <_ (D x. (K^(u - 1))) <-> ((G` (v + 1))M(G` ((v + 1) + 1))) <_ (D x. (K^((v + 1) - 1)))))
25		fveq2 3835	. . . 4 |- (u = N -> (G` u) = (G` N))
26		opreq1 4026	. . . . 5 |- (u = N -> (u + 1) = (N + 1))
27	26	fveq2d 3839	. . . 4 |- (u = N -> (G` (u + 1)) = (G` (N + 1)))
28	25, 27	opreq12d 4036	. . 3 |- (u = N -> ((G` u)M(G` (u + 1))) = ((G` N)M(G` (N + 1))))
29		opreq1 4026	. . . . 5 |- (u = N -> (u - 1) = (N - 1))
30	29	opreq2d 4034	. . . 4 |- (u = N -> (K^(u - 1)) = (K^(N - 1)))
31	30	opreq2d 4034	. . 3 |- (u = N -> (D x. (K^(u - 1))) = (D x. (K^(N - 1))))
32	28, 31	breq12d 2704	. 2 |- (u = N -> (((G` u)M(G` (u + 1))) <_ (D x. (K^(u - 1))) <-> ((G` N)M(G` (N + 1))) <_ (D x. (K^(N - 1)))))
33		bfp.1	. . . . . 6 |- X = dom dom M
34		bfplem.2	. . . . . 6 |- M e. CMet
35		bfplem.3	. . . . . 6 |- F:X-->X
36		bfplem.4	. . . . . 6 |- Y e. X
37		bfplem.5	. . . . . 6 |- G = ({<.<.a, b>., c>. | ((a e. X /\ b e. X) /\ c = (F` a))} seq1 (NN X. {Y}))
38	33, 34, 35, 36, 37	bfplem2 12055	. . . . 5 |- (G` 1) = Y
39		1nn 6079	. . . . . . 7 |- 1 e. NN
40	33, 34, 35, 36, 37	bfplem3 12056	. . . . . . 7 |- (1 e. NN -> (G` (1 + 1)) = (F` (G` 1)))
41	39, 40	ax-mp 7	. . . . . 6 |- (G` (1 + 1)) = (F` (G` 1))
42	38	fveq2i 3838	. . . . . 6 |- (F` (G` 1)) = (F` Y)
43	41, 42	eqtri 1538	. . . . 5 |- (G` (1 + 1)) = (F` Y)
44	38, 43	opreq12i 4031	. . . 4 |- ((G` 1)M(G` (1 + 1))) = (YM(F` Y))
45		bfplem.6	. . . 4 |- D = (YM(F` Y))
46	44, 45	eqtr4i 1541	. . 3 |- ((G` 1)M(G` (1 + 1))) = D
47	33, 34, 35, 36, 37, 45	bfplem4 12057	. . . . 5 |- (D e. RR /\ 0 <_ D)
48	47	pm3.26i 318	. . . 4 |- D e. RR
49		ax1cn 5423	. . . . . . . . 9 |- 1 e. CC
50	49	subidi 5545	. . . . . . . 8 |- (1 - 1) = 0
51	50	opreq2i 4030	. . . . . . 7 |- (K^(1 - 1)) = (K^0)
52		bfplem.7	. . . . . . . . 9 |- K e. RR+
53		rpcn 6196	. . . . . . . . 9 |- (K e. RR+ -> K e. CC)
54	52, 53	ax-mp 7	. . . . . . . 8 |- K e. CC
55		exp0 6766	. . . . . . . 8 |- (K e. CC -> (K^0) = 1)
56	54, 55	ax-mp 7	. . . . . . 7 |- (K^0) = 1
57	51, 56	eqtri 1538	. . . . . 6 |- (K^(1 - 1)) = 1
58	57	opreq2i 4030	. . . . 5 |- (D x. (K^(1 - 1))) = (D x. 1)
59	48	recni 5468	. . . . . 6 |- D e. CC
60	59	mulid1i 5486	. . . . 5 |- (D x. 1) = D
61	58, 60	eqtr2i 1539	. . . 4 |- D = (D x. (K^(1 - 1)))
62		eqle 5725	. . . 4 |- ((D e. RR /\ D = (D x. (K^(1 - 1)))) -> D <_ (D x. (K^(1 - 1))))
63	48, 61, 62	mp2an 701	. . 3 |- D <_ (D x. (K^(1 - 1)))
64	46, 63	eqbrtri 2707	. 2 |- ((G` 1)M(G` (1 + 1))) <_ (D x. (K^(1 - 1)))
65		lemul2aALT 10655	. . . . 5 |- ((((G` v)M(G` (v + 1))) e. RR /\ (D x. (K^(v - 1))) e. RR /\ (K e. RR /\ 0 <_ K)) -> (((G` v)M(G` (v + 1))) <_ (D x. (K^(v - 1))) -> (K x. ((G` v)M(G` (v + 1)))) <_ (K x. (D x. (K^(v - 1))))))
66	33	metcl 8021	. . . . . 6 |- ((M e. Met /\ (G` v) e. X /\ (G` (v + 1)) e. X) -> ((G` v)M(G` (v + 1))) e. RR)
67	34	cmsmeti 8173	. . . . . . 7 |- M e. Met
68	67	a1i 8	. . . . . 6 |- (v e. NN -> M e. Met)
69	33, 34, 35, 36, 37	bfplem1 12054	. . . . . . 7 |- G:NN-->X
70	69	ffvelrni 3929	. . . . . 6 |- (v e. NN -> (G` v) e. X)
71		peano2nn 6080	. . . . . . 7 |- (v e. NN -> (v + 1) e. NN)
72	69	ffvelrni 3929	. . . . . . 7 |- ((v + 1) e. NN -> (G` (v + 1)) e. X)
73	71, 72	syl 10	. . . . . 6 |- (v e. NN -> (G` (v + 1)) e. X)
74	66, 68, 70, 73	syl3anc 864	. . . . 5 |- (v e. NN -> ((G` v)M(G` (v + 1))) e. RR)
75		remulcl 5458	. . . . . 6 |- ((D e. RR /\ (K^(v - 1)) e. RR) -> (D x. (K^(v - 1))) e. RR)
76		reexpcl 6775	. . . . . . 7 |- ((K e. RR /\ (v - 1) e. NN0) -> (K^(v - 1)) e. RR)
77		rpre 6195	. . . . . . . 8 |- (K e. RR+ -> K e. RR)
78	52, 77	ax-mp 7	. . . . . . 7 |- K e. RR
79		nnm1nn0 6344	. . . . . . 7 |- (v e. NN -> (v - 1) e. NN0)
80	76, 78, 79	sylancr 474	. . . . . 6 |- (v e. NN -> (K^(v - 1)) e. RR)
81	75, 48, 80	sylancr 474	. . . . 5 |- (v e. NN -> (D x. (K^(v - 1))) e. RR)
82		rpge0 6200	. . . . . . . 8 |- (K e. RR+ -> 0 <_ K)
83	77, 82	jca 286	. . . . . . 7 |- (K e. RR+ -> (K e. RR /\ 0 <_ K))
84	52, 83	ax-mp 7	. . . . . 6 |- (K e. RR /\ 0 <_ K)
85	84	a1i 8	. . . . 5 |- (v e. NN -> (K e. RR /\ 0 <_ K))
86	65, 74, 81, 85	syl3anc 864	. . . 4 |- (v e. NN -> (((G` v)M(G` (v + 1))) <_ (D x. (K^(v - 1))) -> (K x. ((G` v)M(G` (v + 1)))) <_ (K x. (D x. (K^(v - 1))))))
87		addsub 5538	. . . . . . . . . 10 |- ((v e. CC /\ 1 e. CC /\ 1 e. CC) -> ((v + 1) - 1) = ((v - 1) + 1))
88		nncn 6075	. . . . . . . . . 10 |- (v e. NN -> v e. CC)
89	49	a1i 8	. . . . . . . . . 10 |- (v e. NN -> 1 e. CC)
90	87, 88, 89, 89	syl3anc 864	. . . . . . . . 9 |- (v e. NN -> ((v + 1) - 1) = ((v - 1) + 1))
91	90	opreq2d 4034	. . . . . . . 8 |- (v e. NN -> (K^((v + 1) - 1)) = (K^((v - 1) + 1)))
92		expp1 6769	. . . . . . . . 9 |- ((K e. CC /\ (v - 1) e. NN0) -> (K^((v - 1) + 1)) = ((K^(v - 1)) x. K))
93	92, 54, 79	sylancr 474	. . . . . . . 8 |- (v e. NN -> (K^((v - 1) + 1)) = ((K^(v - 1)) x. K))
94		mulcom 5460	. . . . . . . . 9 |- (((K^(v - 1)) e. CC /\ K e. CC) -> ((K^(v - 1)) x. K) = (K x. (K^(v - 1))))
95	80	recnd 5469	. . . . . . . . 9 |- (v e. NN -> (K^(v - 1)) e. CC)
96	94, 95, 54	sylancl 11785	. . . . . . . 8 |- (v e. NN -> ((K^(v - 1)) x. K) = (K x. (K^(v - 1))))
97	91, 93, 96	3eqtrd 1554	. . . . . . 7 |- (v e. NN -> (K^((v + 1) - 1)) = (K x. (K^(v - 1))))
98	97	opreq2d 4034	. . . . . 6 |- (v e. NN -> (D x. (K^((v + 1) - 1))) = (D x. (K x. (K^(v - 1)))))
99		mul12 5572	. . . . . . 7 |- ((D e. CC /\ K e. CC /\ (K^(v - 1)) e. CC) -> (D x. (K x. (K^(v - 1)))) = (K x. (D x. (K^(v - 1)))))
100	59	a1i 8	. . . . . . 7 |- (v e. NN -> D e. CC)
101	54	a1i 8	. . . . . . 7 |- (v e. NN -> K e. CC)
102	99, 100, 101, 95	syl3anc 864	. . . . . 6 |- (v e. NN -> (D x. (K x. (K^(v - 1)))) = (K x. (D x. (K^(v - 1)))))
103	98, 102	eqtrd 1550	. . . . 5 |- (v e. NN -> (D x. (K^((v + 1) - 1))) = (K x. (D x. (K^(v - 1)))))
104	103	breq2d 2703	. . . 4 |- (v e. NN -> ((K x. ((G` v)M(G` (v + 1)))) <_ (D x. (K^((v + 1) - 1))) <-> (K x. ((G` v)M(G` (v + 1)))) <_ (K x. (D x. (K^(v - 1))))))
105	86, 104	sylibrd 202	. . 3 |- (v e. NN -> (((G` v)M(G` (v + 1))) <_ (D x. (K^(v - 1))) -> (K x. ((G` v)M(G` (v + 1)))) <_ (D x. (K^((v + 1) - 1)))))
106		bfplem.8	. . . . 5 |- K < 1
107		bfplem.9	. . . . 5 |- A.x e. X A.y e. X ((F` x)M(F` y)) <_ (K x. (xMy))
108	33, 34, 35, 36, 37, 45, 52, 106, 107	bfplem5 12058	. . . 4 |- (v e. NN -> ((G` (v + 1))M(G` ((v + 1) + 1))) <_ (K x. ((G` v)M(G` (v + 1)))))
109		letr 5679	. . . . 5 |- ((((G` (v + 1))M(G` ((v + 1) + 1))) e. RR /\ (K x. ((G` v)M(G` (v + 1)))) e. RR /\ (D x. (K^((v + 1) - 1))) e. RR) -> ((((G` (v + 1))M(G` ((v + 1) + 1))) <_ (K x. ((G` v)M(G` (v + 1)))) /\ (K x. ((G` v)M(G` (v + 1)))) <_ (D x. (K^((v + 1) - 1)))) -> ((G` (v + 1))M(G` ((v + 1) + 1))) <_ (D x. (K^((v + 1) - 1)))))
110	33	metcl 8021	. . . . . . 7 |- ((M e. Met /\ (G` (v + 1)) e. X /\ (G` ((v + 1) + 1)) e. X) -> ((G` (v + 1))M(G` ((v + 1) + 1))) e. RR)
111	67	a1i 8	. . . . . . 7 |- ((v + 1) e. NN -> M e. Met)
112		peano2nn 6080	. . . . . . . 8 |- ((v + 1) e. NN -> ((v + 1) + 1) e. NN)
113	69	ffvelrni 3929	. . . . . . . 8 |- (((v + 1) + 1) e. NN -> (G` ((v + 1) + 1)) e. X)
114	112, 113	syl 10	. . . . . . 7 |- ((v + 1) e. NN -> (G` ((v + 1) + 1)) e. X)
115	110, 111, 72, 114	syl3anc 864	. . . . . 6 |- ((v + 1) e. NN -> ((G` (v + 1))M(G` ((v + 1) + 1))) e. RR)
116	71, 115	syl 10	. . . . 5 |- (v e. NN -> ((G` (v + 1))M(G` ((v + 1) + 1))) e. RR)
117		remulcl 5458	. . . . . 6 |- ((K e. RR /\ ((G` v)M(G` (v + 1))) e. RR) -> (K x. ((G` v)M(G` (v + 1)))) e. RR)
118	117, 78, 74	sylancr 474	. . . . 5 |- (v e. NN -> (K x. ((G` v)M(G` (v + 1)))) e. RR)
119		remulcl 5458	. . . . . 6 |- ((D e. RR /\ (K^((v + 1) - 1)) e. RR) -> (D x. (K^((v + 1) - 1))) e. RR)
120		reexpcl 6775	. . . . . . 7 |- ((K e. RR /\ ((v + 1) - 1) e. NN0) -> (K^((v + 1) - 1)) e. RR)
121		nnm1nn0 6344	. . . . . . . 8 |- ((v + 1) e. NN -> ((v + 1) - 1) e. NN0)
122	71, 121	syl 10	. . . . . . 7 |- (v e. NN -> ((v + 1) - 1) e. NN0)
123	120, 78, 122	sylancr 474	. . . . . 6 |- (v e. NN -> (K^((v + 1) - 1)) e. RR)
124	119, 48, 123	sylancr 474	. . . . 5 |- (v e. NN -> (D x. (K^((v + 1) - 1))) e. RR)
125	109, 116, 118, 124	syl3anc 864	. . . 4 |- (v e. NN -> ((((G` (v + 1))M(G` ((v + 1) + 1))) <_ (K x. ((G` v)M(G` (v + 1)))) /\ (K x. ((G` v)M(G` (v + 1)))) <_ (D x. (K^((v + 1) - 1)))) -> ((G` (v + 1))M(G` ((v + 1) + 1))) <_ (D x. (K^((v + 1) - 1)))))
126	108, 125	mpand 705	. . 3 |- (v e. NN -> ((K x. ((G` v)M(G` (v + 1)))) <_ (D x. (K^((v + 1) - 1))) -> ((G` (v + 1))M(G` ((v + 1) + 1))) <_ (D x. (K^((v + 1) - 1)))))
127	105, 126	syld 27	. 2 |- (v e. NN -> (((G` v)M(G` (v + 1))) <_ (D x. (K^(v - 1))) -> ((G` (v + 1))M(G` ((v + 1) + 1))) <_ (D x. (K^((v + 1) - 1)))))
128	8, 16, 24, 32, 64, 127	nnind 6082	1 |- (N e. NN -> ((G` N)M(G` (N + 1))) <_ (D x. (K^(N - 1))))

Syntax hints:   -> wi 3   /\ wa 221   = wceq 992   e. wcel 994  A.wral 1691  {csn 2467   class class class wbr 2692   X. cxp 3249  dom cdm 3251  -->wf 3259  ` cfv 3263  (class class class)co 4021  {copab2 4022  CCcc 5386  RRcr 5387  0cc0 5388  1c1 5389   + caddc 5391   x. cmul 5393   - cmin 5446   <_ cle 5449  NNcn 5450  NN0cn0 5451  RR+crp 5454   < clt 5640   seq1 cseq1 6672  ^cexp 6763  Metcme 7999  CMetcms 8132

This theorem is referenced by:  bfplem7 12060

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089  ax-inf2 4770

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-nel 1631  df-ral 1695  df-rex 1696  df-reu 1697  df-rab 1698  df-v 1858  df-sbc 1987  df-csb 2052  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-pss 2107  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-int 2601  df-iun 2635  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-opr 4023  df-oprab 4024  df-1st 4140  df-2nd 4141  df-rdg 4233  df-1o 4269  df-oadd 4271  df-omul 4272  df-er 4401  df-ec 4403  df-qs 4406  df-en 4509  df-dom 4510  df-sdom 4511  df-ni 5154  df-pli 5155  df-mi 5156  df-lti 5157  df-plpq 5189  df-mpq 5190  df-enq 5191  df-nq 5192  df-plq 5193  df-mq 5194  df-rq 5195  df-ltq 5196  df-1q 5197  df-np 5240  df-1p 5241  df-plp 5242  df-mp 5243  df-ltp 5244  df-plpr 5318  df-mpr 5319  df-enr 5320  df-nr 5321  df-plr 5322  df-mr 5323  df-ltr 5324  df-0r 5325  df-1r 5326  df-m1r 5327  df-c 5394  df-0 5395  df-1 5396  df-i 5397  df-r 5398  df-plus 5399  df-mul 5400  df-lt 5401  df-sub 5510  df-neg 5512  df-pnf 5641  df-mnf 5642  df-xr 5643  df-ltxr 5644  df-le 5645  df-n 6070  df-2 6116  df-rp 6191  df-n0 6268  df-z 6304  df-seq1 6673  df-exp 6764  df-met 8003  df-cmet 8135

Copyright terms: Public domain