Step | Hyp | Ref
| Expression |
1 | | ax-hgprmladderOLD 40235 |
. 2
⊢
∃𝑑 ∈
(ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) |
2 | | 1nn0 11185 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 |
3 | | 1nn 10908 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
4 | 2, 3 | decnncl 11394 |
. . . . . . . . . . 11
⊢ ;11 ∈ ℕ |
5 | 4 | nnzi 11278 |
. . . . . . . . . 10
⊢ ;11 ∈ ℤ |
6 | | 8nn0 11192 |
. . . . . . . . . . . . 13
⊢ 8 ∈
ℕ0 |
7 | | 8nn 11068 |
. . . . . . . . . . . . 13
⊢ 8 ∈
ℕ |
8 | 6, 7 | decnncl 11394 |
. . . . . . . . . . . 12
⊢ ;88 ∈ ℕ |
9 | | 10nnOLD 11070 |
. . . . . . . . . . . . 13
⊢ 10 ∈
ℕ |
10 | | 2nn0 11186 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ0 |
11 | | 9nn 11069 |
. . . . . . . . . . . . . . 15
⊢ 9 ∈
ℕ |
12 | 10, 11 | decnncl 11394 |
. . . . . . . . . . . . . 14
⊢ ;29 ∈ ℕ |
13 | 12 | nnnn0i 11177 |
. . . . . . . . . . . . 13
⊢ ;29 ∈
ℕ0 |
14 | | nnexpcl 12735 |
. . . . . . . . . . . . 13
⊢ ((10
∈ ℕ ∧ ;29 ∈
ℕ0) → (10↑;29) ∈ ℕ) |
15 | 9, 13, 14 | mp2an 704 |
. . . . . . . . . . . 12
⊢
(10↑;29) ∈
ℕ |
16 | 8, 15 | nnmulcli 10921 |
. . . . . . . . . . 11
⊢ (;88 · (10↑;29)) ∈ ℕ |
17 | 16 | nnzi 11278 |
. . . . . . . . . 10
⊢ (;88 · (10↑;29)) ∈ ℤ |
18 | | 1re 9918 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
19 | 8 | nnrei 10906 |
. . . . . . . . . . . . 13
⊢ ;88 ∈ ℝ |
20 | 18, 19 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℝ ∧ ;88 ∈
ℝ) |
21 | | 0le1 10430 |
. . . . . . . . . . . . 13
⊢ 0 ≤
1 |
22 | | 1lt10OLD 11115 |
. . . . . . . . . . . . . 14
⊢ 1 <
10 |
23 | 7, 6, 2, 22 | decltiOLD 11424 |
. . . . . . . . . . . . 13
⊢ 1 <
;88 |
24 | 21, 23 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (0 ≤ 1
∧ 1 < ;88) |
25 | | nnexpcl 12735 |
. . . . . . . . . . . . . . 15
⊢ ((10
∈ ℕ ∧ 1 ∈ ℕ0) → (10↑1) ∈
ℕ) |
26 | 9, 2, 25 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢
(10↑1) ∈ ℕ |
27 | 26 | nnrei 10906 |
. . . . . . . . . . . . 13
⊢
(10↑1) ∈ ℝ |
28 | 15 | nnrei 10906 |
. . . . . . . . . . . . 13
⊢
(10↑;29) ∈
ℝ |
29 | 27, 28 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢
((10↑1) ∈ ℝ ∧ (10↑;29) ∈ ℝ) |
30 | | 0re 9919 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
31 | | 10reOLD 10986 |
. . . . . . . . . . . . . . 15
⊢ 10 ∈
ℝ |
32 | | 10posOLD 11000 |
. . . . . . . . . . . . . . 15
⊢ 0 <
10 |
33 | 30, 31, 32 | ltleii 10039 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
10 |
34 | 9 | nncni 10907 |
. . . . . . . . . . . . . . 15
⊢ 10 ∈
ℂ |
35 | | exp1 12728 |
. . . . . . . . . . . . . . 15
⊢ (10
∈ ℂ → (10↑1) = 10) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(10↑1) = 10 |
37 | 33, 36 | breqtrri 4610 |
. . . . . . . . . . . . 13
⊢ 0 ≤
(10↑1) |
38 | | 1z 11284 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℤ |
39 | 12 | nnzi 11278 |
. . . . . . . . . . . . . . 15
⊢ ;29 ∈ ℤ |
40 | 31, 38, 39 | 3pm3.2i 1232 |
. . . . . . . . . . . . . 14
⊢ (10
∈ ℝ ∧ 1 ∈ ℤ ∧ ;29 ∈ ℤ) |
41 | | 2nn 11062 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ |
42 | | 9nn0 11193 |
. . . . . . . . . . . . . . . 16
⊢ 9 ∈
ℕ0 |
43 | 41, 42, 2, 22 | decltiOLD 11424 |
. . . . . . . . . . . . . . 15
⊢ 1 <
;29 |
44 | 22, 43 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (1 <
10 ∧ 1 < ;29) |
45 | | ltexp2a 12774 |
. . . . . . . . . . . . . 14
⊢ (((10
∈ ℝ ∧ 1 ∈ ℤ ∧ ;29 ∈ ℤ) ∧ (1 < 10 ∧ 1 <
;29)) → (10↑1) <
(10↑;29)) |
46 | 40, 44, 45 | mp2an 704 |
. . . . . . . . . . . . 13
⊢
(10↑1) < (10↑;29) |
47 | 37, 46 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (0 ≤
(10↑1) ∧ (10↑1) < (10↑;29)) |
48 | | ltmul12a 10758 |
. . . . . . . . . . . 12
⊢ ((((1
∈ ℝ ∧ ;88 ∈
ℝ) ∧ (0 ≤ 1 ∧ 1 < ;88)) ∧ (((10↑1) ∈ ℝ ∧
(10↑;29) ∈ ℝ)
∧ (0 ≤ (10↑1) ∧ (10↑1) < (10↑;29)))) → (1 · (10↑1)) < (;88 · (10↑;29))) |
49 | 20, 24, 29, 47, 48 | mp4an 705 |
. . . . . . . . . . 11
⊢ (1
· (10↑1)) < (;88
· (10↑;29)) |
50 | 26 | nnzi 11278 |
. . . . . . . . . . . . . 14
⊢
(10↑1) ∈ ℤ |
51 | | zmulcl 11303 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ (10↑1) ∈ ℤ) → (1 ·
(10↑1)) ∈ ℤ) |
52 | 38, 50, 51 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (1
· (10↑1)) ∈ ℤ |
53 | | zltp1le 11304 |
. . . . . . . . . . . . 13
⊢ (((1
· (10↑1)) ∈ ℤ ∧ (;88 · (10↑;29)) ∈ ℤ) → ((1 ·
(10↑1)) < (;88 ·
(10↑;29)) ↔ ((1 ·
(10↑1)) + 1) ≤ (;88
· (10↑;29)))) |
54 | 52, 17, 53 | mp2an 704 |
. . . . . . . . . . . 12
⊢ ((1
· (10↑1)) < (;88
· (10↑;29)) ↔ ((1
· (10↑1)) + 1) ≤ (;88 · (10↑;29))) |
55 | | 1t10e1p1e11OLD 39938 |
. . . . . . . . . . . . . 14
⊢ ;11 = ((1 · (10↑1)) +
1) |
56 | 55 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢ ((1
· (10↑1)) + 1) = ;11 |
57 | 56 | breq1i 4590 |
. . . . . . . . . . . 12
⊢ (((1
· (10↑1)) + 1) ≤ (;88 · (10↑;29)) ↔ ;11 ≤ (;88 · (10↑;29))) |
58 | 54, 57 | bitri 263 |
. . . . . . . . . . 11
⊢ ((1
· (10↑1)) < (;88
· (10↑;29)) ↔
;11 ≤ (;88 · (10↑;29))) |
59 | 49, 58 | mpbi 219 |
. . . . . . . . . 10
⊢ ;11 ≤ (;88 · (10↑;29)) |
60 | | eluz2 11569 |
. . . . . . . . . 10
⊢ ((;88 · (10↑;29)) ∈ (ℤ≥‘;11) ↔ (;11 ∈ ℤ ∧ (;88 · (10↑;29)) ∈ ℤ ∧ ;11 ≤ (;88 · (10↑;29)))) |
61 | 5, 17, 59, 60 | mpbir3an 1237 |
. . . . . . . . 9
⊢ (;88 · (10↑;29)) ∈ (ℤ≥‘;11) |
62 | 61 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29)))) → (;88 · (10↑;29)) ∈ (ℤ≥‘;11)) |
63 | | 4nn 11064 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℕ |
64 | 2, 7 | decnncl 11394 |
. . . . . . . . . . . . . 14
⊢ ;18 ∈ ℕ |
65 | 64 | nnnn0i 11177 |
. . . . . . . . . . . . 13
⊢ ;18 ∈
ℕ0 |
66 | | nnexpcl 12735 |
. . . . . . . . . . . . 13
⊢ ((10
∈ ℕ ∧ ;18 ∈
ℕ0) → (10↑;18) ∈ ℕ) |
67 | 9, 65, 66 | mp2an 704 |
. . . . . . . . . . . 12
⊢
(10↑;18) ∈
ℕ |
68 | 63, 67 | nnmulcli 10921 |
. . . . . . . . . . 11
⊢ (4
· (10↑;18)) ∈
ℕ |
69 | 68 | nnzi 11278 |
. . . . . . . . . 10
⊢ (4
· (10↑;18)) ∈
ℤ |
70 | | 4re 10974 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℝ |
71 | 18, 70 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℝ ∧ 4 ∈ ℝ) |
72 | | 1lt4 11076 |
. . . . . . . . . . . . 13
⊢ 1 <
4 |
73 | 21, 72 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (0 ≤ 1
∧ 1 < 4) |
74 | 67 | nnrei 10906 |
. . . . . . . . . . . . 13
⊢
(10↑;18) ∈
ℝ |
75 | 27, 74 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢
((10↑1) ∈ ℝ ∧ (10↑;18) ∈ ℝ) |
76 | 64 | nnzi 11278 |
. . . . . . . . . . . . . . 15
⊢ ;18 ∈ ℤ |
77 | 31, 38, 76 | 3pm3.2i 1232 |
. . . . . . . . . . . . . 14
⊢ (10
∈ ℝ ∧ 1 ∈ ℤ ∧ ;18 ∈ ℤ) |
78 | 3, 6, 2, 22 | decltiOLD 11424 |
. . . . . . . . . . . . . . 15
⊢ 1 <
;18 |
79 | 22, 78 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (1 <
10 ∧ 1 < ;18) |
80 | | ltexp2a 12774 |
. . . . . . . . . . . . . 14
⊢ (((10
∈ ℝ ∧ 1 ∈ ℤ ∧ ;18 ∈ ℤ) ∧ (1 < 10 ∧ 1 <
;18)) → (10↑1) <
(10↑;18)) |
81 | 77, 79, 80 | mp2an 704 |
. . . . . . . . . . . . 13
⊢
(10↑1) < (10↑;18) |
82 | 37, 81 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (0 ≤
(10↑1) ∧ (10↑1) < (10↑;18)) |
83 | | ltmul12a 10758 |
. . . . . . . . . . . 12
⊢ ((((1
∈ ℝ ∧ 4 ∈ ℝ) ∧ (0 ≤ 1 ∧ 1 < 4)) ∧
(((10↑1) ∈ ℝ ∧ (10↑;18) ∈ ℝ) ∧ (0 ≤ (10↑1) ∧
(10↑1) < (10↑;18))))
→ (1 · (10↑1)) < (4 · (10↑;18))) |
84 | 71, 73, 75, 82, 83 | mp4an 705 |
. . . . . . . . . . 11
⊢ (1
· (10↑1)) < (4 · (10↑;18)) |
85 | | 4z 11288 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℤ |
86 | 67 | nnzi 11278 |
. . . . . . . . . . . . . 14
⊢
(10↑;18) ∈
ℤ |
87 | | zmulcl 11303 |
. . . . . . . . . . . . . 14
⊢ ((4
∈ ℤ ∧ (10↑;18)
∈ ℤ) → (4 · (10↑;18)) ∈ ℤ) |
88 | 85, 86, 87 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (4
· (10↑;18)) ∈
ℤ |
89 | | zltp1le 11304 |
. . . . . . . . . . . . 13
⊢ (((1
· (10↑1)) ∈ ℤ ∧ (4 · (10↑;18)) ∈ ℤ) → ((1
· (10↑1)) < (4 · (10↑;18)) ↔ ((1 · (10↑1)) + 1) ≤ (4
· (10↑;18)))) |
90 | 52, 88, 89 | mp2an 704 |
. . . . . . . . . . . 12
⊢ ((1
· (10↑1)) < (4 · (10↑;18)) ↔ ((1 · (10↑1)) + 1) ≤ (4
· (10↑;18))) |
91 | 56 | breq1i 4590 |
. . . . . . . . . . . 12
⊢ (((1
· (10↑1)) + 1) ≤ (4 · (10↑;18)) ↔ ;11 ≤ (4 · (10↑;18))) |
92 | 90, 91 | bitri 263 |
. . . . . . . . . . 11
⊢ ((1
· (10↑1)) < (4 · (10↑;18)) ↔ ;11 ≤ (4 · (10↑;18))) |
93 | 84, 92 | mpbi 219 |
. . . . . . . . . 10
⊢ ;11 ≤ (4 · (10↑;18)) |
94 | | eluz2 11569 |
. . . . . . . . . 10
⊢ ((4
· (10↑;18)) ∈
(ℤ≥‘;11)
↔ (;11 ∈ ℤ ∧
(4 · (10↑;18)) ∈
ℤ ∧ ;11 ≤ (4 ·
(10↑;18)))) |
95 | 5, 69, 93, 94 | mpbir3an 1237 |
. . . . . . . . 9
⊢ (4
· (10↑;18)) ∈
(ℤ≥‘;11) |
96 | 95 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29)))) → (4 · (10↑;18)) ∈
(ℤ≥‘;11)) |
97 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ Even ∧ (4 < 𝑛 ∧ 𝑛 < (4 · (10↑;18)))) → 𝑛 ∈ Even ) |
98 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ Even ∧ (4 < 𝑛 ∧ 𝑛 < (4 · (10↑;18)))) → 4 < 𝑛) |
99 | | evenz 40081 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℤ) |
100 | 99 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ Even → 𝑛 ∈
ℝ) |
101 | 68 | nnrei 10906 |
. . . . . . . . . . . . . . 15
⊢ (4
· (10↑;18)) ∈
ℝ |
102 | | ltle 10005 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℝ ∧ (4
· (10↑;18)) ∈
ℝ) → (𝑛 < (4
· (10↑;18)) →
𝑛 ≤ (4 ·
(10↑;18)))) |
103 | 100, 101,
102 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ Even → (𝑛 < (4 · (10↑;18)) → 𝑛 ≤ (4 · (10↑;18)))) |
104 | 103 | a1d 25 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ Even → (4 <
𝑛 → (𝑛 < (4 · (10↑;18)) → 𝑛 ≤ (4 · (10↑;18))))) |
105 | 104 | imp32 448 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ Even ∧ (4 < 𝑛 ∧ 𝑛 < (4 · (10↑;18)))) → 𝑛 ≤ (4 · (10↑;18))) |
106 | | ax-bgbltosilvaOLD 40233 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ Even ∧ 4 < 𝑛 ∧ 𝑛 ≤ (4 · (10↑;18))) → 𝑛 ∈ GoldbachEven ) |
107 | 97, 98, 105, 106 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ Even ∧ (4 < 𝑛 ∧ 𝑛 < (4 · (10↑;18)))) → 𝑛 ∈ GoldbachEven ) |
108 | 107 | ex 449 |
. . . . . . . . . 10
⊢ (𝑛 ∈ Even → ((4 <
𝑛 ∧ 𝑛 < (4 · (10↑;18))) → 𝑛 ∈ GoldbachEven )) |
109 | 108 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29)))) → (𝑛 ∈ Even → ((4 < 𝑛 ∧ 𝑛 < (4 · (10↑;18))) → 𝑛 ∈ GoldbachEven ))) |
110 | 109 | ralrimiv 2948 |
. . . . . . . 8
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29)))) → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < (4 · (10↑;18))) → 𝑛 ∈ GoldbachEven )) |
111 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) → 𝑑 ∈
(ℤ≥‘3)) |
112 | 111 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29)))) → 𝑑 ∈
(ℤ≥‘3)) |
113 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) → 𝑓 ∈ (RePart‘𝑑)) |
114 | 113 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29)))) → 𝑓 ∈ (RePart‘𝑑)) |
115 | | simpr 476 |
. . . . . . . . 9
⊢ ((((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) |
116 | 115 | ad2antlr 759 |
. . . . . . . 8
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29)))) → ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) |
117 | | simpl1 1057 |
. . . . . . . . 9
⊢ ((((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → (𝑓‘0) = 7) |
118 | 117 | ad2antlr 759 |
. . . . . . . 8
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29)))) → (𝑓‘0) = 7) |
119 | | simpl2 1058 |
. . . . . . . . 9
⊢ ((((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → (𝑓‘1) = ;13) |
120 | 119 | ad2antlr 759 |
. . . . . . . 8
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29)))) → (𝑓‘1) = ;13) |
121 | 6, 11 | decnncl 11394 |
. . . . . . . . . . . . . . 15
⊢ ;89 ∈ ℕ |
122 | 121 | nnrei 10906 |
. . . . . . . . . . . . . 14
⊢ ;89 ∈ ℝ |
123 | 15 | nngt0i 10931 |
. . . . . . . . . . . . . . 15
⊢ 0 <
(10↑;29) |
124 | 28, 123 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢
((10↑;29) ∈
ℝ ∧ 0 < (10↑;29)) |
125 | 19, 122, 124 | 3pm3.2i 1232 |
. . . . . . . . . . . . 13
⊢ (;88 ∈ ℝ ∧ ;89 ∈ ℝ ∧ ((10↑;29) ∈ ℝ ∧ 0 <
(10↑;29))) |
126 | | 8lt9 11099 |
. . . . . . . . . . . . . 14
⊢ 8 <
9 |
127 | 6, 6, 11, 126 | declt 11406 |
. . . . . . . . . . . . 13
⊢ ;88 < ;89 |
128 | | ltmul1a 10751 |
. . . . . . . . . . . . 13
⊢ (((;88 ∈ ℝ ∧ ;89 ∈ ℝ ∧ ((10↑;29) ∈ ℝ ∧ 0 <
(10↑;29))) ∧ ;88 < ;89) → (;88 · (10↑;29)) < (;89 · (10↑;29))) |
129 | 125, 127,
128 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (;88 · (10↑;29)) < (;89 · (10↑;29)) |
130 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑑) = (;89 · (10↑;29)) → ((;88 · (10↑;29)) < (𝑓‘𝑑) ↔ (;88 · (10↑;29)) < (;89 · (10↑;29)))) |
131 | 129, 130 | mpbiri 247 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑑) = (;89 · (10↑;29)) → (;88 · (10↑;29)) < (𝑓‘𝑑)) |
132 | 131 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) → (;88 · (10↑;29)) < (𝑓‘𝑑)) |
133 | 132 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → (;88 · (10↑;29)) < (𝑓‘𝑑)) |
134 | 133 | ad2antlr 759 |
. . . . . . . 8
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29)))) → (;88 · (10↑;29)) < (𝑓‘𝑑)) |
135 | 121, 15 | nnmulcli 10921 |
. . . . . . . . . . . . 13
⊢ (;89 · (10↑;29)) ∈ ℕ |
136 | 135 | nnrei 10906 |
. . . . . . . . . . . 12
⊢ (;89 · (10↑;29)) ∈ ℝ |
137 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑑) = (;89 · (10↑;29)) → ((𝑓‘𝑑) ∈ ℝ ↔ (;89 · (10↑;29)) ∈ ℝ)) |
138 | 136, 137 | mpbiri 247 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑑) = (;89 · (10↑;29)) → (𝑓‘𝑑) ∈ ℝ) |
139 | 138 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) → (𝑓‘𝑑) ∈ ℝ) |
140 | 139 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → (𝑓‘𝑑) ∈ ℝ) |
141 | 140 | ad2antlr 759 |
. . . . . . . 8
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29)))) → (𝑓‘𝑑) ∈ ℝ) |
142 | 62, 96, 110, 112, 114, 116, 118, 120, 134, 141 | bgoldbtbnd 40225 |
. . . . . . 7
⊢ ((((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) ∧ (((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) ∧ (𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29)))) → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOddALTV )) |
143 | 142 | exp31 628 |
. . . . . 6
⊢ ((𝑑 ∈
(ℤ≥‘3) ∧ 𝑓 ∈ (RePart‘𝑑)) → ((((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29))) → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOddALTV )))) |
144 | 143 | rexlimdva 3013 |
. . . . 5
⊢ (𝑑 ∈
(ℤ≥‘3) → (∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29))) → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOddALTV )))) |
145 | 144 | imp 444 |
. . . 4
⊢ ((𝑑 ∈
(ℤ≥‘3) ∧ ∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))) → ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29))) → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOddALTV ))) |
146 | 145 | rexlimiva 3010 |
. . 3
⊢
(∃𝑑 ∈
(ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29))) → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOddALTV ))) |
147 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (7 < 𝑛 ↔ 7 < 𝑁)) |
148 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝑛 < (;88 · (10↑;29)) ↔ 𝑁 < (;88 · (10↑;29)))) |
149 | 147, 148 | anbi12d 743 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) ↔ (7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29))))) |
150 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑛 ∈ GoldbachOddALTV ↔ 𝑁 ∈ GoldbachOddALTV
)) |
151 | 149, 150 | imbi12d 333 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOddALTV ) ↔ ((7 <
𝑁 ∧ 𝑁 < (;88 · (10↑;29))) → 𝑁 ∈ GoldbachOddALTV ))) |
152 | 151 | rspcv 3278 |
. . . . 5
⊢ (𝑁 ∈ Odd →
(∀𝑛 ∈ Odd ((7
< 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOddALTV ) → ((7 <
𝑁 ∧ 𝑁 < (;88 · (10↑;29))) → 𝑁 ∈ GoldbachOddALTV ))) |
153 | 152 | com23 84 |
. . . 4
⊢ (𝑁 ∈ Odd → ((7 <
𝑁 ∧ 𝑁 < (;88 · (10↑;29))) → (∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOddALTV ) → 𝑁 ∈ GoldbachOddALTV
))) |
154 | 153 | 3impib 1254 |
. . 3
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29))) → (∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < (;88 · (10↑;29))) → 𝑛 ∈ GoldbachOddALTV ) → 𝑁 ∈ GoldbachOddALTV
)) |
155 | 146, 154 | sylcom 30 |
. 2
⊢
(∃𝑑 ∈
(ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) → ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29))) → 𝑁 ∈ GoldbachOddALTV )) |
156 | 1, 155 | ax-mp 5 |
1
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29))) → 𝑁 ∈ GoldbachOddALTV ) |