Step | Hyp | Ref
| Expression |
1 | | tgoldbachgtda.o |
. . . . . . . . 9
β’ π = {π§ β β€ β£ Β¬ 2 β₯ π§} |
2 | | tgoldbachgtda.n |
. . . . . . . . 9
β’ (π β π β π) |
3 | | tgoldbachgtda.0 |
. . . . . . . . 9
β’ (π β (;10β;27) β€ π) |
4 | 1, 2, 3 | tgoldbachgnn 33312 |
. . . . . . . 8
β’ (π β π β β) |
5 | 4 | nnnn0d 12480 |
. . . . . . 7
β’ (π β π β
β0) |
6 | | 3nn0 12438 |
. . . . . . . 8
β’ 3 β
β0 |
7 | 6 | a1i 11 |
. . . . . . 7
β’ (π β 3 β
β0) |
8 | | ssidd 3972 |
. . . . . . 7
β’ (π β β β
β) |
9 | 5, 7, 8 | reprfi2 33276 |
. . . . . 6
β’ (π β
(β(reprβ3)π)
β Fin) |
10 | | diffi 9130 |
. . . . . 6
β’
((β(reprβ3)π) β Fin β
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π))
β Fin) |
11 | 9, 10 | syl 17 |
. . . . 5
β’ (π β
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π))
β Fin) |
12 | | difssd 4097 |
. . . . . . 7
β’ (π β
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π))
β (β(reprβ3)π)) |
13 | 12 | sselda 3949 |
. . . . . 6
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β π β (β(reprβ3)π)) |
14 | | vmaf 26484 |
. . . . . . . . . 10
β’
Ξ:ββΆβ |
15 | 14 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (β(reprβ3)π)) β
Ξ:ββΆβ) |
16 | | ssidd 3972 |
. . . . . . . . . . 11
β’ ((π β§ π β (β(reprβ3)π)) β β β
β) |
17 | 5 | nn0zd 12532 |
. . . . . . . . . . . 12
β’ (π β π β β€) |
18 | 17 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (β(reprβ3)π)) β π β β€) |
19 | 6 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (β(reprβ3)π)) β 3 β
β0) |
20 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β (β(reprβ3)π)) β π β (β(reprβ3)π)) |
21 | 16, 18, 19, 20 | reprf 33265 |
. . . . . . . . . 10
β’ ((π β§ π β (β(reprβ3)π)) β π:(0..^3)βΆβ) |
22 | | c0ex 11156 |
. . . . . . . . . . . . 13
β’ 0 β
V |
23 | 22 | tpid1 4734 |
. . . . . . . . . . . 12
β’ 0 β
{0, 1, 2} |
24 | | fzo0to3tp 13665 |
. . . . . . . . . . . 12
β’ (0..^3) =
{0, 1, 2} |
25 | 23, 24 | eleqtrri 2837 |
. . . . . . . . . . 11
β’ 0 β
(0..^3) |
26 | 25 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (β(reprβ3)π)) β 0 β
(0..^3)) |
27 | 21, 26 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ ((π β§ π β (β(reprβ3)π)) β (πβ0) β β) |
28 | 15, 27 | ffvelcdmd 7041 |
. . . . . . . 8
β’ ((π β§ π β (β(reprβ3)π)) β (Ξβ(πβ0)) β
β) |
29 | | tgoldbachgtda.h |
. . . . . . . . . . 11
β’ (π β π»:ββΆ(0[,)+β)) |
30 | | rge0ssre 13380 |
. . . . . . . . . . 11
β’
(0[,)+β) β β |
31 | | fss 6690 |
. . . . . . . . . . 11
β’ ((π»:ββΆ(0[,)+β)
β§ (0[,)+β) β β) β π»:ββΆβ) |
32 | 29, 30, 31 | sylancl 587 |
. . . . . . . . . 10
β’ (π β π»:ββΆβ) |
33 | 32 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (β(reprβ3)π)) β π»:ββΆβ) |
34 | 33, 27 | ffvelcdmd 7041 |
. . . . . . . 8
β’ ((π β§ π β (β(reprβ3)π)) β (π»β(πβ0)) β β) |
35 | 28, 34 | remulcld 11192 |
. . . . . . 7
β’ ((π β§ π β (β(reprβ3)π)) β
((Ξβ(πβ0)) Β· (π»β(πβ0))) β β) |
36 | | 1ex 11158 |
. . . . . . . . . . . . . 14
β’ 1 β
V |
37 | 36 | tpid2 4736 |
. . . . . . . . . . . . 13
β’ 1 β
{0, 1, 2} |
38 | 37, 24 | eleqtrri 2837 |
. . . . . . . . . . . 12
β’ 1 β
(0..^3) |
39 | 38 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (β(reprβ3)π)) β 1 β
(0..^3)) |
40 | 21, 39 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π β§ π β (β(reprβ3)π)) β (πβ1) β β) |
41 | 15, 40 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ ((π β§ π β (β(reprβ3)π)) β (Ξβ(πβ1)) β
β) |
42 | | tgoldbachgtda.k |
. . . . . . . . . . . 12
β’ (π β πΎ:ββΆ(0[,)+β)) |
43 | | fss 6690 |
. . . . . . . . . . . 12
β’ ((πΎ:ββΆ(0[,)+β)
β§ (0[,)+β) β β) β πΎ:ββΆβ) |
44 | 42, 30, 43 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β πΎ:ββΆβ) |
45 | 44 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (β(reprβ3)π)) β πΎ:ββΆβ) |
46 | 45, 40 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ ((π β§ π β (β(reprβ3)π)) β (πΎβ(πβ1)) β β) |
47 | 41, 46 | remulcld 11192 |
. . . . . . . 8
β’ ((π β§ π β (β(reprβ3)π)) β
((Ξβ(πβ1)) Β· (πΎβ(πβ1))) β β) |
48 | | 2ex 12237 |
. . . . . . . . . . . . . 14
β’ 2 β
V |
49 | 48 | tpid3 4739 |
. . . . . . . . . . . . 13
β’ 2 β
{0, 1, 2} |
50 | 49, 24 | eleqtrri 2837 |
. . . . . . . . . . . 12
β’ 2 β
(0..^3) |
51 | 50 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (β(reprβ3)π)) β 2 β
(0..^3)) |
52 | 21, 51 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π β§ π β (β(reprβ3)π)) β (πβ2) β β) |
53 | 15, 52 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ ((π β§ π β (β(reprβ3)π)) β (Ξβ(πβ2)) β
β) |
54 | 45, 52 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ ((π β§ π β (β(reprβ3)π)) β (πΎβ(πβ2)) β β) |
55 | 53, 54 | remulcld 11192 |
. . . . . . . 8
β’ ((π β§ π β (β(reprβ3)π)) β
((Ξβ(πβ2)) Β· (πΎβ(πβ2))) β β) |
56 | 47, 55 | remulcld 11192 |
. . . . . . 7
β’ ((π β§ π β (β(reprβ3)π)) β
(((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2)))) β β) |
57 | 35, 56 | remulcld 11192 |
. . . . . 6
β’ ((π β§ π β (β(reprβ3)π)) β
(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β
β) |
58 | 13, 57 | syldan 592 |
. . . . 5
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β
(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β
β) |
59 | 11, 58 | fsumrecl 15626 |
. . . 4
β’ (π β Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β
β) |
60 | | 0nn0 12435 |
. . . . . . 7
β’ 0 β
β0 |
61 | | qssre 12891 |
. . . . . . . 8
β’ β
β β |
62 | | 4nn0 12439 |
. . . . . . . . . . . 12
β’ 4 β
β0 |
63 | | 2nn0 12437 |
. . . . . . . . . . . . 13
β’ 2 β
β0 |
64 | | nn0ssq 12889 |
. . . . . . . . . . . . . . . 16
β’
β0 β β |
65 | | 8nn0 12443 |
. . . . . . . . . . . . . . . 16
β’ 8 β
β0 |
66 | 64, 65 | sselii 3946 |
. . . . . . . . . . . . . . 15
β’ 8 β
β |
67 | 62, 66 | dp2clq 31779 |
. . . . . . . . . . . . . 14
β’ _48 β β |
68 | 63, 67 | dp2clq 31779 |
. . . . . . . . . . . . 13
β’ _2_48 β β |
69 | 63, 68 | dp2clq 31779 |
. . . . . . . . . . . 12
β’ _2_2_48
β β |
70 | 62, 69 | dp2clq 31779 |
. . . . . . . . . . 11
β’ _4_2_2_48
β β |
71 | 60, 70 | dp2clq 31779 |
. . . . . . . . . 10
β’ _0_4_2_2_48
β β |
72 | 60, 71 | dp2clq 31779 |
. . . . . . . . 9
β’ _0_0_4_2_2_48
β β |
73 | 60, 72 | dp2clq 31779 |
. . . . . . . 8
β’ _0_0_0_4_2_2_48
β β |
74 | 61, 73 | sselii 3946 |
. . . . . . 7
β’ _0_0_0_4_2_2_48
β β |
75 | | dpcl 31789 |
. . . . . . 7
β’ ((0
β β0 β§ _0_0_0_4_2_2_48
β β) β (0._0_0_0_4_2_2_48)
β β) |
76 | 60, 74, 75 | mp2an 691 |
. . . . . 6
β’ (0._0_0_0_4_2_2_48)
β β |
77 | 76 | a1i 11 |
. . . . 5
β’ (π β (0._0_0_0_4_2_2_48)
β β) |
78 | 4 | nnred 12175 |
. . . . . 6
β’ (π β π β β) |
79 | 78 | resqcld 14037 |
. . . . 5
β’ (π β (πβ2) β β) |
80 | 77, 79 | remulcld 11192 |
. . . 4
β’ (π β ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β
β) |
81 | 9, 57 | fsumrecl 15626 |
. . . 4
β’ (π β Ξ£π β (β(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β
β) |
82 | | 7nn0 12442 |
. . . . . . . . 9
β’ 7 β
β0 |
83 | 6, 67 | dp2clq 31779 |
. . . . . . . . . 10
β’ _3_48 β β |
84 | 61, 83 | sselii 3946 |
. . . . . . . . 9
β’ _3_48 β β |
85 | | dpcl 31789 |
. . . . . . . . 9
β’ ((7
β β0 β§ _3_48
β β) β (7._3_48) β β) |
86 | 82, 84, 85 | mp2an 691 |
. . . . . . . 8
β’ (7._3_48) β β |
87 | 86 | a1i 11 |
. . . . . . 7
β’ (π β (7._3_48)
β β) |
88 | 4 | nnrpd 12962 |
. . . . . . . . 9
β’ (π β π β
β+) |
89 | 88 | relogcld 25994 |
. . . . . . . 8
β’ (π β (logβπ) β
β) |
90 | 5 | nn0ge0d 12483 |
. . . . . . . . 9
β’ (π β 0 β€ π) |
91 | 78, 90 | resqrtcld 15309 |
. . . . . . . 8
β’ (π β (ββπ) β
β) |
92 | 88 | sqrtgt0d 15304 |
. . . . . . . . 9
β’ (π β 0 <
(ββπ)) |
93 | 92 | gt0ne0d 11726 |
. . . . . . . 8
β’ (π β (ββπ) β 0) |
94 | 89, 91, 93 | redivcld 11990 |
. . . . . . 7
β’ (π β ((logβπ) / (ββπ)) β
β) |
95 | 87, 94 | remulcld 11192 |
. . . . . 6
β’ (π β ((7._3_48)
Β· ((logβπ) /
(ββπ))) β
β) |
96 | 95, 79 | remulcld 11192 |
. . . . 5
β’ (π β (((7._3_48)
Β· ((logβπ) /
(ββπ)))
Β· (πβ2)) β
β) |
97 | | tgoldbachgtda.1 |
. . . . . 6
β’ ((π β§ π β β) β (πΎβπ) β€ (1._0_7_9_9_55)) |
98 | | tgoldbachgtda.2 |
. . . . . 6
β’ ((π β§ π β β) β (π»βπ) β€ (1._4_14)) |
99 | 1, 4, 3, 29, 42, 97, 98 | hgt750leme 33311 |
. . . . 5
β’ (π β Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β€ (((7._3_48)
Β· ((logβπ) /
(ββπ)))
Β· (πβ2))) |
100 | | 2z 12542 |
. . . . . . . 8
β’ 2 β
β€ |
101 | 100 | a1i 11 |
. . . . . . 7
β’ (π β 2 β
β€) |
102 | 88, 101 | rpexpcld 14157 |
. . . . . 6
β’ (π β (πβ2) β
β+) |
103 | | hgt750lem 33304 |
. . . . . . 7
β’ ((π β β0
β§ (;10β;27) β€ π) β ((7._3_48)
Β· ((logβπ) /
(ββπ))) <
(0._0_0_0_4_2_2_48)) |
104 | 5, 3, 103 | syl2anc 585 |
. . . . . 6
β’ (π β ((7._3_48)
Β· ((logβπ) /
(ββπ))) <
(0._0_0_0_4_2_2_48)) |
105 | 95, 77, 102, 104 | ltmul1dd 13019 |
. . . . 5
β’ (π β (((7._3_48)
Β· ((logβπ) /
(ββπ)))
Β· (πβ2)) <
((0._0_0_0_4_2_2_48)
Β· (πβ2))) |
106 | 59, 96, 80, 99, 105 | lelttrd 11320 |
. . . 4
β’ (π β Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) < ((0._0_0_0_4_2_2_48)
Β· (πβ2))) |
107 | | tgoldbachgtda.3 |
. . . . 5
β’ (π β ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
β«(0(,)1)(((((Ξ βf Β· π»)vtsπ)βπ₯) Β· ((((Ξ βf
Β· πΎ)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯) |
108 | 32, 44, 5 | circlemethhgt 33296 |
. . . . 5
β’ (π β Ξ£π β (β(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) = β«(0(,)1)(((((Ξ
βf Β· π»)vtsπ)βπ₯) Β· ((((Ξ βf
Β· πΎ)vtsπ)βπ₯)β2)) Β· (expβ((i Β·
(2 Β· Ο)) Β· (-π Β· π₯)))) dπ₯) |
109 | 107, 108 | breqtrrd 5138 |
. . . 4
β’ (π β ((0._0_0_0_4_2_2_48)
Β· (πβ2)) β€
Ξ£π β
(β(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2)))))) |
110 | 59, 80, 81, 106, 109 | ltletrd 11322 |
. . 3
β’ (π β Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) < Ξ£π β (β(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2)))))) |
111 | 59, 81 | posdifd 11749 |
. . 3
β’ (π β (Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) < Ξ£π β (β(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β 0 < (Ξ£π β
(β(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β Ξ£π β
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2)))))))) |
112 | 110, 111 | mpbid 231 |
. 2
β’ (π β 0 < (Ξ£π β
(β(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β Ξ£π β
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))))) |
113 | | inss2 4194 |
. . . . . . . 8
β’ (π β© β) β
β |
114 | | prmssnn 16559 |
. . . . . . . 8
β’ β
β β |
115 | 113, 114 | sstri 3958 |
. . . . . . 7
β’ (π β© β) β
β |
116 | 115 | a1i 11 |
. . . . . 6
β’ (π β (π β© β) β
β) |
117 | 8, 17, 7, 116 | reprss 33270 |
. . . . 5
β’ (π β ((π β© β)(reprβ3)π) β
(β(reprβ3)π)) |
118 | 9, 117 | ssfid 9218 |
. . . 4
β’ (π β ((π β© β)(reprβ3)π) β Fin) |
119 | 117 | sselda 3949 |
. . . . 5
β’ ((π β§ π β ((π β© β)(reprβ3)π)) β π β (β(reprβ3)π)) |
120 | 57 | recnd 11190 |
. . . . 5
β’ ((π β§ π β (β(reprβ3)π)) β
(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β
β) |
121 | 119, 120 | syldan 592 |
. . . 4
β’ ((π β§ π β ((π β© β)(reprβ3)π)) β
(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β
β) |
122 | 118, 121 | fsumcl 15625 |
. . 3
β’ (π β Ξ£π β ((π β© β)(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β
β) |
123 | 59 | recnd 11190 |
. . 3
β’ (π β Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β
β) |
124 | | disjdif 4436 |
. . . . 5
β’ (((π β©
β)(reprβ3)π)
β© ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) = β
|
125 | 124 | a1i 11 |
. . . 4
β’ (π β (((π β© β)(reprβ3)π) β©
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π)))
= β
) |
126 | | undif 4446 |
. . . . . 6
β’ (((π β©
β)(reprβ3)π)
β (β(reprβ3)π) β (((π β© β)(reprβ3)π) βͺ
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π)))
= (β(reprβ3)π)) |
127 | 117, 126 | sylib 217 |
. . . . 5
β’ (π β (((π β© β)(reprβ3)π) βͺ
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π)))
= (β(reprβ3)π)) |
128 | 127 | eqcomd 2743 |
. . . 4
β’ (π β
(β(reprβ3)π) =
(((π β©
β)(reprβ3)π)
βͺ ((β(reprβ3)π) β ((π β© β)(reprβ3)π)))) |
129 | 125, 128,
9, 120 | fsumsplit 15633 |
. . 3
β’ (π β Ξ£π β (β(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) = (Ξ£π β ((π β© β)(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) + Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))))) |
130 | 122, 123,
129 | mvrraddd 11574 |
. 2
β’ (π β (Ξ£π β (β(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β Ξ£π β
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2)))))) = Ξ£π β ((π β© β)(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2)))))) |
131 | 112, 130 | breqtrd 5136 |
1
β’ (π β 0 < Ξ£π β ((π β© β)(reprβ3)π)(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2)))))) |