Proof of Theorem tgoldbachltOLD
Step | Hyp | Ref
| Expression |
1 | | 8nn0 11315 |
. . . 4
⊢ 8 ∈
ℕ0 |
2 | | 8nn 11191 |
. . . 4
⊢ 8 ∈
ℕ |
3 | 1, 2 | decnncl 11518 |
. . 3
⊢ ;88 ∈ ℕ |
4 | | 10nnOLD 11193 |
. . . 4
⊢ 10 ∈
ℕ |
5 | | 2nn0 11309 |
. . . . 5
⊢ 2 ∈
ℕ0 |
6 | | 9nn0 11316 |
. . . . 5
⊢ 9 ∈
ℕ0 |
7 | 5, 6 | deccl 11512 |
. . . 4
⊢ ;29 ∈
ℕ0 |
8 | | nnexpcl 12873 |
. . . 4
⊢ ((10
∈ ℕ ∧ ;29 ∈
ℕ0) → (10↑;29) ∈ ℕ) |
9 | 4, 7, 8 | mp2an 708 |
. . 3
⊢
(10↑;29) ∈
ℕ |
10 | 3, 9 | nnmulcli 11044 |
. 2
⊢ (;88 · (10↑;29)) ∈ ℕ |
11 | | id 22 |
. . 3
⊢ ((;88 · (10↑;29)) ∈ ℕ → (;88 · (10↑;29)) ∈ ℕ) |
12 | | breq2 4657 |
. . . . 5
⊢ (𝑚 = (;88 · (10↑;29)) → ((8 · (10↑;30)) < 𝑚 ↔ (8 · (10↑;30)) < (;88 · (10↑;29)))) |
13 | | breq2 4657 |
. . . . . . . 8
⊢ (𝑚 = (;88 · (10↑;29)) → (𝑛 < 𝑚 ↔ 𝑛 < (;88 · (10↑;29)))) |
14 | 13 | anbi2d 740 |
. . . . . . 7
⊢ (𝑚 = (;88 · (10↑;29)) → ((7 < 𝑛 ∧ 𝑛 < 𝑚) ↔ (7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))))) |
15 | 14 | imbi1d 331 |
. . . . . 6
⊢ (𝑚 = (;88 · (10↑;29)) → (((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ) ↔ ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOdd ))) |
16 | 15 | ralbidv 2986 |
. . . . 5
⊢ (𝑚 = (;88 · (10↑;29)) → (∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ) ↔ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOdd ))) |
17 | 12, 16 | anbi12d 747 |
. . . 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 482 |
. . 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 792 |
. . . . . . 7
⊢ ((((;88 · (10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29)))) → 𝑛 ∈ Odd ) |
20 | | simprl 794 |
. . . . . . 7
⊢ ((((;88 · (10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29)))) → 7 < 𝑛) |
21 | | simprr 796 |
. . . . . . 7
⊢ ((((;88 · (10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29)))) → 𝑛 < (;88 · (10↑;29))) |
22 | | tgblthelfgottOLD 41709 |
. . . . . . 7
⊢ ((𝑛 ∈ Odd ∧ 7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOdd ) |
23 | 19, 20, 21, 22 | syl3anc 1326 |
. . . . . 6
⊢ ((((;88 · (10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29)))) → 𝑛 ∈ GoldbachOdd ) |
24 | 23 | ex 450 |
. . . . 5
⊢ (((;88 · (10↑;29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) → ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOdd )) |
25 | 24 | ralrimiva 2966 |
. . . 4
⊢ ((;88 · (10↑;29)) ∈ ℕ → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOdd )) |
26 | 2, 9 | nnmulcli 11044 |
. . . . . . 7
⊢ (8
· (10↑;29)) ∈
ℕ |
27 | 26 | nngt0i 11054 |
. . . . . 6
⊢ 0 < (8
· (10↑;29)) |
28 | 26 | nnrei 11029 |
. . . . . . 7
⊢ (8
· (10↑;29)) ∈
ℝ |
29 | | 3nn0 11310 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ0 |
30 | | 0nn0 11307 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
31 | 29, 30 | deccl 11512 |
. . . . . . . . . 10
⊢ ;30 ∈
ℕ0 |
32 | | nnexpcl 12873 |
. . . . . . . . . 10
⊢ ((10
∈ ℕ ∧ ;30 ∈
ℕ0) → (10↑;30) ∈ ℕ) |
33 | 4, 31, 32 | mp2an 708 |
. . . . . . . . 9
⊢
(10↑;30) ∈
ℕ |
34 | 2, 33 | nnmulcli 11044 |
. . . . . . . 8
⊢ (8
· (10↑;30)) ∈
ℕ |
35 | 34 | nnrei 11029 |
. . . . . . 7
⊢ (8
· (10↑;30)) ∈
ℝ |
36 | 28, 35 | ltaddposi 10577 |
. . . . . 6
⊢ (0 <
(8 · (10↑;29)) ↔
(8 · (10↑;30)) <
((8 · (10↑;30)) + (8
· (10↑;29)))) |
37 | 27, 36 | mpbi 220 |
. . . . 5
⊢ (8
· (10↑;30)) < ((8
· (10↑;30)) + (8
· (10↑;29))) |
38 | | dfdecOLD 11495 |
. . . . . . 7
⊢ ;88 = ((10 · 8) +
8) |
39 | 38 | oveq1i 6660 |
. . . . . 6
⊢ (;88 · (10↑;29)) = (((10 · 8) + 8) ·
(10↑;29)) |
40 | 4, 2 | nnmulcli 11044 |
. . . . . . . 8
⊢ (10
· 8) ∈ ℕ |
41 | 40 | nncni 11030 |
. . . . . . 7
⊢ (10
· 8) ∈ ℂ |
42 | | 8cn 11106 |
. . . . . . 7
⊢ 8 ∈
ℂ |
43 | 9 | nncni 11030 |
. . . . . . 7
⊢
(10↑;29) ∈
ℂ |
44 | 41, 42, 43 | adddiri 10051 |
. . . . . 6
⊢ (((10
· 8) + 8) · (10↑;29)) = (((10 · 8) · (10↑;29)) + (8 · (10↑;29))) |
45 | 41, 43 | mulcomi 10046 |
. . . . . . . . 9
⊢ ((10
· 8) · (10↑;29)) = ((10↑;29) · (10 · 8)) |
46 | 4 | nncni 11030 |
. . . . . . . . . 10
⊢ 10 ∈
ℂ |
47 | 43, 46, 42 | mulassi 10049 |
. . . . . . . . 9
⊢
(((10↑;29) ·
10) · 8) = ((10↑;29)
· (10 · 8)) |
48 | | nncn 11028 |
. . . . . . . . . . . . 13
⊢ (10
∈ ℕ → 10 ∈ ℂ) |
49 | 7 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (10
∈ ℕ → ;29 ∈
ℕ0) |
50 | 48, 49 | expp1d 13009 |
. . . . . . . . . . . 12
⊢ (10
∈ ℕ → (10↑(;29 + 1)) = ((10↑;29) · 10)) |
51 | 4, 50 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(10↑(;29 + 1)) =
((10↑;29) ·
10) |
52 | 51 | eqcomi 2631 |
. . . . . . . . . 10
⊢
((10↑;29) · 10)
= (10↑(;29 +
1)) |
53 | 52 | oveq1i 6660 |
. . . . . . . . 9
⊢
(((10↑;29) ·
10) · 8) = ((10↑(;29 +
1)) · 8) |
54 | 45, 47, 53 | 3eqtr2i 2650 |
. . . . . . . 8
⊢ ((10
· 8) · (10↑;29)) = ((10↑(;29 + 1)) · 8) |
55 | 54 | oveq1i 6660 |
. . . . . . 7
⊢ (((10
· 8) · (10↑;29)) + (8 · (10↑;29))) = (((10↑(;29 + 1)) · 8) + (8 · (10↑;29))) |
56 | | 2p1e3 11151 |
. . . . . . . . . . 11
⊢ (2 + 1) =
3 |
57 | | eqid 2622 |
. . . . . . . . . . 11
⊢ ;29 = ;29 |
58 | 5, 56, 57 | decsucc 11550 |
. . . . . . . . . 10
⊢ (;29 + 1) = ;30 |
59 | 58 | oveq2i 6661 |
. . . . . . . . 9
⊢
(10↑(;29 + 1)) =
(10↑;30) |
60 | 59 | oveq1i 6660 |
. . . . . . . 8
⊢
((10↑(;29 + 1))
· 8) = ((10↑;30)
· 8) |
61 | 60 | oveq1i 6660 |
. . . . . . 7
⊢
(((10↑(;29 + 1))
· 8) + (8 · (10↑;29))) = (((10↑;30) · 8) + (8 · (10↑;29))) |
62 | 33 | nncni 11030 |
. . . . . . . 8
⊢
(10↑;30) ∈
ℂ |
63 | | mulcom 10022 |
. . . . . . . . 9
⊢
(((10↑;30) ∈
ℂ ∧ 8 ∈ ℂ) → ((10↑;30) · 8) = (8 · (10↑;30))) |
64 | 63 | oveq1d 6665 |
. . . . . . . 8
⊢
(((10↑;30) ∈
ℂ ∧ 8 ∈ ℂ) → (((10↑;30) · 8) + (8 · (10↑;29))) = ((8 · (10↑;30)) + (8 · (10↑;29)))) |
65 | 62, 42, 64 | mp2an 708 |
. . . . . . 7
⊢
(((10↑;30) · 8)
+ (8 · (10↑;29))) =
((8 · (10↑;30)) + (8
· (10↑;29))) |
66 | 55, 61, 65 | 3eqtri 2648 |
. . . . . 6
⊢ (((10
· 8) · (10↑;29)) + (8 · (10↑;29))) = ((8 · (10↑;30)) + (8 · (10↑;29))) |
67 | 39, 44, 66 | 3eqtri 2648 |
. . . . 5
⊢ (;88 · (10↑;29)) = ((8 · (10↑;30)) + (8 · (10↑;29))) |
68 | 37, 67 | breqtrri 4680 |
. . . 4
⊢ (8
· (10↑;30)) <
(;88 · (10↑;29)) |
69 | 25, 68 | jctil 560 |
. . 3
⊢ ((;88 · (10↑;29)) ∈ ℕ → ((8 ·
(10↑;30)) < (;88 · (10↑;29)) ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOdd ))) |
70 | 11, 18, 69 | rspcedvd 3317 |
. 2
⊢ ((;88 · (10↑;29)) ∈ ℕ → ∃𝑚 ∈ ℕ ((8 · (10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ))) |
71 | 10, 70 | ax-mp 5 |
1
⊢
∃𝑚 ∈
ℕ ((8 · (10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd )) |