Axiom ax-caucvg 7999

Description: Completeness. Axiom for real and complex numbers, justified by Theorem axcaucvg 7967.

A Cauchy sequence (as defined here, which has a rate convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within 1 / 𝑛 of the nth term.

This axiom should not be used directly; instead use caucvgre 11146 (which is the same, but stated in terms of the ℕ and 1 / 𝑛 notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ax-caucvg.n	⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
ax-caucvg.f	⊢ (𝜑 → 𝐹:𝑁⟶ℝ)
ax-caucvg.cau	⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))

Assertion

Ref	Expression
ax-caucvg	⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))))

Distinct variable groups:   𝑗,𝐹,𝑘,𝑛   𝑥,𝐹,𝑦,𝑗,𝑘   𝑗,𝑁,𝑘,𝑛   𝑥,𝑁,𝑦   𝜑,𝑗,𝑘,𝑛   𝑘,𝑟,𝑛   𝜑,𝑥

Allowed substitution hints:   𝜑(𝑦,𝑟)   𝐹(𝑟)   𝑁(𝑟)

Detailed syntax breakdown of Axiom ax-caucvg

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		cc0 7879	. . . . . 6 class 0
3		vx	. . . . . . 7 setvar 𝑥
4	3	cv 1363	. . . . . 6 class 𝑥
5		cltrr 7883	. . . . . 6 class <ℝ
6	2, 4, 5	wbr 4033	. . . . 5 wff 0 <ℝ 𝑥
7		vj	. . . . . . . . . 10 setvar 𝑗
8	7	cv 1363	. . . . . . . . 9 class 𝑗
9		vk	. . . . . . . . . 10 setvar 𝑘
10	9	cv 1363	. . . . . . . . 9 class 𝑘
11	8, 10, 5	wbr 4033	. . . . . . . 8 wff 𝑗 <ℝ 𝑘
12		cF	. . . . . . . . . . 11 class 𝐹
13	10, 12	cfv 5258	. . . . . . . . . 10 class (𝐹‘𝑘)
14		vy	. . . . . . . . . . . 12 setvar 𝑦
15	14	cv 1363	. . . . . . . . . . 11 class 𝑦
16		caddc 7882	. . . . . . . . . . 11 class +
17	15, 4, 16	co 5922	. . . . . . . . . 10 class (𝑦 + 𝑥)
18	13, 17, 5	wbr 4033	. . . . . . . . 9 wff (𝐹‘𝑘) <ℝ (𝑦 + 𝑥)
19	13, 4, 16	co 5922	. . . . . . . . . 10 class ((𝐹‘𝑘) + 𝑥)
20	15, 19, 5	wbr 4033	. . . . . . . . 9 wff 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)
21	18, 20	wa 104	. . . . . . . 8 wff ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))
22	11, 21	wi 4	. . . . . . 7 wff (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))
23		cN	. . . . . . 7 class 𝑁
24	22, 9, 23	wral 2475	. . . . . 6 wff ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))
25	24, 7, 23	wrex 2476	. . . . 5 wff ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))
26	6, 25	wi 4	. . . 4 wff (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))))
27		cr 7878	. . . 4 class ℝ
28	26, 3, 27	wral 2475	. . 3 wff ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))))
29	28, 14, 27	wrex 2476	. 2 wff ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))))
30	1, 29	wi 4	1 wff (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))))

This axiom is referenced by:  caucvgre  11146