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 result of [OeSilva] p. ?. 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 40075 | . . . 4 class Even | |
3 | 1, 2 | wcel 1977 | . . 3 wff 𝑁 ∈ Even |
4 | c4 10949 | . . . 4 class 4 | |
5 | clt 9953 | . . . 4 class < | |
6 | 4, 1, 5 | wbr 4583 | . . 3 wff 4 < 𝑁 |
7 | c1 9816 | . . . . . . 7 class 1 | |
8 | cc0 9815 | . . . . . . 7 class 0 | |
9 | 7, 8 | cdc 11369 | . . . . . 6 class ;10 |
10 | c8 10953 | . . . . . . 7 class 8 | |
11 | 7, 10 | cdc 11369 | . . . . . 6 class ;18 |
12 | cexp 12722 | . . . . . 6 class ↑ | |
13 | 9, 11, 12 | co 6549 | . . . . 5 class (;10↑;18) |
14 | cmul 9820 | . . . . 5 class · | |
15 | 4, 13, 14 | co 6549 | . . . 4 class (4 · (;10↑;18)) |
16 | cle 9954 | . . . 4 class ≤ | |
17 | 1, 15, 16 | wbr 4583 | . . 3 wff 𝑁 ≤ (4 · (;10↑;18)) |
18 | 3, 6, 17 | w3a 1031 | . 2 wff (𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (;10↑;18))) |
19 | cgbe 40167 | . . 3 class GoldbachEven | |
20 | 1, 19 | wcel 1977 | . 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 40227 tgblthelfgott 40229 |
Copyright terms: Public domain | W3C validator |