Proof of Theorem bgoldbachlt
Step | Hyp | Ref
| Expression |
1 | | 4nn 11913 |
. . 3
⊢ 4 ∈
ℕ |
2 | | 10nn 12309 |
. . . 4
⊢ ;10 ∈ ℕ |
3 | | 1nn0 12106 |
. . . . 5
⊢ 1 ∈
ℕ0 |
4 | | 8nn0 12113 |
. . . . 5
⊢ 8 ∈
ℕ0 |
5 | 3, 4 | deccl 12308 |
. . . 4
⊢ ;18 ∈
ℕ0 |
6 | | nnexpcl 13648 |
. . . 4
⊢ ((;10 ∈ ℕ ∧ ;18 ∈ ℕ0) →
(;10↑;18) ∈ ℕ) |
7 | 2, 5, 6 | mp2an 692 |
. . 3
⊢ (;10↑;18) ∈ ℕ |
8 | 1, 7 | nnmulcli 11855 |
. 2
⊢ (4
· (;10↑;18)) ∈ ℕ |
9 | | id 22 |
. . 3
⊢ ((4
· (;10↑;18)) ∈ ℕ → (4 ·
(;10↑;18)) ∈ ℕ) |
10 | | breq2 5057 |
. . . . 5
⊢ (𝑚 = (4 · (;10↑;18)) → ((4 · (;10↑;18)) ≤ 𝑚 ↔ (4 · (;10↑;18)) ≤ (4 · (;10↑;18)))) |
11 | | breq2 5057 |
. . . . . . . 8
⊢ (𝑚 = (4 · (;10↑;18)) → (𝑛 < 𝑚 ↔ 𝑛 < (4 · (;10↑;18)))) |
12 | 11 | anbi2d 632 |
. . . . . . 7
⊢ (𝑚 = (4 · (;10↑;18)) → ((4 < 𝑛 ∧ 𝑛 < 𝑚) ↔ (4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18))))) |
13 | 12 | imbi1d 345 |
. . . . . 6
⊢ (𝑚 = (4 · (;10↑;18)) → (((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven ) ↔ ((4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven ))) |
14 | 13 | ralbidv 3118 |
. . . . 5
⊢ (𝑚 = (4 · (;10↑;18)) → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven ) ↔ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven ))) |
15 | 10, 14 | anbi12d 634 |
. . . 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 485 |
. . 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 11837 |
. . . . 5
⊢ ((4
· (;10↑;18)) ∈ ℕ → (4 ·
(;10↑;18)) ∈ ℝ) |
18 | 17 | leidd 11398 |
. . . 4
⊢ ((4
· (;10↑;18)) ∈ ℕ → (4 ·
(;10↑;18)) ≤ (4 · (;10↑;18))) |
19 | | simplr 769 |
. . . . . . 7
⊢ ((((4
· (;10↑;18)) ∈ ℕ ∧ 𝑛 ∈ Even ) ∧ (4 <
𝑛 ∧ 𝑛 < (4 · (;10↑;18)))) → 𝑛 ∈ Even ) |
20 | | simprl 771 |
. . . . . . 7
⊢ ((((4
· (;10↑;18)) ∈ ℕ ∧ 𝑛 ∈ Even ) ∧ (4 <
𝑛 ∧ 𝑛 < (4 · (;10↑;18)))) → 4 < 𝑛) |
21 | | evenz 44755 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℤ) |
22 | 21 | zred 12282 |
. . . . . . . . . 10
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℝ) |
23 | | ltle 10921 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℝ ∧ (4
· (;10↑;18)) ∈ ℝ) → (𝑛 < (4 · (;10↑;18)) → 𝑛 ≤ (4 · (;10↑;18)))) |
24 | 22, 17, 23 | syl2anr 600 |
. . . . . . . . 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 422 |
. . . . . . 7
⊢ ((((4
· (;10↑;18)) ∈ ℕ ∧ 𝑛 ∈ Even ) ∧ (4 <
𝑛 ∧ 𝑛 < (4 · (;10↑;18)))) → 𝑛 ≤ (4 · (;10↑;18))) |
27 | | ax-bgbltosilva 44935 |
. . . . . . 7
⊢ ((𝑛 ∈ Even ∧ 4 < 𝑛 ∧ 𝑛 ≤ (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven ) |
28 | 19, 20, 26, 27 | syl3anc 1373 |
. . . . . 6
⊢ ((((4
· (;10↑;18)) ∈ ℕ ∧ 𝑛 ∈ Even ) ∧ (4 <
𝑛 ∧ 𝑛 < (4 · (;10↑;18)))) → 𝑛 ∈ GoldbachEven ) |
29 | 28 | ex 416 |
. . . . 5
⊢ (((4
· (;10↑;18)) ∈ ℕ ∧ 𝑛 ∈ Even ) → ((4 <
𝑛 ∧ 𝑛 < (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven )) |
30 | 29 | ralrimiva 3105 |
. . . 4
⊢ ((4
· (;10↑;18)) ∈ ℕ →
∀𝑛 ∈ Even ((4
< 𝑛 ∧ 𝑛 < (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven )) |
31 | 18, 30 | jca 515 |
. . 3
⊢ ((4
· (;10↑;18)) ∈ ℕ → ((4 ·
(;10↑;18)) ≤ (4 · (;10↑;18)) ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven ))) |
32 | 9, 16, 31 | rspcedvd 3540 |
. 2
⊢ ((4
· (;10↑;18)) ∈ ℕ → ∃𝑚 ∈ ℕ ((4 ·
(;10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven ))) |
33 | 8, 32 | ax-mp 5 |
1
⊢
∃𝑚 ∈
ℕ ((4 · (;10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven )) |