Mathbox for Asger C. Ipsen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > knoppndvlem20 | Structured version Visualization version GIF version |
Description: Lemma for knoppndv 34477. (Contributed by Asger C. Ipsen, 18-Aug-2021.) |
Ref | Expression |
---|---|
knoppndvlem20.c | ⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) |
knoppndvlem20.n | ⊢ (𝜑 → 𝑁 ∈ ℕ) |
knoppndvlem20.1 | ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) |
Ref | Expression |
---|---|
knoppndvlem20 | ⊢ (𝜑 → (1 − (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈ ℝ+) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | knoppndvlem20.c | . . . . 5 ⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) | |
2 | knoppndvlem20.n | . . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ) | |
3 | knoppndvlem20.1 | . . . . 5 ⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) | |
4 | 1, 2, 3 | knoppndvlem12 34466 | . . . 4 ⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) ≠ 1 ∧ 1 < (((2 · 𝑁) · (abs‘𝐶)) − 1))) |
5 | 4 | simprd 499 | . . 3 ⊢ (𝜑 → 1 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) |
6 | 2re 11928 | . . . . . . . . 9 ⊢ 2 ∈ ℝ | |
7 | 6 | a1i 11 | . . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℝ) |
8 | 2 | nnred 11869 | . . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℝ) |
9 | 7, 8 | remulcld 10887 | . . . . . . 7 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ) |
10 | 1 | knoppndvlem3 34457 | . . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1)) |
11 | 10 | simpld 498 | . . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℝ) |
12 | 11 | recnd 10885 | . . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ) |
13 | 12 | abscld 15024 | . . . . . . 7 ⊢ (𝜑 → (abs‘𝐶) ∈ ℝ) |
14 | 9, 13 | remulcld 10887 | . . . . . 6 ⊢ (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) ∈ ℝ) |
15 | 1red 10858 | . . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ) | |
16 | 14, 15 | resubcld 11284 | . . . . 5 ⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ∈ ℝ) |
17 | 0red 10860 | . . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ) | |
18 | 0lt1 11378 | . . . . . . 7 ⊢ 0 < 1 | |
19 | 18 | a1i 11 | . . . . . 6 ⊢ (𝜑 → 0 < 1) |
20 | 17, 15, 16, 19, 5 | lttrd 11017 | . . . . 5 ⊢ (𝜑 → 0 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) |
21 | 16, 20 | elrpd 12649 | . . . 4 ⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ∈ ℝ+) |
22 | 21 | recgt1d 12666 | . . 3 ⊢ (𝜑 → (1 < (((2 · 𝑁) · (abs‘𝐶)) − 1) ↔ (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) < 1)) |
23 | 5, 22 | mpbid 235 | . 2 ⊢ (𝜑 → (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) < 1) |
24 | 21 | rprecred 12663 | . . . 4 ⊢ (𝜑 → (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈ ℝ) |
25 | 24, 15 | jca 515 | . . 3 ⊢ (𝜑 → ((1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈ ℝ ∧ 1 ∈ ℝ)) |
26 | difrp 12648 | . . 3 ⊢ (((1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) < 1 ↔ (1 − (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈ ℝ+)) | |
27 | 25, 26 | syl 17 | . 2 ⊢ (𝜑 → ((1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) < 1 ↔ (1 − (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈ ℝ+)) |
28 | 23, 27 | mpbid 235 | 1 ⊢ (𝜑 → (1 − (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈ ℝ+) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∈ wcel 2111 ≠ wne 2941 class class class wbr 5067 ‘cfv 6397 (class class class)co 7231 ℝcr 10752 0cc0 10753 1c1 10754 · cmul 10758 < clt 10891 − cmin 11086 -cneg 11087 / cdiv 11513 ℕcn 11854 2c2 11909 ℝ+crp 12610 (,)cioo 12959 abscabs 14821 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-sep 5206 ax-nul 5213 ax-pow 5272 ax-pr 5336 ax-un 7541 ax-cnex 10809 ax-resscn 10810 ax-1cn 10811 ax-icn 10812 ax-addcl 10813 ax-addrcl 10814 ax-mulcl 10815 ax-mulrcl 10816 ax-mulcom 10817 ax-addass 10818 ax-mulass 10819 ax-distr 10820 ax-i2m1 10821 ax-1ne0 10822 ax-1rid 10823 ax-rnegex 10824 ax-rrecex 10825 ax-cnre 10826 ax-pre-lttri 10827 ax-pre-lttrn 10828 ax-pre-ltadd 10829 ax-pre-mulgt0 10830 ax-pre-sup 10831 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3067 df-rex 3068 df-reu 3069 df-rmo 3070 df-rab 3071 df-v 3422 df-sbc 3709 df-csb 3826 df-dif 3883 df-un 3885 df-in 3887 df-ss 3897 df-pss 3899 df-nul 4252 df-if 4454 df-pw 4529 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4834 df-iun 4920 df-br 5068 df-opab 5130 df-mpt 5150 df-tr 5176 df-id 5469 df-eprel 5474 df-po 5482 df-so 5483 df-fr 5523 df-we 5525 df-xp 5571 df-rel 5572 df-cnv 5573 df-co 5574 df-dm 5575 df-rn 5576 df-res 5577 df-ima 5578 df-pred 6175 df-ord 6233 df-on 6234 df-lim 6235 df-suc 6236 df-iota 6355 df-fun 6399 df-fn 6400 df-f 6401 df-f1 6402 df-fo 6403 df-f1o 6404 df-fv 6405 df-riota 7188 df-ov 7234 df-oprab 7235 df-mpo 7236 df-om 7663 df-1st 7779 df-2nd 7780 df-wrecs 8067 df-recs 8128 df-rdg 8166 df-er 8411 df-en 8647 df-dom 8648 df-sdom 8649 df-sup 9082 df-pnf 10893 df-mnf 10894 df-xr 10895 df-ltxr 10896 df-le 10897 df-sub 11088 df-neg 11089 df-div 11514 df-nn 11855 df-2 11917 df-3 11918 df-n0 12115 df-z 12201 df-uz 12463 df-rp 12611 df-ioo 12963 df-seq 13599 df-exp 13660 df-cj 14686 df-re 14687 df-im 14688 df-sqrt 14822 df-abs 14823 |
This theorem is referenced by: knoppndvlem21 34475 knoppndvlem22 34476 |
Copyright terms: Public domain | W3C validator |