Theorem caucvgsr 6978

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 6902 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 6977).

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

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

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

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

Hypotheses

Ref	Expression
caucvgsr.f	⊢ (𝜑 → 𝐹:N⟶R)
caucvgsr.cau	⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~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‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))
3		1pi 6505	. . . . . . . . . . 11 ⊢ 1𝑜 ∈ N
4		breq1 3788	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1𝑜 → (𝑛 <N 𝑘 ↔ 1𝑜 <N 𝑘))
5		fveq2 5198	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1𝑜 → (𝐹‘𝑛) = (𝐹‘1𝑜))
6		opeq1 3570	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 1𝑜 → ⟨𝑛, 1𝑜⟩ = ⟨1𝑜, 1𝑜⟩)
7	6	eceq1d 6165	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 1𝑜 → [⟨𝑛, 1𝑜⟩] ~Q = [⟨1𝑜, 1𝑜⟩] ~Q )
8	7	fveq2d 5202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 1𝑜 → (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) = (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ))
9	8	breq2d 3797	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 1𝑜 → (𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) ↔ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )))
10	9	abbidv 2196	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 1𝑜 → {𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )} = {𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )})
11	8	breq1d 3795	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 1𝑜 → ((*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢 ↔ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢))
12	11	abbidv 2196	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 1𝑜 → {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢} = {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢})
13	10, 12	opeq12d 3578	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1𝑜 → ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩)
14	13	oveq1d 5547	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1𝑜 → (⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P) = (⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P))
15	14	opeq1d 3576	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1𝑜 → ⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩ = ⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩)
16	15	eceq1d 6165	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1𝑜 → [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R = [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
17	16	oveq2d 5548	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1𝑜 → ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) = ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))
18	5, 17	breq12d 3798	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1𝑜 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ↔ (𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )))
19	5, 16	oveq12d 5550	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 1𝑜 → ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) = ((𝐹‘1𝑜) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))
20	19	breq2d 3797	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1𝑜 → ((𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ↔ (𝐹‘𝑘) <R ((𝐹‘1𝑜) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )))
21	18, 20	anbi12d 456	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1𝑜 → (((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) ↔ ((𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1𝑜) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))
22	4, 21	imbi12d 232	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1𝑜 → ((𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))) ↔ (1𝑜 <N 𝑘 → ((𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1𝑜) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )))))
23	22	ralbidv 2368	. . . . . . . . . . . 12 ⊢ (𝑛 = 1𝑜 → (∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))) ↔ ∀𝑘 ∈ N (1𝑜 <N 𝑘 → ((𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1𝑜) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )))))
24	23	rspcv 2697	. . . . . . . . . . 11 ⊢ (1𝑜 ∈ N → (∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))) → ∀𝑘 ∈ N (1𝑜 <N 𝑘 → ((𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1𝑜) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )))))
25	3, 2, 24	mpsyl 64	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ N (1𝑜 <N 𝑘 → ((𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1𝑜) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))
26		simpl 107	. . . . . . . . . . . 12 ⊢ (((𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1𝑜) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → (𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))
27	26	imim2i 12	. . . . . . . . . . 11 ⊢ ((1𝑜 <N 𝑘 → ((𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1𝑜) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))) → (1𝑜 <N 𝑘 → (𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )))
28	27	ralimi 2426	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ N (1𝑜 <N 𝑘 → ((𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘1𝑜) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))) → ∀𝑘 ∈ N (1𝑜 <N 𝑘 → (𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )))
29	25, 28	syl 14	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ N (1𝑜 <N 𝑘 → (𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )))
30		breq2 3789	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑚 → (1𝑜 <N 𝑘 ↔ 1𝑜 <N 𝑚))
31		fveq2 5198	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
32	31	oveq1d 5547	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) = ((𝐹‘𝑚) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))
33	32	breq2d 3797	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑚 → ((𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ↔ (𝐹‘1𝑜) <R ((𝐹‘𝑚) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )))
34	30, 33	imbi12d 232	. . . . . . . . . 10 ⊢ (𝑘 = 𝑚 → ((1𝑜 <N 𝑘 → (𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) ↔ (1𝑜 <N 𝑚 → (𝐹‘1𝑜) <R ((𝐹‘𝑚) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))
35	34	rspcv 2697	. . . . . . . . 9 ⊢ (𝑚 ∈ N → (∀𝑘 ∈ N (1𝑜 <N 𝑘 → (𝐹‘1𝑜) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )) → (1𝑜 <N 𝑚 → (𝐹‘1𝑜) <R ((𝐹‘𝑚) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))
36	29, 35	mpan9 275	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (1𝑜 <N 𝑚 → (𝐹‘1𝑜) <R ((𝐹‘𝑚) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )))
37		df-1nqqs 6541	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1Q = [⟨1𝑜, 1𝑜⟩] ~Q
38	37	fveq2i 5201	. . . . . . . . . . . . . . . . . . 19 ⊢ (*Q‘1Q) = (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )
39		rec1nq 6585	. . . . . . . . . . . . . . . . . . 19 ⊢ (*Q‘1Q) = 1Q
40	38, 39	eqtr3i 2103	. . . . . . . . . . . . . . . . . 18 ⊢ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) = 1Q
41	40	breq2i 3793	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) ↔ 𝑙 <Q 1Q)
42	41	abbii 2194	. . . . . . . . . . . . . . . 16 ⊢ {𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )} = {𝑙 ∣ 𝑙 <Q 1Q}
43	40	breq1i 3792	. . . . . . . . . . . . . . . . 17 ⊢ ((*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢 ↔ 1Q <Q 𝑢)
44	43	abbii 2194	. . . . . . . . . . . . . . . 16 ⊢ {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢} = {𝑢 ∣ 1Q <Q 𝑢}
45	42, 44	opeq12i 3575	. . . . . . . . . . . . . . 15 ⊢ ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
46		df-i1p 6657	. . . . . . . . . . . . . . 15 ⊢ 1P = ⟨{𝑙 ∣ 𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
47	45, 46	eqtr4i 2104	. . . . . . . . . . . . . 14 ⊢ ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ = 1P
48	47	oveq1i 5542	. . . . . . . . . . . . 13 ⊢ (⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P) = (1P +P 1P)
49	48	opeq1i 3573	. . . . . . . . . . . 12 ⊢ ⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩ = ⟨(1P +P 1P), 1P⟩
50		eceq1 6164	. . . . . . . . . . . 12 ⊢ (⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩ = ⟨(1P +P 1P), 1P⟩ → [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R = [⟨(1P +P 1P), 1P⟩] ~R )
51	49, 50	ax-mp 7	. . . . . . . . . . 11 ⊢ [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R = [⟨(1P +P 1P), 1P⟩] ~R
52		df-1r 6909	. . . . . . . . . . 11 ⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R
53	51, 52	eqtr4i 2104	. . . . . . . . . 10 ⊢ [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R = 1R
54	53	oveq2i 5543	. . . . . . . . 9 ⊢ ((𝐹‘𝑚) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) = ((𝐹‘𝑚) +R 1R)
55	54	breq2i 3793	. . . . . . . 8 ⊢ ((𝐹‘1𝑜) <R ((𝐹‘𝑚) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨1𝑜, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ↔ (𝐹‘1𝑜) <R ((𝐹‘𝑚) +R 1R))
56	36, 55	syl6ib 159	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (1𝑜 <N 𝑚 → (𝐹‘1𝑜) <R ((𝐹‘𝑚) +R 1R)))
57	56	imp 122	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 1𝑜 <N 𝑚) → (𝐹‘1𝑜) <R ((𝐹‘𝑚) +R 1R))
58	1	adantr 270	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → 𝐹:N⟶R)
59	3	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → 1𝑜 ∈ N)
60	58, 59	ffvelrnd 5324	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝐹‘1𝑜) ∈ R)
61		ltadd1sr 6953	. . . . . . . . 9 ⊢ ((𝐹‘1𝑜) ∈ R → (𝐹‘1𝑜) <R ((𝐹‘1𝑜) +R 1R))
62	60, 61	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝐹‘1𝑜) <R ((𝐹‘1𝑜) +R 1R))
63	62	adantr 270	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 1𝑜 = 𝑚) → (𝐹‘1𝑜) <R ((𝐹‘1𝑜) +R 1R))
64		fveq2 5198	. . . . . . . . 9 ⊢ (1𝑜 = 𝑚 → (𝐹‘1𝑜) = (𝐹‘𝑚))
65	64	oveq1d 5547	. . . . . . . 8 ⊢ (1𝑜 = 𝑚 → ((𝐹‘1𝑜) +R 1R) = ((𝐹‘𝑚) +R 1R))
66	65	adantl 271	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 1𝑜 = 𝑚) → ((𝐹‘1𝑜) +R 1R) = ((𝐹‘𝑚) +R 1R))
67	63, 66	breqtrd 3809	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 1𝑜 = 𝑚) → (𝐹‘1𝑜) <R ((𝐹‘𝑚) +R 1R))
68		nlt1pig 6531	. . . . . . . . 9 ⊢ (𝑚 ∈ N → ¬ 𝑚 <N 1𝑜)
69	68	adantl 271	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ¬ 𝑚 <N 1𝑜)
70	69	pm2.21d 581	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝑚 <N 1𝑜 → (𝐹‘1𝑜) <R ((𝐹‘𝑚) +R 1R)))
71	70	imp 122	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ 𝑚 <N 1𝑜) → (𝐹‘1𝑜) <R ((𝐹‘𝑚) +R 1R))
72		pitri3or 6512	. . . . . . . 8 ⊢ ((1𝑜 ∈ N ∧ 𝑚 ∈ N) → (1𝑜 <N 𝑚 ∨ 1𝑜 = 𝑚 ∨ 𝑚 <N 1𝑜))
73	3, 72	mpan 414	. . . . . . 7 ⊢ (𝑚 ∈ N → (1𝑜 <N 𝑚 ∨ 1𝑜 = 𝑚 ∨ 𝑚 <N 1𝑜))
74	73	adantl 271	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (1𝑜 <N 𝑚 ∨ 1𝑜 = 𝑚 ∨ 𝑚 <N 1𝑜))
75	57, 67, 71, 74	mpjao3dan 1238	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝐹‘1𝑜) <R ((𝐹‘𝑚) +R 1R))
76		ltasrg 6947	. . . . . . 7 ⊢ ((𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R) → (𝑓 <R 𝑔 ↔ (ℎ +R 𝑓) <R (ℎ +R 𝑔)))
77	76	adantl 271	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ (𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R)) → (𝑓 <R 𝑔 ↔ (ℎ +R 𝑓) <R (ℎ +R 𝑔)))
78	1	ffvelrnda 5323	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (𝐹‘𝑚) ∈ R)
79		1sr 6928	. . . . . . 7 ⊢ 1R ∈ R
80		addclsr 6930	. . . . . . 7 ⊢ (((𝐹‘𝑚) ∈ R ∧ 1R ∈ R) → ((𝐹‘𝑚) +R 1R) ∈ R)
81	78, 79, 80	sylancl 404	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘𝑚) +R 1R) ∈ R)
82		m1r 6929	. . . . . . 7 ⊢ -1R ∈ R
83	82	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → -1R ∈ R)
84		addcomsrg 6932	. . . . . . 7 ⊢ ((𝑓 ∈ R ∧ 𝑔 ∈ R) → (𝑓 +R 𝑔) = (𝑔 +R 𝑓))
85	84	adantl 271	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ N) ∧ (𝑓 ∈ R ∧ 𝑔 ∈ R)) → (𝑓 +R 𝑔) = (𝑔 +R 𝑓))
86	77, 60, 81, 83, 85	caovord2d 5690	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘1𝑜) <R ((𝐹‘𝑚) +R 1R) ↔ ((𝐹‘1𝑜) +R -1R) <R (((𝐹‘𝑚) +R 1R) +R -1R)))
87	75, 86	mpbid 145	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘1𝑜) +R -1R) <R (((𝐹‘𝑚) +R 1R) +R -1R))
88	79	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → 1R ∈ R)
89		addasssrg 6933	. . . . . 6 ⊢ (((𝐹‘𝑚) ∈ R ∧ 1R ∈ R ∧ -1R ∈ R) → (((𝐹‘𝑚) +R 1R) +R -1R) = ((𝐹‘𝑚) +R (1R +R -1R)))
90	78, 88, 83, 89	syl3anc 1169	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (((𝐹‘𝑚) +R 1R) +R -1R) = ((𝐹‘𝑚) +R (1R +R -1R)))
91		addcomsrg 6932	. . . . . . . . 9 ⊢ ((1R ∈ R ∧ -1R ∈ R) → (1R +R -1R) = (-1R +R 1R))
92	79, 82, 91	mp2an 416	. . . . . . . 8 ⊢ (1R +R -1R) = (-1R +R 1R)
93		m1p1sr 6937	. . . . . . . 8 ⊢ (-1R +R 1R) = 0R
94	92, 93	eqtri 2101	. . . . . . 7 ⊢ (1R +R -1R) = 0R
95	94	oveq2i 5543	. . . . . 6 ⊢ ((𝐹‘𝑚) +R (1R +R -1R)) = ((𝐹‘𝑚) +R 0R)
96		0idsr 6944	. . . . . . 7 ⊢ ((𝐹‘𝑚) ∈ R → ((𝐹‘𝑚) +R 0R) = (𝐹‘𝑚))
97	78, 96	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘𝑚) +R 0R) = (𝐹‘𝑚))
98	95, 97	syl5eq 2125	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘𝑚) +R (1R +R -1R)) = (𝐹‘𝑚))
99	90, 98	eqtrd 2113	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → (((𝐹‘𝑚) +R 1R) +R -1R) = (𝐹‘𝑚))
100	87, 99	breqtrd 3809	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ N) → ((𝐹‘1𝑜) +R -1R) <R (𝐹‘𝑚))
101	100	ralrimiva 2434	. 2 ⊢ (𝜑 → ∀𝑚 ∈ N ((𝐹‘1𝑜) +R -1R) <R (𝐹‘𝑚))
102	1, 2, 101	caucvgsrlembnd 6977	1 ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑘) +R 𝑥)))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102   ↔ wb 103   ∨ w3o 918   ∧ w3a 919   = wceq 1284   ∈ wcel 1433  {cab 2067  ∀wral 2348  ∃wrex 2349  ⟨cop 3401   class class class wbr 3785  ⟶wf 4918  ‘cfv 4922  (class class class)co 5532  1_𝑜c1o 6017  [cec 6127  Ncnpi 6462   <_N clti 6465   ~_Q ceq 6469  1_Qc1q 6471  *_Qcrq 6474   <_Q cltq 6475  1_Pc1p 6482   +_P cpp 6483   ~_R cer 6486  Rcnr 6487  0_Rc0r 6488  1_Rc1r 6489  -1_Rcm1r 6490   +_R cplr 6491   <_R cltr 6493

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-coll 3893  ax-sep 3896  ax-nul 3904  ax-pow 3948  ax-pr 3964  ax-un 4188  ax-setind 4280  ax-iinf 4329

This theorem depends on definitions:  df-bi 115  df-dc 776  df-3or 920  df-3an 921  df-tru 1287  df-fal 1290  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ne 2246  df-ral 2353  df-rex 2354  df-reu 2355  df-rmo 2356  df-rab 2357  df-v 2603  df-sbc 2816  df-csb 2909  df-dif 2975  df-un 2977  df-in 2979  df-ss 2986  df-nul 3252  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-int 3637  df-iun 3680  df-br 3786  df-opab 3840  df-mpt 3841  df-tr 3876  df-eprel 4044  df-id 4048  df-po 4051  df-iso 4052  df-iord 4121  df-on 4123  df-suc 4126  df-iom 4332  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-iota 4887  df-fun 4924  df-fn 4925  df-f 4926  df-f1 4927  df-fo 4928  df-f1o 4929  df-fv 4930  df-riota 5488  df-ov 5535  df-oprab 5536  df-mpt2 5537  df-1st 5787  df-2nd 5788  df-recs 5943  df-irdg 5980  df-1o 6024  df-2o 6025  df-oadd 6028  df-omul 6029  df-er 6129  df-ec 6131  df-qs 6135  df-ni 6494  df-pli 6495  df-mi 6496  df-lti 6497  df-plpq 6534  df-mpq 6535  df-enq 6537  df-nqqs 6538  df-plqqs 6539  df-mqqs 6540  df-1nqqs 6541  df-rq 6542  df-ltnqqs 6543  df-enq0 6614  df-nq0 6615  df-0nq0 6616  df-plq0 6617  df-mq0 6618  df-inp 6656  df-i1p 6657  df-iplp 6658  df-imp 6659  df-iltp 6660  df-enr 6903  df-nr 6904  df-plr 6905  df-mr 6906  df-ltr 6907  df-0r 6908  df-1r 6909  df-m1r 6910

This theorem is referenced by:  axcaucvglemres  7065