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

Theorem resqrexlemsqa 11053
Description: Lemma for resqrex 11055. The square of a limit is 𝐴. (Contributed by Jim Kingdon, 7-Aug-2021.)
Hypotheses
Ref Expression
resqrexlemex.seq 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (β„• Γ— {(1 + 𝐴)}))
resqrexlemex.a (πœ‘ β†’ 𝐴 ∈ ℝ)
resqrexlemex.agt0 (πœ‘ β†’ 0 ≀ 𝐴)
resqrexlemgt0.rr (πœ‘ β†’ 𝐿 ∈ ℝ)
resqrexlemgt0.lim (πœ‘ β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘–) < (𝐿 + 𝑒) ∧ 𝐿 < ((πΉβ€˜π‘–) + 𝑒)))
Assertion
Ref Expression
resqrexlemsqa (πœ‘ β†’ (𝐿↑2) = 𝐴)
Distinct variable groups:   𝐴,𝑒,𝑗   𝑦,𝐴,𝑧   𝑒,𝐹,𝑗   𝑦,𝐹,𝑧   𝑖,𝐹   𝑒,𝐿,𝑗,𝑖   𝑦,𝐿,𝑧   𝑒,𝑖,𝑗   πœ‘,𝑦,𝑧
Allowed substitution hints:   πœ‘(𝑒,𝑖,𝑗)   𝐴(𝑖)

