Theorem caucvgsrlemoffcau 8109

Description: Lemma for caucvgsr 8113. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-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 ))))
caucvgsrlembnd.bnd	⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚))
caucvgsrlembnd.offset	⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R)))

Assertion

Ref	Expression
caucvgsrlemoffcau	⊢ (𝜑 → ∀𝑛 ∈ 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 ))))

Distinct variable groups:   𝐴,𝑎   𝐴,𝑚   𝐹,𝑎   𝑘,𝑎,𝑛,𝜑   𝑛,𝑙,𝑢

Allowed substitution hints:   𝜑(𝑢,𝑚,𝑙)   𝐴(𝑢,𝑘,𝑛,𝑙)   𝐹(𝑢,𝑘,𝑚,𝑛,𝑙)   𝐺(𝑢,𝑘,𝑚,𝑛,𝑎,𝑙)

Proof of Theorem caucvgsrlemoffcau

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

Step	Hyp	Ref	Expression
1		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 ))))
2		caucvgsr.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:N⟶R)
3		caucvgsrlembnd.bnd	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚))
4		caucvgsrlembnd.offset	. . . . . . . . . . . 12 ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R)))
5	2, 1, 3, 4	caucvgsrlemoffval 8107	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ N) → ((𝐺‘𝑛) +R 𝐴) = ((𝐹‘𝑛) +R 1R))
6	5	adantr 276	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → ((𝐺‘𝑛) +R 𝐴) = ((𝐹‘𝑛) +R 1R))
7	6	eqcomd 2238	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → ((𝐹‘𝑛) +R 1R) = ((𝐺‘𝑛) +R 𝐴))
8	2	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → 𝐹:N⟶R)
9		simpr 110	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → 𝑘 ∈ N)
10	8, 9	ffvelcdmd 5812	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (𝐹‘𝑘) ∈ R)
11		simplr 529	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → 𝑛 ∈ N)
12		recnnpr 7859	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ N → ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ ∈ P)
13		prsrcl 8095	. . . . . . . . . . . 12 ⊢ (⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ ∈ P → [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ∈ R)
14	11, 12, 13	3syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ∈ R)
15		1sr 8062	. . . . . . . . . . . 12 ⊢ 1R ∈ R
16	15	a1i 9	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → 1R ∈ R)
17		addcomsrg 8066	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ R ∧ 𝑔 ∈ R) → (𝑓 +R 𝑔) = (𝑔 +R 𝑓))
18	17	adantl 277	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧ (𝑓 ∈ R ∧ 𝑔 ∈ R)) → (𝑓 +R 𝑔) = (𝑔 +R 𝑓))
19		addasssrg 8067	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R) → ((𝑓 +R 𝑔) +R ℎ) = (𝑓 +R (𝑔 +R ℎ)))
20	19	adantl 277	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧ (𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R)) → ((𝑓 +R 𝑔) +R ℎ) = (𝑓 +R (𝑔 +R ℎ)))
21	10, 14, 16, 18, 20	caov32d 6234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 1R) = (((𝐹‘𝑘) +R 1R) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))
22	2, 1, 3, 4	caucvgsrlemoffval 8107	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ N) → ((𝐺‘𝑘) +R 𝐴) = ((𝐹‘𝑘) +R 1R))
23	22	adantlr 477	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → ((𝐺‘𝑘) +R 𝐴) = ((𝐹‘𝑘) +R 1R))
24	23	oveq1d 6064	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (((𝐺‘𝑘) +R 𝐴) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) = (((𝐹‘𝑘) +R 1R) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))
25	2, 1, 3, 4	caucvgsrlemofff 8108	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺:N⟶R)
26	25	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → 𝐺:N⟶R)
27	26, 9	ffvelcdmd 5812	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (𝐺‘𝑘) ∈ R)
28	3	caucvgsrlemasr 8101	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ R)
29	28	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → 𝐴 ∈ R)
30	27, 29, 14, 18, 20	caov32d 6234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (((𝐺‘𝑘) +R 𝐴) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) = (((𝐺‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 𝐴))
31	21, 24, 30	3eqtr2d 2271	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 1R) = (((𝐺‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 𝐴))
32	7, 31	breq12d 4121	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (((𝐹‘𝑛) +R 1R) <R (((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 1R) ↔ ((𝐺‘𝑛) +R 𝐴) <R (((𝐺‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 𝐴)))
33		ltasrg 8081	. . . . . . . . . 10 ⊢ ((𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R) → (𝑓 <R 𝑔 ↔ (ℎ +R 𝑓) <R (ℎ +R 𝑔)))
34	33	adantl 277	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) ∧ (𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R)) → (𝑓 <R 𝑔 ↔ (ℎ +R 𝑓) <R (ℎ +R 𝑔)))
35	8, 11	ffvelcdmd 5812	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (𝐹‘𝑛) ∈ R)
36		addclsr 8064	. . . . . . . . . 10 ⊢ (((𝐹‘𝑘) ∈ 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 ) ∈ R)
37	10, 14, 36	syl2anc 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∈ R)
38	34, 35, 37, 16, 18	caovord2d 6223	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ↔ ((𝐹‘𝑛) +R 1R) <R (((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 1R)))
39	26, 11	ffvelcdmd 5812	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (𝐺‘𝑛) ∈ R)
40		addclsr 8064	. . . . . . . . . 10 ⊢ (((𝐺‘𝑘) ∈ 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 ) ∈ R)
41	27, 14, 40	syl2anc 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → ((𝐺‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∈ R)
42	34, 39, 41, 29, 18	caovord2d 6223	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → ((𝐺‘𝑛) <R ((𝐺‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ↔ ((𝐺‘𝑛) +R 𝐴) <R (((𝐺‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 𝐴)))
43	32, 38, 42	3bitr4d 220	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ 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 )))
44	23	eqcomd 2238	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → ((𝐹‘𝑘) +R 1R) = ((𝐺‘𝑘) +R 𝐴))
45	35, 14, 16, 18, 20	caov32d 6234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 1R) = (((𝐹‘𝑛) +R 1R) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))
46	6	oveq1d 6064	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (((𝐺‘𝑛) +R 𝐴) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) = (((𝐹‘𝑛) +R 1R) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))
47	39, 29, 14, 18, 20	caov32d 6234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (((𝐺‘𝑛) +R 𝐴) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) = (((𝐺‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 𝐴))
48	45, 46, 47	3eqtr2d 2271	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 1R) = (((𝐺‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 𝐴))
49	44, 48	breq12d 4121	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → (((𝐹‘𝑘) +R 1R) <R (((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 1R) ↔ ((𝐺‘𝑘) +R 𝐴) <R (((𝐺‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 𝐴)))
50		addclsr 8064	. . . . . . . . . 10 ⊢ (((𝐹‘𝑛) ∈ 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 ) ∈ R)
51	35, 14, 50	syl2anc 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∈ R)
52	34, 10, 51, 16, 18	caovord2d 6223	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → ((𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ↔ ((𝐹‘𝑘) +R 1R) <R (((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 1R)))
53		addclsr 8064	. . . . . . . . . 10 ⊢ (((𝐺‘𝑛) ∈ 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 ) ∈ R)
54	39, 14, 53	syl2anc 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → ((𝐺‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∈ R)
55	34, 27, 54, 29, 18	caovord2d 6223	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ N) ∧ 𝑘 ∈ N) → ((𝐺‘𝑘) <R ((𝐺‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ↔ ((𝐺‘𝑘) +R 𝐴) <R (((𝐺‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) +R 𝐴)))
56	49, 52, 55	3bitr4d 220	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ 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 )))
57	43, 56	anbi12d 473	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ 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 )) ↔ ((𝐺‘𝑛) <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 ))))
58	57	biimpd 144	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ 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 )) → ((𝐺‘𝑛) <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 ))))
59	58	imim2d 54	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ 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 ))) → (𝑛 <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 )))))
60	59	ralimdva 2609	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ 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 ))) → ∀𝑘 ∈ 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 )))))
61	60	ralimdva 2609	. 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 ))) → ∀𝑛 ∈ 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 )))))
62	1, 61	mpd 13	1 ⊢ (𝜑 → ∀𝑛 ∈ 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 ))))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1005   = wceq 1398   ∈ wcel 2203  {cab 2218  ∀wral 2520  ⟨cop 3691   class class class wbr 4108   ↦ cmpt 4170  ⟶wf 5347  ‘cfv 5351  (class class class)co 6049  1_oc1o 6639  [cec 6764  Ncnpi 7583   <_N clti 7586   ~_Q ceq 7590  *_Qcrq 7595   <_Q cltq 7596  Pcnp 7602  1_Pc1p 7603   +_P cpp 7604   ~_R cer 7607  Rcnr 7608  1_Rc1r 7610  -1_Rcm1r 7611   +_R cplr 7612   ·_R cmr 7613   <_R cltr 7614

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 2205  ax-14 2206  ax-ext 2214  ax-coll 4224  ax-sep 4227  ax-nul 4235  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-setind 4658  ax-iinf 4709

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 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2814  df-sbc 3042  df-csb 3138  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-nul 3508  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-int 3949  df-iun 3992  df-br 4109  df-opab 4171  df-mpt 4172  df-tr 4208  df-eprel 4409  df-id 4413  df-po 4416  df-iso 4417  df-iord 4486  df-on 4488  df-suc 4491  df-iom 4712  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-rn 4759  df-res 4760  df-ima 4761  df-iota 5311  df-fun 5353  df-fn 5354  df-f 5355  df-f1 5356  df-fo 5357  df-f1o 5358  df-fv 5359  df-ov 6052  df-oprab 6053  df-mpo 6054  df-1st 6333  df-2nd 6334  df-recs 6535  df-irdg 6600  df-1o 6646  df-2o 6647  df-oadd 6650  df-omul 6651  df-er 6766  df-ec 6768  df-qs 6772  df-ni 7615  df-pli 7616  df-mi 7617  df-lti 7618  df-plpq 7655  df-mpq 7656  df-enq 7658  df-nqqs 7659  df-plqqs 7660  df-mqqs 7661  df-1nqqs 7662  df-rq 7663  df-ltnqqs 7664  df-enq0 7735  df-nq0 7736  df-0nq0 7737  df-plq0 7738  df-mq0 7739  df-inp 7777  df-i1p 7778  df-iplp 7779  df-imp 7780  df-iltp 7781  df-enr 8037  df-nr 8038  df-plr 8039  df-mr 8040  df-ltr 8041  df-0r 8042  df-1r 8043  df-m1r 8044

This theorem is referenced by:  caucvgsrlemoffres  8111