Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-bgbltosilvaOLD | Structured version Visualization version Unicode version |
Description: Obsolete version of ax-bgbltosilva 41698 as of 9-Sep-2021. (Contributed by AV, 3-Aug-2020.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-bgbltosilvaOLD | Even ; GoldbachEven |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cN | . . . 4 | |
2 | ceven 41537 | . . . 4 Even | |
3 | 1, 2 | wcel 1990 | . . 3 Even |
4 | c4 11072 | . . . 4 | |
5 | clt 10074 | . . . 4 | |
6 | 4, 1, 5 | wbr 4653 | . . 3 |
7 | c10 11078 | . . . . . 6 | |
8 | c1 9937 | . . . . . . 7 | |
9 | c8 11076 | . . . . . . 7 | |
10 | 8, 9 | cdc 11493 | . . . . . 6 ; |
11 | cexp 12860 | . . . . . 6 | |
12 | 7, 10, 11 | co 6650 | . . . . 5 ; |
13 | cmul 9941 | . . . . 5 | |
14 | 4, 12, 13 | co 6650 | . . . 4 ; |
15 | cle 10075 | . . . 4 | |
16 | 1, 14, 15 | wbr 4653 | . . 3 ; |
17 | 3, 6, 16 | w3a 1037 | . 2 Even ; |
18 | cgbe 41633 | . . 3 GoldbachEven | |
19 | 1, 18 | wcel 1990 | . 2 GoldbachEven |
20 | 17, 19 | wi 4 | 1 Even ; GoldbachEven |
Colors of variables: wff setvar class |
This axiom is referenced by: bgoldbachltOLD 41707 tgblthelfgottOLD 41709 |
Copyright terms: Public domain | W3C validator |