Proof of Theorem tgoldbachlt
| Step | Hyp | Ref
| Expression |
| 1 | | 8nn0 12549 |
. . . 4
⊢ 8 ∈
ℕ0 |
| 2 | | 8nn 12361 |
. . . 4
⊢ 8 ∈
ℕ |
| 3 | 1, 2 | decnncl 12753 |
. . 3
⊢ ;88 ∈ ℕ |
| 4 | | 10nn 12749 |
. . . 4
⊢ ;10 ∈ ℕ |
| 5 | | 2nn0 12543 |
. . . . 5
⊢ 2 ∈
ℕ0 |
| 6 | | 9nn0 12550 |
. . . . 5
⊢ 9 ∈
ℕ0 |
| 7 | 5, 6 | deccl 12748 |
. . . 4
⊢ ;29 ∈
ℕ0 |
| 8 | | nnexpcl 14115 |
. . . 4
⊢ ((;10 ∈ ℕ ∧ ;29 ∈ ℕ0) →
(;10↑;29) ∈ ℕ) |
| 9 | 4, 7, 8 | mp2an 692 |
. . 3
⊢ (;10↑;29) ∈ ℕ |
| 10 | 3, 9 | nnmulcli 12291 |
. 2
⊢ (;88 · (;10↑;29)) ∈ ℕ |
| 11 | | id 22 |
. . 3
⊢ ((;88 · (;10↑;29)) ∈ ℕ → (;88 · (;10↑;29)) ∈ ℕ) |
| 12 | | breq2 5147 |
. . . . 5
⊢ (𝑚 = (;88 · (;10↑;29)) → ((8 · (;10↑;30)) < 𝑚 ↔ (8 · (;10↑;30)) < (;88 · (;10↑;29)))) |
| 13 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑚 = (;88 · (;10↑;29)) → (𝑛 < 𝑚 ↔ 𝑛 < (;88 · (;10↑;29)))) |
| 14 | 13 | anbi2d 630 |
. . . . . . 7
⊢ (𝑚 = (;88 · (;10↑;29)) → ((7 < 𝑛 ∧ 𝑛 < 𝑚) ↔ (7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))))) |
| 15 | 14 | imbi1d 341 |
. . . . . 6
⊢ (𝑚 = (;88 · (;10↑;29)) → (((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ) ↔ ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ))) |
| 16 | 15 | ralbidv 3178 |
. . . . 5
⊢ (𝑚 = (;88 · (;10↑;29)) → (∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ) ↔ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ))) |
| 17 | 12, 16 | anbi12d 632 |
. . . 4
⊢ (𝑚 = (;88 · (;10↑;29)) → (((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd )) ↔ ((8 ·
(;10↑;30)) < (;88 · (;10↑;29)) ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd )))) |
| 18 | 17 | adantl 481 |
. . 3
⊢ (((;88 · (;10↑;29)) ∈ ℕ ∧ 𝑚 = (;88 · (;10↑;29))) → (((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd )) ↔ ((8 ·
(;10↑;30)) < (;88 · (;10↑;29)) ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd )))) |
| 19 | | simplr 769 |
. . . . . . 7
⊢ ((((;88 · (;10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29)))) → 𝑛 ∈ Odd ) |
| 20 | | simprl 771 |
. . . . . . 7
⊢ ((((;88 · (;10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29)))) → 7 < 𝑛) |
| 21 | | simprr 773 |
. . . . . . 7
⊢ ((((;88 · (;10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29)))) → 𝑛 < (;88 · (;10↑;29))) |
| 22 | | tgblthelfgott 47802 |
. . . . . . 7
⊢ ((𝑛 ∈ Odd ∧ 7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ) |
| 23 | 19, 20, 21, 22 | syl3anc 1373 |
. . . . . 6
⊢ ((((;88 · (;10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29)))) → 𝑛 ∈ GoldbachOdd ) |
| 24 | 23 | ex 412 |
. . . . 5
⊢ (((;88 · (;10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) → ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd )) |
| 25 | 24 | ralrimiva 3146 |
. . . 4
⊢ ((;88 · (;10↑;29)) ∈ ℕ → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd )) |
| 26 | 2, 9 | nnmulcli 12291 |
. . . . . . 7
⊢ (8
· (;10↑;29)) ∈ ℕ |
| 27 | 26 | nngt0i 12305 |
. . . . . 6
⊢ 0 < (8
· (;10↑;29)) |
| 28 | 26 | nnrei 12275 |
. . . . . . 7
⊢ (8
· (;10↑;29)) ∈ ℝ |
| 29 | | 3nn0 12544 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ0 |
| 30 | | 0nn0 12541 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
| 31 | 29, 30 | deccl 12748 |
. . . . . . . . . 10
⊢ ;30 ∈
ℕ0 |
| 32 | | nnexpcl 14115 |
. . . . . . . . . 10
⊢ ((;10 ∈ ℕ ∧ ;30 ∈ ℕ0) →
(;10↑;30) ∈ ℕ) |
| 33 | 4, 31, 32 | mp2an 692 |
. . . . . . . . 9
⊢ (;10↑;30) ∈ ℕ |
| 34 | 2, 33 | nnmulcli 12291 |
. . . . . . . 8
⊢ (8
· (;10↑;30)) ∈ ℕ |
| 35 | 34 | nnrei 12275 |
. . . . . . 7
⊢ (8
· (;10↑;30)) ∈ ℝ |
| 36 | 28, 35 | ltaddposi 11812 |
. . . . . 6
⊢ (0 <
(8 · (;10↑;29)) ↔ (8 · (;10↑;30)) < ((8 · (;10↑;30)) + (8 · (;10↑;29)))) |
| 37 | 27, 36 | mpbi 230 |
. . . . 5
⊢ (8
· (;10↑;30)) < ((8 · (;10↑;30)) + (8 · (;10↑;29))) |
| 38 | | dfdec10 12736 |
. . . . . . 7
⊢ ;88 = ((;10 · 8) + 8) |
| 39 | 38 | oveq1i 7441 |
. . . . . 6
⊢ (;88 · (;10↑;29)) = (((;10 · 8) + 8) · (;10↑;29)) |
| 40 | 4, 2 | nnmulcli 12291 |
. . . . . . . 8
⊢ (;10 · 8) ∈
ℕ |
| 41 | 40 | nncni 12276 |
. . . . . . 7
⊢ (;10 · 8) ∈
ℂ |
| 42 | | 8cn 12363 |
. . . . . . 7
⊢ 8 ∈
ℂ |
| 43 | 9 | nncni 12276 |
. . . . . . 7
⊢ (;10↑;29) ∈ ℂ |
| 44 | 41, 42, 43 | adddiri 11274 |
. . . . . 6
⊢ (((;10 · 8) + 8) · (;10↑;29)) = (((;10 · 8) · (;10↑;29)) + (8 · (;10↑;29))) |
| 45 | 41, 43 | mulcomi 11269 |
. . . . . . . . 9
⊢ ((;10 · 8) · (;10↑;29)) = ((;10↑;29) · (;10 · 8)) |
| 46 | 4 | nncni 12276 |
. . . . . . . . . 10
⊢ ;10 ∈ ℂ |
| 47 | 43, 46, 42 | mulassi 11272 |
. . . . . . . . 9
⊢ (((;10↑;29) · ;10) · 8) = ((;10↑;29) · (;10 · 8)) |
| 48 | | nncn 12274 |
. . . . . . . . . . . . 13
⊢ (;10 ∈ ℕ → ;10 ∈ ℂ) |
| 49 | 7 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (;10 ∈ ℕ → ;29 ∈
ℕ0) |
| 50 | 48, 49 | expp1d 14187 |
. . . . . . . . . . . 12
⊢ (;10 ∈ ℕ → (;10↑(;29 + 1)) = ((;10↑;29) · ;10)) |
| 51 | 4, 50 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (;10↑(;29 + 1)) = ((;10↑;29) · ;10) |
| 52 | 51 | eqcomi 2746 |
. . . . . . . . . 10
⊢ ((;10↑;29) · ;10) = (;10↑(;29 + 1)) |
| 53 | 52 | oveq1i 7441 |
. . . . . . . . 9
⊢ (((;10↑;29) · ;10) · 8) = ((;10↑(;29 + 1)) · 8) |
| 54 | 45, 47, 53 | 3eqtr2i 2771 |
. . . . . . . 8
⊢ ((;10 · 8) · (;10↑;29)) = ((;10↑(;29 + 1)) · 8) |
| 55 | 54 | oveq1i 7441 |
. . . . . . 7
⊢ (((;10 · 8) · (;10↑;29)) + (8 · (;10↑;29))) = (((;10↑(;29 + 1)) · 8) + (8 · (;10↑;29))) |
| 56 | | 2p1e3 12408 |
. . . . . . . . . . 11
⊢ (2 + 1) =
3 |
| 57 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ;29 = ;29 |
| 58 | 5, 56, 57 | decsucc 12774 |
. . . . . . . . . 10
⊢ (;29 + 1) = ;30 |
| 59 | 58 | oveq2i 7442 |
. . . . . . . . 9
⊢ (;10↑(;29 + 1)) = (;10↑;30) |
| 60 | 59 | oveq1i 7441 |
. . . . . . . 8
⊢ ((;10↑(;29 + 1)) · 8) = ((;10↑;30) · 8) |
| 61 | 60 | oveq1i 7441 |
. . . . . . 7
⊢ (((;10↑(;29 + 1)) · 8) + (8 · (;10↑;29))) = (((;10↑;30) · 8) + (8 · (;10↑;29))) |
| 62 | 33 | nncni 12276 |
. . . . . . . 8
⊢ (;10↑;30) ∈ ℂ |
| 63 | | mulcom 11241 |
. . . . . . . . 9
⊢ (((;10↑;30) ∈ ℂ ∧ 8 ∈ ℂ) →
((;10↑;30) · 8) = (8 · (;10↑;30))) |
| 64 | 63 | oveq1d 7446 |
. . . . . . . 8
⊢ (((;10↑;30) ∈ ℂ ∧ 8 ∈ ℂ) →
(((;10↑;30) · 8) + (8 · (;10↑;29))) = ((8 · (;10↑;30)) + (8 · (;10↑;29)))) |
| 65 | 62, 42, 64 | mp2an 692 |
. . . . . . 7
⊢ (((;10↑;30) · 8) + (8 · (;10↑;29))) = ((8 · (;10↑;30)) + (8 · (;10↑;29))) |
| 66 | 55, 61, 65 | 3eqtri 2769 |
. . . . . 6
⊢ (((;10 · 8) · (;10↑;29)) + (8 · (;10↑;29))) = ((8 · (;10↑;30)) + (8 · (;10↑;29))) |
| 67 | 39, 44, 66 | 3eqtri 2769 |
. . . . 5
⊢ (;88 · (;10↑;29)) = ((8 · (;10↑;30)) + (8 · (;10↑;29))) |
| 68 | 37, 67 | breqtrri 5170 |
. . . 4
⊢ (8
· (;10↑;30)) < (;88 · (;10↑;29)) |
| 69 | 25, 68 | jctil 519 |
. . 3
⊢ ((;88 · (;10↑;29)) ∈ ℕ → ((8 · (;10↑;30)) < (;88 · (;10↑;29)) ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ))) |
| 70 | 11, 18, 69 | rspcedvd 3624 |
. 2
⊢ ((;88 · (;10↑;29)) ∈ ℕ → ∃𝑚 ∈ ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ))) |
| 71 | 10, 70 | ax-mp 5 |
1
⊢
∃𝑚 ∈
ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd )) |