Proof of Theorem bgoldbachltOLD
Step | Hyp | Ref
| Expression |
1 | | 4nn 11064 |
. . 3
⊢ 4 ∈
ℕ |
2 | | 10nnOLD 11070 |
. . . 4
⊢ 10 ∈
ℕ |
3 | | 1nn0 11185 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
4 | | 8nn 11068 |
. . . . . 6
⊢ 8 ∈
ℕ |
5 | 3, 4 | decnncl 11394 |
. . . . 5
⊢ ;18 ∈ ℕ |
6 | 5 | nnnn0i 11177 |
. . . 4
⊢ ;18 ∈
ℕ0 |
7 | | nnexpcl 12735 |
. . . 4
⊢ ((10
∈ ℕ ∧ ;18 ∈
ℕ0) → (10↑;18) ∈ ℕ) |
8 | 2, 6, 7 | mp2an 704 |
. . 3
⊢
(10↑;18) ∈
ℕ |
9 | 1, 8 | nnmulcli 10921 |
. 2
⊢ (4
· (10↑;18)) ∈
ℕ |
10 | | id 22 |
. . 3
⊢ ((4
· (10↑;18)) ∈
ℕ → (4 · (10↑;18)) ∈ ℕ) |
11 | | breq2 4587 |
. . . . 5
⊢ (𝑚 = (4 · (10↑;18)) → ((4 · (10↑;18)) ≤ 𝑚 ↔ (4 · (10↑;18)) ≤ (4 · (10↑;18)))) |
12 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑚 = (4 · (10↑;18)) → (𝑛 < 𝑚 ↔ 𝑛 < (4 · (10↑;18)))) |
13 | 12 | anbi2d 736 |
. . . . . . 7
⊢ (𝑚 = (4 · (10↑;18)) → ((4 < 𝑛 ∧ 𝑛 < 𝑚) ↔ (4 < 𝑛 ∧ 𝑛 < (4 · (10↑;18))))) |
14 | 13 | imbi1d 330 |
. . . . . 6
⊢ (𝑚 = (4 · (10↑;18)) → (((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven ) ↔ ((4 < 𝑛 ∧ 𝑛 < (4 · (10↑;18))) → 𝑛 ∈ GoldbachEven ))) |
15 | 14 | ralbidv 2969 |
. . . . 5
⊢ (𝑚 = (4 · (10↑;18)) → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven ) ↔ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < (4 · (10↑;18))) → 𝑛 ∈ GoldbachEven ))) |
16 | 11, 15 | anbi12d 743 |
. . . 4
⊢ (𝑚 = (4 · (10↑;18)) → (((4 ·
(10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven )) ↔ ((4 ·
(10↑;18)) ≤ (4 ·
(10↑;18)) ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < (4 · (10↑;18))) → 𝑛 ∈ GoldbachEven )))) |
17 | 16 | adantl 481 |
. . 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 )))) |
18 | | nnre 10904 |
. . . . 5
⊢ ((4
· (10↑;18)) ∈
ℕ → (4 · (10↑;18)) ∈ ℝ) |
19 | 18 | leidd 10473 |
. . . 4
⊢ ((4
· (10↑;18)) ∈
ℕ → (4 · (10↑;18)) ≤ (4 · (10↑;18))) |
20 | | simplr 788 |
. . . . . . 7
⊢ ((((4
· (10↑;18)) ∈
ℕ ∧ 𝑛 ∈ Even
) ∧ (4 < 𝑛 ∧
𝑛 < (4 ·
(10↑;18)))) → 𝑛 ∈ Even ) |
21 | | simprl 790 |
. . . . . . 7
⊢ ((((4
· (10↑;18)) ∈
ℕ ∧ 𝑛 ∈ Even
) ∧ (4 < 𝑛 ∧
𝑛 < (4 ·
(10↑;18)))) → 4 <
𝑛) |
22 | | evenz 40081 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℤ) |
23 | 22 | zred 11358 |
. . . . . . . . . 10
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℝ) |
24 | | ltle 10005 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℝ ∧ (4
· (10↑;18)) ∈
ℝ) → (𝑛 < (4
· (10↑;18)) →
𝑛 ≤ (4 ·
(10↑;18)))) |
25 | 23, 18, 24 | syl2anr 494 |
. . . . . . . . 9
⊢ (((4
· (10↑;18)) ∈
ℕ ∧ 𝑛 ∈ Even
) → (𝑛 < (4
· (10↑;18)) →
𝑛 ≤ (4 ·
(10↑;18)))) |
26 | 25 | a1d 25 |
. . . . . . . 8
⊢ (((4
· (10↑;18)) ∈
ℕ ∧ 𝑛 ∈ Even
) → (4 < 𝑛 →
(𝑛 < (4 ·
(10↑;18)) → 𝑛 ≤ (4 · (10↑;18))))) |
27 | 26 | imp32 448 |
. . . . . . 7
⊢ ((((4
· (10↑;18)) ∈
ℕ ∧ 𝑛 ∈ Even
) ∧ (4 < 𝑛 ∧
𝑛 < (4 ·
(10↑;18)))) → 𝑛 ≤ (4 · (10↑;18))) |
28 | | ax-bgbltosilvaOLD 40233 |
. . . . . . 7
⊢ ((𝑛 ∈ Even ∧ 4 < 𝑛 ∧ 𝑛 ≤ (4 · (10↑;18))) → 𝑛 ∈ GoldbachEven ) |
29 | 20, 21, 27, 28 | syl3anc 1318 |
. . . . . 6
⊢ ((((4
· (10↑;18)) ∈
ℕ ∧ 𝑛 ∈ Even
) ∧ (4 < 𝑛 ∧
𝑛 < (4 ·
(10↑;18)))) → 𝑛 ∈ GoldbachEven
) |
30 | 29 | ex 449 |
. . . . 5
⊢ (((4
· (10↑;18)) ∈
ℕ ∧ 𝑛 ∈ Even
) → ((4 < 𝑛 ∧
𝑛 < (4 ·
(10↑;18))) → 𝑛 ∈ GoldbachEven
)) |
31 | 30 | ralrimiva 2949 |
. . . 4
⊢ ((4
· (10↑;18)) ∈
ℕ → ∀𝑛
∈ Even ((4 < 𝑛
∧ 𝑛 < (4 ·
(10↑;18))) → 𝑛 ∈ GoldbachEven
)) |
32 | 19, 31 | jca 553 |
. . 3
⊢ ((4
· (10↑;18)) ∈
ℕ → ((4 · (10↑;18)) ≤ (4 · (10↑;18)) ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < (4 · (10↑;18))) → 𝑛 ∈ GoldbachEven ))) |
33 | 10, 17, 32 | rspcedvd 3289 |
. 2
⊢ ((4
· (10↑;18)) ∈
ℕ → ∃𝑚
∈ ℕ ((4 · (10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven ))) |
34 | 9, 33 | ax-mp 5 |
1
⊢
∃𝑚 ∈
ℕ ((4 · (10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven )) |