![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > resqrexlemnmsq | GIF version |
Description: Lemma for resqrex 10113. The difference between the squares of two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 30-Jul-2021.) |
Ref | Expression |
---|---|
resqrexlemex.seq | ⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+) |
resqrexlemex.a | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
resqrexlemex.agt0 | ⊢ (𝜑 → 0 ≤ 𝐴) |
resqrexlemnmsq.n | ⊢ (𝜑 → 𝑁 ∈ ℕ) |
resqrexlemnmsq.m | ⊢ (𝜑 → 𝑀 ∈ ℕ) |
resqrexlemnmsq.nm | ⊢ (𝜑 → 𝑁 ≤ 𝑀) |
Ref | Expression |
---|---|
resqrexlemnmsq | ⊢ (𝜑 → (((𝐹‘𝑁)↑2) − ((𝐹‘𝑀)↑2)) < (((𝐹‘1)↑2) / (4↑(𝑁 − 1)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resqrexlemex.seq | . . . . . . . 8 ⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+) | |
2 | resqrexlemex.a | . . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
3 | resqrexlemex.agt0 | . . . . . . . 8 ⊢ (𝜑 → 0 ≤ 𝐴) | |
4 | 1, 2, 3 | resqrexlemf 10094 | . . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶ℝ+) |
5 | resqrexlemnmsq.n | . . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ) | |
6 | 4, 5 | ffvelrnd 5355 | . . . . . 6 ⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ+) |
7 | 6 | rpred 8906 | . . . . 5 ⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ) |
8 | 7 | resqcld 9780 | . . . 4 ⊢ (𝜑 → ((𝐹‘𝑁)↑2) ∈ ℝ) |
9 | 8 | recnd 7261 | . . 3 ⊢ (𝜑 → ((𝐹‘𝑁)↑2) ∈ ℂ) |
10 | resqrexlemnmsq.m | . . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ) | |
11 | 4, 10 | ffvelrnd 5355 | . . . . . 6 ⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ+) |
12 | 11 | rpred 8906 | . . . . 5 ⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ) |
13 | 12 | resqcld 9780 | . . . 4 ⊢ (𝜑 → ((𝐹‘𝑀)↑2) ∈ ℝ) |
14 | 13 | recnd 7261 | . . 3 ⊢ (𝜑 → ((𝐹‘𝑀)↑2) ∈ ℂ) |
15 | 2 | recnd 7261 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℂ) |
16 | 9, 14, 15 | nnncan2d 7573 | . 2 ⊢ (𝜑 → ((((𝐹‘𝑁)↑2) − 𝐴) − (((𝐹‘𝑀)↑2) − 𝐴)) = (((𝐹‘𝑁)↑2) − ((𝐹‘𝑀)↑2))) |
17 | 8, 2 | resubcld 7604 | . . . 4 ⊢ (𝜑 → (((𝐹‘𝑁)↑2) − 𝐴) ∈ ℝ) |
18 | 13, 2 | resubcld 7604 | . . . 4 ⊢ (𝜑 → (((𝐹‘𝑀)↑2) − 𝐴) ∈ ℝ) |
19 | 17, 18 | resubcld 7604 | . . 3 ⊢ (𝜑 → ((((𝐹‘𝑁)↑2) − 𝐴) − (((𝐹‘𝑀)↑2) − 𝐴)) ∈ ℝ) |
20 | 1nn 8169 | . . . . . . . 8 ⊢ 1 ∈ ℕ | |
21 | 20 | a1i 9 | . . . . . . 7 ⊢ (𝜑 → 1 ∈ ℕ) |
22 | 4, 21 | ffvelrnd 5355 | . . . . . 6 ⊢ (𝜑 → (𝐹‘1) ∈ ℝ+) |
23 | 2z 8512 | . . . . . . 7 ⊢ 2 ∈ ℤ | |
24 | 23 | a1i 9 | . . . . . 6 ⊢ (𝜑 → 2 ∈ ℤ) |
25 | 22, 24 | rpexpcld 9778 | . . . . 5 ⊢ (𝜑 → ((𝐹‘1)↑2) ∈ ℝ+) |
26 | 4nn 8314 | . . . . . . . 8 ⊢ 4 ∈ ℕ | |
27 | 26 | a1i 9 | . . . . . . 7 ⊢ (𝜑 → 4 ∈ ℕ) |
28 | 27 | nnrpd 8905 | . . . . . 6 ⊢ (𝜑 → 4 ∈ ℝ+) |
29 | 5 | nnzd 8601 | . . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℤ) |
30 | 1zzd 8511 | . . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ) | |
31 | 29, 30 | zsubcld 8607 | . . . . . 6 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
32 | 28, 31 | rpexpcld 9778 | . . . . 5 ⊢ (𝜑 → (4↑(𝑁 − 1)) ∈ ℝ+) |
33 | 25, 32 | rpdivcld 8924 | . . . 4 ⊢ (𝜑 → (((𝐹‘1)↑2) / (4↑(𝑁 − 1))) ∈ ℝ+) |
34 | 33 | rpred 8906 | . . 3 ⊢ (𝜑 → (((𝐹‘1)↑2) / (4↑(𝑁 − 1))) ∈ ℝ) |
35 | 1, 2, 3 | resqrexlemover 10097 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝐴 < ((𝐹‘𝑀)↑2)) |
36 | 10, 35 | mpdan 412 | . . . . 5 ⊢ (𝜑 → 𝐴 < ((𝐹‘𝑀)↑2)) |
37 | difrp 8903 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ ((𝐹‘𝑀)↑2) ∈ ℝ) → (𝐴 < ((𝐹‘𝑀)↑2) ↔ (((𝐹‘𝑀)↑2) − 𝐴) ∈ ℝ+)) | |
38 | 2, 13, 37 | syl2anc 403 | . . . . 5 ⊢ (𝜑 → (𝐴 < ((𝐹‘𝑀)↑2) ↔ (((𝐹‘𝑀)↑2) − 𝐴) ∈ ℝ+)) |
39 | 36, 38 | mpbid 145 | . . . 4 ⊢ (𝜑 → (((𝐹‘𝑀)↑2) − 𝐴) ∈ ℝ+) |
40 | 17, 39 | ltsubrpd 8939 | . . 3 ⊢ (𝜑 → ((((𝐹‘𝑁)↑2) − 𝐴) − (((𝐹‘𝑀)↑2) − 𝐴)) < (((𝐹‘𝑁)↑2) − 𝐴)) |
41 | 1, 2, 3 | resqrexlemcalc3 10103 | . . . 4 ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (((𝐹‘𝑁)↑2) − 𝐴) ≤ (((𝐹‘1)↑2) / (4↑(𝑁 − 1)))) |
42 | 5, 41 | mpdan 412 | . . 3 ⊢ (𝜑 → (((𝐹‘𝑁)↑2) − 𝐴) ≤ (((𝐹‘1)↑2) / (4↑(𝑁 − 1)))) |
43 | 19, 17, 34, 40, 42 | ltletrd 7646 | . 2 ⊢ (𝜑 → ((((𝐹‘𝑁)↑2) − 𝐴) − (((𝐹‘𝑀)↑2) − 𝐴)) < (((𝐹‘1)↑2) / (4↑(𝑁 − 1)))) |
44 | 16, 43 | eqbrtrrd 3827 | 1 ⊢ (𝜑 → (((𝐹‘𝑁)↑2) − ((𝐹‘𝑀)↑2)) < (((𝐹‘1)↑2) / (4↑(𝑁 − 1)))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 = wceq 1285 ∈ wcel 1434 {csn 3416 class class class wbr 3805 × cxp 4389 ‘cfv 4952 (class class class)co 5563 ↦ cmpt2 5565 ℝcr 7094 0cc0 7095 1c1 7096 + caddc 7098 < clt 7267 ≤ cle 7268 − cmin 7398 / cdiv 7879 ℕcn 8158 2c2 8208 4c4 8210 ℤcz 8484 ℝ+crp 8867 seqcseq 9573 ↑cexp 9624 |
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 ax-cnex 7181 ax-resscn 7182 ax-1cn 7183 ax-1re 7184 ax-icn 7185 ax-addcl 7186 ax-addrcl 7187 ax-mulcl 7188 ax-mulrcl 7189 ax-addcom 7190 ax-mulcom 7191 ax-addass 7192 ax-mulass 7193 ax-distr 7194 ax-i2m1 7195 ax-0lt1 7196 ax-1rid 7197 ax-0id 7198 ax-rnegex 7199 ax-precex 7200 ax-cnre 7201 ax-pre-ltirr 7202 ax-pre-ltwlin 7203 ax-pre-lttrn 7204 ax-pre-apti 7205 ax-pre-ltadd 7206 ax-pre-mulgt0 7207 ax-pre-mulext 7208 |
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-nel 2345 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-if 3369 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-id 4076 df-po 4079 df-iso 4080 df-iord 4149 df-on 4151 df-ilim 4152 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 5519 df-ov 5566 df-oprab 5567 df-mpt2 5568 df-1st 5818 df-2nd 5819 df-recs 5974 df-frec 6060 df-pnf 7269 df-mnf 7270 df-xr 7271 df-ltxr 7272 df-le 7273 df-sub 7400 df-neg 7401 df-reap 7794 df-ap 7801 df-div 7880 df-inn 8159 df-2 8217 df-3 8218 df-4 8219 df-n0 8408 df-z 8485 df-uz 8753 df-rp 8868 df-iseq 9574 df-iexp 9625 |
This theorem is referenced by: resqrexlemnm 10105 |
Copyright terms: Public domain | W3C validator |