![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > caucvgsrlemoffval | GIF version |
Description: Lemma for caucvgsr 7497. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-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 )))) |
caucvgsrlembnd.bnd | ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚)) |
caucvgsrlembnd.offset | ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R))) |
Ref | Expression |
---|---|
caucvgsrlemoffval | ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ((𝐺‘𝐽) +R 𝐴) = ((𝐹‘𝐽) +R 1R)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | caucvgsrlembnd.offset | . . . . 5 ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R))) | |
2 | 1 | a1i 9 | . . . 4 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R)))) |
3 | fveq2 5353 | . . . . . . 7 ⊢ (𝑎 = 𝐽 → (𝐹‘𝑎) = (𝐹‘𝐽)) | |
4 | 3 | oveq1d 5721 | . . . . . 6 ⊢ (𝑎 = 𝐽 → ((𝐹‘𝑎) +R 1R) = ((𝐹‘𝐽) +R 1R)) |
5 | 4 | oveq1d 5721 | . . . . 5 ⊢ (𝑎 = 𝐽 → (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R)) = (((𝐹‘𝐽) +R 1R) +R (𝐴 ·R -1R))) |
6 | 5 | adantl 273 | . . . 4 ⊢ (((𝜑 ∧ 𝐽 ∈ N) ∧ 𝑎 = 𝐽) → (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R)) = (((𝐹‘𝐽) +R 1R) +R (𝐴 ·R -1R))) |
7 | simpr 109 | . . . 4 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → 𝐽 ∈ N) | |
8 | caucvgsr.f | . . . . . . 7 ⊢ (𝜑 → 𝐹:N⟶R) | |
9 | 8 | ffvelrnda 5487 | . . . . . 6 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐹‘𝐽) ∈ R) |
10 | 1sr 7447 | . . . . . 6 ⊢ 1R ∈ R | |
11 | addclsr 7449 | . . . . . 6 ⊢ (((𝐹‘𝐽) ∈ R ∧ 1R ∈ R) → ((𝐹‘𝐽) +R 1R) ∈ R) | |
12 | 9, 10, 11 | sylancl 407 | . . . . 5 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ((𝐹‘𝐽) +R 1R) ∈ R) |
13 | caucvgsrlembnd.bnd | . . . . . . . 8 ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚)) | |
14 | 13 | caucvgsrlemasr 7485 | . . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ R) |
15 | 14 | adantr 272 | . . . . . 6 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → 𝐴 ∈ R) |
16 | m1r 7448 | . . . . . 6 ⊢ -1R ∈ R | |
17 | mulclsr 7450 | . . . . . 6 ⊢ ((𝐴 ∈ R ∧ -1R ∈ R) → (𝐴 ·R -1R) ∈ R) | |
18 | 15, 16, 17 | sylancl 407 | . . . . 5 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐴 ·R -1R) ∈ R) |
19 | addclsr 7449 | . . . . 5 ⊢ ((((𝐹‘𝐽) +R 1R) ∈ R ∧ (𝐴 ·R -1R) ∈ R) → (((𝐹‘𝐽) +R 1R) +R (𝐴 ·R -1R)) ∈ R) | |
20 | 12, 18, 19 | syl2anc 406 | . . . 4 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (((𝐹‘𝐽) +R 1R) +R (𝐴 ·R -1R)) ∈ R) |
21 | 2, 6, 7, 20 | fvmptd 5434 | . . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐺‘𝐽) = (((𝐹‘𝐽) +R 1R) +R (𝐴 ·R -1R))) |
22 | 21 | oveq1d 5721 | . 2 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ((𝐺‘𝐽) +R 𝐴) = ((((𝐹‘𝐽) +R 1R) +R (𝐴 ·R -1R)) +R 𝐴)) |
23 | addasssrg 7452 | . . 3 ⊢ ((((𝐹‘𝐽) +R 1R) ∈ R ∧ (𝐴 ·R -1R) ∈ R ∧ 𝐴 ∈ R) → ((((𝐹‘𝐽) +R 1R) +R (𝐴 ·R -1R)) +R 𝐴) = (((𝐹‘𝐽) +R 1R) +R ((𝐴 ·R -1R) +R 𝐴))) | |
24 | 12, 18, 15, 23 | syl3anc 1184 | . 2 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ((((𝐹‘𝐽) +R 1R) +R (𝐴 ·R -1R)) +R 𝐴) = (((𝐹‘𝐽) +R 1R) +R ((𝐴 ·R -1R) +R 𝐴))) |
25 | addcomsrg 7451 | . . . . . 6 ⊢ (((𝐴 ·R -1R) ∈ R ∧ 𝐴 ∈ R) → ((𝐴 ·R -1R) +R 𝐴) = (𝐴 +R (𝐴 ·R -1R))) | |
26 | 18, 15, 25 | syl2anc 406 | . . . . 5 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ((𝐴 ·R -1R) +R 𝐴) = (𝐴 +R (𝐴 ·R -1R))) |
27 | pn0sr 7467 | . . . . . 6 ⊢ (𝐴 ∈ R → (𝐴 +R (𝐴 ·R -1R)) = 0R) | |
28 | 15, 27 | syl 14 | . . . . 5 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐴 +R (𝐴 ·R -1R)) = 0R) |
29 | 26, 28 | eqtrd 2132 | . . . 4 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ((𝐴 ·R -1R) +R 𝐴) = 0R) |
30 | 29 | oveq2d 5722 | . . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (((𝐹‘𝐽) +R 1R) +R ((𝐴 ·R -1R) +R 𝐴)) = (((𝐹‘𝐽) +R 1R) +R 0R)) |
31 | 0idsr 7463 | . . . 4 ⊢ (((𝐹‘𝐽) +R 1R) ∈ R → (((𝐹‘𝐽) +R 1R) +R 0R) = ((𝐹‘𝐽) +R 1R)) | |
32 | 12, 31 | syl 14 | . . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (((𝐹‘𝐽) +R 1R) +R 0R) = ((𝐹‘𝐽) +R 1R)) |
33 | 30, 32 | eqtrd 2132 | . 2 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (((𝐹‘𝐽) +R 1R) +R ((𝐴 ·R -1R) +R 𝐴)) = ((𝐹‘𝐽) +R 1R)) |
34 | 22, 24, 33 | 3eqtrd 2136 | 1 ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ((𝐺‘𝐽) +R 𝐴) = ((𝐹‘𝐽) +R 1R)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1299 ∈ wcel 1448 {cab 2086 ∀wral 2375 〈cop 3477 class class class wbr 3875 ↦ cmpt 3929 ⟶wf 5055 ‘cfv 5059 (class class class)co 5706 1oc1o 6236 [cec 6357 Ncnpi 6981 <N clti 6984 ~Q ceq 6988 *Qcrq 6993 <Q cltq 6994 1Pc1p 7001 +P cpp 7002 ~R cer 7005 Rcnr 7006 0Rc0r 7007 1Rc1r 7008 -1Rcm1r 7009 +R cplr 7010 ·R cmr 7011 <R cltr 7012 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-13 1459 ax-14 1460 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-coll 3983 ax-sep 3986 ax-nul 3994 ax-pow 4038 ax-pr 4069 ax-un 4293 ax-setind 4390 ax-iinf 4440 |
This theorem depends on definitions: df-bi 116 df-dc 787 df-3or 931 df-3an 932 df-tru 1302 df-fal 1305 df-nf 1405 df-sb 1704 df-eu 1963 df-mo 1964 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ne 2268 df-ral 2380 df-rex 2381 df-reu 2382 df-rab 2384 df-v 2643 df-sbc 2863 df-csb 2956 df-dif 3023 df-un 3025 df-in 3027 df-ss 3034 df-nul 3311 df-pw 3459 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-int 3719 df-iun 3762 df-br 3876 df-opab 3930 df-mpt 3931 df-tr 3967 df-eprel 4149 df-id 4153 df-po 4156 df-iso 4157 df-iord 4226 df-on 4228 df-suc 4231 df-iom 4443 df-xp 4483 df-rel 4484 df-cnv 4485 df-co 4486 df-dm 4487 df-rn 4488 df-res 4489 df-ima 4490 df-iota 5024 df-fun 5061 df-fn 5062 df-f 5063 df-f1 5064 df-fo 5065 df-f1o 5066 df-fv 5067 df-ov 5709 df-oprab 5710 df-mpo 5711 df-1st 5969 df-2nd 5970 df-recs 6132 df-irdg 6197 df-1o 6243 df-2o 6244 df-oadd 6247 df-omul 6248 df-er 6359 df-ec 6361 df-qs 6365 df-ni 7013 df-pli 7014 df-mi 7015 df-lti 7016 df-plpq 7053 df-mpq 7054 df-enq 7056 df-nqqs 7057 df-plqqs 7058 df-mqqs 7059 df-1nqqs 7060 df-rq 7061 df-ltnqqs 7062 df-enq0 7133 df-nq0 7134 df-0nq0 7135 df-plq0 7136 df-mq0 7137 df-inp 7175 df-i1p 7176 df-iplp 7177 df-imp 7178 df-enr 7422 df-nr 7423 df-plr 7424 df-mr 7425 df-ltr 7426 df-0r 7427 df-1r 7428 df-m1r 7429 |
This theorem is referenced by: caucvgsrlemoffcau 7493 caucvgsrlemoffgt1 7494 caucvgsrlemoffres 7495 |
Copyright terms: Public domain | W3C validator |