Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-bgbltosilva | Structured version Visualization version GIF version |
Description: The binary Goldbach conjecture is valid for all even numbers less than or equal to 4x10^18, see section 2 in [OeSilva] p. 2042. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
Ref | Expression |
---|---|
ax-bgbltosilva | ⊢ ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (;10↑;18))) → 𝑁 ∈ GoldbachEven ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cN | . . . 4 class 𝑁 | |
2 | ceven 44630 | . . . 4 class Even | |
3 | 1, 2 | wcel 2114 | . . 3 wff 𝑁 ∈ Even |
4 | c4 11773 | . . . 4 class 4 | |
5 | clt 10753 | . . . 4 class < | |
6 | 4, 1, 5 | wbr 5030 | . . 3 wff 4 < 𝑁 |
7 | c1 10616 | . . . . . . 7 class 1 | |
8 | cc0 10615 | . . . . . . 7 class 0 | |
9 | 7, 8 | cdc 12179 | . . . . . 6 class ;10 |
10 | c8 11777 | . . . . . . 7 class 8 | |
11 | 7, 10 | cdc 12179 | . . . . . 6 class ;18 |
12 | cexp 13521 | . . . . . 6 class ↑ | |
13 | 9, 11, 12 | co 7170 | . . . . 5 class (;10↑;18) |
14 | cmul 10620 | . . . . 5 class · | |
15 | 4, 13, 14 | co 7170 | . . . 4 class (4 · (;10↑;18)) |
16 | cle 10754 | . . . 4 class ≤ | |
17 | 1, 15, 16 | wbr 5030 | . . 3 wff 𝑁 ≤ (4 · (;10↑;18)) |
18 | 3, 6, 17 | w3a 1088 | . 2 wff (𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (;10↑;18))) |
19 | cgbe 44751 | . . 3 class GoldbachEven | |
20 | 1, 19 | wcel 2114 | . 2 wff 𝑁 ∈ GoldbachEven |
21 | 18, 20 | wi 4 | 1 wff ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (;10↑;18))) → 𝑁 ∈ GoldbachEven ) |
Colors of variables: wff setvar class |
This axiom is referenced by: bgoldbachlt 44819 tgblthelfgott 44821 |
Copyright terms: Public domain | W3C validator |