Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-caucvg | Unicode version |
Description: Completeness. Axiom for
real and complex numbers, justified by Theorem
axcaucvg 7862.
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 of the nth term. This axiom should not be used directly; instead use caucvgre 10945 (which is the same, but stated in terms of the and notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-caucvg.n | |
ax-caucvg.f | |
ax-caucvg.cau |
Ref | Expression |
---|---|
ax-caucvg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . 2 | |
2 | cc0 7774 | . . . . . 6 | |
3 | vx | . . . . . . 7 | |
4 | 3 | cv 1347 | . . . . . 6 |
5 | cltrr 7778 | . . . . . 6 | |
6 | 2, 4, 5 | wbr 3989 | . . . . 5 |
7 | vj | . . . . . . . . . 10 | |
8 | 7 | cv 1347 | . . . . . . . . 9 |
9 | vk | . . . . . . . . . 10 | |
10 | 9 | cv 1347 | . . . . . . . . 9 |
11 | 8, 10, 5 | wbr 3989 | . . . . . . . 8 |
12 | cF | . . . . . . . . . . 11 | |
13 | 10, 12 | cfv 5198 | . . . . . . . . . 10 |
14 | vy | . . . . . . . . . . . 12 | |
15 | 14 | cv 1347 | . . . . . . . . . . 11 |
16 | caddc 7777 | . . . . . . . . . . 11 | |
17 | 15, 4, 16 | co 5853 | . . . . . . . . . 10 |
18 | 13, 17, 5 | wbr 3989 | . . . . . . . . 9 |
19 | 13, 4, 16 | co 5853 | . . . . . . . . . 10 |
20 | 15, 19, 5 | wbr 3989 | . . . . . . . . 9 |
21 | 18, 20 | wa 103 | . . . . . . . 8 |
22 | 11, 21 | wi 4 | . . . . . . 7 |
23 | cN | . . . . . . 7 | |
24 | 22, 9, 23 | wral 2448 | . . . . . 6 |
25 | 24, 7, 23 | wrex 2449 | . . . . 5 |
26 | 6, 25 | wi 4 | . . . 4 |
27 | cr 7773 | . . . 4 | |
28 | 26, 3, 27 | wral 2448 | . . 3 |
29 | 28, 14, 27 | wrex 2449 | . 2 |
30 | 1, 29 | wi 4 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: caucvgre 10945 |
Copyright terms: Public domain | W3C validator |