Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > caucvgsr | GIF version |
Description: A Cauchy sequence of
signed reals with a modulus of convergence
converges to a signed real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies). The HoTT book
theorem has a modulus of
convergence (that is, a rate of convergence) specified by (11.2.9) in
HoTT whereas this theorem fixes the rate of convergence to say that
all terms after the nth term must be within 1 / 𝑛 of the nth term
(it should later be able to prove versions of this theorem with a
different fixed rate or a modulus of convergence supplied as a
hypothesis).
This is similar to caucvgprpr 7627 but is for signed reals rather than positive reals. Here is an outline of how we prove it: 1. Choose a lower bound for the sequence (see caucvgsrlembnd 7716). 2. Offset each element of the sequence so that each element of the resulting sequence is greater than one (greater than zero would not suffice, because the limit as well as the elements of the sequence need to be positive) (see caucvgsrlemofff 7712). 3. Since a signed real (element of R) which is greater than zero can be mapped to a positive real (element of P), perform that mapping on each element of the sequence and invoke caucvgprpr 7627 to get a limit (see caucvgsrlemgt1 7710). 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 7710). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 7715). (Contributed by Jim Kingdon, 20-Jun-2021.) |
Ref | Expression |
---|---|
caucvgsr.f | ⊢ (𝜑 → 𝐹:N⟶R) |
caucvgsr.cau | ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) |
Ref | Expression |
---|---|
caucvgsr | ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑘) +R 𝑥))))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | caucvgsr.f | . 2 ⊢ (𝜑 → 𝐹:N⟶R) | |
2 | caucvgsr.cau | . 2 ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) | |
3 | breq1 3968 | . . . . . . . . . . . . 13 ⊢ (𝑛 = 1o → (𝑛 <N 𝑘 ↔ 1o <N 𝑘)) | |
4 | fveq2 5467 | . . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1o → (𝐹‘𝑛) = (𝐹‘1o)) | |
5 | opeq1 3741 | . . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 1o → 〈𝑛, 1o〉 = 〈1o, 1o〉) | |
6 | 5 | eceq1d 6513 | . . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 1o → [〈𝑛, 1o〉] ~Q = [〈1o, 1o〉] ~Q ) |
7 | 6 | fveq2d 5471 | . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 1o → (*Q‘[〈𝑛, 1o〉] ~Q ) = (*Q‘[〈1o, 1o〉] ~Q )) |
8 | 7 | breq2d 3977 | . . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 1o → (𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q ) ↔ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q ))) |
9 | 8 | abbidv 2275 | . . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1o → {𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )} = {𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}) |
10 | 7 | breq1d 3975 | . . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 1o → ((*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢 ↔ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢)) |
11 | 10 | abbidv 2275 | . . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1o → {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢} = {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}) |
12 | 9, 11 | opeq12d 3749 | . . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1o → 〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 = 〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉) |
13 | 12 | oveq1d 5836 | . . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1o → (〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P) = (〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P)) |
14 | 13 | opeq1d 3747 | . . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1o → 〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉 = 〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉) |
15 | 14 | eceq1d 6513 | . . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1o → [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R = [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) |
16 | 15 | oveq2d 5837 | . . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1o → ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) = ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )) |
17 | 4, 16 | breq12d 3978 | . . . . . . . . . . . . . 14 ⊢ (𝑛 = 1o → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ↔ (𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))) |
18 | 4, 15 | oveq12d 5839 | . . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1o → ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) = ((𝐹‘1o) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )) |
19 | 18 | breq2d 3977 | . . . . . . . . . . . . . 14 ⊢ (𝑛 = 1o → ((𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ↔ (𝐹‘𝑘) <R ((𝐹‘1o) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))) |
20 | 17, 19 | anbi12d 465 | . . . . . . . . . . . . 13 ⊢ (𝑛 = 1o → (((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )) ↔ ((𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1o) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) |
21 | 3, 20 | imbi12d 233 | . . . . . . . . . . . 12 ⊢ (𝑛 = 1o → ((𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))) ↔ (1o <N 𝑘 → ((𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1o) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))))) |
22 | 21 | ralbidv 2457 | . . . . . . . . . . 11 ⊢ (𝑛 = 1o → (∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈𝑛, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈𝑛, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))) ↔ ∀𝑘 ∈ N (1o <N 𝑘 → ((𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1o) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))))) |
23 | 1pi 7230 | . . . . . . . . . . . 12 ⊢ 1o ∈ N | |
24 | 23 | a1i 9 | . . . . . . . . . . 11 ⊢ (𝜑 → 1o ∈ N) |
25 | 22, 2, 24 | rspcdva 2821 | . . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ N (1o <N 𝑘 → ((𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1o) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) |
26 | simpl 108 | . . . . . . . . . . . 12 ⊢ (((𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1o) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )) → (𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )) | |
27 | 26 | imim2i 12 | . . . . . . . . . . 11 ⊢ ((1o <N 𝑘 → ((𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1o) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))) → (1o <N 𝑘 → (𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))) |
28 | 27 | ralimi 2520 | . . . . . . . . . 10 ⊢ (∀𝑘 ∈ N (1o <N 𝑘 → ((𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1o) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))) → ∀𝑘 ∈ N (1o <N 𝑘 → (𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))) |
29 | 25, 28 | syl 14 | . . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ N (1o <N 𝑘 → (𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))) |
30 | breq2 3969 | . . . . . . . . . . 11 ⊢ (𝑘 = 𝑚 → (1o <N 𝑘 ↔ 1o <N 𝑚)) | |
31 | fveq2 5467 | . . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚)) | |
32 | 31 | oveq1d 5836 | . . . . . . . . . . . 12 ⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) = ((𝐹‘𝑚) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )) |
33 | 32 | breq2d 3977 | . . . . . . . . . . 11 ⊢ (𝑘 = 𝑚 → ((𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ↔ (𝐹‘1o) <R ((𝐹‘𝑚) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))) |
34 | 30, 33 | imbi12d 233 | . . . . . . . . . 10 ⊢ (𝑘 = 𝑚 → ((1o <N 𝑘 → (𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )) ↔ (1o <N 𝑚 → (𝐹‘1o) <R ((𝐹‘𝑚) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) |
35 | 34 | rspcv 2812 | . . . . . . . . 9 ⊢ (𝑚 ∈ N → (∀𝑘 ∈ N (1o <N 𝑘 → (𝐹‘1o) <R ((𝐹‘𝑘) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )) → (1o <N 𝑚 → (𝐹‘1o) <R ((𝐹‘𝑚) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R )))) |
36 | 29, 35 | mpan9 279 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (1o <N 𝑚 → (𝐹‘1o) <R ((𝐹‘𝑚) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ))) |
37 | df-1nqqs 7266 | . . . . . . . . . . . . . . . . . . . 20 ⊢ 1Q = [〈1o, 1o〉] ~Q | |
38 | 37 | fveq2i 5470 | . . . . . . . . . . . . . . . . . . 19 ⊢ (*Q‘1Q) = (*Q‘[〈1o, 1o〉] ~Q ) |
39 | rec1nq 7310 | . . . . . . . . . . . . . . . . . . 19 ⊢ (*Q‘1Q) = 1Q | |
40 | 38, 39 | eqtr3i 2180 | . . . . . . . . . . . . . . . . . 18 ⊢ (*Q‘[〈1o, 1o〉] ~Q ) = 1Q |
41 | 40 | breq2i 3973 | . . . . . . . . . . . . . . . . 17 ⊢ (𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q ) ↔ 𝑙 <Q 1Q) |
42 | 41 | abbii 2273 | . . . . . . . . . . . . . . . 16 ⊢ {𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )} = {𝑙 ∣ 𝑙 <Q 1Q} |
43 | 40 | breq1i 3972 | . . . . . . . . . . . . . . . . 17 ⊢ ((*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢 ↔ 1Q <Q 𝑢) |
44 | 43 | abbii 2273 | . . . . . . . . . . . . . . . 16 ⊢ {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢} = {𝑢 ∣ 1Q <Q 𝑢} |
45 | 42, 44 | opeq12i 3746 | . . . . . . . . . . . . . . 15 ⊢ 〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 = 〈{𝑙 ∣ 𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}〉 |
46 | df-i1p 7382 | . . . . . . . . . . . . . . 15 ⊢ 1P = 〈{𝑙 ∣ 𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}〉 | |
47 | 45, 46 | eqtr4i 2181 | . . . . . . . . . . . . . 14 ⊢ 〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 = 1P |
48 | 47 | oveq1i 5831 | . . . . . . . . . . . . 13 ⊢ (〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P) = (1P +P 1P) |
49 | 48 | opeq1i 3744 | . . . . . . . . . . . 12 ⊢ 〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉 = 〈(1P +P 1P), 1P〉 |
50 | eceq1 6512 | . . . . . . . . . . . 12 ⊢ (〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉 = 〈(1P +P 1P), 1P〉 → [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R = [〈(1P +P 1P), 1P〉] ~R ) | |
51 | 49, 50 | ax-mp 5 | . . . . . . . . . . 11 ⊢ [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R = [〈(1P +P 1P), 1P〉] ~R |
52 | df-1r 7647 | . . . . . . . . . . 11 ⊢ 1R = [〈(1P +P 1P), 1P〉] ~R | |
53 | 51, 52 | eqtr4i 2181 | . . . . . . . . . 10 ⊢ [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R = 1R |
54 | 53 | oveq2i 5832 | . . . . . . . . 9 ⊢ ((𝐹‘𝑚) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) = ((𝐹‘𝑚) +R 1R) |
55 | 54 | breq2i 3973 | . . . . . . . 8 ⊢ ((𝐹‘1o) <R ((𝐹‘𝑚) +R [〈(〈{𝑙 ∣ 𝑙 <Q (*Q‘[〈1o, 1o〉] ~Q )}, {𝑢 ∣ (*Q‘[〈1o, 1o〉] ~Q ) <Q 𝑢}〉 +P 1P), 1P〉] ~R ) ↔ (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R)) |
56 | 36, 55 | syl6ib 160 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (1o <N 𝑚 → (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R))) |
57 | 56 | imp 123 | . . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 1o <N 𝑚) → (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R)) |
58 | 1 | adantr 274 | . . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → 𝐹:N⟶R) |
59 | 23 | a1i 9 | . . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → 1o ∈ N) |
60 | 58, 59 | ffvelrnd 5602 | . . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝐹‘1o) ∈ R) |
61 | ltadd1sr 7691 | . . . . . . . . 9 ⊢ ((𝐹‘1o) ∈ R → (𝐹‘1o) <R ((𝐹‘1o) +R 1R)) | |
62 | 60, 61 | syl 14 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝐹‘1o) <R ((𝐹‘1o) +R 1R)) |
63 | 62 | adantr 274 | . . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 1o = 𝑚) → (𝐹‘1o) <R ((𝐹‘1o) +R 1R)) |
64 | fveq2 5467 | . . . . . . . . 9 ⊢ (1o = 𝑚 → (𝐹‘1o) = (𝐹‘𝑚)) | |
65 | 64 | oveq1d 5836 | . . . . . . . 8 ⊢ (1o = 𝑚 → ((𝐹‘1o) +R 1R) = ((𝐹‘𝑚) +R 1R)) |
66 | 65 | adantl 275 | . . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 1o = 𝑚) → ((𝐹‘1o) +R 1R) = ((𝐹‘𝑚) +R 1R)) |
67 | 63, 66 | breqtrd 3990 | . . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 1o = 𝑚) → (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R)) |
68 | nlt1pig 7256 | . . . . . . . . 9 ⊢ (𝑚 ∈ N → ¬ 𝑚 <N 1o) | |
69 | 68 | adantl 275 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ¬ 𝑚 <N 1o) |
70 | 69 | pm2.21d 609 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝑚 <N 1o → (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R))) |
71 | 70 | imp 123 | . . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 𝑚 <N 1o) → (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R)) |
72 | pitri3or 7237 | . . . . . . . 8 ⊢ ((1o ∈ N ∧ 𝑚 ∈ N) → (1o <N 𝑚 ∨ 1o = 𝑚 ∨ 𝑚 <N 1o)) | |
73 | 23, 72 | mpan 421 | . . . . . . 7 ⊢ (𝑚 ∈ N → (1o <N 𝑚 ∨ 1o = 𝑚 ∨ 𝑚 <N 1o)) |
74 | 73 | adantl 275 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (1o <N 𝑚 ∨ 1o = 𝑚 ∨ 𝑚 <N 1o)) |
75 | 57, 67, 71, 74 | mpjao3dan 1289 | . . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R)) |
76 | ltasrg 7685 | . . . . . . 7 ⊢ ((𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R) → (𝑓 <R 𝑔 ↔ (ℎ +R 𝑓) <R (ℎ +R 𝑔))) | |
77 | 76 | adantl 275 | . . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ (𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R)) → (𝑓 <R 𝑔 ↔ (ℎ +R 𝑓) <R (ℎ +R 𝑔))) |
78 | 1 | ffvelrnda 5601 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝐹‘𝑚) ∈ R) |
79 | 1sr 7666 | . . . . . . 7 ⊢ 1R ∈ R | |
80 | addclsr 7668 | . . . . . . 7 ⊢ (((𝐹‘𝑚) ∈ R ∧ 1R ∈ R) → ((𝐹‘𝑚) +R 1R) ∈ R) | |
81 | 78, 79, 80 | sylancl 410 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘𝑚) +R 1R) ∈ R) |
82 | m1r 7667 | . . . . . . 7 ⊢ -1R ∈ R | |
83 | 82 | a1i 9 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → -1R ∈ R) |
84 | addcomsrg 7670 | . . . . . . 7 ⊢ ((𝑓 ∈ R ∧ 𝑔 ∈ R) → (𝑓 +R 𝑔) = (𝑔 +R 𝑓)) | |
85 | 84 | adantl 275 | . . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ (𝑓 ∈ R ∧ 𝑔 ∈ R)) → (𝑓 +R 𝑔) = (𝑔 +R 𝑓)) |
86 | 77, 60, 81, 83, 85 | caovord2d 5987 | . . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘1o) <R ((𝐹‘𝑚) +R 1R) ↔ ((𝐹‘1o) +R -1R) <R (((𝐹‘𝑚) +R 1R) +R -1R))) |
87 | 75, 86 | mpbid 146 | . . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘1o) +R -1R) <R (((𝐹‘𝑚) +R 1R) +R -1R)) |
88 | 79 | a1i 9 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → 1R ∈ R) |
89 | addasssrg 7671 | . . . . . 6 ⊢ (((𝐹‘𝑚) ∈ R ∧ 1R ∈ R ∧ -1R ∈ R) → (((𝐹‘𝑚) +R 1R) +R -1R) = ((𝐹‘𝑚) +R (1R +R -1R))) | |
90 | 78, 88, 83, 89 | syl3anc 1220 | . . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (((𝐹‘𝑚) +R 1R) +R -1R) = ((𝐹‘𝑚) +R (1R +R -1R))) |
91 | addcomsrg 7670 | . . . . . . . . 9 ⊢ ((1R ∈ R ∧ -1R ∈ R) → (1R +R -1R) = (-1R +R 1R)) | |
92 | 79, 82, 91 | mp2an 423 | . . . . . . . 8 ⊢ (1R +R -1R) = (-1R +R 1R) |
93 | m1p1sr 7675 | . . . . . . . 8 ⊢ (-1R +R 1R) = 0R | |
94 | 92, 93 | eqtri 2178 | . . . . . . 7 ⊢ (1R +R -1R) = 0R |
95 | 94 | oveq2i 5832 | . . . . . 6 ⊢ ((𝐹‘𝑚) +R (1R +R -1R)) = ((𝐹‘𝑚) +R 0R) |
96 | 0idsr 7682 | . . . . . . 7 ⊢ ((𝐹‘𝑚) ∈ R → ((𝐹‘𝑚) +R 0R) = (𝐹‘𝑚)) | |
97 | 78, 96 | syl 14 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘𝑚) +R 0R) = (𝐹‘𝑚)) |
98 | 95, 97 | syl5eq 2202 | . . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘𝑚) +R (1R +R -1R)) = (𝐹‘𝑚)) |
99 | 90, 98 | eqtrd 2190 | . . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (((𝐹‘𝑚) +R 1R) +R -1R) = (𝐹‘𝑚)) |
100 | 87, 99 | breqtrd 3990 | . . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘1o) +R -1R) <R (𝐹‘𝑚)) |
101 | 100 | ralrimiva 2530 | . 2 ⊢ (𝜑 → ∀𝑚 ∈ N ((𝐹‘1o) +R -1R) <R (𝐹‘𝑚)) |
102 | 1, 2, 101 | caucvgsrlembnd 7716 | 1 ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑘) +R 𝑥))))) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ w3o 962 ∧ w3a 963 = wceq 1335 ∈ wcel 2128 {cab 2143 ∀wral 2435 ∃wrex 2436 〈cop 3563 class class class wbr 3965 ⟶wf 5165 ‘cfv 5169 (class class class)co 5821 1oc1o 6353 [cec 6475 Ncnpi 7187 <N clti 7190 ~Q ceq 7194 1Qc1q 7196 *Qcrq 7199 <Q cltq 7200 1Pc1p 7207 +P cpp 7208 ~R cer 7211 Rcnr 7212 0Rc0r 7213 1Rc1r 7214 -1Rcm1r 7215 +R cplr 7216 <R cltr 7218 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-13 2130 ax-14 2131 ax-ext 2139 ax-coll 4079 ax-sep 4082 ax-nul 4090 ax-pow 4135 ax-pr 4169 ax-un 4393 ax-setind 4495 ax-iinf 4546 |
This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1338 df-fal 1341 df-nf 1441 df-sb 1743 df-eu 2009 df-mo 2010 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ne 2328 df-ral 2440 df-rex 2441 df-reu 2442 df-rmo 2443 df-rab 2444 df-v 2714 df-sbc 2938 df-csb 3032 df-dif 3104 df-un 3106 df-in 3108 df-ss 3115 df-nul 3395 df-pw 3545 df-sn 3566 df-pr 3567 df-op 3569 df-uni 3773 df-int 3808 df-iun 3851 df-br 3966 df-opab 4026 df-mpt 4027 df-tr 4063 df-eprel 4249 df-id 4253 df-po 4256 df-iso 4257 df-iord 4326 df-on 4328 df-suc 4331 df-iom 4549 df-xp 4591 df-rel 4592 df-cnv 4593 df-co 4594 df-dm 4595 df-rn 4596 df-res 4597 df-ima 4598 df-iota 5134 df-fun 5171 df-fn 5172 df-f 5173 df-f1 5174 df-fo 5175 df-f1o 5176 df-fv 5177 df-riota 5777 df-ov 5824 df-oprab 5825 df-mpo 5826 df-1st 6085 df-2nd 6086 df-recs 6249 df-irdg 6314 df-1o 6360 df-2o 6361 df-oadd 6364 df-omul 6365 df-er 6477 df-ec 6479 df-qs 6483 df-ni 7219 df-pli 7220 df-mi 7221 df-lti 7222 df-plpq 7259 df-mpq 7260 df-enq 7262 df-nqqs 7263 df-plqqs 7264 df-mqqs 7265 df-1nqqs 7266 df-rq 7267 df-ltnqqs 7268 df-enq0 7339 df-nq0 7340 df-0nq0 7341 df-plq0 7342 df-mq0 7343 df-inp 7381 df-i1p 7382 df-iplp 7383 df-imp 7384 df-iltp 7385 df-enr 7641 df-nr 7642 df-plr 7643 df-mr 7644 df-ltr 7645 df-0r 7646 df-1r 7647 df-m1r 7648 |
This theorem is referenced by: axcaucvglemres 7814 |
Copyright terms: Public domain | W3C validator |