Proof of Theorem tgoldbachgtde
Step | Hyp | Ref
| Expression |
1 | | tgoldbachgtda.o |
. . . . . . . . 9
|
2 | | tgoldbachgtda.n |
. . . . . . . . 9
|
3 | | tgoldbachgtda.0 |
. . . . . . . . 9
;; |
4 | 1, 2, 3 | tgoldbachgnn 30737 |
. . . . . . . 8
|
5 | 4 | nnnn0d 11351 |
. . . . . . 7
|
6 | | 3nn0 11310 |
. . . . . . . 8
|
7 | 6 | a1i 11 |
. . . . . . 7
|
8 | | ssid 3624 |
. . . . . . . 8
|
9 | 8 | a1i 11 |
. . . . . . 7
|
10 | 5, 7, 9 | reprfi2 30701 |
. . . . . 6
repr |
11 | | diffi 8192 |
. . . . . 6
repr repr repr |
12 | 10, 11 | syl 17 |
. . . . 5
repr repr |
13 | | difssd 3738 |
. . . . . . 7
repr repr repr |
14 | 13 | sselda 3603 |
. . . . . 6
repr repr repr |
15 | | vmaf 24845 |
. . . . . . . . . 10
Λ |
16 | 15 | a1i 11 |
. . . . . . . . 9
repr Λ |
17 | 8 | a1i 11 |
. . . . . . . . . . 11
repr |
18 | 5 | nn0zd 11480 |
. . . . . . . . . . . 12
|
19 | 18 | adantr 481 |
. . . . . . . . . . 11
repr |
20 | 6 | a1i 11 |
. . . . . . . . . . 11
repr |
21 | | simpr 477 |
. . . . . . . . . . 11
repr repr |
22 | 17, 19, 20, 21 | reprf 30690 |
. . . . . . . . . 10
repr ..^ |
23 | | c0ex 10034 |
. . . . . . . . . . . . 13
|
24 | 23 | tpid1 4303 |
. . . . . . . . . . . 12
|
25 | | fzo0to3tp 12554 |
. . . . . . . . . . . 12
..^ |
26 | 24, 25 | eleqtrri 2700 |
. . . . . . . . . . 11
..^ |
27 | 26 | a1i 11 |
. . . . . . . . . 10
repr ..^ |
28 | 22, 27 | ffvelrnd 6360 |
. . . . . . . . 9
repr |
29 | 16, 28 | ffvelrnd 6360 |
. . . . . . . 8
repr Λ |
30 | | tgoldbachgtda.h |
. . . . . . . . . . 11
|
31 | | rge0ssre 12280 |
. . . . . . . . . . 11
|
32 | | fss 6056 |
. . . . . . . . . . 11
|
33 | 30, 31, 32 | sylancl 694 |
. . . . . . . . . 10
|
34 | 33 | adantr 481 |
. . . . . . . . 9
repr |
35 | 34, 28 | ffvelrnd 6360 |
. . . . . . . 8
repr |
36 | 29, 35 | remulcld 10070 |
. . . . . . 7
repr Λ |
37 | | 1ex 10035 |
. . . . . . . . . . . . . 14
|
38 | 37 | tpid2 4304 |
. . . . . . . . . . . . 13
|
39 | 38, 25 | eleqtrri 2700 |
. . . . . . . . . . . 12
..^ |
40 | 39 | a1i 11 |
. . . . . . . . . . 11
repr ..^ |
41 | 22, 40 | ffvelrnd 6360 |
. . . . . . . . . 10
repr |
42 | 16, 41 | ffvelrnd 6360 |
. . . . . . . . 9
repr Λ |
43 | | tgoldbachgtda.k |
. . . . . . . . . . . 12
|
44 | | fss 6056 |
. . . . . . . . . . . 12
|
45 | 43, 31, 44 | sylancl 694 |
. . . . . . . . . . 11
|
46 | 45 | adantr 481 |
. . . . . . . . . 10
repr |
47 | 46, 41 | ffvelrnd 6360 |
. . . . . . . . 9
repr |
48 | 42, 47 | remulcld 10070 |
. . . . . . . 8
repr Λ |
49 | | 2ex 11092 |
. . . . . . . . . . . . . 14
|
50 | 49 | tpid3 4307 |
. . . . . . . . . . . . 13
|
51 | 50, 25 | eleqtrri 2700 |
. . . . . . . . . . . 12
..^ |
52 | 51 | a1i 11 |
. . . . . . . . . . 11
repr ..^ |
53 | 22, 52 | ffvelrnd 6360 |
. . . . . . . . . 10
repr |
54 | 16, 53 | ffvelrnd 6360 |
. . . . . . . . 9
repr Λ |
55 | 46, 53 | ffvelrnd 6360 |
. . . . . . . . 9
repr |
56 | 54, 55 | remulcld 10070 |
. . . . . . . 8
repr Λ |
57 | 48, 56 | remulcld 10070 |
. . . . . . 7
repr Λ Λ |
58 | 36, 57 | remulcld 10070 |
. . . . . 6
repr Λ Λ Λ |
59 | 14, 58 | syldan 487 |
. . . . 5
repr repr Λ Λ Λ |
60 | 12, 59 | fsumrecl 14465 |
. . . 4
repr reprΛ Λ Λ |
61 | | 0nn0 11307 |
. . . . . . 7
|
62 | | qssre 11798 |
. . . . . . . 8
|
63 | | 4nn0 11311 |
. . . . . . . . . . . 12
|
64 | | 2nn0 11309 |
. . . . . . . . . . . . 13
|
65 | | nn0ssq 11796 |
. . . . . . . . . . . . . . . 16
|
66 | | 8nn0 11315 |
. . . . . . . . . . . . . . . 16
|
67 | 65, 66 | sselii 3600 |
. . . . . . . . . . . . . . 15
|
68 | 63, 67 | dp2clq 29588 |
. . . . . . . . . . . . . 14
_ |
69 | 64, 68 | dp2clq 29588 |
. . . . . . . . . . . . 13
__ |
70 | 64, 69 | dp2clq 29588 |
. . . . . . . . . . . 12
___ |
71 | 63, 70 | dp2clq 29588 |
. . . . . . . . . . 11
____ |
72 | 61, 71 | dp2clq 29588 |
. . . . . . . . . 10
_____ |
73 | 61, 72 | dp2clq 29588 |
. . . . . . . . 9
______ |
74 | 61, 73 | dp2clq 29588 |
. . . . . . . 8
_______ |
75 | 62, 74 | sselii 3600 |
. . . . . . 7
_______ |
76 | | dpcl 29598 |
. . . . . . 7
_______ _______ |
77 | 61, 75, 76 | mp2an 708 |
. . . . . 6
_______ |
78 | 77 | a1i 11 |
. . . . 5
_______ |
79 | 4 | nnred 11035 |
. . . . . 6
|
80 | 79 | resqcld 13035 |
. . . . 5
|
81 | 78, 80 | remulcld 10070 |
. . . 4
_______ |
82 | 10, 58 | fsumrecl 14465 |
. . . 4
reprΛ Λ Λ |
83 | | 7nn0 11314 |
. . . . . . . . 9
|
84 | 6, 68 | dp2clq 29588 |
. . . . . . . . . 10
__ |
85 | 62, 84 | sselii 3600 |
. . . . . . . . 9
__ |
86 | | dpcl 29598 |
. . . . . . . . 9
__ __ |
87 | 83, 85, 86 | mp2an 708 |
. . . . . . . 8
__ |
88 | 87 | a1i 11 |
. . . . . . 7
__ |
89 | 4 | nnrpd 11870 |
. . . . . . . . 9
|
90 | 89 | relogcld 24369 |
. . . . . . . 8
|
91 | 5 | nn0ge0d 11354 |
. . . . . . . . 9
|
92 | 79, 91 | resqrtcld 14156 |
. . . . . . . 8
|
93 | 89 | sqrtgt0d 14151 |
. . . . . . . . 9
|
94 | 93 | gt0ne0d 10592 |
. . . . . . . 8
|
95 | 90, 92, 94 | redivcld 10853 |
. . . . . . 7
|
96 | 88, 95 | remulcld 10070 |
. . . . . 6
__ |
97 | 96, 80 | remulcld 10070 |
. . . . 5
__ |
98 | | tgoldbachgtda.1 |
. . . . . 6
_____ |
99 | | tgoldbachgtda.2 |
. . . . . 6
__ |
100 | 1, 4, 3, 30, 43, 98, 99 | hgt750leme 30736 |
. . . . 5
repr reprΛ Λ Λ __ |
101 | | 2z 11409 |
. . . . . . . 8
|
102 | 101 | a1i 11 |
. . . . . . 7
|
103 | 89, 102 | rpexpcld 13032 |
. . . . . 6
|
104 | | hgt750lem 30729 |
. . . . . . 7
;; __ _______ |
105 | 5, 3, 104 | syl2anc 693 |
. . . . . 6
__ _______ |
106 | 96, 78, 103, 105 | ltmul1dd 11927 |
. . . . 5
__ _______ |
107 | 60, 97, 81, 100, 106 | lelttrd 10195 |
. . . 4
repr reprΛ Λ Λ _______ |
108 | | tgoldbachgtda.3 |
. . . . 5
_______ Λ vts Λ
vts |
109 | 33, 45, 5 | circlemethhgt 30721 |
. . . . 5
reprΛ Λ Λ Λ vts Λ
vts |
110 | 108, 109 | breqtrrd 4681 |
. . . 4
_______ reprΛ Λ Λ |
111 | 60, 81, 82, 107, 110 | ltletrd 10197 |
. . 3
repr reprΛ Λ Λ reprΛ Λ Λ |
112 | 60, 82 | posdifd 10614 |
. . 3
repr reprΛ Λ Λ reprΛ Λ Λ
reprΛ Λ Λ repr reprΛ Λ Λ |
113 | 111, 112 | mpbid 222 |
. 2
reprΛ Λ Λ repr reprΛ Λ Λ |
114 | | inss2 3834 |
. . . . . . . 8
|
115 | | prmssnn 15390 |
. . . . . . . 8
|
116 | 114, 115 | sstri 3612 |
. . . . . . 7
|
117 | 116 | a1i 11 |
. . . . . 6
|
118 | 9, 18, 7, 117 | reprss 30695 |
. . . . 5
repr repr |
119 | 10, 118 | ssfid 8183 |
. . . 4
repr |
120 | 118 | sselda 3603 |
. . . . 5
repr repr |
121 | 58 | recnd 10068 |
. . . . 5
repr Λ Λ Λ |
122 | 120, 121 | syldan 487 |
. . . 4
repr Λ Λ Λ |
123 | 119, 122 | fsumcl 14464 |
. . 3
reprΛ Λ Λ |
124 | 60 | recnd 10068 |
. . 3
repr reprΛ Λ Λ |
125 | | disjdif 4040 |
. . . . 5
repr repr repr |
126 | 125 | a1i 11 |
. . . 4
repr repr repr |
127 | | undif 4049 |
. . . . . 6
repr repr
repr repr repr repr |
128 | 118, 127 | sylib 208 |
. . . . 5
repr repr repr repr |
129 | 128 | eqcomd 2628 |
. . . 4
repr repr repr repr |
130 | 126, 129,
10, 121 | fsumsplit 14471 |
. . 3
reprΛ Λ Λ
reprΛ Λ Λ repr reprΛ Λ Λ |
131 | 123, 124,
130 | mvrraddd 10445 |
. 2
reprΛ Λ Λ repr reprΛ Λ Λ reprΛ Λ Λ |
132 | 113, 131 | breqtrd 4679 |
1
reprΛ Λ Λ |