Proof of Theorem tgoldbachlt
Step | Hyp | Ref
| Expression |
1 | | 8nn0 11732 |
. . . 4
⊢ 8 ∈
ℕ0 |
2 | | 8nn 11540 |
. . . 4
⊢ 8 ∈
ℕ |
3 | 1, 2 | decnncl 11932 |
. . 3
⊢ ;88 ∈ ℕ |
4 | | 10nn 11927 |
. . . 4
⊢ ;10 ∈ ℕ |
5 | | 2nn0 11726 |
. . . . 5
⊢ 2 ∈
ℕ0 |
6 | | 9nn0 11733 |
. . . . 5
⊢ 9 ∈
ℕ0 |
7 | 5, 6 | deccl 11926 |
. . . 4
⊢ ;29 ∈
ℕ0 |
8 | | nnexpcl 13257 |
. . . 4
⊢ ((;10 ∈ ℕ ∧ ;29 ∈ ℕ0) →
(;10↑;29) ∈ ℕ) |
9 | 4, 7, 8 | mp2an 679 |
. . 3
⊢ (;10↑;29) ∈ ℕ |
10 | 3, 9 | nnmulcli 11465 |
. 2
⊢ (;88 · (;10↑;29)) ∈ ℕ |
11 | | id 22 |
. . 3
⊢ ((;88 · (;10↑;29)) ∈ ℕ → (;88 · (;10↑;29)) ∈ ℕ) |
12 | | breq2 4933 |
. . . . 5
⊢ (𝑚 = (;88 · (;10↑;29)) → ((8 · (;10↑;30)) < 𝑚 ↔ (8 · (;10↑;30)) < (;88 · (;10↑;29)))) |
13 | | breq2 4933 |
. . . . . . . 8
⊢ (𝑚 = (;88 · (;10↑;29)) → (𝑛 < 𝑚 ↔ 𝑛 < (;88 · (;10↑;29)))) |
14 | 13 | anbi2d 619 |
. . . . . . 7
⊢ (𝑚 = (;88 · (;10↑;29)) → ((7 < 𝑛 ∧ 𝑛 < 𝑚) ↔ (7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))))) |
15 | 14 | imbi1d 334 |
. . . . . 6
⊢ (𝑚 = (;88 · (;10↑;29)) → (((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ) ↔ ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ))) |
16 | 15 | ralbidv 3148 |
. . . . 5
⊢ (𝑚 = (;88 · (;10↑;29)) → (∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ) ↔ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ))) |
17 | 12, 16 | anbi12d 621 |
. . . 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 474 |
. . 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 756 |
. . . . . . 7
⊢ ((((;88 · (;10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29)))) → 𝑛 ∈ Odd ) |
20 | | simprl 758 |
. . . . . . 7
⊢ ((((;88 · (;10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29)))) → 7 < 𝑛) |
21 | | simprr 760 |
. . . . . . 7
⊢ ((((;88 · (;10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29)))) → 𝑛 < (;88 · (;10↑;29))) |
22 | | tgblthelfgott 43346 |
. . . . . . 7
⊢ ((𝑛 ∈ Odd ∧ 7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ) |
23 | 19, 20, 21, 22 | syl3anc 1351 |
. . . . . 6
⊢ ((((;88 · (;10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29)))) → 𝑛 ∈ GoldbachOdd ) |
24 | 23 | ex 405 |
. . . . 5
⊢ (((;88 · (;10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) → ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd )) |
25 | 24 | ralrimiva 3133 |
. . . 4
⊢ ((;88 · (;10↑;29)) ∈ ℕ → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd )) |
26 | 2, 9 | nnmulcli 11465 |
. . . . . . 7
⊢ (8
· (;10↑;29)) ∈ ℕ |
27 | 26 | nngt0i 11479 |
. . . . . 6
⊢ 0 < (8
· (;10↑;29)) |
28 | 26 | nnrei 11449 |
. . . . . . 7
⊢ (8
· (;10↑;29)) ∈ ℝ |
29 | | 3nn0 11727 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ0 |
30 | | 0nn0 11724 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
31 | 29, 30 | deccl 11926 |
. . . . . . . . . 10
⊢ ;30 ∈
ℕ0 |
32 | | nnexpcl 13257 |
. . . . . . . . . 10
⊢ ((;10 ∈ ℕ ∧ ;30 ∈ ℕ0) →
(;10↑;30) ∈ ℕ) |
33 | 4, 31, 32 | mp2an 679 |
. . . . . . . . 9
⊢ (;10↑;30) ∈ ℕ |
34 | 2, 33 | nnmulcli 11465 |
. . . . . . . 8
⊢ (8
· (;10↑;30)) ∈ ℕ |
35 | 34 | nnrei 11449 |
. . . . . . 7
⊢ (8
· (;10↑;30)) ∈ ℝ |
36 | 28, 35 | ltaddposi 10990 |
. . . . . 6
⊢ (0 <
(8 · (;10↑;29)) ↔ (8 · (;10↑;30)) < ((8 · (;10↑;30)) + (8 · (;10↑;29)))) |
37 | 27, 36 | mpbi 222 |
. . . . 5
⊢ (8
· (;10↑;30)) < ((8 · (;10↑;30)) + (8 · (;10↑;29))) |
38 | | dfdec10 11914 |
. . . . . . 7
⊢ ;88 = ((;10 · 8) + 8) |
39 | 38 | oveq1i 6986 |
. . . . . 6
⊢ (;88 · (;10↑;29)) = (((;10 · 8) + 8) · (;10↑;29)) |
40 | 4, 2 | nnmulcli 11465 |
. . . . . . . 8
⊢ (;10 · 8) ∈
ℕ |
41 | 40 | nncni 11450 |
. . . . . . 7
⊢ (;10 · 8) ∈
ℂ |
42 | | 8cn 11542 |
. . . . . . 7
⊢ 8 ∈
ℂ |
43 | 9 | nncni 11450 |
. . . . . . 7
⊢ (;10↑;29) ∈ ℂ |
44 | 41, 42, 43 | adddiri 10453 |
. . . . . 6
⊢ (((;10 · 8) + 8) · (;10↑;29)) = (((;10 · 8) · (;10↑;29)) + (8 · (;10↑;29))) |
45 | 41, 43 | mulcomi 10448 |
. . . . . . . . 9
⊢ ((;10 · 8) · (;10↑;29)) = ((;10↑;29) · (;10 · 8)) |
46 | 4 | nncni 11450 |
. . . . . . . . . 10
⊢ ;10 ∈ ℂ |
47 | 43, 46, 42 | mulassi 10451 |
. . . . . . . . 9
⊢ (((;10↑;29) · ;10) · 8) = ((;10↑;29) · (;10 · 8)) |
48 | | nncn 11448 |
. . . . . . . . . . . . 13
⊢ (;10 ∈ ℕ → ;10 ∈ ℂ) |
49 | 7 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (;10 ∈ ℕ → ;29 ∈
ℕ0) |
50 | 48, 49 | expp1d 13326 |
. . . . . . . . . . . 12
⊢ (;10 ∈ ℕ → (;10↑(;29 + 1)) = ((;10↑;29) · ;10)) |
51 | 4, 50 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (;10↑(;29 + 1)) = ((;10↑;29) · ;10) |
52 | 51 | eqcomi 2788 |
. . . . . . . . . 10
⊢ ((;10↑;29) · ;10) = (;10↑(;29 + 1)) |
53 | 52 | oveq1i 6986 |
. . . . . . . . 9
⊢ (((;10↑;29) · ;10) · 8) = ((;10↑(;29 + 1)) · 8) |
54 | 45, 47, 53 | 3eqtr2i 2809 |
. . . . . . . 8
⊢ ((;10 · 8) · (;10↑;29)) = ((;10↑(;29 + 1)) · 8) |
55 | 54 | oveq1i 6986 |
. . . . . . 7
⊢ (((;10 · 8) · (;10↑;29)) + (8 · (;10↑;29))) = (((;10↑(;29 + 1)) · 8) + (8 · (;10↑;29))) |
56 | | 2p1e3 11589 |
. . . . . . . . . . 11
⊢ (2 + 1) =
3 |
57 | | eqid 2779 |
. . . . . . . . . . 11
⊢ ;29 = ;29 |
58 | 5, 56, 57 | decsucc 11953 |
. . . . . . . . . 10
⊢ (;29 + 1) = ;30 |
59 | 58 | oveq2i 6987 |
. . . . . . . . 9
⊢ (;10↑(;29 + 1)) = (;10↑;30) |
60 | 59 | oveq1i 6986 |
. . . . . . . 8
⊢ ((;10↑(;29 + 1)) · 8) = ((;10↑;30) · 8) |
61 | 60 | oveq1i 6986 |
. . . . . . 7
⊢ (((;10↑(;29 + 1)) · 8) + (8 · (;10↑;29))) = (((;10↑;30) · 8) + (8 · (;10↑;29))) |
62 | 33 | nncni 11450 |
. . . . . . . 8
⊢ (;10↑;30) ∈ ℂ |
63 | | mulcom 10421 |
. . . . . . . . 9
⊢ (((;10↑;30) ∈ ℂ ∧ 8 ∈ ℂ) →
((;10↑;30) · 8) = (8 · (;10↑;30))) |
64 | 63 | oveq1d 6991 |
. . . . . . . 8
⊢ (((;10↑;30) ∈ ℂ ∧ 8 ∈ ℂ) →
(((;10↑;30) · 8) + (8 · (;10↑;29))) = ((8 · (;10↑;30)) + (8 · (;10↑;29)))) |
65 | 62, 42, 64 | mp2an 679 |
. . . . . . 7
⊢ (((;10↑;30) · 8) + (8 · (;10↑;29))) = ((8 · (;10↑;30)) + (8 · (;10↑;29))) |
66 | 55, 61, 65 | 3eqtri 2807 |
. . . . . 6
⊢ (((;10 · 8) · (;10↑;29)) + (8 · (;10↑;29))) = ((8 · (;10↑;30)) + (8 · (;10↑;29))) |
67 | 39, 44, 66 | 3eqtri 2807 |
. . . . 5
⊢ (;88 · (;10↑;29)) = ((8 · (;10↑;30)) + (8 · (;10↑;29))) |
68 | 37, 67 | breqtrri 4956 |
. . . 4
⊢ (8
· (;10↑;30)) < (;88 · (;10↑;29)) |
69 | 25, 68 | jctil 512 |
. . 3
⊢ ((;88 · (;10↑;29)) ∈ ℕ → ((8 · (;10↑;30)) < (;88 · (;10↑;29)) ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (;10↑;29))) → 𝑛 ∈ GoldbachOdd ))) |
70 | 11, 18, 69 | rspcedvd 3543 |
. 2
⊢ ((;88 · (;10↑;29)) ∈ ℕ → ∃𝑚 ∈ ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ))) |
71 | 10, 70 | ax-mp 5 |
1
⊢
∃𝑚 ∈
ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd )) |