bfplem1 - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > bfplem1		Structured version Visualization version GIF version

Theorem bfplem1 33621

Description: Lemma for bfp 33623. The sequence 𝐺, which simply starts from any point in the space and iterates 𝐹, satisfies the property that the distance from 𝐺(𝑛) to 𝐺(𝑛 + 1) decreases by at least 𝐾 after each step. Thus, the total distance from any 𝐺(𝑖) to 𝐺(𝑗) is bounded by a geometric series, and the sequence is Cauchy. Therefore, it converges to a point ((⇝_𝑡‘𝐽)‘𝐺) since the space is complete. (Contributed by Jeff Madsen, 17-Jun-2014.)

**Hypotheses**
Ref	Expression
bfp.2	⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
bfp.3	⊢ (𝜑 → 𝑋 ≠ ∅)
bfp.4	⊢ (𝜑 → 𝐾 ∈ ℝ⁺)
bfp.5	⊢ (𝜑 → 𝐾 < 1)
bfp.6	⊢ (𝜑 → 𝐹:𝑋⟶𝑋)
bfp.7	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))
bfp.8	⊢ 𝐽 = (MetOpen‘𝐷)
bfp.9	⊢ (𝜑 → 𝐴 ∈ 𝑋)
bfp.10	⊢ 𝐺 = seq1((𝐹 ∘ 1^st ), (ℕ × {𝐴}))

**Assertion**
Ref	Expression
bfplem1	⊢ (𝜑 → 𝐺(⇝_𝑡‘𝐽)((⇝_𝑡‘𝐽)‘𝐺))

Distinct variable groups: 𝑥,𝑦,𝐷 𝑥,𝐺,𝑦 𝑥,𝐽,𝑦 𝜑,𝑥,𝑦 𝑥,𝐹,𝑦 𝑥,𝐾,𝑦 𝑥,𝑋,𝑦 Allowed substitution hints: 𝐴(𝑥,𝑦)

