![]() |
Metamath
Proof Explorer Theorem List (p. 276 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pntrlog2bndlem5 27501* | Lemma for pntrlog2bnd 27504. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.) |
โข ๐ = (๐ โ โ โฆ ฮฃ๐ โ (1...(โโ๐))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ / ๐))))) & โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข ๐ = (๐ โ โ โฆ if(๐ โ โ+, (๐ ยท (logโ๐)), 0)) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ โ๐ฆ โ โ+ (absโ((๐ โ๐ฆ) / ๐ฆ)) โค ๐ต) โ โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((((absโ(๐ โ๐ฅ)) ยท (logโ๐ฅ)) โ ((2 / (logโ๐ฅ)) ยท ฮฃ๐ โ (1...(โโ๐ฅ))((absโ(๐ โ(๐ฅ / ๐))) ยท (logโ๐)))) / ๐ฅ)) โ โค๐(1)) | ||
Theorem | pntrlog2bndlem6a 27502* | Lemma for pntrlog2bndlem6 27503. (Contributed by Mario Carneiro, 7-Jun-2016.) |
โข ๐ = (๐ โ โ โฆ ฮฃ๐ โ (1...(โโ๐))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ / ๐))))) & โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข ๐ = (๐ โ โ โฆ if(๐ โ โ+, (๐ ยท (logโ๐)), 0)) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ โ๐ฆ โ โ+ (absโ((๐ โ๐ฆ) / ๐ฆ)) โค ๐ต) & โข (๐ โ ๐ด โ โ) & โข (๐ โ 1 โค ๐ด) โ โข ((๐ โง ๐ฅ โ (1(,)+โ)) โ (1...(โโ๐ฅ)) = ((1...(โโ(๐ฅ / ๐ด))) โช (((โโ(๐ฅ / ๐ด)) + 1)...(โโ๐ฅ)))) | ||
Theorem | pntrlog2bndlem6 27503* | Lemma for pntrlog2bnd 27504. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.) |
โข ๐ = (๐ โ โ โฆ ฮฃ๐ โ (1...(โโ๐))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ / ๐))))) & โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข ๐ = (๐ โ โ โฆ if(๐ โ โ+, (๐ ยท (logโ๐)), 0)) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ โ๐ฆ โ โ+ (absโ((๐ โ๐ฆ) / ๐ฆ)) โค ๐ต) & โข (๐ โ ๐ด โ โ) & โข (๐ โ 1 โค ๐ด) โ โข (๐ โ (๐ฅ โ (1(,)+โ) โฆ ((((absโ(๐ โ๐ฅ)) ยท (logโ๐ฅ)) โ ((2 / (logโ๐ฅ)) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐ด)))((absโ(๐ โ(๐ฅ / ๐))) ยท (logโ๐)))) / ๐ฅ)) โ โค๐(1)) | ||
Theorem | pntrlog2bnd 27504* | A bound on ๐ (๐ฅ)logโ2(๐ฅ). Equation 10.6.15 of [Shapiro], p. 431. (Contributed by Mario Carneiro, 1-Jun-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) โ โข ((๐ด โ โ โง 1 โค ๐ด) โ โ๐ โ โ+ โ๐ฅ โ (1(,)+โ)((((absโ(๐ โ๐ฅ)) ยท (logโ๐ฅ)) โ ((2 / (logโ๐ฅ)) ยท ฮฃ๐ โ (1...(โโ(๐ฅ / ๐ด)))((absโ(๐ โ(๐ฅ / ๐))) ยท (logโ๐)))) / ๐ฅ) โค ๐) | ||
Theorem | pntpbnd1a 27505* | Lemma for pntpbnd 27508. (Contributed by Mario Carneiro, 11-Apr-2016.) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ธ โ (0(,)1)) & โข ๐ = (expโ(2 / ๐ธ)) & โข (๐ โ ๐ โ (๐(,)+โ)) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐ < ๐ โง ๐ โค (๐พ ยท ๐))) & โข (๐ โ (absโ(๐ โ๐)) โค (absโ((๐ โ(๐ + 1)) โ (๐ โ๐)))) โ โข (๐ โ (absโ((๐ โ๐) / ๐)) โค ๐ธ) | ||
Theorem | pntpbnd1 27506* | Lemma for pntpbnd 27508. (Contributed by Mario Carneiro, 11-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ธ โ (0(,)1)) & โข ๐ = (expโ(2 / ๐ธ)) & โข (๐ โ ๐ โ (๐(,)+โ)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ โ๐ โ โ โ๐ โ โค (absโฮฃ๐ฆ โ (๐...๐)((๐ โ๐ฆ) / (๐ฆ ยท (๐ฆ + 1)))) โค ๐ด) & โข ๐ถ = (๐ด + 2) & โข (๐ โ ๐พ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) & โข (๐ โ ยฌ โ๐ฆ โ โ ((๐ < ๐ฆ โง ๐ฆ โค (๐พ ยท ๐)) โง (absโ((๐ โ๐ฆ) / ๐ฆ)) โค ๐ธ)) โ โข (๐ โ ฮฃ๐ โ (((โโ๐) + 1)...(โโ(๐พ ยท ๐)))(absโ((๐ โ๐) / (๐ ยท (๐ + 1)))) โค ๐ด) | ||
Theorem | pntpbnd2 27507* | Lemma for pntpbnd 27508. (Contributed by Mario Carneiro, 11-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ธ โ (0(,)1)) & โข ๐ = (expโ(2 / ๐ธ)) & โข (๐ โ ๐ โ (๐(,)+โ)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ โ๐ โ โ โ๐ โ โค (absโฮฃ๐ฆ โ (๐...๐)((๐ โ๐ฆ) / (๐ฆ ยท (๐ฆ + 1)))) โค ๐ด) & โข ๐ถ = (๐ด + 2) & โข (๐ โ ๐พ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) & โข (๐ โ ยฌ โ๐ฆ โ โ ((๐ < ๐ฆ โง ๐ฆ โค (๐พ ยท ๐)) โง (absโ((๐ โ๐ฆ) / ๐ฆ)) โค ๐ธ)) โ โข ยฌ ๐ | ||
Theorem | pntpbnd 27508* | Lemma for pnt 27534. Establish smallness of ๐ at a point. Lemma 10.6.1 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 10-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) โ โข โ๐ โ โ+ โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ โ โ ((๐ฆ < ๐ โง ๐ โค (๐ ยท ๐ฆ)) โง (absโ((๐ โ๐) / ๐)) โค ๐) | ||
Theorem | pntibndlem1 27509 | Lemma for pntibnd 27513. (Contributed by Mario Carneiro, 10-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข ๐ฟ = ((1 / 4) / (๐ด + 3)) โ โข (๐ โ ๐ฟ โ (0(,)1)) | ||
Theorem | pntibndlem2a 27510* | Lemma for pntibndlem2 27511. (Contributed by Mario Carneiro, 7-Jun-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข ๐ฟ = ((1 / 4) / (๐ด + 3)) & โข (๐ โ โ๐ฅ โ โ+ (absโ((๐ โ๐ฅ) / ๐ฅ)) โค ๐ด) & โข (๐ โ ๐ต โ โ+) & โข ๐พ = (expโ(๐ต / (๐ธ / 2))) & โข ๐ถ = ((2 ยท ๐ต) + (logโ2)) & โข (๐ โ ๐ธ โ (0(,)1)) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โ โ) โ โข ((๐ โง ๐ข โ (๐[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) โ (๐ข โ โ โง ๐ โค ๐ข โง ๐ข โค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) | ||
Theorem | pntibndlem2 27511* | Lemma for pntibnd 27513. The main work, after eliminating all the quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข ๐ฟ = ((1 / 4) / (๐ด + 3)) & โข (๐ โ โ๐ฅ โ โ+ (absโ((๐ โ๐ฅ) / ๐ฅ)) โค ๐ด) & โข (๐ โ ๐ต โ โ+) & โข ๐พ = (expโ(๐ต / (๐ธ / 2))) & โข ๐ถ = ((2 ยท ๐ต) + (logโ2)) & โข (๐ โ ๐ธ โ (0(,)1)) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ+) & โข (๐ โ โ๐ฅ โ (1(,)+โ)โ๐ฆ โ (๐ฅ[,](2 ยท ๐ฅ))((ฯโ๐ฆ) โ (ฯโ๐ฅ)) โค ((2 ยท (๐ฆ โ ๐ฅ)) + (๐ ยท (๐ฅ / (logโ๐ฅ))))) & โข ๐ = ((expโ(๐ / (๐ธ / 4))) + ๐) & โข (๐ โ ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) & โข (๐ โ ๐ โ (๐(,)+โ)) & โข (๐ โ ((๐ < ๐ โง ๐ โค ((๐ / 2) ยท ๐)) โง (absโ((๐ โ๐) / ๐)) โค (๐ธ / 2))) โ โข (๐ โ โ๐ง โ โ+ ((๐ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) | ||
Theorem | pntibndlem3 27512* | Lemma for pntibnd 27513. Package up pntibndlem2 27511 in quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข ๐ฟ = ((1 / 4) / (๐ด + 3)) & โข (๐ โ โ๐ฅ โ โ+ (absโ((๐ โ๐ฅ) / ๐ฅ)) โค ๐ด) & โข (๐ โ ๐ต โ โ+) & โข ๐พ = (expโ(๐ต / (๐ธ / 2))) & โข ๐ถ = ((2 ยท ๐ต) + (logโ2)) & โข (๐ โ ๐ธ โ (0(,)1)) & โข (๐ โ ๐ โ โ+) & โข (๐ โ โ๐ โ (๐พ[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐ โ๐) / ๐)) โค (๐ธ / 2))) โ โข (๐ โ โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) | ||
Theorem | pntibnd 27513* | Lemma for pnt 27534. Establish smallness of ๐ on an interval. Lemma 10.6.2 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 10-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) โ โข โ๐ โ โ+ โ๐ โ (0(,)1)โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐) | ||
Theorem | pntlemd 27514 | Lemma for pnt 27534. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, ๐ด is C^*, ๐ต is c1, ๐ฟ is ฮป, ๐ท is c2, and ๐น is c3. (Contributed by Mario Carneiro, 13-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) โ โข (๐ โ (๐ฟ โ โ+ โง ๐ท โ โ+ โง ๐น โ โ+)) | ||
Theorem | pntlemc 27515* | Lemma for pnt 27534. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, ๐ is ฮฑ, ๐ธ is ฮต, and ๐พ is K. (Contributed by Mario Carneiro, 13-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) โ โข (๐ โ (๐ธ โ โ+ โง ๐พ โ โ+ โง (๐ธ โ (0(,)1) โง 1 < ๐พ โง (๐ โ ๐ธ) โ โ+))) | ||
Theorem | pntlema 27516* | Lemma for pnt 27534. Closure for the constants used in the proof. The mammoth expression ๐ is a number large enough to satisfy all the lower bounds needed for ๐. For comparison with Equation 10.6.27 of [Shapiro], p. 434, ๐ is x2, ๐ is x1, ๐ถ is the big-O constant in Equation 10.6.29 of [Shapiro], p. 435, and ๐ is the unnamed lower bound of "for sufficiently large x" in Equation 10.6.34 of [Shapiro], p. 436. (Contributed by Mario Carneiro, 13-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) โ โข (๐ โ ๐ โ โ+) | ||
Theorem | pntlemb 27517* | Lemma for pnt 27534. Unpack all the lower bounds contained in ๐, in the form they will be used. For comparison with Equation 10.6.27 of [Shapiro], p. 434, ๐ is x. (Contributed by Mario Carneiro, 13-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) & โข (๐ โ ๐ โ (๐[,)+โ)) โ โข (๐ โ (๐ โ โ+ โง (1 < ๐ โง e โค (โโ๐) โง (โโ๐) โค (๐ / ๐)) โง ((4 / (๐ฟ ยท ๐ธ)) โค (โโ๐) โง (((logโ๐) / (logโ๐พ)) + 2) โค (((logโ๐) / (logโ๐พ)) / 4) โง ((๐ ยท 3) + ๐ถ) โค (((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต))) ยท (logโ๐))))) | ||
Theorem | pntlemg 27518* | Lemma for pnt 27534. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, ๐ is j^* and ๐ is ฤต. (Contributed by Mario Carneiro, 13-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) & โข (๐ โ ๐ โ (๐[,)+โ)) & โข ๐ = ((โโ((logโ๐) / (logโ๐พ))) + 1) & โข ๐ = (โโ(((logโ๐) / (logโ๐พ)) / 2)) โ โข (๐ โ (๐ โ โ โง ๐ โ (โคโฅโ๐) โง (((logโ๐) / (logโ๐พ)) / 4) โค (๐ โ ๐))) | ||
Theorem | pntlemh 27519* | Lemma for pnt 27534. Bounds on the subintervals in the induction. (Contributed by Mario Carneiro, 13-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) & โข (๐ โ ๐ โ (๐[,)+โ)) & โข ๐ = ((โโ((logโ๐) / (logโ๐พ))) + 1) & โข ๐ = (โโ(((logโ๐) / (logโ๐พ)) / 2)) โ โข ((๐ โง ๐ฝ โ (๐...๐)) โ (๐ < (๐พโ๐ฝ) โง (๐พโ๐ฝ) โค (โโ๐))) | ||
Theorem | pntlemn 27520* | Lemma for pnt 27534. The "naive" base bound, which we will slightly improve. (Contributed by Mario Carneiro, 13-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) & โข (๐ โ ๐ โ (๐[,)+โ)) & โข ๐ = ((โโ((logโ๐) / (logโ๐พ))) + 1) & โข ๐ = (โโ(((logโ๐) / (logโ๐พ)) / 2)) & โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐ โ๐ง) / ๐ง)) โค ๐) โ โข ((๐ โง (๐ฝ โ โ โง ๐ฝ โค (๐ / ๐))) โ 0 โค (((๐ / ๐ฝ) โ (absโ((๐ โ(๐ / ๐ฝ)) / ๐))) ยท (logโ๐ฝ))) | ||
Theorem | pntlemq 27521* | Lemma for pntlemj 27523. (Contributed by Mario Carneiro, 7-Jun-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) & โข (๐ โ ๐ โ (๐[,)+โ)) & โข ๐ = ((โโ((logโ๐) / (logโ๐พ))) + 1) & โข ๐ = (โโ(((logโ๐) / (logโ๐พ)) / 2)) & โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐ โ๐ง) / ๐ง)) โค ๐) & โข (๐ โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) & โข ๐ = (((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1)...(โโ(๐ / (๐พโ๐ฝ)))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ (((๐พโ๐ฝ) < ๐ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) & โข (๐ โ ๐ฝ โ (๐..^๐)) & โข ๐ผ = (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐))) โ โข (๐ โ ๐ผ โ ๐) | ||
Theorem | pntlemr 27522* | Lemma for pntlemj 27523. (Contributed by Mario Carneiro, 7-Jun-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) & โข (๐ โ ๐ โ (๐[,)+โ)) & โข ๐ = ((โโ((logโ๐) / (logโ๐พ))) + 1) & โข ๐ = (โโ(((logโ๐) / (logโ๐พ)) / 2)) & โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐ โ๐ง) / ๐ง)) โค ๐) & โข (๐ โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) & โข ๐ = (((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1)...(โโ(๐ / (๐พโ๐ฝ)))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ (((๐พโ๐ฝ) < ๐ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) & โข (๐ โ ๐ฝ โ (๐..^๐)) & โข ๐ผ = (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐))) โ โข (๐ โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) โค ((โฏโ๐ผ) ยท ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))))) | ||
Theorem | pntlemj 27523* | Lemma for pnt 27534. The induction step. Using pntibnd 27513, we find an interval in ๐พโ๐ฝ...๐พโ(๐ฝ + 1) which is sufficiently large and has a much smaller value, ๐ (๐ง) / ๐ง โค ๐ธ (instead of our original bound ๐ (๐ง) / ๐ง โค ๐). (Contributed by Mario Carneiro, 13-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) & โข (๐ โ ๐ โ (๐[,)+โ)) & โข ๐ = ((โโ((logโ๐) / (logโ๐พ))) + 1) & โข ๐ = (โโ(((logโ๐) / (logโ๐พ)) / 2)) & โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐ โ๐ง) / ๐ง)) โค ๐) & โข (๐ โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) & โข ๐ = (((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1)...(โโ(๐ / (๐พโ๐ฝ)))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ (((๐พโ๐ฝ) < ๐ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) & โข (๐ โ ๐ฝ โ (๐..^๐)) & โข ๐ผ = (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐))) โ โข (๐ โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) โค ฮฃ๐ โ ๐ (((๐ / ๐) โ (absโ((๐ โ(๐ / ๐)) / ๐))) ยท (logโ๐))) | ||
Theorem | pntlemi 27524* | Lemma for pnt 27534. Eliminate some assumptions from pntlemj 27523. (Contributed by Mario Carneiro, 13-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) & โข (๐ โ ๐ โ (๐[,)+โ)) & โข ๐ = ((โโ((logโ๐) / (logโ๐พ))) + 1) & โข ๐ = (โโ(((logโ๐) / (logโ๐พ)) / 2)) & โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐ โ๐ง) / ๐ง)) โค ๐) & โข (๐ โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) & โข ๐ = (((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1)...(โโ(๐ / (๐พโ๐ฝ)))) โ โข ((๐ โง ๐ฝ โ (๐..^๐)) โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) โค ฮฃ๐ โ ๐ (((๐ / ๐) โ (absโ((๐ โ(๐ / ๐)) / ๐))) ยท (logโ๐))) | ||
Theorem | pntlemf 27525* | Lemma for pnt 27534. Add up the pieces in pntlemi 27524 to get an estimate slightly better than the naive lower bound 0. (Contributed by Mario Carneiro, 13-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) & โข (๐ โ ๐ โ (๐[,)+โ)) & โข ๐ = ((โโ((logโ๐) / (logโ๐พ))) + 1) & โข ๐ = (โโ(((logโ๐) / (logโ๐พ)) / 2)) & โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐ โ๐ง) / ๐ง)) โค ๐) & โข (๐ โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) โ โข (๐ โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต)) ยท ((logโ๐)โ2))) โค ฮฃ๐ โ (1...(โโ(๐ / ๐)))(((๐ / ๐) โ (absโ((๐ โ(๐ / ๐)) / ๐))) ยท (logโ๐))) | ||
Theorem | pntlemk 27526* | Lemma for pnt 27534. Evaluate the naive part of the estimate. (Contributed by Mario Carneiro, 14-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) & โข (๐ โ ๐ โ (๐[,)+โ)) & โข ๐ = ((โโ((logโ๐) / (logโ๐พ))) + 1) & โข ๐ = (โโ(((logโ๐) / (logโ๐พ)) / 2)) & โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐ โ๐ง) / ๐ง)) โค ๐) & โข (๐ โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) โ โข (๐ โ (2 ยท ฮฃ๐ โ (1...(โโ(๐ / ๐)))((๐ / ๐) ยท (logโ๐))) โค ((๐ ยท ((logโ๐) + 3)) ยท (logโ๐))) | ||
Theorem | pntlemo 27527* | Lemma for pnt 27534. Combine all the estimates to establish a smaller eventual bound on ๐ (๐) / ๐. (Contributed by Mario Carneiro, 14-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) & โข (๐ โ ๐ โ (๐[,)+โ)) & โข ๐ = ((โโ((logโ๐) / (logโ๐พ))) + 1) & โข ๐ = (โโ(((logโ๐) / (logโ๐พ)) / 2)) & โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐ โ๐ง) / ๐ง)) โค ๐) & โข (๐ โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) & โข (๐ โ โ๐ง โ (1(,)+โ)((((absโ(๐ โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ (1...(โโ(๐ง / ๐)))((absโ(๐ โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐ถ) โ โข (๐ โ (absโ((๐ โ๐) / ๐)) โค (๐ โ (๐น ยท (๐โ3)))) | ||
Theorem | pntleme 27528* | Lemma for pnt 27534. Package up pntlemo 27527 in quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) & โข (๐ โ ๐ถ โ โ+) & โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) & โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐ โ๐ง) / ๐ง)) โค ๐) & โข (๐ โ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐ธ)) & โข (๐ โ โ๐ง โ (1(,)+โ)((((absโ(๐ โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ (1...(โโ(๐ง / ๐)))((absโ(๐ โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐ถ) โ โข (๐ โ โ๐ค โ โ+ โ๐ฃ โ (๐ค[,)+โ)(absโ((๐ โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3)))) | ||
Theorem | pntlem3 27529* | Lemma for pnt 27534. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 8-Apr-2016.) (Proof shortened by AV, 27-Sep-2020.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ โ๐ฅ โ โ+ (absโ((๐ โ๐ฅ) / ๐ฅ)) โค ๐ด) & โข ๐ = {๐ก โ (0[,]๐ด) โฃ โ๐ฆ โ โ+ โ๐ง โ (๐ฆ[,)+โ)(absโ((๐ โ๐ง) / ๐ง)) โค ๐ก} & โข (๐ โ ๐ถ โ โ+) & โข ((๐ โง ๐ข โ ๐) โ (๐ข โ (๐ถ ยท (๐ขโ3))) โ ๐) โ โข (๐ โ (๐ฅ โ โ+ โฆ ((ฯโ๐ฅ) / ๐ฅ)) โ๐ 1) | ||
Theorem | pntlemp 27530* | Lemma for pnt 27534. Wrapping up more quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ โ๐ฅ โ โ+ (absโ((๐ โ๐ฅ) / ๐ฅ)) โค ๐ด) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ต / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐)) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โค ๐ด) & โข ๐ธ = (๐ / ๐ท) & โข ๐พ = (expโ(๐ต / ๐ธ)) & โข (๐ โ (๐ โ โ+ โง 1 โค ๐)) & โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐ โ๐ง) / ๐ง)) โค ๐) โ โข (๐ โ โ๐ค โ โ+ โ๐ฃ โ (๐ค[,)+โ)(absโ((๐ โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3)))) | ||
Theorem | pntleml 27531* | Lemma for pnt 27534. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 14-Apr-2016.) |
โข ๐ = (๐ โ โ+ โฆ ((ฯโ๐) โ ๐)) & โข (๐ โ ๐ด โ โ+) & โข (๐ โ โ๐ฅ โ โ+ (absโ((๐ โ๐ฅ) / ๐ฅ)) โค ๐ด) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ฟ โ (0(,)1)) & โข ๐ท = (๐ด + 1) & โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) & โข (๐ โ โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ต / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐)) ยท ๐ง))(absโ((๐ โ๐ข) / ๐ข)) โค ๐)) โ โข (๐ โ (๐ฅ โ โ+ โฆ ((ฯโ๐ฅ) / ๐ฅ)) โ๐ 1) | ||
Theorem | pnt3 27532 | The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to ๐ฅ. (Contributed by Mario Carneiro, 1-Jun-2016.) |
โข (๐ฅ โ โ+ โฆ ((ฯโ๐ฅ) / ๐ฅ)) โ๐ 1 | ||
Theorem | pnt2 27533 | The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to ๐ฅ. (Contributed by Mario Carneiro, 1-Jun-2016.) |
โข (๐ฅ โ โ+ โฆ ((ฮธโ๐ฅ) / ๐ฅ)) โ๐ 1 | ||
Theorem | pnt 27534 | The Prime Number Theorem: the number of prime numbers less than ๐ฅ tends asymptotically to ๐ฅ / log(๐ฅ) as ๐ฅ goes to infinity. This is Metamath 100 proof #5. (Contributed by Mario Carneiro, 1-Jun-2016.) |
โข (๐ฅ โ (1(,)+โ) โฆ ((ฯโ๐ฅ) / (๐ฅ / (logโ๐ฅ)))) โ๐ 1 | ||
Theorem | abvcxp 27535* | Raising an absolute value to a power less than one yields another absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) |
โข ๐ด = (AbsValโ๐ ) & โข ๐ต = (Baseโ๐ ) & โข ๐บ = (๐ฅ โ ๐ต โฆ ((๐นโ๐ฅ)โ๐๐)) โ โข ((๐น โ ๐ด โง ๐ โ (0(,]1)) โ ๐บ โ ๐ด) | ||
Theorem | padicfval 27536* | Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) |
โข ๐ฝ = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ-(๐ pCnt ๐ฅ))))) โ โข (๐ โ โ โ (๐ฝโ๐) = (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ-(๐ pCnt ๐ฅ))))) | ||
Theorem | padicval 27537* | Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) |
โข ๐ฝ = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ-(๐ pCnt ๐ฅ))))) โ โข ((๐ โ โ โง ๐ โ โ) โ ((๐ฝโ๐)โ๐) = if(๐ = 0, 0, (๐โ-(๐ pCnt ๐)))) | ||
Theorem | ostth2lem1 27538* | Lemma for ostth2 27557, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 27557. If a power is upper bounded by a linear term, the exponent must be less than one. Or in big-O notation, ๐ โ ๐(๐ดโ๐) for any 1 < ๐ด. (Contributed by Mario Carneiro, 10-Sep-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข ((๐ โง ๐ โ โ) โ (๐ดโ๐) โค (๐ ยท ๐ต)) โ โข (๐ โ ๐ด โค 1) | ||
Theorem | qrngbas 27539 | The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
โข ๐ = (โfld โพs โ) โ โข โ = (Baseโ๐) | ||
Theorem | qdrng 27540 | The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.) |
โข ๐ = (โfld โพs โ) โ โข ๐ โ DivRing | ||
Theorem | qrng0 27541 | The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
โข ๐ = (โfld โพs โ) โ โข 0 = (0gโ๐) | ||
Theorem | qrng1 27542 | The unity element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
โข ๐ = (โfld โพs โ) โ โข 1 = (1rโ๐) | ||
Theorem | qrngneg 27543 | The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
โข ๐ = (โfld โพs โ) โ โข (๐ โ โ โ ((invgโ๐)โ๐) = -๐) | ||
Theorem | qrngdiv 27544 | The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
โข ๐ = (โfld โพs โ) โ โข ((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โ (๐(/rโ๐)๐) = (๐ / ๐)) | ||
Theorem | qabvle 27545 | By using induction on ๐, we show a long-range inequality coming from the triangle inequality. (Contributed by Mario Carneiro, 10-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) โ โข ((๐น โ ๐ด โง ๐ โ โ0) โ (๐นโ๐) โค ๐) | ||
Theorem | qabvexp 27546 | Induct the product rule abvmul 20698 to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) โ โข ((๐น โ ๐ด โง ๐ โ โ โง ๐ โ โ0) โ (๐นโ(๐โ๐)) = ((๐นโ๐)โ๐)) | ||
Theorem | ostthlem1 27547* | Lemma for ostth 27559. If two absolute values agree on the positive integers greater than one, then they agree for all rational numbers and thus are equal as functions. (Contributed by Mario Carneiro, 9-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) & โข (๐ โ ๐น โ ๐ด) & โข (๐ โ ๐บ โ ๐ด) & โข ((๐ โง ๐ โ (โคโฅโ2)) โ (๐นโ๐) = (๐บโ๐)) โ โข (๐ โ ๐น = ๐บ) | ||
Theorem | ostthlem2 27548* | Lemma for ostth 27559. Refine ostthlem1 27547 so that it is sufficient to only show equality on the primes. (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 20-Jun-2015.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) & โข (๐ โ ๐น โ ๐ด) & โข (๐ โ ๐บ โ ๐ด) & โข ((๐ โง ๐ โ โ) โ (๐นโ๐) = (๐บโ๐)) โ โข (๐ โ ๐น = ๐บ) | ||
Theorem | qabsabv 27549 | The regular absolute value function on the rationals is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 9-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) โ โข (abs โพ โ) โ ๐ด | ||
Theorem | padicabv 27550* | The p-adic absolute value (with arbitrary base) is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) & โข ๐น = (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ(๐ pCnt ๐ฅ)))) โ โข ((๐ โ โ โง ๐ โ (0(,)1)) โ ๐น โ ๐ด) | ||
Theorem | padicabvf 27551* | The p-adic absolute value is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) & โข ๐ฝ = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ-(๐ pCnt ๐ฅ))))) โ โข ๐ฝ:โโถ๐ด | ||
Theorem | padicabvcxp 27552* | All positive powers of the p-adic absolute value are absolute values. (Contributed by Mario Carneiro, 9-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) & โข ๐ฝ = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ-(๐ pCnt ๐ฅ))))) โ โข ((๐ โ โ โง ๐ โ โ+) โ (๐ฆ โ โ โฆ (((๐ฝโ๐)โ๐ฆ)โ๐๐ )) โ ๐ด) | ||
Theorem | ostth1 27553* | - Lemma for ostth 27559: trivial case. (Not that the proof is trivial, but that we are proving that the function is trivial.) If ๐น is equal to 1 on the primes, then by complete induction and the multiplicative property abvmul 20698 of the absolute value, ๐น is equal to 1 on all the integers, and ostthlem1 27547 extends this to the other rational numbers. (Contributed by Mario Carneiro, 10-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) & โข ๐ฝ = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ-(๐ pCnt ๐ฅ))))) & โข ๐พ = (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, 1)) & โข (๐ โ ๐น โ ๐ด) & โข (๐ โ โ๐ โ โ ยฌ 1 < (๐นโ๐)) & โข (๐ โ โ๐ โ โ ยฌ (๐นโ๐) < 1) โ โข (๐ โ ๐น = ๐พ) | ||
Theorem | ostth2lem2 27554* | Lemma for ostth2 27557. (Contributed by Mario Carneiro, 10-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) & โข ๐ฝ = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ-(๐ pCnt ๐ฅ))))) & โข ๐พ = (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, 1)) & โข (๐ โ ๐น โ ๐ด) & โข (๐ โ ๐ โ (โคโฅโ2)) & โข (๐ โ 1 < (๐นโ๐)) & โข ๐ = ((logโ(๐นโ๐)) / (logโ๐)) & โข (๐ โ ๐ โ (โคโฅโ2)) & โข ๐ = ((logโ(๐นโ๐)) / (logโ๐)) & โข ๐ = if((๐นโ๐) โค 1, 1, (๐นโ๐)) โ โข ((๐ โง ๐ โ โ0 โง ๐ โ (0...((๐โ๐) โ 1))) โ (๐นโ๐) โค ((๐ ยท ๐) ยท (๐โ๐))) | ||
Theorem | ostth2lem3 27555* | Lemma for ostth2 27557. (Contributed by Mario Carneiro, 10-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) & โข ๐ฝ = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ-(๐ pCnt ๐ฅ))))) & โข ๐พ = (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, 1)) & โข (๐ โ ๐น โ ๐ด) & โข (๐ โ ๐ โ (โคโฅโ2)) & โข (๐ โ 1 < (๐นโ๐)) & โข ๐ = ((logโ(๐นโ๐)) / (logโ๐)) & โข (๐ โ ๐ โ (โคโฅโ2)) & โข ๐ = ((logโ(๐นโ๐)) / (logโ๐)) & โข ๐ = if((๐นโ๐) โค 1, 1, (๐นโ๐)) & โข ๐ = ((logโ๐) / (logโ๐)) โ โข ((๐ โง ๐ โ โ) โ (((๐นโ๐) / (๐โ๐๐))โ๐) โค (๐ ยท ((๐ ยท ๐) ยท (๐ + 1)))) | ||
Theorem | ostth2lem4 27556* | Lemma for ostth2 27557. (Contributed by Mario Carneiro, 10-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) & โข ๐ฝ = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ-(๐ pCnt ๐ฅ))))) & โข ๐พ = (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, 1)) & โข (๐ โ ๐น โ ๐ด) & โข (๐ โ ๐ โ (โคโฅโ2)) & โข (๐ โ 1 < (๐นโ๐)) & โข ๐ = ((logโ(๐นโ๐)) / (logโ๐)) & โข (๐ โ ๐ โ (โคโฅโ2)) & โข ๐ = ((logโ(๐นโ๐)) / (logโ๐)) & โข ๐ = if((๐นโ๐) โค 1, 1, (๐นโ๐)) & โข ๐ = ((logโ๐) / (logโ๐)) โ โข (๐ โ (1 < (๐นโ๐) โง ๐ โค ๐)) | ||
Theorem | ostth2 27557* | - Lemma for ostth 27559: regular case. (Contributed by Mario Carneiro, 10-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) & โข ๐ฝ = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ-(๐ pCnt ๐ฅ))))) & โข ๐พ = (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, 1)) & โข (๐ โ ๐น โ ๐ด) & โข (๐ โ ๐ โ (โคโฅโ2)) & โข (๐ โ 1 < (๐นโ๐)) & โข ๐ = ((logโ(๐นโ๐)) / (logโ๐)) โ โข (๐ โ โ๐ โ (0(,]1)๐น = (๐ฆ โ โ โฆ ((absโ๐ฆ)โ๐๐))) | ||
Theorem | ostth3 27558* | - Lemma for ostth 27559: p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) & โข ๐ฝ = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ-(๐ pCnt ๐ฅ))))) & โข ๐พ = (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, 1)) & โข (๐ โ ๐น โ ๐ด) & โข (๐ โ โ๐ โ โ ยฌ 1 < (๐นโ๐)) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐นโ๐) < 1) & โข ๐ = -((logโ(๐นโ๐)) / (logโ๐)) & โข ๐ = if((๐นโ๐) โค (๐นโ๐), (๐นโ๐), (๐นโ๐)) โ โข (๐ โ โ๐ โ โ+ ๐น = (๐ฆ โ โ โฆ (((๐ฝโ๐)โ๐ฆ)โ๐๐))) | ||
Theorem | ostth 27559* | Ostrowski's theorem, which classifies all absolute values on โ. Any such absolute value must either be the trivial absolute value ๐พ, a constant exponent 0 < ๐ โค 1 times the regular absolute value, or a positive exponent times the p-adic absolute value. (Contributed by Mario Carneiro, 10-Sep-2014.) |
โข ๐ = (โfld โพs โ) & โข ๐ด = (AbsValโ๐) & โข ๐ฝ = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, (๐โ-(๐ pCnt ๐ฅ))))) & โข ๐พ = (๐ฅ โ โ โฆ if(๐ฅ = 0, 0, 1)) โ โข (๐น โ ๐ด โ (๐น = ๐พ โจ โ๐ โ (0(,]1)๐น = (๐ฆ โ โ โฆ ((absโ๐ฆ)โ๐๐)) โจ โ๐ โ โ+ โ๐ โ ran ๐ฝ ๐น = (๐ฆ โ โ โฆ ((๐โ๐ฆ)โ๐๐)))) | ||
The surreal numbers can be represented in several equivalent ways. In [Alling], Norman Alling made this notion explicit by giving a set of axioms that all representations admit, then proving that there is an order and birthday preserving bijection between any systems that satisfy these axioms. In this section, we start with the definition of surreal numbers given in [Gonshor] and derive Alling's axioms. After deriving them we no longer refer to the explicit definition of surreals. In particular, we never take advantage of the fact that the empty set is a surreal number under our definition. | ||
Syntax | csur 27560 | Declare the class of all surreal numbers (see df-no 27563). |
class No | ||
Syntax | cslt 27561 | Declare the less-than relation over surreal numbers (see df-slt 27564). |
class <s | ||
Syntax | cbday 27562 | Declare the birthday function for surreal numbers (see df-bday 27565). |
class bday | ||
Definition | df-no 27563* |
Define the class of surreal numbers. The surreal numbers are a proper
class of numbers developed by John H. Conway and introduced by Donald
Knuth in 1975. They form a proper class into which all ordered fields
can be embedded. The approach we take to defining them was first
introduced by Hary Gonshor, and is based on the conception of a
"sign
expansion" of a surreal number. We define the surreals as
ordinal-indexed sequences of 1o and
2o, analagous to Gonshor's
( โ ) and ( + ).
After introducing this definition, we will abstract away from it using axioms that Norman Alling developed in "Foundations of Analysis over Surreal Number Fields." This is done in an effort to be agnostic towards the exact implementation of surreals. (Contributed by Scott Fenton, 9-Jun-2011.) |
โข No = {๐ โฃ โ๐ โ On ๐:๐โถ{1o, 2o}} | ||
Definition | df-slt 27564* | Next, we introduce surreal less-than, a comparison relation over the surreals by lexicographically ordering them. (Contributed by Scott Fenton, 9-Jun-2011.) |
โข <s = {โจ๐, ๐โฉ โฃ ((๐ โ No โง ๐ โ No ) โง โ๐ฅ โ On (โ๐ฆ โ ๐ฅ (๐โ๐ฆ) = (๐โ๐ฆ) โง (๐โ๐ฅ){โจ1o, โ โฉ, โจ1o, 2oโฉ, โจโ , 2oโฉ} (๐โ๐ฅ)))} | ||
Definition | df-bday 27565 | Finally, we introduce the birthday function. This function maps each surreal to an ordinal. In our implementation, this is the domain of the sign function. The important properties of this function are established later. (Contributed by Scott Fenton, 11-Jun-2011.) |
โข bday = (๐ฅ โ No โฆ dom ๐ฅ) | ||
Theorem | elno 27566* | Membership in the surreals. (Shortened proof on 2012-Apr-14, SF). (Contributed by Scott Fenton, 11-Jun-2011.) |
โข (๐ด โ No โ โ๐ฅ โ On ๐ด:๐ฅโถ{1o, 2o}) | ||
Theorem | sltval 27567* | The value of the surreal less-than relation. (Contributed by Scott Fenton, 14-Jun-2011.) |
โข ((๐ด โ No โง ๐ต โ No ) โ (๐ด <s ๐ต โ โ๐ฅ โ On (โ๐ฆ โ ๐ฅ (๐ดโ๐ฆ) = (๐ตโ๐ฆ) โง (๐ดโ๐ฅ){โจ1o, โ โฉ, โจ1o, 2oโฉ, โจโ , 2oโฉ} (๐ตโ๐ฅ)))) | ||
Theorem | bdayval 27568 | The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011.) |
โข (๐ด โ No โ ( bday โ๐ด) = dom ๐ด) | ||
Theorem | nofun 27569 | A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011.) |
โข (๐ด โ No โ Fun ๐ด) | ||
Theorem | nodmon 27570 | The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
โข (๐ด โ No โ dom ๐ด โ On) | ||
Theorem | norn 27571 | The range of a surreal is a subset of the surreal signs. (Contributed by Scott Fenton, 16-Jun-2011.) |
โข (๐ด โ No โ ran ๐ด โ {1o, 2o}) | ||
Theorem | nofnbday 27572 | A surreal is a function over its birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
โข (๐ด โ No โ ๐ด Fn ( bday โ๐ด)) | ||
Theorem | nodmord 27573 | The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011.) |
โข (๐ด โ No โ Ord dom ๐ด) | ||
Theorem | elno2 27574 | An alternative condition for membership in No . (Contributed by Scott Fenton, 21-Mar-2012.) |
โข (๐ด โ No โ (Fun ๐ด โง dom ๐ด โ On โง ran ๐ด โ {1o, 2o})) | ||
Theorem | elno3 27575 | Another condition for membership in No . (Contributed by Scott Fenton, 14-Apr-2012.) |
โข (๐ด โ No โ (๐ด:dom ๐ดโถ{1o, 2o} โง dom ๐ด โ On)) | ||
Theorem | sltval2 27576* | Alternate expression for surreal less-than. Two surreals obey surreal less-than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011.) |
โข ((๐ด โ No โง ๐ต โ No ) โ (๐ด <s ๐ต โ (๐ดโโฉ {๐ โ On โฃ (๐ดโ๐) โ (๐ตโ๐)}){โจ1o, โ โฉ, โจ1o, 2oโฉ, โจโ , 2oโฉ} (๐ตโโฉ {๐ โ On โฃ (๐ดโ๐) โ (๐ตโ๐)}))) | ||
Theorem | nofv 27577 | The function value of a surreal is either a sign or the empty set. (Contributed by Scott Fenton, 22-Jun-2011.) |
โข (๐ด โ No โ ((๐ดโ๐) = โ โจ (๐ดโ๐) = 1o โจ (๐ดโ๐) = 2o)) | ||
Theorem | nosgnn0 27578 | โ is not a surreal sign. (Contributed by Scott Fenton, 16-Jun-2011.) |
โข ยฌ โ โ {1o, 2o} | ||
Theorem | nosgnn0i 27579 | If ๐ is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011.) |
โข ๐ โ {1o, 2o} โ โข โ โ ๐ | ||
Theorem | noreson 27580 | The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011.) |
โข ((๐ด โ No โง ๐ต โ On) โ (๐ด โพ ๐ต) โ No ) | ||
Theorem | sltintdifex 27581* | If ๐ด <s ๐ต, then the intersection of all the ordinals that have differing signs in ๐ด and ๐ต exists. (Contributed by Scott Fenton, 22-Feb-2012.) |
โข ((๐ด โ No โง ๐ต โ No ) โ (๐ด <s ๐ต โ โฉ {๐ โ On โฃ (๐ดโ๐) โ (๐ตโ๐)} โ V)) | ||
Theorem | sltres 27582 | If the restrictions of two surreals to a given ordinal obey surreal less-than, then so do the two surreals themselves. (Contributed by Scott Fenton, 4-Sep-2011.) |
โข ((๐ด โ No โง ๐ต โ No โง ๐ โ On) โ ((๐ด โพ ๐) <s (๐ต โพ ๐) โ ๐ด <s ๐ต)) | ||
Theorem | noxp1o 27583 | The Cartesian product of an ordinal and {1o} is a surreal. (Contributed by Scott Fenton, 12-Jun-2011.) |
โข (๐ด โ On โ (๐ด ร {1o}) โ No ) | ||
Theorem | noseponlem 27584* | Lemma for nosepon 27585. Consider a case of proper subset domain. (Contributed by Scott Fenton, 21-Sep-2020.) |
โข ((๐ด โ No โง ๐ต โ No โง dom ๐ด โ dom ๐ต) โ ยฌ โ๐ฅ โ On (๐ดโ๐ฅ) = (๐ตโ๐ฅ)) | ||
Theorem | nosepon 27585* | Given two unequal surreals, the minimal ordinal at which they differ is an ordinal. (Contributed by Scott Fenton, 21-Sep-2020.) |
โข ((๐ด โ No โง ๐ต โ No โง ๐ด โ ๐ต) โ โฉ {๐ฅ โ On โฃ (๐ดโ๐ฅ) โ (๐ตโ๐ฅ)} โ On) | ||
Theorem | noextend 27586 | Extending a surreal by one sign value results in a new surreal. (Contributed by Scott Fenton, 22-Nov-2021.) |
โข ๐ โ {1o, 2o} โ โข (๐ด โ No โ (๐ด โช {โจdom ๐ด, ๐โฉ}) โ No ) | ||
Theorem | noextendseq 27587 | Extend a surreal by a sequence of ordinals. (Contributed by Scott Fenton, 30-Nov-2021.) |
โข ๐ โ {1o, 2o} โ โข ((๐ด โ No โง ๐ต โ On) โ (๐ด โช ((๐ต โ dom ๐ด) ร {๐})) โ No ) | ||
Theorem | noextenddif 27588* | Calculate the place where a surreal and its extension differ. (Contributed by Scott Fenton, 22-Nov-2021.) |
โข ๐ โ {1o, 2o} โ โข (๐ด โ No โ โฉ {๐ฅ โ On โฃ (๐ดโ๐ฅ) โ ((๐ด โช {โจdom ๐ด, ๐โฉ})โ๐ฅ)} = dom ๐ด) | ||
Theorem | noextendlt 27589 | Extending a surreal with a negative sign results in a smaller surreal. (Contributed by Scott Fenton, 22-Nov-2021.) |
โข (๐ด โ No โ (๐ด โช {โจdom ๐ด, 1oโฉ}) <s ๐ด) | ||
Theorem | noextendgt 27590 | Extending a surreal with a positive sign results in a bigger surreal. (Contributed by Scott Fenton, 22-Nov-2021.) |
โข (๐ด โ No โ ๐ด <s (๐ด โช {โจdom ๐ด, 2oโฉ})) | ||
Theorem | nolesgn2o 27591 | Given ๐ด less-than or equal to ๐ต, equal to ๐ต up to ๐, and ๐ด(๐) = 2o, then ๐ต(๐) = 2o. (Contributed by Scott Fenton, 6-Dec-2021.) |
โข (((๐ด โ No โง ๐ต โ No โง ๐ โ On) โง ((๐ด โพ ๐) = (๐ต โพ ๐) โง (๐ดโ๐) = 2o) โง ยฌ ๐ต <s ๐ด) โ (๐ตโ๐) = 2o) | ||
Theorem | nolesgn2ores 27592 | Given ๐ด less-than or equal to ๐ต, equal to ๐ต up to ๐, and ๐ด(๐) = 2o, then (๐ด โพ suc ๐) = (๐ต โพ suc ๐). (Contributed by Scott Fenton, 6-Dec-2021.) |
โข (((๐ด โ No โง ๐ต โ No โง ๐ โ On) โง ((๐ด โพ ๐) = (๐ต โพ ๐) โง (๐ดโ๐) = 2o) โง ยฌ ๐ต <s ๐ด) โ (๐ด โพ suc ๐) = (๐ต โพ suc ๐)) | ||
Theorem | nogesgn1o 27593 | Given ๐ด greater than or equal to ๐ต, equal to ๐ต up to ๐, and ๐ด(๐) = 1o, then ๐ต(๐) = 1o. (Contributed by Scott Fenton, 9-Aug-2024.) |
โข (((๐ด โ No โง ๐ต โ No โง ๐ โ On) โง ((๐ด โพ ๐) = (๐ต โพ ๐) โง (๐ดโ๐) = 1o) โง ยฌ ๐ด <s ๐ต) โ (๐ตโ๐) = 1o) | ||
Theorem | nogesgn1ores 27594 | Given ๐ด greater than or equal to ๐ต, equal to ๐ต up to ๐, and ๐ด(๐) = 1o, then (๐ด โพ suc ๐) = (๐ต โพ suc ๐). (Contributed by Scott Fenton, 6-Dec-2021.) |
โข (((๐ด โ No โง ๐ต โ No โง ๐ โ On) โง ((๐ด โพ ๐) = (๐ต โพ ๐) โง (๐ดโ๐) = 1o) โง ยฌ ๐ด <s ๐ต) โ (๐ด โพ suc ๐) = (๐ต โพ suc ๐)) | ||
Theorem | sltsolem1 27595 | Lemma for sltso 27596. The "sign expansion" binary relation totally orders the surreal signs. (Contributed by Scott Fenton, 8-Jun-2011.) |
โข {โจ1o, โ โฉ, โจ1o, 2oโฉ, โจโ , 2oโฉ} Or ({1o, 2o} โช {โ }) | ||
Theorem | sltso 27596 | Less-than totally orders the surreals. Axiom O of [Alling] p. 184. (Contributed by Scott Fenton, 9-Jun-2011.) |
โข <s Or No | ||
Theorem | bdayfo 27597 | The birthday function maps the surreals onto the ordinals. Axiom B of [Alling] p. 184. (Proof shortened on 14-Apr-2012 by SF). (Contributed by Scott Fenton, 11-Jun-2011.) |
โข bday : No โontoโOn | ||
Theorem | fvnobday 27598 | The value of a surreal at its birthday is โ . (Contributed by Scott Fenton, 14-Jun-2011.) (Proof shortened by SF, 14-Apr-2012.) |
โข (๐ด โ No โ (๐ดโ( bday โ๐ด)) = โ ) | ||
Theorem | nosepnelem 27599* | Lemma for nosepne 27600. (Contributed by Scott Fenton, 24-Nov-2021.) |
โข ((๐ด โ No โง ๐ต โ No โง ๐ด <s ๐ต) โ (๐ดโโฉ {๐ฅ โ On โฃ (๐ดโ๐ฅ) โ (๐ตโ๐ฅ)}) โ (๐ตโโฉ {๐ฅ โ On โฃ (๐ดโ๐ฅ) โ (๐ตโ๐ฅ)})) | ||
Theorem | nosepne 27600* | The value of two non-equal surreals at the first place they differ is different. (Contributed by Scott Fenton, 24-Nov-2021.) |
โข ((๐ด โ No โง ๐ต โ No โง ๐ด โ ๐ต) โ (๐ดโโฉ {๐ฅ โ On โฃ (๐ดโ๐ฅ) โ (๐ตโ๐ฅ)}) โ (๐ตโโฉ {๐ฅ โ On โฃ (๐ดโ๐ฅ) โ (๐ตโ๐ฅ)})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |