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

Theorem caucvgsrlemcl 6930
 Description: Lemma for caucvgsr 6943. Terms of the sequence from caucvgsrlemgt1 6936 can be mapped to positive reals. (Contributed by Jim Kingdon, 2-Jul-2021.)
Hypotheses
Ref Expression
caucvgsrlemcl.f (𝜑𝐹:NR)
caucvgsrlemcl.gt1 (𝜑 → ∀𝑚N 1R <R (𝐹𝑚))
Assertion
Ref Expression
caucvgsrlemcl ((𝜑𝐴N) → (𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) ∈ P)
Distinct variable groups:   𝐴,𝑚   𝑦,𝐴   𝑚,𝐹   𝑦,𝐹
Allowed substitution hints:   𝜑(𝑦,𝑚)

Proof of Theorem caucvgsrlemcl
StepHypRef Expression
1 caucvgsrlemcl.f . . . . 5 (𝜑𝐹:NR)
21ffvelrnda 5329 . . . 4 ((𝜑𝐴N) → (𝐹𝐴) ∈ R)
3 0lt1sr 6907 . . . . 5 0R <R 1R
4 caucvgsrlemcl.gt1 . . . . . 6 (𝜑 → ∀𝑚N 1R <R (𝐹𝑚))
5 fveq2 5205 . . . . . . . 8 (𝑚 = 𝐴 → (𝐹𝑚) = (𝐹𝐴))
65breq2d 3803 . . . . . . 7 (𝑚 = 𝐴 → (1R <R (𝐹𝑚) ↔ 1R <R (𝐹𝐴)))
76rspcv 2669 . . . . . 6 (𝐴N → (∀𝑚N 1R <R (𝐹𝑚) → 1R <R (𝐹𝐴)))
84, 7mpan9 269 . . . . 5 ((𝜑𝐴N) → 1R <R (𝐹𝐴))
9 ltsosr 6906 . . . . . 6 <R Or R
10 ltrelsr 6880 . . . . . 6 <R ⊆ (R × R)
119, 10sotri 4747 . . . . 5 ((0R <R 1R ∧ 1R <R (𝐹𝐴)) → 0R <R (𝐹𝐴))
123, 8, 11sylancr 399 . . . 4 ((𝜑𝐴N) → 0R <R (𝐹𝐴))
13 srpospr 6924 . . . 4 (((𝐹𝐴) ∈ R ∧ 0R <R (𝐹𝐴)) → ∃!𝑦P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹𝐴))
142, 12, 13syl2anc 397 . . 3 ((𝜑𝐴N) → ∃!𝑦P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹𝐴))
15 eqcom 2058 . . . 4 ([⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹𝐴) ↔ (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R )
1615reubii 2512 . . 3 (∃!𝑦P [⟨(𝑦 +P 1P), 1P⟩] ~R = (𝐹𝐴) ↔ ∃!𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R )
1714, 16sylib 131 . 2 ((𝜑𝐴N) → ∃!𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R )
18 riotacl 5509 . 2 (∃!𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R → (𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) ∈ P)
1917, 18syl 14 1 ((𝜑𝐴N) → (𝑦P (𝐹𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) ∈ P)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   = wceq 1259   ∈ wcel 1409  ∀wral 2323  ∃!wreu 2325  ⟨cop 3405   class class class wbr 3791  ⟶wf 4925  ‘cfv 4929  ℩crio 5494  (class class class)co 5539  [cec 6134  Ncnpi 6427  Pcnp 6446  1Pc1p 6447   +P cpp 6448   ~R cer 6451  Rcnr 6452  0Rc0r 6453  1Rc1r 6454
 Copyright terms: Public domain W3C validator