Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-gbow | Structured version Visualization version Unicode version |
Description: Define the set of weak odd Goldbach numbers, which are positive odd integers that can be expressed as the sum of three primes. By this definition, the weak ternary Goldbach conjecture can be expressed as Odd GoldbachOddW . (Contributed by AV, 14-Jun-2020.) |
Ref | Expression |
---|---|
df-gbow | GoldbachOddW Odd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cgbow 41634 | . 2 GoldbachOddW | |
2 | vz | . . . . . . . 8 | |
3 | 2 | cv 1482 | . . . . . . 7 |
4 | vp | . . . . . . . . . 10 | |
5 | 4 | cv 1482 | . . . . . . . . 9 |
6 | vq | . . . . . . . . . 10 | |
7 | 6 | cv 1482 | . . . . . . . . 9 |
8 | caddc 9939 | . . . . . . . . 9 | |
9 | 5, 7, 8 | co 6650 | . . . . . . . 8 |
10 | vr | . . . . . . . . 9 | |
11 | 10 | cv 1482 | . . . . . . . 8 |
12 | 9, 11, 8 | co 6650 | . . . . . . 7 |
13 | 3, 12 | wceq 1483 | . . . . . 6 |
14 | cprime 15385 | . . . . . 6 | |
15 | 13, 10, 14 | wrex 2913 | . . . . 5 |
16 | 15, 6, 14 | wrex 2913 | . . . 4 |
17 | 16, 4, 14 | wrex 2913 | . . 3 |
18 | codd 41538 | . . 3 Odd | |
19 | 17, 2, 18 | crab 2916 | . 2 Odd |
20 | 1, 19 | wceq 1483 | 1 GoldbachOddW Odd |
Colors of variables: wff setvar class |
This definition is referenced by: isgbow 41640 |
Copyright terms: Public domain | W3C validator |