Theorem caucvgsr 8065

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 7975 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 8064).

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 8060).

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 7975 to get a limit (see caucvgsrlemgt1 8058).

4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 8058).

5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 8063). (Contributed by Jim Kingdon, 20-Jun-2021.)

Hypotheses

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 ))))

Assertion

Ref	Expression
caucvgsr	⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑘) +R 𝑥)))))

Distinct variable groups:   𝑗,𝐹,𝑘,𝑙,𝑢   𝑛,𝐹,𝑘,𝑙,𝑢   𝑥,𝐹,𝑦,𝑗,𝑘   𝜑,𝑗,𝑘,𝑥   𝜑,𝑛

Allowed substitution hints:   𝜑(𝑦,𝑢,𝑙)

Proof of Theorem caucvgsr

Dummy variables 𝑓 𝑔 ℎ 𝑚 are mutually distinct and distinct from all other variables.

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 4096	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1o → (𝑛 <N 𝑘 ↔ 1o <N 𝑘))
4		fveq2 5648	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1o → (𝐹‘𝑛) = (𝐹‘1o))
5		opeq1 3867	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 1o → ⟨𝑛, 1o⟩ = ⟨1o, 1o⟩)
6	5	eceq1d 6781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 1o → [⟨𝑛, 1o⟩] ~Q = [⟨1o, 1o⟩] ~Q )
7	6	fveq2d 5652	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 1o → (*Q‘[⟨𝑛, 1o⟩] ~Q ) = (*Q‘[⟨1o, 1o⟩] ~Q ))
8	7	breq2d 4105	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 1o → (𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q ) ↔ 𝑙 <Q (*Q‘[⟨1o, 1o⟩] ~Q )))
9	8	abbidv 2350	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1o → {𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )} = {𝑙 ∣ 𝑙 <Q (*Q‘[⟨1o, 1o⟩] ~Q )})
10	7	breq1d 4103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 1o → ((*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢 ↔ (*Q‘[⟨1o, 1o⟩] ~Q ) <Q 𝑢))
11	10	abbidv 2350	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1o → {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢} = {𝑢 ∣ (*Q‘[⟨1o, 1o⟩] ~Q ) <Q 𝑢})
12	9, 11	opeq12d 3875	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1o → ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1o, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1o, 1o⟩] ~Q ) <Q 𝑢}⟩)
13	12	oveq1d 6043	. . . . . . . . . . . . . . . . . 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 3873	. . . . . . . . . . . . . . . . 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 6781	. . . . . . . . . . . . . . . 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 6044	. . . . . . . . . . . . . . 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 4106	. . . . . . . . . . . . . 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 6046	. . . . . . . . . . . . . . 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 4105	. . . . . . . . . . . . . 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 473	. . . . . . . . . . . . 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 234	. . . . . . . . . . . 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 2533	. . . . . . . . . . 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 7578	. . . . . . . . . . . 12 ⊢ 1o ∈ N
24	23	a1i 9	. . . . . . . . . . 11 ⊢ (𝜑 → 1o ∈ N)
25	22, 2, 24	rspcdva 2916	. . . . . . . . . 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 109	. . . . . . . . . . . 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 2596	. . . . . . . . . 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 4097	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑚 → (1o <N 𝑘 ↔ 1o <N 𝑚))
31		fveq2 5648	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
32	31	oveq1d 6043	. . . . . . . . . . . 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 4105	. . . . . . . . . . 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 234	. . . . . . . . . 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 2907	. . . . . . . . 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 281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (1o <N 𝑚 → (𝐹‘1o) <R ((𝐹‘𝑚) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1o, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1o, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )))
37		df-1nqqs 7614	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1Q = [⟨1o, 1o⟩] ~Q
38	37	fveq2i 5651	. . . . . . . . . . . . . . . . . . 19 ⊢ (*Q‘1Q) = (*Q‘[⟨1o, 1o⟩] ~Q )
39		rec1nq 7658	. . . . . . . . . . . . . . . . . . 19 ⊢ (*Q‘1Q) = 1Q
40	38, 39	eqtr3i 2254	. . . . . . . . . . . . . . . . . 18 ⊢ (*Q‘[⟨1o, 1o⟩] ~Q ) = 1Q
41	40	breq2i 4101	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 <Q (*Q‘[⟨1o, 1o⟩] ~Q ) ↔ 𝑙 <Q 1Q)
42	41	abbii 2347	. . . . . . . . . . . . . . . 16 ⊢ {𝑙 ∣ 𝑙 <Q (*Q‘[⟨1o, 1o⟩] ~Q )} = {𝑙 ∣ 𝑙 <Q 1Q}
43	40	breq1i 4100	. . . . . . . . . . . . . . . . 17 ⊢ ((*Q‘[⟨1o, 1o⟩] ~Q ) <Q 𝑢 ↔ 1Q <Q 𝑢)
44	43	abbii 2347	. . . . . . . . . . . . . . . 16 ⊢ {𝑢 ∣ (*Q‘[⟨1o, 1o⟩] ~Q ) <Q 𝑢} = {𝑢 ∣ 1Q <Q 𝑢}
45	42, 44	opeq12i 3872	. . . . . . . . . . . . . . 15 ⊢ ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1o, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1o, 1o⟩] ~Q ) <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
46		df-i1p 7730	. . . . . . . . . . . . . . 15 ⊢ 1P = ⟨{𝑙 ∣ 𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
47	45, 46	eqtr4i 2255	. . . . . . . . . . . . . 14 ⊢ ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1o, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1o, 1o⟩] ~Q ) <Q 𝑢}⟩ = 1P
48	47	oveq1i 6038	. . . . . . . . . . . . 13 ⊢ (⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1o, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1o, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P) = (1P +P 1P)
49	48	opeq1i 3870	. . . . . . . . . . . 12 ⊢ ⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1o, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1o, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩ = ⟨(1P +P 1P), 1P⟩
50		eceq1 6780	. . . . . . . . . . . 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 7995	. . . . . . . . . . 11 ⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R
53	51, 52	eqtr4i 2255	. . . . . . . . . 10 ⊢ [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1o, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1o, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R = 1R
54	53	oveq2i 6039	. . . . . . . . 9 ⊢ ((𝐹‘𝑚) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1o, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1o, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) = ((𝐹‘𝑚) +R 1R)
55	54	breq2i 4101	. . . . . . . 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	imbitrdi 161	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (1o <N 𝑚 → (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R)))
57	56	imp 124	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 1o <N 𝑚) → (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R))
58	1	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → 𝐹:N⟶R)
59	23	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → 1o ∈ N)
60	58, 59	ffvelcdmd 5791	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝐹‘1o) ∈ R)
61		ltadd1sr 8039	. . . . . . . . 9 ⊢ ((𝐹‘1o) ∈ R → (𝐹‘1o) <R ((𝐹‘1o) +R 1R))
62	60, 61	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝐹‘1o) <R ((𝐹‘1o) +R 1R))
63	62	adantr 276	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 1o = 𝑚) → (𝐹‘1o) <R ((𝐹‘1o) +R 1R))
64		fveq2 5648	. . . . . . . . 9 ⊢ (1o = 𝑚 → (𝐹‘1o) = (𝐹‘𝑚))
65	64	oveq1d 6043	. . . . . . . 8 ⊢ (1o = 𝑚 → ((𝐹‘1o) +R 1R) = ((𝐹‘𝑚) +R 1R))
66	65	adantl 277	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 1o = 𝑚) → ((𝐹‘1o) +R 1R) = ((𝐹‘𝑚) +R 1R))
67	63, 66	breqtrd 4119	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 1o = 𝑚) → (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R))
68		nlt1pig 7604	. . . . . . . . 9 ⊢ (𝑚 ∈ N → ¬ 𝑚 <N 1o)
69	68	adantl 277	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ¬ 𝑚 <N 1o)
70	69	pm2.21d 624	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝑚 <N 1o → (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R)))
71	70	imp 124	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 𝑚 <N 1o) → (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R))
72		pitri3or 7585	. . . . . . . 8 ⊢ ((1o ∈ N ∧ 𝑚 ∈ N) → (1o <N 𝑚 ∨ 1o = 𝑚 ∨ 𝑚 <N 1o))
73	23, 72	mpan 424	. . . . . . 7 ⊢ (𝑚 ∈ N → (1o <N 𝑚 ∨ 1o = 𝑚 ∨ 𝑚 <N 1o))
74	73	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (1o <N 𝑚 ∨ 1o = 𝑚 ∨ 𝑚 <N 1o))
75	57, 67, 71, 74	mpjao3dan 1344	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝐹‘1o) <R ((𝐹‘𝑚) +R 1R))
76		ltasrg 8033	. . . . . . 7 ⊢ ((𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R) → (𝑓 <R 𝑔 ↔ (ℎ +R 𝑓) <R (ℎ +R 𝑔)))
77	76	adantl 277	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ (𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R)) → (𝑓 <R 𝑔 ↔ (ℎ +R 𝑓) <R (ℎ +R 𝑔)))
78	1	ffvelcdmda 5790	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝐹‘𝑚) ∈ R)
79		1sr 8014	. . . . . . 7 ⊢ 1R ∈ R
80		addclsr 8016	. . . . . . 7 ⊢ (((𝐹‘𝑚) ∈ R ∧ 1R ∈ R) → ((𝐹‘𝑚) +R 1R) ∈ R)
81	78, 79, 80	sylancl 413	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘𝑚) +R 1R) ∈ R)
82		m1r 8015	. . . . . . 7 ⊢ -1R ∈ R
83	82	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → -1R ∈ R)
84		addcomsrg 8018	. . . . . . 7 ⊢ ((𝑓 ∈ R ∧ 𝑔 ∈ R) → (𝑓 +R 𝑔) = (𝑔 +R 𝑓))
85	84	adantl 277	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ (𝑓 ∈ R ∧ 𝑔 ∈ R)) → (𝑓 +R 𝑔) = (𝑔 +R 𝑓))
86	77, 60, 81, 83, 85	caovord2d 6202	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘1o) <R ((𝐹‘𝑚) +R 1R) ↔ ((𝐹‘1o) +R -1R) <R (((𝐹‘𝑚) +R 1R) +R -1R)))
87	75, 86	mpbid 147	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘1o) +R -1R) <R (((𝐹‘𝑚) +R 1R) +R -1R))
88	79	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → 1R ∈ R)
89		addasssrg 8019	. . . . . 6 ⊢ (((𝐹‘𝑚) ∈ R ∧ 1R ∈ R ∧ -1R ∈ R) → (((𝐹‘𝑚) +R 1R) +R -1R) = ((𝐹‘𝑚) +R (1R +R -1R)))
90	78, 88, 83, 89	syl3anc 1274	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (((𝐹‘𝑚) +R 1R) +R -1R) = ((𝐹‘𝑚) +R (1R +R -1R)))
91		addcomsrg 8018	. . . . . . . . 9 ⊢ ((1R ∈ R ∧ -1R ∈ R) → (1R +R -1R) = (-1R +R 1R))
92	79, 82, 91	mp2an 426	. . . . . . . 8 ⊢ (1R +R -1R) = (-1R +R 1R)
93		m1p1sr 8023	. . . . . . . 8 ⊢ (-1R +R 1R) = 0R
94	92, 93	eqtri 2252	. . . . . . 7 ⊢ (1R +R -1R) = 0R
95	94	oveq2i 6039	. . . . . 6 ⊢ ((𝐹‘𝑚) +R (1R +R -1R)) = ((𝐹‘𝑚) +R 0R)
96		0idsr 8030	. . . . . . 7 ⊢ ((𝐹‘𝑚) ∈ R → ((𝐹‘𝑚) +R 0R) = (𝐹‘𝑚))
97	78, 96	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘𝑚) +R 0R) = (𝐹‘𝑚))
98	95, 97	eqtrid 2276	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘𝑚) +R (1R +R -1R)) = (𝐹‘𝑚))
99	90, 98	eqtrd 2264	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (((𝐹‘𝑚) +R 1R) +R -1R) = (𝐹‘𝑚))
100	87, 99	breqtrd 4119	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘1o) +R -1R) <R (𝐹‘𝑚))
101	100	ralrimiva 2606	. 2 ⊢ (𝜑 → ∀𝑚 ∈ N ((𝐹‘1o) +R -1R) <R (𝐹‘𝑚))
102	1, 2, 101	caucvgsrlembnd 8064	1 ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑘) +R 𝑥)))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ w3o 1004   ∧ w3a 1005   = wceq 1398   ∈ wcel 2202  {cab 2217  ∀wral 2511  ∃wrex 2512  ⟨cop 3676   class class class wbr 4093  ⟶wf 5329  ‘cfv 5333  (class class class)co 6028  1_oc1o 6618  [cec 6743  Ncnpi 7535   <_N clti 7538   ~_Q ceq 7542  1_Qc1q 7544  *_Qcrq 7547   <_Q cltq 7548  1_Pc1p 7555   +_P cpp 7556   ~_R cer 7559  Rcnr 7560  0_Rc0r 7561  1_Rc1r 7562  -1_Rcm1r 7563   +_R cplr 7564   <_R cltr 7566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-coll 4209  ax-sep 4212  ax-nul 4220  ax-pow 4270  ax-pr 4305  ax-un 4536  ax-setind 4641  ax-iinf 4692

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-ral 2516  df-rex 2517  df-reu 2518  df-rmo 2519  df-rab 2520  df-v 2805  df-sbc 3033  df-csb 3129  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-nul 3497  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-int 3934  df-iun 3977  df-br 4094  df-opab 4156  df-mpt 4157  df-tr 4193  df-eprel 4392  df-id 4396  df-po 4399  df-iso 4400  df-iord 4469  df-on 4471  df-suc 4474  df-iom 4695  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-res 4743  df-ima 4744  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-f1 5338  df-fo 5339  df-f1o 5340  df-fv 5341  df-riota 5981  df-ov 6031  df-oprab 6032  df-mpo 6033  df-1st 6312  df-2nd 6313  df-recs 6514  df-irdg 6579  df-1o 6625  df-2o 6626  df-oadd 6629  df-omul 6630  df-er 6745  df-ec 6747  df-qs 6751  df-ni 7567  df-pli 7568  df-mi 7569  df-lti 7570  df-plpq 7607  df-mpq 7608  df-enq 7610  df-nqqs 7611  df-plqqs 7612  df-mqqs 7613  df-1nqqs 7614  df-rq 7615  df-ltnqqs 7616  df-enq0 7687  df-nq0 7688  df-0nq0 7689  df-plq0 7690  df-mq0 7691  df-inp 7729  df-i1p 7730  df-iplp 7731  df-imp 7732  df-iltp 7733  df-enr 7989  df-nr 7990  df-plr 7991  df-mr 7992  df-ltr 7993  df-0r 7994  df-1r 7995  df-m1r 7996

This theorem is referenced by:  axcaucvglemres  8162