Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bgoldbtbnd Structured version   Visualization version   Unicode version

Theorem bgoldbtbnd 38898
 Description: If the binary Goldbach conjecture is valid up to an integer , and there is a series ("ladder") of primes with a difference of at most up to an integer , then the strong ternary Goldbach conjecture is valid up to , see section 1.2.2 in [Helfgott] p. 4 with N = 4 x 10^18, taken from [OeSilva], and M = 8.875 x 10^30. (Contributed by AV, 1-Aug-2020.)
Hypotheses
Ref Expression
bgoldbtbnd.m ;
bgoldbtbnd.n ;
bgoldbtbnd.b Even GoldbachEven
bgoldbtbnd.d
bgoldbtbnd.f RePart
bgoldbtbnd.i ..^
bgoldbtbnd.0
bgoldbtbnd.1 ;
bgoldbtbnd.l
bgoldbtbnd.r
Assertion
Ref Expression
bgoldbtbnd Odd GoldbachOddALTV
Distinct variable groups:   ,   ,   ,,   ,
Allowed substitution hints:   ()   ()   ()   (,)

Proof of Theorem bgoldbtbnd
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprl 763 . . . . 5 Odd Odd
2 bgoldbtbnd.d . . . . . . . . 9
3 eluzge3nn 11197 . . . . . . . . 9
42, 3syl 17 . . . . . . . 8
5 iccelpart 38741 . . . . . . . 8 RePart ..^
64, 5syl 17 . . . . . . 7 RePart ..^
7 bgoldbtbnd.f . . . . . . . . 9 RePart
8 fveq1 5862 . . . . . . . . . . . . 13
9 fveq1 5862 . . . . . . . . . . . . 13
108, 9oveq12d 6306 . . . . . . . . . . . 12
1110eleq2d 2513 . . . . . . . . . . 11
12 fveq1 5862 . . . . . . . . . . . . . 14
13 fveq1 5862 . . . . . . . . . . . . . 14
1412, 13oveq12d 6306 . . . . . . . . . . . . 13
1514eleq2d 2513 . . . . . . . . . . . 12
1615rexbidv 2900 . . . . . . . . . . 11 ..^ ..^
1711, 16imbi12d 322 . . . . . . . . . 10 ..^ ..^
1817rspcv 3145 . . . . . . . . 9 RePart RePart ..^ ..^
197, 18syl 17 . . . . . . . 8 RePart ..^ ..^
20 oddz 38754 . . . . . . . . . . . . . . 15 Odd
2120zred 11037 . . . . . . . . . . . . . 14 Odd
2221rexrd 9687 . . . . . . . . . . . . 13 Odd
2322ad2antrl 733 . . . . . . . . . . . 12 Odd
24 7re 10689 . . . . . . . . . . . . . . . . 17
25 ltle 9719 . . . . . . . . . . . . . . . . 17
2624, 21, 25sylancr 668 . . . . . . . . . . . . . . . 16 Odd
2726com12 32 . . . . . . . . . . . . . . 15 Odd
2827adantr 467 . . . . . . . . . . . . . 14 Odd
2928impcom 432 . . . . . . . . . . . . 13 Odd
3029adantl 468 . . . . . . . . . . . 12 Odd
31 bgoldbtbnd.m . . . . . . . . . . . . . . 15 ;
32 eluzelre 11166 . . . . . . . . . . . . . . . 16 ;
3332rexrd 9687 . . . . . . . . . . . . . . 15 ;
3431, 33syl 17 . . . . . . . . . . . . . 14
3534adantr 467 . . . . . . . . . . . . 13 Odd
36 bgoldbtbnd.r . . . . . . . . . . . . . . 15
3736rexrd 9687 . . . . . . . . . . . . . 14
3837adantr 467 . . . . . . . . . . . . 13 Odd
39 simprrr 774 . . . . . . . . . . . . 13 Odd
40 bgoldbtbnd.l . . . . . . . . . . . . . 14
4140adantr 467 . . . . . . . . . . . . 13 Odd
4223, 35, 38, 39, 41xrlttrd 11453 . . . . . . . . . . . 12 Odd
43 bgoldbtbnd.0 . . . . . . . . . . . . . . . 16
4443oveq1d 6303 . . . . . . . . . . . . . . 15
4544eleq2d 2513 . . . . . . . . . . . . . 14
4645adantr 467 . . . . . . . . . . . . 13 Odd
4724rexri 9690 . . . . . . . . . . . . . 14
48 elico1 11676 . . . . . . . . . . . . . 14
4947, 38, 48sylancr 668 . . . . . . . . . . . . 13 Odd
5046, 49bitrd 257 . . . . . . . . . . . 12 Odd
5123, 30, 42, 50mpbir3and 1190 . . . . . . . . . . 11 Odd
52 fzo0sn0fzo1 11998 . . . . . . . . . . . . . . . . 17 ..^ ..^
5352eleq2d 2513 . . . . . . . . . . . . . . . 16 ..^ ..^
54 elun 3573 . . . . . . . . . . . . . . . 16 ..^ ..^
5553, 54syl6bb 265 . . . . . . . . . . . . . . 15 ..^ ..^
564, 55syl 17 . . . . . . . . . . . . . 14 ..^ ..^
5756adantr 467 . . . . . . . . . . . . 13 Odd ..^ ..^
58 elsn 3981 . . . . . . . . . . . . . . . 16
59 fveq2 5863 . . . . . . . . . . . . . . . . . . . . 21
60 oveq1 6295 . . . . . . . . . . . . . . . . . . . . . . 23
61 0p1e1 10718 . . . . . . . . . . . . . . . . . . . . . . 23
6260, 61syl6eq 2500 . . . . . . . . . . . . . . . . . . . . . 22
6362fveq2d 5867 . . . . . . . . . . . . . . . . . . . . 21
6459, 63oveq12d 6306 . . . . . . . . . . . . . . . . . . . 20
65 bgoldbtbnd.1 . . . . . . . . . . . . . . . . . . . . . 22 ;
6643, 65oveq12d 6306 . . . . . . . . . . . . . . . . . . . . 21 ;
6766adantr 467 . . . . . . . . . . . . . . . . . . . 20 Odd ;
6864, 67sylan9eq 2504 . . . . . . . . . . . . . . . . . . 19 Odd ;
6968eleq2d 2513 . . . . . . . . . . . . . . . . . 18 Odd ;
701adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23 Odd ; Odd
71 simprrl 773 . . . . . . . . . . . . . . . . . . . . . . . 24 Odd
7271adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23 Odd ;
73 simpr 463 . . . . . . . . . . . . . . . . . . . . . . 23 Odd ; ;
74 bgoldbtbndlem1 38894 . . . . . . . . . . . . . . . . . . . . . . 23 Odd ; GoldbachOddALTV
7570, 72, 73, 74syl3anc 1267 . . . . . . . . . . . . . . . . . . . . . 22 Odd ; GoldbachOddALTV
76 isgboa 38848 . . . . . . . . . . . . . . . . . . . . . 22 GoldbachOddALTV Odd Odd Odd Odd
7775, 76sylib 200 . . . . . . . . . . . . . . . . . . . . 21 Odd ; Odd Odd Odd Odd
7877simprd 465 . . . . . . . . . . . . . . . . . . . 20 Odd ; Odd Odd Odd
7978ex 436 . . . . . . . . . . . . . . . . . . 19 Odd ; Odd Odd Odd
8079adantl 468 . . . . . . . . . . . . . . . . . 18 Odd ; Odd Odd Odd
8169, 80sylbid 219 . . . . . . . . . . . . . . . . 17 Odd Odd Odd Odd
8281ex 436 . . . . . . . . . . . . . . . 16 Odd Odd Odd Odd
8358, 82sylbi 199 . . . . . . . . . . . . . . 15 Odd Odd Odd Odd
84 bgoldbtbnd.i . . . . . . . . . . . . . . . . . . 19 ..^
85 fzo0ss1 11945 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
8685sseli 3427 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
87 fveq2 5863 . . . . . . . . . . . . . . . . . . . . . . 23
8887eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . 22
89 oveq1 6295 . . . . . . . . . . . . . . . . . . . . . . . . 25
9089fveq2d 5867 . . . . . . . . . . . . . . . . . . . . . . . 24
9190, 87oveq12d 6306 . . . . . . . . . . . . . . . . . . . . . . 23
9291breq1d 4411 . . . . . . . . . . . . . . . . . . . . . 22
9391breq2d 4413 . . . . . . . . . . . . . . . . . . . . . 22
9488, 92, 933anbi123d 1338 . . . . . . . . . . . . . . . . . . . . 21
9594rspcv 3145 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
9686, 95syl 17 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
9784, 96mpan9 472 . . . . . . . . . . . . . . . . . 18 ..^
98 bgoldbtbnd.n . . . . . . . . . . . . . . . . . . . . . . 23 ;
99 bgoldbtbnd.b . . . . . . . . . . . . . . . . . . . . . . 23 Even GoldbachEven
10031, 98, 99, 2, 7, 84, 43, 65, 40, 36bgoldbtbndlem4 38897 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Odd Odd Odd Odd
101100ad2ant2r 752 . . . . . . . . . . . . . . . . . . . . 21 ..^ Odd Odd Odd Odd
102101expcomd 440 . . . . . . . . . . . . . . . . . . . 20 ..^ Odd Odd Odd Odd
103 simplll 767 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Odd
104 simprl 763 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Odd Odd
105 simpllr 768 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Odd ..^
106 eqid 2450 . . . . . . . . . . . . . . . . . . . . . . . 24
10731, 98, 99, 2, 7, 84, 43, 65, 40, 36, 106bgoldbtbndlem3 38896 . . . . . . . . . . . . . . . . . . . . . . 23 Odd ..^ Even
108103, 104, 105, 107syl3anc 1267 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Odd Even
109 breq2 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
110 breq1 4404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
111109, 110anbi12d 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
112 eleq1 2516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 GoldbachEven GoldbachEven
113111, 112imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 GoldbachEven GoldbachEven
114113cbvralv 3018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Even GoldbachEven Even GoldbachEven
115 breq2 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
116 breq1 4404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
117115, 116anbi12d 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
118 eleq1 2516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 GoldbachEven GoldbachEven
119117, 118imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 GoldbachEven GoldbachEven
120119rspcv 3145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Even Even GoldbachEven GoldbachEven
121114, 120syl5bi 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Even Even GoldbachEven GoldbachEven
122 pm3.35 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 GoldbachEven GoldbachEven
123 isgbe 38846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 GoldbachEven Even Odd Odd
124 eldifi 3554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
1251243ad2ant1 1028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
126125adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ..^
127126ad5antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Even ..^ Odd Odd Odd
128 eleq1 2516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Odd Odd
1291283anbi3d 1344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Odd Odd Odd Odd Odd Odd
130 oveq2 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
131130eqeq2d 2460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
132129, 131anbi12d 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Odd Odd Odd Odd Odd Odd
133132adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Even ..^ Odd Odd Odd Odd Odd Odd Odd Odd Odd
134 oddprmALTV 38810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Odd
1351343ad2ant1 1028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Odd
136135adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ..^ Odd
137136ad4antlr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Even ..^ Odd Odd
138 3simpa 1004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Odd Odd Odd Odd
139137, 138anim12ci 570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Even ..^ Odd Odd Odd Odd Odd Odd
140 df-3an 986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Odd Odd Odd Odd Odd Odd
141139, 140sylibr 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Even ..^ Odd Odd Odd Odd Odd Odd
14220zcnd 11038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Odd
143142ad2antrl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Even ..^ Odd
144 prmz 14619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
145144zcnd 11038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
146124, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
1471463ad2ant1 1028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
148147adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ..^
149148ad2antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Even ..^ Odd
150143, 149npcand 9987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Even ..^ Odd
151150adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Even ..^ Odd
152151ad2antrl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Odd Odd Even ..^ Odd
153 oveq1 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
154152, 153sylan9req 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Odd Odd Even ..^ Odd
155154exp31 608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Odd Odd Even ..^ Odd
156155com23 81 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Odd Odd Even ..^ Odd
1571563impia 1204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Odd Odd Even ..^ Odd
158157impcom 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Even ..^ Odd Odd Odd
159141, 158jca 535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Even ..^ Odd Odd Odd Odd Odd Odd
160127, 133, 159rspcedvd 3154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Even ..^ Odd Odd Odd Odd Odd Odd
161160ex 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Even ..^ Odd Odd Odd Odd Odd Odd
162161reximdva 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Even ..^ Odd Odd Odd Odd Odd Odd
163162reximdva 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Even ..^ Odd Odd Odd Odd Odd Odd
164163exp41 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Even ..^ Odd Odd Odd Odd Odd Odd
165164com25 94 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Even Odd Odd ..^ Odd Odd Odd Odd
166165imp 431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Even Odd Odd ..^ Odd Odd Odd Odd
167123, 166sylbi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 GoldbachEven ..^ Odd Odd Odd Odd
168167a1d 26 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 GoldbachEven Even ..^ Odd Odd Odd Odd
169122, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 GoldbachEven Even ..^ Odd Odd Odd Odd
170169ex 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 GoldbachEven Even ..^ Odd Odd Odd Odd
171170ancoms 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 GoldbachEven Even ..^ Odd Odd Odd Odd
172171com13 83 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Even GoldbachEven ..^ Odd Odd Odd Odd
173121, 172syld 45 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Even Even GoldbachEven ..^ Odd Odd Odd Odd
174173com23 81 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Even Even GoldbachEven ..^ Odd Odd Odd Odd
1751743impib 1205 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Even Even GoldbachEven ..^ Odd Odd Odd Odd
176175com15 96 . . . . . . . . . . . . . . . . . . . . . . . . 25 Even GoldbachEven ..^ Odd Even Odd Odd Odd
17799, 176mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ Odd Even Odd Odd Odd
178177impl 625 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Odd Even Odd Odd Odd
179178imp 431 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Odd Even Odd Odd Odd
180108, 179syld 45 . . . . . . . . . . . . . . . . . . . . 21 ..^ Odd Odd Odd Odd
181180expcomd 440 . . . . . . . . . . . . . . . . . . . 20 ..^ Odd Odd Odd Odd
18221ad2antrl 733 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Odd
183144zred 11037 . . . . . . . . . . . . . . . . . . . . . . . . 25
184124, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
1851843ad2ant1 1028 . . . . . . . . . . . . . . . . . . . . . . 23
186185ad2antlr 732 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Odd
187182, 186resubcld 10044 . . . . . . . . . . . . . . . . . . . . 21 ..^ Odd
188 4re 10683 . . . . . . . . . . . . . . . . . . . . 21
189 lelttric 9738 . . . . . . . . . . . . . . . . . . . . 21
190187, 188, 189sylancl 667 . . . . . . . . . . . . . . . . . . . 20 ..^ Odd
191102, 181, 190mpjaod 383 . . . . . . . . . . . . . . . . . . 19 ..^ Odd Odd Odd Odd
192191ex 436 . . . . . . . . . . . . . . . . . 18 ..^ Odd Odd Odd Odd
19397, 192mpdan 673 . . . . . . . . . . . . . . . . 17 ..^ Odd Odd Odd Odd
194193expcom 437 . . . . . . . . . . . . . . . 16 ..^ Odd Odd Odd Odd
195194impd 433 . . . . . . . . . . . . . . 15 ..^ Odd Odd Odd Odd
19683, 195jaoi 381 . . . . . . . . . . . . . 14 ..^ Odd Odd Odd Odd
197196com12 32 . . . . . . . . . . . . 13 Odd ..^ Odd Odd Odd
19857, 197sylbid 219 . . . . . . . . . . . 12 Odd ..^ Odd Odd Odd
199198rexlimdv 2876 . . . . . . . . . . 11 Odd ..^ Odd Odd Odd
20051, 199embantd 56 . . . . . . . . . 10 Odd ..^ Odd Odd Odd
201200ex 436 . . . . . . . . 9 Odd ..^ Odd Odd Odd
202201com23 81 . . . . . . . 8 ..^ Odd Odd Odd Odd
20319, 202syld 45 . . . . . . 7 RePart ..^ Odd Odd Odd Odd
2046, 203mpd 15 . . . . . 6 Odd Odd Odd Odd
205204imp 431 . . . . 5 Odd Odd Odd Odd
2061, 205jca 535 . . . 4 Odd Odd Odd Odd Odd
207206, 76sylibr 216 . . 3 Odd GoldbachOddALTV
208207exp32 609 . 2 Odd GoldbachOddALTV
209208ralrimiv 2799 1 Odd GoldbachOddALTV
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wo 370   wa 371   w3a 984   wceq 1443   wcel 1886  wral 2736  wrex 2737   cdif 3400   cun 3401  csn 3967   class class class wbr 4401  cfv 5581  (class class class)co 6288  cc 9534  cr 9535  cc0 9536  c1 9537   caddc 9539  cxr 9671   clt 9672   cle 9673   cmin 9857  cn 10606  c2 10656  c3 10657  c4 10658  c7 10661  ;cdc 11048  cuz 11156  cico 11634  ..^cfzo 11912  cprime 14615  RePartciccp 38721   Even ceven 38747   Odd codd 38748   GoldbachEven cgbe 38840   GoldbachOddALTV cgboa 38842 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-fal 1449  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-2o 7180  df-oadd 7183  df-er 7360  df-map 7471  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-sup 7953  df-inf 7954  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-4 10667  df-5 10668  df-6 10669  df-7 10670  df-8 10671  df-9 10672  df-10 10673  df-n0 10867  df-z 10935  df-dec 11049  df-uz 11157  df-rp 11300  df-ico 11638  df-fz 11782  df-fzo 11913  df-seq 12211  df-exp 12270  df-cj 13155  df-re 13156  df-im 13157  df-sqrt 13291  df-abs 13292  df-dvds 14299  df-prm 14616  df-iccp 38722  df-even 38749  df-odd 38750  df-gbe 38843  df-gboa 38845 This theorem is referenced by:  tgblthelfgott  38902
 Copyright terms: Public domain W3C validator