Theorem caucvgsrlemfv 6967

Description: Lemma for caucvgsr 6978. Coercing sequence value from a positive real to a signed real. (Contributed by Jim Kingdon, 29-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 ))))
caucvgsrlemgt1.gt1	⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐹‘𝑚))
caucvgsrlemf.xfr	⊢ 𝐺 = (𝑥 ∈ N ↦ (℩𝑦 ∈ P (𝐹‘𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))

Assertion

Ref	Expression
caucvgsrlemfv	⊢ ((𝜑 ∧ 𝐴 ∈ N) → [⟨((𝐺‘𝐴) +P 1P), 1P⟩] ~R = (𝐹‘𝐴))

Distinct variable groups:   𝐴,𝑚   𝑥,𝐴,𝑦   𝑚,𝐹   𝑥,𝐹,𝑦   𝜑,𝑥

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

Proof of Theorem caucvgsrlemfv

Step	Hyp	Ref	Expression
1		caucvgsrlemf.xfr	. . . . . . 7 ⊢ 𝐺 = (𝑥 ∈ N ↦ (℩𝑦 ∈ P (𝐹‘𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
2	1	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → 𝐺 = (𝑥 ∈ N ↦ (℩𝑦 ∈ P (𝐹‘𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R )))
3		fveq2 5198	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
4	3	eqeq1d 2089	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ↔ (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
5	4	riotabidv 5490	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (℩𝑦 ∈ P (𝐹‘𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) = (℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
6	5	adantl 271	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ N) ∧ 𝑥 = 𝐴) → (℩𝑦 ∈ P (𝐹‘𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) = (℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
7		simpr 108	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → 𝐴 ∈ N)
8		caucvgsr.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:N⟶R)
9		caucvgsrlemgt1.gt1	. . . . . . 7 ⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐹‘𝑚))
10	8, 9	caucvgsrlemcl 6965	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → (℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) ∈ P)
11	2, 6, 7, 10	fvmptd 5274	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → (𝐺‘𝐴) = (℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
12	11	oveq1d 5547	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → ((𝐺‘𝐴) +P 1P) = ((℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P))
13	12	opeq1d 3576	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → ⟨((𝐺‘𝐴) +P 1P), 1P⟩ = ⟨((℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P), 1P⟩)
14	13	eceq1d 6165	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → [⟨((𝐺‘𝐴) +P 1P), 1P⟩] ~R = [⟨((℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P), 1P⟩] ~R )
15		eqcom 2083	. . . . . . 7 ⊢ ((𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ↔ [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹‘𝐴))
16	15	a1i 9	. . . . . 6 ⊢ (𝑦 ∈ P → ((𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ↔ [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹‘𝐴)))
17	16	riotabiia 5505	. . . . 5 ⊢ (℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) = (℩𝑦 ∈ P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹‘𝐴))
18	17	oveq1i 5542	. . . 4 ⊢ ((℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P) = ((℩𝑦 ∈ P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹‘𝐴)) +P 1P)
19	18	opeq1i 3573	. . 3 ⊢ ⟨((℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P), 1P⟩ = ⟨((℩𝑦 ∈ P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹‘𝐴)) +P 1P), 1P⟩
20		eceq1 6164	. . 3 ⊢ (⟨((℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P), 1P⟩ = ⟨((℩𝑦 ∈ P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹‘𝐴)) +P 1P), 1P⟩ → [⟨((℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P), 1P⟩] ~R = [⟨((℩𝑦 ∈ P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹‘𝐴)) +P 1P), 1P⟩] ~R )
21	19, 20	mp1i 10	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → [⟨((℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P), 1P⟩] ~R = [⟨((℩𝑦 ∈ P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹‘𝐴)) +P 1P), 1P⟩] ~R )
22	8	ffvelrnda 5323	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → (𝐹‘𝐴) ∈ R)
23		0lt1sr 6942	. . . 4 ⊢ 0R <R 1R
24		fveq2 5198	. . . . . . 7 ⊢ (𝑚 = 𝐴 → (𝐹‘𝑚) = (𝐹‘𝐴))
25	24	breq2d 3797	. . . . . 6 ⊢ (𝑚 = 𝐴 → (1R <R (𝐹‘𝑚) ↔ 1R <R (𝐹‘𝐴)))
26	25	rspcv 2697	. . . . 5 ⊢ (𝐴 ∈ N → (∀𝑚 ∈ N 1R <R (𝐹‘𝑚) → 1R <R (𝐹‘𝐴)))
27	9, 26	mpan9 275	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → 1R <R (𝐹‘𝐴))
28		ltsosr 6941	. . . . 5 ⊢ <R Or R
29		ltrelsr 6915	. . . . 5 ⊢ <R ⊆ (R × R)
30	28, 29	sotri 4740	. . . 4 ⊢ ((0R <R 1R ∧ 1R <R (𝐹‘𝐴)) → 0R <R (𝐹‘𝐴))
31	23, 27, 30	sylancr 405	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → 0R <R (𝐹‘𝐴))
32		prsrriota 6964	. . 3 ⊢ (((𝐹‘𝐴) ∈ R ∧ 0R <R (𝐹‘𝐴)) → [⟨((℩𝑦 ∈ P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹‘𝐴)) +P 1P), 1P⟩] ~R = (𝐹‘𝐴))
33	22, 31, 32	syl2anc 403	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → [⟨((℩𝑦 ∈ P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹‘𝐴)) +P 1P), 1P⟩] ~R = (𝐹‘𝐴))
34	14, 21, 33	3eqtrd 2117	1 ⊢ ((𝜑 ∧ 𝐴 ∈ N) → [⟨((𝐺‘𝐴) +P 1P), 1P⟩] ~R = (𝐹‘𝐴))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   = wceq 1284   ∈ wcel 1433  {cab 2067  ∀wral 2348  ⟨cop 3401   class class class wbr 3785   ↦ cmpt 3839  ⟶wf 4918  ‘cfv 4922  ℩crio 5487  (class class class)co 5532  1_𝑜c1o 6017  [cec 6127  Ncnpi 6462   <_N clti 6465   ~_Q ceq 6469  *_Qcrq 6474   <_Q cltq 6475  Pcnp 6481  1_Pc1p 6482   +_P cpp 6483   ~_R cer 6486  Rcnr 6487  0_Rc0r 6488  1_Rc1r 6489   +_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-iltp 6660  df-enr 6903  df-nr 6904  df-ltr 6907  df-0r 6908  df-1r 6909

This theorem is referenced by:  caucvgsrlemcau  6969  caucvgsrlembound  6970  caucvgsrlemgt1  6971