Proof of Theorem bfplem1 Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bfp.2	. . 3 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
2		cmetmet 23084	. . . . 5 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
3	1, 2	syl 17	. . . 4 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
4		nnuz 11723	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
5		bfp.10	. . . . 5 ⊢ 𝐺 = seq1((𝐹 ∘ 1^st ), (ℕ × {𝐴}))
6		1zzd 11408	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
7		bfp.9	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
8		bfp.6	. . . . 5 ⊢ (𝜑 → 𝐹:𝑋⟶𝑋)
9	4, 5, 6, 7, 8	algrf 15286	. . . 4 ⊢ (𝜑 → 𝐺:ℕ⟶𝑋)
10	8, 7	ffvelrnd 6360	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝑋)
11		metcl 22137	. . . . . 6 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (𝐹‘𝐴) ∈ 𝑋) → (𝐴𝐷(𝐹‘𝐴)) ∈ ℝ)
12	3, 7, 10, 11	syl3anc 1326	. . . . 5 ⊢ (𝜑 → (𝐴𝐷(𝐹‘𝐴)) ∈ ℝ)
13		bfp.4	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℝ⁺)
14	12, 13	rerpdivcld 11903	. . . 4 ⊢ (𝜑 → ((𝐴𝐷(𝐹‘𝐴)) / 𝐾) ∈ ℝ)
15		bfp.5	. . . 4 ⊢ (𝜑 → 𝐾 < 1)
16		fveq2 6191	. . . . . . . . 9 ⊢ (𝑗 = 1 → (𝐺‘𝑗) = (𝐺‘1))
17		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑗 = 1 → (𝑗 + 1) = (1 + 1))
18	17	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑗 = 1 → (𝐺‘(𝑗 + 1)) = (𝐺‘(1 + 1)))
19	16, 18	oveq12d 6668	. . . . . . . 8 ⊢ (𝑗 = 1 → ((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) = ((𝐺‘1)𝐷(𝐺‘(1 + 1))))
20		oveq2 6658	. . . . . . . . 9 ⊢ (𝑗 = 1 → (𝐾↑𝑗) = (𝐾↑1))
21	20	oveq2d 6666	. . . . . . . 8 ⊢ (𝑗 = 1 → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗)) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑1)))
22	19, 21	breq12d 4666	. . . . . . 7 ⊢ (𝑗 = 1 → (((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗)) ↔ ((𝐺‘1)𝐷(𝐺‘(1 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑1))))
23	22	imbi2d 330	. . . . . 6 ⊢ (𝑗 = 1 → ((𝜑 → ((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗))) ↔ (𝜑 → ((𝐺‘1)𝐷(𝐺‘(1 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑1)))))
24		fveq2 6191	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → (𝐺‘𝑗) = (𝐺‘𝑘))
25		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1))
26	25	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → (𝐺‘(𝑗 + 1)) = (𝐺‘(𝑘 + 1)))
27	24, 26	oveq12d 6668	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → ((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) = ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))))
28		oveq2 6658	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → (𝐾↑𝑗) = (𝐾↑𝑘))
29	28	oveq2d 6666	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗)) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)))
30	27, 29	breq12d 4666	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗)) ↔ ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘))))
31	30	imbi2d 330	. . . . . 6 ⊢ (𝑗 = 𝑘 → ((𝜑 → ((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗))) ↔ (𝜑 → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)))))
32		fveq2 6191	. . . . . . . . 9 ⊢ (𝑗 = (𝑘 + 1) → (𝐺‘𝑗) = (𝐺‘(𝑘 + 1)))
33		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑗 = (𝑘 + 1) → (𝑗 + 1) = ((𝑘 + 1) + 1))
34	33	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑗 = (𝑘 + 1) → (𝐺‘(𝑗 + 1)) = (𝐺‘((𝑘 + 1) + 1)))
35	32, 34	oveq12d 6668	. . . . . . . 8 ⊢ (𝑗 = (𝑘 + 1) → ((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) = ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))))
36		oveq2 6658	. . . . . . . . 9 ⊢ (𝑗 = (𝑘 + 1) → (𝐾↑𝑗) = (𝐾↑(𝑘 + 1)))
37	36	oveq2d 6666	. . . . . . . 8 ⊢ (𝑗 = (𝑘 + 1) → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗)) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))
38	35, 37	breq12d 4666	. . . . . . 7 ⊢ (𝑗 = (𝑘 + 1) → (((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗)) ↔ ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))))
39	38	imbi2d 330	. . . . . 6 ⊢ (𝑗 = (𝑘 + 1) → ((𝜑 → ((𝐺‘𝑗)𝐷(𝐺‘(𝑗 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑗))) ↔ (𝜑 → ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))))
40	12	leidd 10594	. . . . . . 7 ⊢ (𝜑 → (𝐴𝐷(𝐹‘𝐴)) ≤ (𝐴𝐷(𝐹‘𝐴)))
41	4, 5, 6, 7	algr0 15285	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘1) = 𝐴)
42		1nn 11031	. . . . . . . . . 10 ⊢ 1 ∈ ℕ
43	4, 5, 6, 7, 8	algrp1 15287	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 ∈ ℕ) → (𝐺‘(1 + 1)) = (𝐹‘(𝐺‘1)))
44	42, 43	mpan2 707	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘(1 + 1)) = (𝐹‘(𝐺‘1)))
45	41	fveq2d 6195	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐺‘1)) = (𝐹‘𝐴))
46	44, 45	eqtrd 2656	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(1 + 1)) = (𝐹‘𝐴))
47	41, 46	oveq12d 6668	. . . . . . 7 ⊢ (𝜑 → ((𝐺‘1)𝐷(𝐺‘(1 + 1))) = (𝐴𝐷(𝐹‘𝐴)))
48	13	rpred 11872	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℝ)
49	48	recnd 10068	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℂ)
50	49	exp1d 13003	. . . . . . . . 9 ⊢ (𝜑 → (𝐾↑1) = 𝐾)
51	50	oveq2d 6666	. . . . . . . 8 ⊢ (𝜑 → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑1)) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · 𝐾))
52	12	recnd 10068	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷(𝐹‘𝐴)) ∈ ℂ)
53	13	rpne0d 11877	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≠ 0)
54	52, 49, 53	divcan1d 10802	. . . . . . . 8 ⊢ (𝜑 → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · 𝐾) = (𝐴𝐷(𝐹‘𝐴)))
55	51, 54	eqtrd 2656	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑1)) = (𝐴𝐷(𝐹‘𝐴)))
56	40, 47, 55	3brtr4d 4685	. . . . . 6 ⊢ (𝜑 → ((𝐺‘1)𝐷(𝐺‘(1 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑1)))
57	9	ffvelrnda 6359	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ 𝑋)
58		peano2nn 11032	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
59		ffvelrn 6357	. . . . . . . . . . . . 13 ⊢ ((𝐺:ℕ⟶𝑋 ∧ (𝑘 + 1) ∈ ℕ) → (𝐺‘(𝑘 + 1)) ∈ 𝑋)
60	9, 58, 59	syl2an 494	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘(𝑘 + 1)) ∈ 𝑋)
61	57, 60	jca 554	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝑘) ∈ 𝑋 ∧ (𝐺‘(𝑘 + 1)) ∈ 𝑋))
62		bfp.7	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))
63	62	ralrimivva 2971	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))
64	63	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))
65		fveq2 6191	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐺‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑘)))
66	65	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐺‘𝑘) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘𝑦)))
67		oveq1 6657	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝐺‘𝑘) → (𝑥𝐷𝑦) = ((𝐺‘𝑘)𝐷𝑦))
68	67	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐺‘𝑘) → (𝐾 · (𝑥𝐷𝑦)) = (𝐾 · ((𝐺‘𝑘)𝐷𝑦)))
69	66, 68	breq12d 4666	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐺‘𝑘) → (((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)) ↔ ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘𝑦)) ≤ (𝐾 · ((𝐺‘𝑘)𝐷𝑦))))
70		fveq2 6191	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘(𝑘 + 1)) → (𝐹‘𝑦) = (𝐹‘(𝐺‘(𝑘 + 1))))
71	70	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐺‘(𝑘 + 1)) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘𝑦)) = ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))))
72		oveq2 6658	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘(𝑘 + 1)) → ((𝐺‘𝑘)𝐷𝑦) = ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))))
73	72	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐺‘(𝑘 + 1)) → (𝐾 · ((𝐺‘𝑘)𝐷𝑦)) = (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))))
74	71, 73	breq12d 4666	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐺‘(𝑘 + 1)) → (((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘𝑦)) ≤ (𝐾 · ((𝐺‘𝑘)𝐷𝑦)) ↔ ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))))))
75	69, 74	rspc2v 3322	. . . . . . . . . . 11 ⊢ (((𝐺‘𝑘) ∈ 𝑋 ∧ (𝐺‘(𝑘 + 1)) ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))))))
76	61, 64, 75	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))))
77	3	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋))
78	8	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:𝑋⟶𝑋)
79	78, 57	ffvelrnd 6360	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝐺‘𝑘)) ∈ 𝑋)
80	78, 60	ffvelrnd 6360	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝐺‘(𝑘 + 1))) ∈ 𝑋)
81		metcl 22137	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘(𝐺‘𝑘)) ∈ 𝑋 ∧ (𝐹‘(𝐺‘(𝑘 + 1))) ∈ 𝑋) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ∈ ℝ)
82	77, 79, 80, 81	syl3anc 1326	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ∈ ℝ)
83	48	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐾 ∈ ℝ)
84		metcl 22137	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐺‘𝑘) ∈ 𝑋 ∧ (𝐺‘(𝑘 + 1)) ∈ 𝑋) → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ∈ ℝ)
85	77, 57, 60, 84	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ∈ ℝ)
86	83, 85	remulcld 10070	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ∈ ℝ)
87	14	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝐴)) / 𝐾) ∈ ℝ)
88	58	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
89	88	nnnn0d 11351	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ₀)
90	83, 89	reexpcld 13025	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐾↑(𝑘 + 1)) ∈ ℝ)
91	87, 90	remulcld 10070	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))) ∈ ℝ)
92		letr 10131	. . . . . . . . . . 11 ⊢ ((((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ∈ ℝ ∧ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ∈ ℝ ∧ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))) ∈ ℝ) → ((((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ∧ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))))
93	82, 86, 91, 92	syl3anc 1326	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ∧ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))))
94	76, 93	mpand 711	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))) → ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))))
95		nnnn0 11299	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
96		reexpcl 12877	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℝ ∧ 𝑘 ∈ ℕ₀) → (𝐾↑𝑘) ∈ ℝ)
97	48, 95, 96	syl2an 494	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐾↑𝑘) ∈ ℝ)
98	87, 97	remulcld 10070	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) ∈ ℝ)
99	13	rpgt0d 11875	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 𝐾)
100	99	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 < 𝐾)
101		lemul1 10875	. . . . . . . . . . 11 ⊢ ((((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ∈ ℝ ∧ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) ∈ ℝ ∧ (𝐾 ∈ ℝ ∧ 0 < 𝐾)) → (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) ↔ (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) · 𝐾) ≤ ((((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) · 𝐾)))
102	85, 98, 83, 100, 101	syl112anc 1330	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) ↔ (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) · 𝐾) ≤ ((((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) · 𝐾)))
103	85	recnd 10068	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ∈ ℂ)
104	49	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐾 ∈ ℂ)
105	103, 104	mulcomd 10061	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) · 𝐾) = (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))))
106	87	recnd 10068	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝐴)) / 𝐾) ∈ ℂ)
107	97	recnd 10068	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐾↑𝑘) ∈ ℂ)
108	106, 107, 104	mulassd 10063	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) · 𝐾) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · ((𝐾↑𝑘) · 𝐾)))
109		expp1 12867	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (𝐾↑(𝑘 + 1)) = ((𝐾↑𝑘) · 𝐾))
110	49, 95, 109	syl2an 494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐾↑(𝑘 + 1)) = ((𝐾↑𝑘) · 𝐾))
111	110	oveq2d 6666	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · ((𝐾↑𝑘) · 𝐾)))
112	108, 111	eqtr4d 2659	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) · 𝐾) = (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))
113	105, 112	breq12d 4666	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) · 𝐾) ≤ ((((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) · 𝐾) ↔ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))))
114	102, 113	bitrd 268	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) ↔ (𝐾 · ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))))
115	4, 5, 6, 7, 8	algrp1 15287	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘(𝑘 + 1)) = (𝐹‘(𝐺‘𝑘)))
116	4, 5, 6, 7, 8	algrp1 15287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ) → (𝐺‘((𝑘 + 1) + 1)) = (𝐹‘(𝐺‘(𝑘 + 1))))
117	58, 116	sylan2 491	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘((𝑘 + 1) + 1)) = (𝐹‘(𝐺‘(𝑘 + 1))))
118	115, 117	oveq12d 6668	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) = ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))))
119	118	breq1d 4663	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))) ↔ ((𝐹‘(𝐺‘𝑘))𝐷(𝐹‘(𝐺‘(𝑘 + 1)))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))))
120	94, 114, 119	3imtr4d 283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) → ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1)))))
121	120	expcom 451	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝜑 → (((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)) → ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))))
122	121	a2d 29	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝜑 → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘))) → (𝜑 → ((𝐺‘(𝑘 + 1))𝐷(𝐺‘((𝑘 + 1) + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑(𝑘 + 1))))))
123	23, 31, 39, 31, 56, 122	nnind 11038	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝜑 → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘))))
124	123	impcom 446	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝑘)𝐷(𝐺‘(𝑘 + 1))) ≤ (((𝐴𝐷(𝐹‘𝐴)) / 𝐾) · (𝐾↑𝑘)))
125	3, 9, 14, 13, 15, 124	geomcau 33555	. . 3 ⊢ (𝜑 → 𝐺 ∈ (Cau‘𝐷))
126		bfp.8	. . . 4 ⊢ 𝐽 = (MetOpen‘𝐷)
127	126	cmetcau 23087	. . 3 ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐺 ∈ (Cau‘𝐷)) → 𝐺 ∈ dom (⇝_𝑡‘𝐽))
128	1, 125, 127	syl2anc 693	. 2 ⊢ (𝜑 → 𝐺 ∈ dom (⇝_𝑡‘𝐽))
129		metxmet 22139	. . . 4 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
130	126	methaus 22325	. . . 4 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus)
131	3, 129, 130	3syl 18	. . 3 ⊢ (𝜑 → 𝐽 ∈ Haus)
132		lmfun 21185	. . 3 ⊢ (𝐽 ∈ Haus → Fun (⇝_𝑡‘𝐽))
133		funfvbrb 6330	. . 3 ⊢ (Fun (⇝_𝑡‘𝐽) → (𝐺 ∈ dom (⇝_𝑡‘𝐽) ↔ 𝐺(⇝_𝑡‘𝐽)((⇝_𝑡‘𝐽)‘𝐺)))
134	131, 132, 133	3syl 18	. 2 ⊢ (𝜑 → (𝐺 ∈ dom (⇝_𝑡‘𝐽) ↔ 𝐺(⇝_𝑡‘𝐽)((⇝_𝑡‘𝐽)‘𝐺)))
135	128, 134	mpbid 222	1 ⊢ (𝜑 → 𝐺(⇝_𝑡‘𝐽)((⇝_𝑡‘𝐽)‘𝐺))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∅c0 3915 {csn 4177 class class class wbr 4653 × cxp 5112 dom cdm 5114 ∘ ccom 5118 Fun wfun 5882 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 1^st c1st 7166 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 / cdiv 10684 ℕcn 11020 ℕ₀cn0 11292 ℝ⁺crp 11832 seqcseq 12801 ↑cexp 12860 ∞Metcxmt 19731 Metcme 19732 MetOpencmopn 19736 ⇝_𝑡clm 21030 Hauscha 21112 Caucca 23051 CMetcms 23052

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-rest 16083 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-top 20699 df-topon 20716 df-bases 20750 df-ntr 20824 df-nei 20902 df-lm 21033 df-haus 21119 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-cfil 23053 df-cau 23054 df-cmet 23055

This theorem is referenced by: bfplem2 33622

W3C validator