Step | Hyp | Ref
| Expression |
1 | | tgoldbachgtd.o |
. . 3
β’ π = {π§ β β€ β£ Β¬ 2 β₯ π§} |
2 | | tgoldbachgtd.n |
. . . 4
β’ (π β π β π) |
3 | 2 | ad3antrrr 727 |
. . 3
β’ ((((π β§ β β ((0[,)+β) βm
β)) β§ π β
((0[,)+β) βm β)) β§ (βπ β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β π β π) |
4 | | tgoldbachgtd.1 |
. . . 4
β’ (π β (;10β;27) β€ π) |
5 | 4 | ad3antrrr 727 |
. . 3
β’ ((((π β§ β β ((0[,)+β) βm
β)) β§ π β
((0[,)+β) βm β)) β§ (βπ β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β (;10β;27) β€ π) |
6 | | elmapi 8846 |
. . . 4
β’ (β β ((0[,)+β)
βm β) β β:ββΆ(0[,)+β)) |
7 | 6 | ad3antlr 728 |
. . 3
β’ ((((π β§ β β ((0[,)+β) βm
β)) β§ π β
((0[,)+β) βm β)) β§ (βπ β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β β:ββΆ(0[,)+β)) |
8 | | elmapi 8846 |
. . . 4
β’ (π β ((0[,)+β)
βm β) β π:ββΆ(0[,)+β)) |
9 | 8 | ad2antlr 724 |
. . 3
β’ ((((π β§ β β ((0[,)+β) βm
β)) β§ π β
((0[,)+β) βm β)) β§ (βπ β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β π:ββΆ(0[,)+β)) |
10 | | simpr1 1193 |
. . . . 5
β’ ((((π β§ β β ((0[,)+β) βm
β)) β§ π β
((0[,)+β) βm β)) β§ (βπ β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β βπ β β (πβπ) β€ (1._0_7_9_9_55)) |
11 | | fveq2 6892 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
12 | 11 | breq1d 5159 |
. . . . . 6
β’ (π = π β ((πβπ) β€ (1._0_7_9_9_55)
β (πβπ) β€ (1._0_7_9_9_55))) |
13 | 12 | cbvralvw 3233 |
. . . . 5
β’
(βπ β
β (πβπ) β€ (1._0_7_9_9_55)
β βπ β
β (πβπ) β€ (1._0_7_9_9_55)) |
14 | 10, 13 | sylib 217 |
. . . 4
β’ ((((π β§ β β ((0[,)+β) βm
β)) β§ π β
((0[,)+β) βm β)) β§ (βπ β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β βπ β β (πβπ) β€ (1._0_7_9_9_55)) |
15 | 14 | r19.21bi 3247 |
. . 3
β’
(((((π β§ β β ((0[,)+β)
βm β)) β§ π β ((0[,)+β) βm
β)) β§ (βπ
β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β§ π β β) β (πβπ) β€ (1._0_7_9_9_55)) |
16 | | simpr2 1194 |
. . . . 5
β’ ((((π β§ β β ((0[,)+β) βm
β)) β§ π β
((0[,)+β) βm β)) β§ (βπ β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β βπ β β (ββπ) β€ (1._4_14)) |
17 | | fveq2 6892 |
. . . . . . 7
β’ (π = π β (ββπ) = (ββπ)) |
18 | 17 | breq1d 5159 |
. . . . . 6
β’ (π = π β ((ββπ) β€ (1._4_14)
β (ββπ) β€ (1._4_14))) |
19 | 18 | cbvralvw 3233 |
. . . . 5
β’
(βπ β
β (ββπ) β€ (1._4_14)
β βπ β
β (ββπ) β€ (1._4_14)) |
20 | 16, 19 | sylib 217 |
. . . 4
β’ ((((π β§ β β ((0[,)+β) βm
β)) β§ π β
((0[,)+β) βm β)) β§ (βπ β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β βπ β β (ββπ) β€ (1._4_14)) |
21 | 20 | r19.21bi 3247 |
. . 3
β’
(((((π β§ β β ((0[,)+β)
βm β)) β§ π β ((0[,)+β) βm
β)) β§ (βπ
β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β§ π β β) β (ββπ) β€ (1._4_14)) |
22 | | simpr3 1195 |
. . . 4
β’ ((((π β§ β β ((0[,)+β) βm
β)) β§ π β
((0[,)+β) βm β)) β§ (βπ β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯) |
23 | | fveq2 6892 |
. . . . . . 7
β’ (π₯ = π¦ β (((Ξ βf
Β· β)vtsπ)βπ₯) = (((Ξ βf Β·
β)vtsπ)βπ¦)) |
24 | | fveq2 6892 |
. . . . . . . 8
β’ (π₯ = π¦ β (((Ξ βf
Β· π)vtsπ)βπ₯) = (((Ξ βf Β·
π)vtsπ)βπ¦)) |
25 | 24 | oveq1d 7427 |
. . . . . . 7
β’ (π₯ = π¦ β ((((Ξ βf
Β· π)vtsπ)βπ₯)β2) = ((((Ξ βf
Β· π)vtsπ)βπ¦)β2)) |
26 | 23, 25 | oveq12d 7430 |
. . . . . 6
β’ (π₯ = π¦ β ((((Ξ βf
Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) = ((((Ξ βf
Β· β)vtsπ)βπ¦) Β· ((((Ξ βf
Β· π)vtsπ)βπ¦)β2))) |
27 | | oveq2 7420 |
. . . . . . . 8
β’ (π₯ = π¦ β (-π Β· π₯) = (-π Β· π¦)) |
28 | 27 | oveq2d 7428 |
. . . . . . 7
β’ (π₯ = π¦ β ((i Β· (2 Β· Ο))
Β· (-π Β· π₯)) = ((i Β· (2 Β·
Ο)) Β· (-π
Β· π¦))) |
29 | 28 | fveq2d 6896 |
. . . . . 6
β’ (π₯ = π¦ β (expβ((i Β· (2 Β·
Ο)) Β· (-π
Β· π₯))) =
(expβ((i Β· (2 Β· Ο)) Β· (-π Β· π¦)))) |
30 | 26, 29 | oveq12d 7430 |
. . . . 5
β’ (π₯ = π¦ β (((((Ξ βf
Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) = (((((Ξ βf
Β· β)vtsπ)βπ¦) Β· ((((Ξ βf
Β· π)vtsπ)βπ¦)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π¦))))) |
31 | 30 | cbvitgv 25527 |
. . . 4
β’
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯ = β«(0(,)1)(((((Ξ
βf Β· β)vtsπ)βπ¦) Β· ((((Ξ βf
Β· π)vtsπ)βπ¦)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π¦)))) dπ¦ |
32 | 22, 31 | breqtrdi 5190 |
. . 3
β’ ((((π β§ β β ((0[,)+β) βm
β)) β§ π β
((0[,)+β) βm β)) β§ (βπ β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ¦) Β· ((((Ξ βf
Β· π)vtsπ)βπ¦)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π¦)))) dπ¦) |
33 | 1, 3, 5, 7, 9, 15,
21, 32 | tgoldbachgtda 33968 |
. 2
β’ ((((π β§ β β ((0[,)+β) βm
β)) β§ π β
((0[,)+β) βm β)) β§ (βπ β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) β 0 < (β―β((π β©
β)(reprβ3)π))) |
34 | 1, 2, 4 | hgt749d 33956 |
. 2
β’ (π β ββ β ((0[,)+β) βm
β)βπ β
((0[,)+β) βm β)(βπ β β (πβπ) β€ (1._0_7_9_9_55)
β§ βπ β
β (ββπ) β€ (1._4_14)
β§ ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· β)vtsπ)βπ₯) Β· ((((Ξ βf
Β· π)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯)) |
35 | 33, 34 | r19.29vva 3212 |
1
β’ (π β 0 <
(β―β((π β©
β)(reprβ3)π))) |