Proof of Theorem bgoldbachlt
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 4nn 12350 | . . 3
⊢ 4 ∈
ℕ | 
| 2 |  | 10nn 12751 | . . . 4
⊢ ;10 ∈ ℕ | 
| 3 |  | 1nn0 12544 | . . . . 5
⊢ 1 ∈
ℕ0 | 
| 4 |  | 8nn0 12551 | . . . . 5
⊢ 8 ∈
ℕ0 | 
| 5 | 3, 4 | deccl 12750 | . . . 4
⊢ ;18 ∈
ℕ0 | 
| 6 |  | nnexpcl 14116 | . . . 4
⊢ ((;10 ∈ ℕ ∧ ;18 ∈ ℕ0) →
(;10↑;18) ∈ ℕ) | 
| 7 | 2, 5, 6 | mp2an 692 | . . 3
⊢ (;10↑;18) ∈ ℕ | 
| 8 | 1, 7 | nnmulcli 12292 | . 2
⊢ (4
· (;10↑;18)) ∈ ℕ | 
| 9 |  | id 22 | . . 3
⊢ ((4
· (;10↑;18)) ∈ ℕ → (4 ·
(;10↑;18)) ∈ ℕ) | 
| 10 |  | breq2 5146 | . . . . 5
⊢ (𝑚 = (4 · (;10↑;18)) → ((4 · (;10↑;18)) ≤ 𝑚 ↔ (4 · (;10↑;18)) ≤ (4 · (;10↑;18)))) | 
| 11 |  | breq2 5146 | . . . . . . . 8
⊢ (𝑚 = (4 · (;10↑;18)) → (𝑛 < 𝑚 ↔ 𝑛 < (4 · (;10↑;18)))) | 
| 12 | 11 | anbi2d 630 | . . . . . . 7
⊢ (𝑚 = (4 · (;10↑;18)) → ((4 < 𝑛 ∧ 𝑛 < 𝑚) ↔ (4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18))))) | 
| 13 | 12 | imbi1d 341 | . . . . . 6
⊢ (𝑚 = (4 · (;10↑;18)) → (((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven ) ↔ ((4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven ))) | 
| 14 | 13 | ralbidv 3177 | . . . . 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 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 )))) | 
| 17 |  | nnre 12274 | . . . . 5
⊢ ((4
· (;10↑;18)) ∈ ℕ → (4 ·
(;10↑;18)) ∈ ℝ) | 
| 18 | 17 | leidd 11830 | . . . 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 47622 | . . . . . . . . . . 11
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℤ) | 
| 22 | 21 | zred 12724 | . . . . . . . . . 10
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℝ) | 
| 23 |  | ltle 11350 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℝ ∧ (4
· (;10↑;18)) ∈ ℝ) → (𝑛 < (4 · (;10↑;18)) → 𝑛 ≤ (4 · (;10↑;18)))) | 
| 24 | 22, 17, 23 | syl2anr 597 | . . . . . . . . 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 418 | . . . . . . 7
⊢ ((((4
· (;10↑;18)) ∈ ℕ ∧ 𝑛 ∈ Even ) ∧ (4 <
𝑛 ∧ 𝑛 < (4 · (;10↑;18)))) → 𝑛 ≤ (4 · (;10↑;18))) | 
| 27 |  | ax-bgbltosilva 47802 | . . . . . . 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 412 | . . . . 5
⊢ (((4
· (;10↑;18)) ∈ ℕ ∧ 𝑛 ∈ Even ) → ((4 <
𝑛 ∧ 𝑛 < (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven )) | 
| 30 | 29 | ralrimiva 3145 | . . . 4
⊢ ((4
· (;10↑;18)) ∈ ℕ →
∀𝑛 ∈ Even ((4
< 𝑛 ∧ 𝑛 < (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven )) | 
| 31 | 18, 30 | jca 511 | . . 3
⊢ ((4
· (;10↑;18)) ∈ ℕ → ((4 ·
(;10↑;18)) ≤ (4 · (;10↑;18)) ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < (4 · (;10↑;18))) → 𝑛 ∈ GoldbachEven ))) | 
| 32 | 9, 16, 31 | rspcedvd 3623 | . 2
⊢ ((4
· (;10↑;18)) ∈ ℕ → ∃𝑚 ∈ ℕ ((4 ·
(;10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven ))) | 
| 33 | 8, 32 | ax-mp 5 | 1
⊢
∃𝑚 ∈
ℕ ((4 · (;10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven )) |