Proof of Theorem resqrexlemsqa
Dummy variables π‘Ž 𝑏 𝑐 𝑑 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 resqrexlemex.seq . . . . . . 7 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (β„• Γ— {(1 + 𝐴)}))
2 resqrexlemex.a . . . . . . 7 (πœ‘ β†’ 𝐴 ∈ ℝ)
3 resqrexlemex.agt0 . . . . . . 7 (πœ‘ β†’ 0 ≀ 𝐴)
41, 2, 3resqrexlemf 11036 . . . . . 6 (πœ‘ β†’ 𝐹:β„•βŸΆβ„+)
54ffvelcdmda 5668 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ β„•) β†’ (πΉβ€˜π‘₯) ∈ ℝ+)
6 2z 9301 . . . . . 6 2 ∈ β„€
76a1i 9 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ β„•) β†’ 2 ∈ β„€)
85, 7rpexpcld 10698 . . . 4 ((πœ‘ ∧ π‘₯ ∈ β„•) β†’ ((πΉβ€˜π‘₯)↑2) ∈ ℝ+)
9 eqid 2189 . . . 4 (π‘₯ ∈ β„• ↦ ((πΉβ€˜π‘₯)↑2)) = (π‘₯ ∈ β„• ↦ ((πΉβ€˜π‘₯)↑2))
108, 9fmptd 5687 . . 3 (πœ‘ β†’ (π‘₯ ∈ β„• ↦ ((πΉβ€˜π‘₯)↑2)):β„•βŸΆβ„+)
11 rpssre 9684 . . . 4 ℝ+ βŠ† ℝ
1211a1i 9 . . 3 (πœ‘ β†’ ℝ+ βŠ† ℝ)
1310, 12fssd 5394 . 2 (πœ‘ β†’ (π‘₯ ∈ β„• ↦ ((πΉβ€˜π‘₯)↑2)):β„•βŸΆβ„)
14 resqrexlemgt0.rr . . 3 (πœ‘ β†’ 𝐿 ∈ ℝ)
1514resqcld 10700 . 2 (πœ‘ β†’ (𝐿↑2) ∈ ℝ)
16 resqrexlemgt0.lim . . . 4 (πœ‘ β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘–) < (𝐿 + 𝑒) ∧ 𝐿 < ((πΉβ€˜π‘–) + 𝑒)))
17 oveq2 5900 . . . . . . . . 9 (𝑒 = π‘Ž β†’ (𝐿 + 𝑒) = (𝐿 + π‘Ž))
1817breq2d 4030 . . . . . . . 8 (𝑒 = π‘Ž β†’ ((πΉβ€˜π‘–) < (𝐿 + 𝑒) ↔ (πΉβ€˜π‘–) < (𝐿 + π‘Ž)))
19 oveq2 5900 . . . . . . . . 9 (𝑒 = π‘Ž β†’ ((πΉβ€˜π‘–) + 𝑒) = ((πΉβ€˜π‘–) + π‘Ž))
2019breq2d 4030 . . . . . . . 8 (𝑒 = π‘Ž β†’ (𝐿 < ((πΉβ€˜π‘–) + 𝑒) ↔ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž)))
2118, 20anbi12d 473 . . . . . . 7 (𝑒 = π‘Ž β†’ (((πΉβ€˜π‘–) < (𝐿 + 𝑒) ∧ 𝐿 < ((πΉβ€˜π‘–) + 𝑒)) ↔ ((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž))))
2221rexralbidv 2516 . . . . . 6 (𝑒 = π‘Ž β†’ (βˆƒπ‘— ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘–) < (𝐿 + 𝑒) ∧ 𝐿 < ((πΉβ€˜π‘–) + 𝑒)) ↔ βˆƒπ‘— ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž))))
2322cbvralv 2718 . . . . 5 (βˆ€π‘’ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘–) < (𝐿 + 𝑒) ∧ 𝐿 < ((πΉβ€˜π‘–) + 𝑒)) ↔ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž)))
24 fveq2 5531 . . . . . . . 8 (𝑗 = 𝑏 β†’ (β„€β‰₯β€˜π‘—) = (β„€β‰₯β€˜π‘))
2524raleqdv 2692 . . . . . . 7 (𝑗 = 𝑏 β†’ (βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž)) ↔ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘)((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž))))
2625cbvrexv 2719 . . . . . 6 (βˆƒπ‘— ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž)) ↔ βˆƒπ‘ ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘)((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž)))
2726ralbii 2496 . . . . 5 (βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž)) ↔ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘)((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž)))
28 fveq2 5531 . . . . . . . . . 10 (𝑖 = 𝑐 β†’ (πΉβ€˜π‘–) = (πΉβ€˜π‘))
2928breq1d 4028 . . . . . . . . 9 (𝑖 = 𝑐 β†’ ((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ↔ (πΉβ€˜π‘) < (𝐿 + π‘Ž)))
3028oveq1d 5907 . . . . . . . . . 10 (𝑖 = 𝑐 β†’ ((πΉβ€˜π‘–) + π‘Ž) = ((πΉβ€˜π‘) + π‘Ž))
3130breq2d 4030 . . . . . . . . 9 (𝑖 = 𝑐 β†’ (𝐿 < ((πΉβ€˜π‘–) + π‘Ž) ↔ 𝐿 < ((πΉβ€˜π‘) + π‘Ž)))
3229, 31anbi12d 473 . . . . . . . 8 (𝑖 = 𝑐 β†’ (((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž)) ↔ ((πΉβ€˜π‘) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘) + π‘Ž))))
3332cbvralv 2718 . . . . . . 7 (βˆ€π‘– ∈ (β„€β‰₯β€˜π‘)((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž)) ↔ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((πΉβ€˜π‘) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘) + π‘Ž)))
3433rexbii 2497 . . . . . 6 (βˆƒπ‘ ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘)((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž)) ↔ βˆƒπ‘ ∈ β„• βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((πΉβ€˜π‘) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘) + π‘Ž)))
3534ralbii 2496 . . . . 5 (βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘)((πΉβ€˜π‘–) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘–) + π‘Ž)) ↔ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„• βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((πΉβ€˜π‘) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘) + π‘Ž)))
3623, 27, 353bitri 206 . . . 4 (βˆ€π‘’ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘–) < (𝐿 + 𝑒) ∧ 𝐿 < ((πΉβ€˜π‘–) + 𝑒)) ↔ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„• βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((πΉβ€˜π‘) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘) + π‘Ž)))
3716, 36sylib 122 . . 3 (πœ‘ β†’ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„• βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((πΉβ€˜π‘) < (𝐿 + π‘Ž) ∧ 𝐿 < ((πΉβ€˜π‘) + π‘Ž)))
381, 2, 3, 14, 37, 9resqrexlemglsq 11051 . 2 (πœ‘ β†’ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„• βˆ€π‘‘ ∈ (β„€β‰₯β€˜π‘)(((π‘₯ ∈ β„• ↦ ((πΉβ€˜π‘₯)↑2))β€˜π‘‘) < ((𝐿↑2) + π‘Ž) ∧ (𝐿↑2) < (((π‘₯ ∈ β„• ↦ ((πΉβ€˜π‘₯)↑2))β€˜π‘‘) + π‘Ž)))
391, 2, 3, 14, 37, 9resqrexlemga 11052 . 2 (πœ‘ β†’ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„• βˆ€π‘‘ ∈ (β„€β‰₯β€˜π‘)(((π‘₯ ∈ β„• ↦ ((πΉβ€˜π‘₯)↑2))β€˜π‘‘) < (𝐴 + π‘Ž) ∧ 𝐴 < (((π‘₯ ∈ β„• ↦ ((πΉβ€˜π‘₯)↑2))β€˜π‘‘) + π‘Ž)))
4013, 15, 38, 2, 39recvguniq 11024 1 (πœ‘ β†’ (𝐿↑2) = 𝐴)
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2160  βˆ€wral 2468  βˆƒwrex 2469   βŠ† wss 3144  {csn 3607   class class class wbr 4018   ↦ cmpt 4079   Γ— cxp 4639  β€˜cfv 5232  (class class class)co 5892   ∈ cmpo 5894  β„cr 7830  0cc0 7831  1c1 7832   + caddc 7834   < clt 8012   ≀ cle 8013   / cdiv 8649  β„•cn 8939  2c2 8990  β„€cz 9273  β„€β‰₯cuz 9548  β„+crp 9673  seqcseq 10465  β†‘cexp 10539
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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-iinf 4602  ax-cnex 7922  ax-resscn 7923  ax-1cn 7924  ax-1re 7925  ax-icn 7926  ax-addcl 7927  ax-addrcl 7928  ax-mulcl 7929  ax-mulrcl 7930  ax-addcom 7931  ax-mulcom 7932  ax-addass 7933  ax-mulass 7934  ax-distr 7935  ax-i2m1 7936  ax-0lt1 7937  ax-1rid 7938  ax-0id 7939  ax-rnegex 7940  ax-precex 7941  ax-cnre 7942  ax-pre-ltirr 7943  ax-pre-ltwlin 7944  ax-pre-lttrn 7945  ax-pre-apti 7946  ax-pre-ltadd 7947  ax-pre-mulgt0 7948  ax-pre-mulext 7949  ax-arch 7950
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4308  df-po 4311  df-iso 4312  df-iord 4381  df-on 4383  df-ilim 4384  df-suc 4386  df-iom 4605  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5234  df-fn 5235  df-f 5236  df-f1 5237  df-fo 5238  df-f1o 5239  df-fv 5240  df-riota 5848  df-ov 5895  df-oprab 5896  df-mpo 5897  df-1st 6160  df-2nd 6161  df-recs 6325  df-frec 6411  df-pnf 8014  df-mnf 8015  df-xr 8016  df-ltxr 8017  df-le 8018  df-sub 8150  df-neg 8151  df-reap 8552  df-ap 8559  df-div 8650  df-inn 8940  df-2 8998  df-3 8999  df-4 9000  df-n0 9197  df-z 9274  df-uz 9549  df-rp 9674  df-seqfrec 10466  df-exp 10540
This theorem is referenced by:  resqrexlemex  11054
  Copyright terms: Public domain W3C validator