Step | Hyp | Ref
| Expression |
1 | | 4nn 12243 |
. . 3
โข 4 โ
โ |
2 | | 10nn 12641 |
. . . 4
โข ;10 โ โ |
3 | | 1nn0 12436 |
. . . . 5
โข 1 โ
โ0 |
4 | | 8nn0 12443 |
. . . . 5
โข 8 โ
โ0 |
5 | 3, 4 | deccl 12640 |
. . . 4
โข ;18 โ
โ0 |
6 | | nnexpcl 13987 |
. . . 4
โข ((;10 โ โ โง ;18 โ โ0) โ
(;10โ;18) โ โ) |
7 | 2, 5, 6 | mp2an 691 |
. . 3
โข (;10โ;18) โ โ |
8 | 1, 7 | nnmulcli 12185 |
. 2
โข (4
ยท (;10โ;18)) โ โ |
9 | | id 22 |
. . 3
โข ((4
ยท (;10โ;18)) โ โ โ (4 ยท
(;10โ;18)) โ โ) |
10 | | breq2 5114 |
. . . . 5
โข (๐ = (4 ยท (;10โ;18)) โ ((4 ยท (;10โ;18)) โค ๐ โ (4 ยท (;10โ;18)) โค (4 ยท (;10โ;18)))) |
11 | | breq2 5114 |
. . . . . . . 8
โข (๐ = (4 ยท (;10โ;18)) โ (๐ < ๐ โ ๐ < (4 ยท (;10โ;18)))) |
12 | 11 | anbi2d 630 |
. . . . . . 7
โข (๐ = (4 ยท (;10โ;18)) โ ((4 < ๐ โง ๐ < ๐) โ (4 < ๐ โง ๐ < (4 ยท (;10โ;18))))) |
13 | 12 | imbi1d 342 |
. . . . . 6
โข (๐ = (4 ยท (;10โ;18)) โ (((4 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachEven ) โ ((4 < ๐ โง ๐ < (4 ยท (;10โ;18))) โ ๐ โ GoldbachEven ))) |
14 | 13 | ralbidv 3175 |
. . . . 5
โข (๐ = (4 ยท (;10โ;18)) โ (โ๐ โ Even ((4 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachEven ) โ โ๐ โ Even ((4 < ๐ โง ๐ < (4 ยท (;10โ;18))) โ ๐ โ GoldbachEven ))) |
15 | 10, 14 | anbi12d 632 |
. . . 4
โข (๐ = (4 ยท (;10โ;18)) โ (((4 ยท (;10โ;18)) โค ๐ โง โ๐ โ Even ((4 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachEven )) โ ((4 ยท
(;10โ;18)) โค (4 ยท (;10โ;18)) โง โ๐ โ Even ((4 < ๐ โง ๐ < (4 ยท (;10โ;18))) โ ๐ โ GoldbachEven )))) |
16 | 15 | adantl 483 |
. . 3
โข (((4
ยท (;10โ;18)) โ โ โง ๐ = (4 ยท (;10โ;18))) โ (((4 ยท (;10โ;18)) โค ๐ โง โ๐ โ Even ((4 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachEven )) โ ((4 ยท
(;10โ;18)) โค (4 ยท (;10โ;18)) โง โ๐ โ Even ((4 < ๐ โง ๐ < (4 ยท (;10โ;18))) โ ๐ โ GoldbachEven )))) |
17 | | nnre 12167 |
. . . . 5
โข ((4
ยท (;10โ;18)) โ โ โ (4 ยท
(;10โ;18)) โ โ) |
18 | 17 | leidd 11728 |
. . . 4
โข ((4
ยท (;10โ;18)) โ โ โ (4 ยท
(;10โ;18)) โค (4 ยท (;10โ;18))) |
19 | | simplr 768 |
. . . . . . 7
โข ((((4
ยท (;10โ;18)) โ โ โง ๐ โ Even ) โง (4 <
๐ โง ๐ < (4 ยท (;10โ;18)))) โ ๐ โ Even ) |
20 | | simprl 770 |
. . . . . . 7
โข ((((4
ยท (;10โ;18)) โ โ โง ๐ โ Even ) โง (4 <
๐ โง ๐ < (4 ยท (;10โ;18)))) โ 4 < ๐) |
21 | | evenz 45896 |
. . . . . . . . . . 11
โข (๐ โ Even โ ๐ โ
โค) |
22 | 21 | zred 12614 |
. . . . . . . . . 10
โข (๐ โ Even โ ๐ โ
โ) |
23 | | ltle 11250 |
. . . . . . . . . 10
โข ((๐ โ โ โง (4
ยท (;10โ;18)) โ โ) โ (๐ < (4 ยท (;10โ;18)) โ ๐ โค (4 ยท (;10โ;18)))) |
24 | 22, 17, 23 | syl2anr 598 |
. . . . . . . . 9
โข (((4
ยท (;10โ;18)) โ โ โง ๐ โ Even ) โ (๐ < (4 ยท (;10โ;18)) โ ๐ โค (4 ยท (;10โ;18)))) |
25 | 24 | a1d 25 |
. . . . . . . 8
โข (((4
ยท (;10โ;18)) โ โ โง ๐ โ Even ) โ (4 <
๐ โ (๐ < (4 ยท (;10โ;18)) โ ๐ โค (4 ยท (;10โ;18))))) |
26 | 25 | imp32 420 |
. . . . . . 7
โข ((((4
ยท (;10โ;18)) โ โ โง ๐ โ Even ) โง (4 <
๐ โง ๐ < (4 ยท (;10โ;18)))) โ ๐ โค (4 ยท (;10โ;18))) |
27 | | ax-bgbltosilva 46076 |
. . . . . . 7
โข ((๐ โ Even โง 4 < ๐ โง ๐ โค (4 ยท (;10โ;18))) โ ๐ โ GoldbachEven ) |
28 | 19, 20, 26, 27 | syl3anc 1372 |
. . . . . 6
โข ((((4
ยท (;10โ;18)) โ โ โง ๐ โ Even ) โง (4 <
๐ โง ๐ < (4 ยท (;10โ;18)))) โ ๐ โ GoldbachEven ) |
29 | 28 | ex 414 |
. . . . 5
โข (((4
ยท (;10โ;18)) โ โ โง ๐ โ Even ) โ ((4 <
๐ โง ๐ < (4 ยท (;10โ;18))) โ ๐ โ GoldbachEven )) |
30 | 29 | ralrimiva 3144 |
. . . 4
โข ((4
ยท (;10โ;18)) โ โ โ
โ๐ โ Even ((4
< ๐ โง ๐ < (4 ยท (;10โ;18))) โ ๐ โ GoldbachEven )) |
31 | 18, 30 | jca 513 |
. . 3
โข ((4
ยท (;10โ;18)) โ โ โ ((4 ยท
(;10โ;18)) โค (4 ยท (;10โ;18)) โง โ๐ โ Even ((4 < ๐ โง ๐ < (4 ยท (;10โ;18))) โ ๐ โ GoldbachEven ))) |
32 | 9, 16, 31 | rspcedvd 3586 |
. 2
โข ((4
ยท (;10โ;18)) โ โ โ โ๐ โ โ ((4 ยท
(;10โ;18)) โค ๐ โง โ๐ โ Even ((4 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachEven ))) |
33 | 8, 32 | ax-mp 5 |
1
โข
โ๐ โ
โ ((4 ยท (;10โ;18)) โค ๐ โง โ๐ โ Even ((4 < ๐ โง ๐ < ๐) โ ๐ โ GoldbachEven )) |