ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  caucvgsrlemfv GIF version

Theorem caucvgsrlemfv 7099
Description: Lemma for caucvgsr 7110. Coercing sequence value from a positive real to a signed real. (Contributed by Jim Kingdon, 29-Jun-2021.)
Hypotheses
Ref Expression
caucvgsr.f (𝜑𝐹:NR)
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
StepHypRef Expression
1 caucvgsrlemf.xfr . . . . . . 7 𝐺 = (𝑥N ↦ (𝑦P (𝐹𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
21a1i 9 . . . . . 6 ((𝜑𝐴N) → 𝐺 = (𝑥N ↦ (𝑦P (𝐹𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R )))
3 fveq2 5230 . . . . . . . . 9 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
43eqeq1d 2091 . . . . . . . 8 (𝑥 = 𝐴 → ((𝐹𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ↔ (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
54riotabidv 5522 . . . . . . 7 (𝑥 = 𝐴 → (𝑦P (𝐹𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) = (𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
65adantl 271 . . . . . 6 (((𝜑𝐴N) ∧ 𝑥 = 𝐴) → (𝑦P (𝐹𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) = (𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
7 simpr 108 . . . . . 6 ((𝜑𝐴N) → 𝐴N)
8 caucvgsr.f . . . . . . 7 (𝜑𝐹:NR)
9 caucvgsrlemgt1.gt1 . . . . . . 7 (𝜑 → ∀𝑚N 1R <R (𝐹𝑚))
108, 9caucvgsrlemcl 7097 . . . . . 6 ((𝜑𝐴N) → (𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) ∈ P)
112, 6, 7, 10fvmptd 5306 . . . . 5 ((𝜑𝐴N) → (𝐺𝐴) = (𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
1211oveq1d 5579 . . . 4 ((𝜑𝐴N) → ((𝐺𝐴) +P 1P) = ((𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P))
1312opeq1d 3596 . . 3 ((𝜑𝐴N) → ⟨((𝐺𝐴) +P 1P), 1P⟩ = ⟨((𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P), 1P⟩)
1413eceq1d 6230 . 2 ((𝜑𝐴N) → [⟨((𝐺𝐴) +P 1P), 1P⟩] ~R = [⟨((𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P), 1P⟩] ~R )
15 eqcom 2085 . . . . . . 7 ((𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ↔ [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹𝐴))
1615a1i 9 . . . . . 6 (𝑦P → ((𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ↔ [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹𝐴)))
1716riotabiia 5537 . . . . 5 (𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) = (𝑦P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹𝐴))
1817oveq1i 5574 . . . 4 ((𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P) = ((𝑦P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹𝐴)) +P 1P)
1918opeq1i 3593 . . 3 ⟨((𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P), 1P⟩ = ⟨((𝑦P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹𝐴)) +P 1P), 1P
20 eceq1 6229 . . 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 )
2119, 20mp1i 10 . 2 ((𝜑𝐴N) → [⟨((𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) +P 1P), 1P⟩] ~R = [⟨((𝑦P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹𝐴)) +P 1P), 1P⟩] ~R )
228ffvelrnda 5355 . . 3 ((𝜑𝐴N) → (𝐹𝐴) ∈ R)
23 0lt1sr 7074 . . . 4 0R <R 1R
24 fveq2 5230 . . . . . . 7 (𝑚 = 𝐴 → (𝐹𝑚) = (𝐹𝐴))
2524breq2d 3817 . . . . . 6 (𝑚 = 𝐴 → (1R <R (𝐹𝑚) ↔ 1R <R (𝐹𝐴)))
2625rspcv 2706 . . . . 5 (𝐴N → (∀𝑚N 1R <R (𝐹𝑚) → 1R <R (𝐹𝐴)))
279, 26mpan9 275 . . . 4 ((𝜑𝐴N) → 1R <R (𝐹𝐴))
28 ltsosr 7073 . . . . 5 <R Or R
29 ltrelsr 7047 . . . . 5 <R ⊆ (R × R)
3028, 29sotri 4770 . . . 4 ((0R <R 1R ∧ 1R <R (𝐹𝐴)) → 0R <R (𝐹𝐴))
3123, 27, 30sylancr 405 . . 3 ((𝜑𝐴N) → 0R <R (𝐹𝐴))
32 prsrriota 7096 . . 3 (((𝐹𝐴) ∈ R ∧ 0R <R (𝐹𝐴)) → [⟨((𝑦P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹𝐴)) +P 1P), 1P⟩] ~R = (𝐹𝐴))
3322, 31, 32syl2anc 403 . 2 ((𝜑𝐴N) → [⟨((𝑦P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹𝐴)) +P 1P), 1P⟩] ~R = (𝐹𝐴))
3414, 21, 333eqtrd 2119 1 ((𝜑𝐴N) → [⟨((𝐺𝐴) +P 1P), 1P⟩] ~R = (𝐹𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1285  wcel 1434  {cab 2069  wral 2353  cop 3419   class class class wbr 3805  cmpt 3859  wf 4948  cfv 4952  crio 5519  (class class class)co 5564  1𝑜c1o 6079  [cec 6192  Ncnpi 6594   <N clti 6597   ~Q ceq 6601  *Qcrq 6606   <Q cltq 6607  Pcnp 6613  1Pc1p 6614   +P cpp 6615   ~R cer 6618  Rcnr 6619  0Rc0r 6620  1Rc1r 6621   +R cplr 6623   <R cltr 6625
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 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3913  ax-sep 3916  ax-nul 3924  ax-pow 3968  ax-pr 3992  ax-un 4216  ax-setind 4308  ax-iinf 4357
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-reu 2360  df-rmo 2361  df-rab 2362  df-v 2612  df-sbc 2825  df-csb 2918  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-nul 3268  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-int 3657  df-iun 3700  df-br 3806  df-opab 3860  df-mpt 3861  df-tr 3896  df-eprel 4072  df-id 4076  df-po 4079  df-iso 4080  df-iord 4149  df-on 4151  df-suc 4154  df-iom 4360  df-xp 4397  df-rel 4398  df-cnv 4399  df-co 4400  df-dm 4401  df-rn 4402  df-res 4403  df-ima 4404  df-iota 4917  df-fun 4954  df-fn 4955  df-f 4956  df-f1 4957  df-fo 4958  df-f1o 4959  df-fv 4960  df-riota 5520  df-ov 5567  df-oprab 5568  df-mpt2 5569  df-1st 5819  df-2nd 5820  df-recs 5975  df-irdg 6040  df-1o 6086  df-2o 6087  df-oadd 6090  df-omul 6091  df-er 6194  df-ec 6196  df-qs 6200  df-ni 6626  df-pli 6627  df-mi 6628  df-lti 6629  df-plpq 6666  df-mpq 6667  df-enq 6669  df-nqqs 6670  df-plqqs 6671  df-mqqs 6672  df-1nqqs 6673  df-rq 6674  df-ltnqqs 6675  df-enq0 6746  df-nq0 6747  df-0nq0 6748  df-plq0 6749  df-mq0 6750  df-inp 6788  df-i1p 6789  df-iplp 6790  df-iltp 6792  df-enr 7035  df-nr 7036  df-ltr 7039  df-0r 7040  df-1r 7041
This theorem is referenced by:  caucvgsrlemcau  7101  caucvgsrlembound  7102  caucvgsrlemgt1  7103
  Copyright terms: Public domain W3C validator