Step |
Hyp |
Ref |
Expression |
1 |
|
hgt750lemc.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
2 |
|
hgt750lemd.0 |
⊢ ( 𝜑 → ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) |
3 |
|
fzfid |
⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin ) |
4 |
|
diffi |
⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin ) |
5 |
3 4
|
syl |
⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin ) |
6 |
|
vmaf |
⊢ Λ : ℕ ⟶ ℝ |
7 |
6
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → Λ : ℕ ⟶ ℝ ) |
8 |
|
fz1ssnn |
⊢ ( 1 ... 𝑁 ) ⊆ ℕ |
9 |
8
|
a1i |
⊢ ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ℕ ) |
10 |
9
|
ssdifssd |
⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ℙ ) ⊆ ℕ ) |
11 |
10
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → 𝑖 ∈ ℕ ) |
12 |
7 11
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ ) |
13 |
5 12
|
fsumrecl |
⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ∈ ℝ ) |
14 |
|
2rp |
⊢ 2 ∈ ℝ+ |
15 |
14
|
a1i |
⊢ ( 𝜑 → 2 ∈ ℝ+ ) |
16 |
15
|
relogcld |
⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℝ ) |
17 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
18 |
|
4re |
⊢ 4 ∈ ℝ |
19 |
|
2re |
⊢ 2 ∈ ℝ |
20 |
|
6re |
⊢ 6 ∈ ℝ |
21 |
20 19
|
pm3.2i |
⊢ ( 6 ∈ ℝ ∧ 2 ∈ ℝ ) |
22 |
|
dp2cl |
⊢ ( ( 6 ∈ ℝ ∧ 2 ∈ ℝ ) → _ 6 2 ∈ ℝ ) |
23 |
21 22
|
ax-mp |
⊢ _ 6 2 ∈ ℝ |
24 |
19 23
|
pm3.2i |
⊢ ( 2 ∈ ℝ ∧ _ 6 2 ∈ ℝ ) |
25 |
|
dp2cl |
⊢ ( ( 2 ∈ ℝ ∧ _ 6 2 ∈ ℝ ) → _ 2 _ 6 2 ∈ ℝ ) |
26 |
24 25
|
ax-mp |
⊢ _ 2 _ 6 2 ∈ ℝ |
27 |
18 26
|
pm3.2i |
⊢ ( 4 ∈ ℝ ∧ _ 2 _ 6 2 ∈ ℝ ) |
28 |
|
dp2cl |
⊢ ( ( 4 ∈ ℝ ∧ _ 2 _ 6 2 ∈ ℝ ) → _ 4 _ 2 _ 6 2 ∈ ℝ ) |
29 |
27 28
|
ax-mp |
⊢ _ 4 _ 2 _ 6 2 ∈ ℝ |
30 |
|
dpcl |
⊢ ( ( 1 ∈ ℕ0 ∧ _ 4 _ 2 _ 6 2 ∈ ℝ ) → ( 1 . _ 4 _ 2 _ 6 2 ) ∈ ℝ ) |
31 |
17 29 30
|
mp2an |
⊢ ( 1 . _ 4 _ 2 _ 6 2 ) ∈ ℝ |
32 |
31
|
a1i |
⊢ ( 𝜑 → ( 1 . _ 4 _ 2 _ 6 2 ) ∈ ℝ ) |
33 |
1
|
nnred |
⊢ ( 𝜑 → 𝑁 ∈ ℝ ) |
34 |
1
|
nnrpd |
⊢ ( 𝜑 → 𝑁 ∈ ℝ+ ) |
35 |
34
|
rpge0d |
⊢ ( 𝜑 → 0 ≤ 𝑁 ) |
36 |
33 35
|
resqrtcld |
⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ ) |
37 |
32 36
|
remulcld |
⊢ ( 𝜑 → ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) ∈ ℝ ) |
38 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
39 |
|
0re |
⊢ 0 ∈ ℝ |
40 |
|
1re |
⊢ 1 ∈ ℝ |
41 |
39 40
|
pm3.2i |
⊢ ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) |
42 |
|
dp2cl |
⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → _ 0 1 ∈ ℝ ) |
43 |
41 42
|
ax-mp |
⊢ _ 0 1 ∈ ℝ |
44 |
39 43
|
pm3.2i |
⊢ ( 0 ∈ ℝ ∧ _ 0 1 ∈ ℝ ) |
45 |
|
dp2cl |
⊢ ( ( 0 ∈ ℝ ∧ _ 0 1 ∈ ℝ ) → _ 0 _ 0 1 ∈ ℝ ) |
46 |
44 45
|
ax-mp |
⊢ _ 0 _ 0 1 ∈ ℝ |
47 |
39 46
|
pm3.2i |
⊢ ( 0 ∈ ℝ ∧ _ 0 _ 0 1 ∈ ℝ ) |
48 |
|
dp2cl |
⊢ ( ( 0 ∈ ℝ ∧ _ 0 _ 0 1 ∈ ℝ ) → _ 0 _ 0 _ 0 1 ∈ ℝ ) |
49 |
47 48
|
ax-mp |
⊢ _ 0 _ 0 _ 0 1 ∈ ℝ |
50 |
|
dpcl |
⊢ ( ( 0 ∈ ℕ0 ∧ _ 0 _ 0 _ 0 1 ∈ ℝ ) → ( 0 . _ 0 _ 0 _ 0 1 ) ∈ ℝ ) |
51 |
38 49 50
|
mp2an |
⊢ ( 0 . _ 0 _ 0 _ 0 1 ) ∈ ℝ |
52 |
51
|
a1i |
⊢ ( 𝜑 → ( 0 . _ 0 _ 0 _ 0 1 ) ∈ ℝ ) |
53 |
52 36
|
remulcld |
⊢ ( 𝜑 → ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) ∈ ℝ ) |
54 |
1
|
nnzd |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
55 |
|
chpvalz |
⊢ ( 𝑁 ∈ ℤ → ( ψ ‘ 𝑁 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) ) |
56 |
54 55
|
syl |
⊢ ( 𝜑 → ( ψ ‘ 𝑁 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) ) |
57 |
|
chtvalz |
⊢ ( 𝑁 ∈ ℤ → ( θ ‘ 𝑁 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑖 ) ) |
58 |
54 57
|
syl |
⊢ ( 𝜑 → ( θ ‘ 𝑁 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑖 ) ) |
59 |
|
inss2 |
⊢ ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℙ |
60 |
59
|
a1i |
⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℙ ) |
61 |
60
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → 𝑖 ∈ ℙ ) |
62 |
|
vmaprm |
⊢ ( 𝑖 ∈ ℙ → ( Λ ‘ 𝑖 ) = ( log ‘ 𝑖 ) ) |
63 |
61 62
|
syl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → ( Λ ‘ 𝑖 ) = ( log ‘ 𝑖 ) ) |
64 |
63
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑖 ) ) |
65 |
58 64
|
eqtr4d |
⊢ ( 𝜑 → ( θ ‘ 𝑁 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ) |
66 |
56 65
|
oveq12d |
⊢ ( 𝜑 → ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) − Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ) ) |
67 |
|
infi |
⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( ( 1 ... 𝑁 ) ∩ ℙ ) ∈ Fin ) |
68 |
3 67
|
syl |
⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ℙ ) ∈ Fin ) |
69 |
6
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → Λ : ℕ ⟶ ℝ ) |
70 |
|
inss1 |
⊢ ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ( 1 ... 𝑁 ) |
71 |
70 8
|
sstri |
⊢ ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℕ |
72 |
71
|
a1i |
⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℕ ) |
73 |
72
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → 𝑖 ∈ ℕ ) |
74 |
69 73
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ ) |
75 |
74
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ ) |
76 |
68 75
|
fsumcl |
⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ∈ ℂ ) |
77 |
12
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ ) |
78 |
5 77
|
fsumcl |
⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ∈ ℂ ) |
79 |
|
inindif |
⊢ ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∩ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ∅ |
80 |
79
|
a1i |
⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∩ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ∅ ) |
81 |
|
inundif |
⊢ ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ( 1 ... 𝑁 ) |
82 |
81
|
eqcomi |
⊢ ( 1 ... 𝑁 ) = ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) |
83 |
82
|
a1i |
⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) ) |
84 |
6
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → Λ : ℕ ⟶ ℝ ) |
85 |
9
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ℕ ) |
86 |
84 85
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ ) |
87 |
86
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ ) |
88 |
80 83 3 87
|
fsumsplit |
⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ) ) |
89 |
76 78 88
|
mvrladdd |
⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) − Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ) |
90 |
66 89
|
eqtr2d |
⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) = ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) ) |
91 |
|
fveq2 |
⊢ ( 𝑥 = 𝑁 → ( ψ ‘ 𝑥 ) = ( ψ ‘ 𝑁 ) ) |
92 |
|
fveq2 |
⊢ ( 𝑥 = 𝑁 → ( θ ‘ 𝑥 ) = ( θ ‘ 𝑁 ) ) |
93 |
91 92
|
oveq12d |
⊢ ( 𝑥 = 𝑁 → ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) = ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) ) |
94 |
|
fveq2 |
⊢ ( 𝑥 = 𝑁 → ( √ ‘ 𝑥 ) = ( √ ‘ 𝑁 ) ) |
95 |
94
|
oveq2d |
⊢ ( 𝑥 = 𝑁 → ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑥 ) ) = ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) ) |
96 |
93 95
|
breq12d |
⊢ ( 𝑥 = 𝑁 → ( ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑥 ) ) ↔ ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) ) ) |
97 |
|
ax-ros336 |
⊢ ∀ 𝑥 ∈ ℝ+ ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑥 ) ) |
98 |
97
|
a1i |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑥 ) ) ) |
99 |
96 98 34
|
rspcdva |
⊢ ( 𝜑 → ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) ) |
100 |
90 99
|
eqbrtrd |
⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) ) |
101 |
40
|
a1i |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
102 |
|
log2le1 |
⊢ ( log ‘ 2 ) < 1 |
103 |
102
|
a1i |
⊢ ( 𝜑 → ( log ‘ 2 ) < 1 ) |
104 |
|
10nn0 |
⊢ ; 1 0 ∈ ℕ0 |
105 |
|
7nn0 |
⊢ 7 ∈ ℕ0 |
106 |
104 105
|
nn0expcli |
⊢ ( ; 1 0 ↑ 7 ) ∈ ℕ0 |
107 |
106
|
nn0rei |
⊢ ( ; 1 0 ↑ 7 ) ∈ ℝ |
108 |
107
|
a1i |
⊢ ( 𝜑 → ( ; 1 0 ↑ 7 ) ∈ ℝ ) |
109 |
52 108
|
remulcld |
⊢ ( 𝜑 → ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( ; 1 0 ↑ 7 ) ) ∈ ℝ ) |
110 |
104
|
nn0rei |
⊢ ; 1 0 ∈ ℝ |
111 |
|
0z |
⊢ 0 ∈ ℤ |
112 |
|
3z |
⊢ 3 ∈ ℤ |
113 |
110 111 112
|
3pm3.2i |
⊢ ( ; 1 0 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ ) |
114 |
|
1lt10 |
⊢ 1 < ; 1 0 |
115 |
|
3pos |
⊢ 0 < 3 |
116 |
114 115
|
pm3.2i |
⊢ ( 1 < ; 1 0 ∧ 0 < 3 ) |
117 |
|
ltexp2a |
⊢ ( ( ( ; 1 0 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ ) ∧ ( 1 < ; 1 0 ∧ 0 < 3 ) ) → ( ; 1 0 ↑ 0 ) < ( ; 1 0 ↑ 3 ) ) |
118 |
113 116 117
|
mp2an |
⊢ ( ; 1 0 ↑ 0 ) < ( ; 1 0 ↑ 3 ) |
119 |
104
|
numexp0 |
⊢ ( ; 1 0 ↑ 0 ) = 1 |
120 |
119
|
eqcomi |
⊢ 1 = ( ; 1 0 ↑ 0 ) |
121 |
110
|
recni |
⊢ ; 1 0 ∈ ℂ |
122 |
|
10pos |
⊢ 0 < ; 1 0 |
123 |
39 122
|
gtneii |
⊢ ; 1 0 ≠ 0 |
124 |
|
4z |
⊢ 4 ∈ ℤ |
125 |
|
expm1 |
⊢ ( ( ; 1 0 ∈ ℂ ∧ ; 1 0 ≠ 0 ∧ 4 ∈ ℤ ) → ( ; 1 0 ↑ ( 4 − 1 ) ) = ( ( ; 1 0 ↑ 4 ) / ; 1 0 ) ) |
126 |
121 123 124 125
|
mp3an |
⊢ ( ; 1 0 ↑ ( 4 − 1 ) ) = ( ( ; 1 0 ↑ 4 ) / ; 1 0 ) |
127 |
|
4m1e3 |
⊢ ( 4 − 1 ) = 3 |
128 |
127
|
oveq2i |
⊢ ( ; 1 0 ↑ ( 4 − 1 ) ) = ( ; 1 0 ↑ 3 ) |
129 |
|
4nn0 |
⊢ 4 ∈ ℕ0 |
130 |
104 129
|
nn0expcli |
⊢ ( ; 1 0 ↑ 4 ) ∈ ℕ0 |
131 |
130
|
nn0cni |
⊢ ( ; 1 0 ↑ 4 ) ∈ ℂ |
132 |
|
divrec2 |
⊢ ( ( ( ; 1 0 ↑ 4 ) ∈ ℂ ∧ ; 1 0 ∈ ℂ ∧ ; 1 0 ≠ 0 ) → ( ( ; 1 0 ↑ 4 ) / ; 1 0 ) = ( ( 1 / ; 1 0 ) · ( ; 1 0 ↑ 4 ) ) ) |
133 |
131 121 123 132
|
mp3an |
⊢ ( ( ; 1 0 ↑ 4 ) / ; 1 0 ) = ( ( 1 / ; 1 0 ) · ( ; 1 0 ↑ 4 ) ) |
134 |
126 128 133
|
3eqtr3ri |
⊢ ( ( 1 / ; 1 0 ) · ( ; 1 0 ↑ 4 ) ) = ( ; 1 0 ↑ 3 ) |
135 |
118 120 134
|
3brtr4i |
⊢ 1 < ( ( 1 / ; 1 0 ) · ( ; 1 0 ↑ 4 ) ) |
136 |
|
1rp |
⊢ 1 ∈ ℝ+ |
137 |
136
|
dp0h |
⊢ ( 0 . 1 ) = ( 1 / ; 1 0 ) |
138 |
137
|
oveq1i |
⊢ ( ( 0 . 1 ) · ( ; 1 0 ↑ 4 ) ) = ( ( 1 / ; 1 0 ) · ( ; 1 0 ↑ 4 ) ) |
139 |
135 138
|
breqtrri |
⊢ 1 < ( ( 0 . 1 ) · ( ; 1 0 ↑ 4 ) ) |
140 |
139
|
a1i |
⊢ ( 𝜑 → 1 < ( ( 0 . 1 ) · ( ; 1 0 ↑ 4 ) ) ) |
141 |
|
4p1e5 |
⊢ ( 4 + 1 ) = 5 |
142 |
|
5nn0 |
⊢ 5 ∈ ℕ0 |
143 |
142
|
nn0zi |
⊢ 5 ∈ ℤ |
144 |
38 136 141 124 143
|
dpexpp1 |
⊢ ( ( 0 . 1 ) · ( ; 1 0 ↑ 4 ) ) = ( ( 0 . _ 0 1 ) · ( ; 1 0 ↑ 5 ) ) |
145 |
38 136
|
rpdp2cl |
⊢ _ 0 1 ∈ ℝ+ |
146 |
|
5p1e6 |
⊢ ( 5 + 1 ) = 6 |
147 |
|
6nn0 |
⊢ 6 ∈ ℕ0 |
148 |
147
|
nn0zi |
⊢ 6 ∈ ℤ |
149 |
38 145 146 143 148
|
dpexpp1 |
⊢ ( ( 0 . _ 0 1 ) · ( ; 1 0 ↑ 5 ) ) = ( ( 0 . _ 0 _ 0 1 ) · ( ; 1 0 ↑ 6 ) ) |
150 |
38 145
|
rpdp2cl |
⊢ _ 0 _ 0 1 ∈ ℝ+ |
151 |
|
6p1e7 |
⊢ ( 6 + 1 ) = 7 |
152 |
105
|
nn0zi |
⊢ 7 ∈ ℤ |
153 |
38 150 151 148 152
|
dpexpp1 |
⊢ ( ( 0 . _ 0 _ 0 1 ) · ( ; 1 0 ↑ 6 ) ) = ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( ; 1 0 ↑ 7 ) ) |
154 |
144 149 153
|
3eqtrri |
⊢ ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( ; 1 0 ↑ 7 ) ) = ( ( 0 . 1 ) · ( ; 1 0 ↑ 4 ) ) |
155 |
140 154
|
breqtrrdi |
⊢ ( 𝜑 → 1 < ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( ; 1 0 ↑ 7 ) ) ) |
156 |
38 150
|
rpdp2cl |
⊢ _ 0 _ 0 _ 0 1 ∈ ℝ+ |
157 |
38 156
|
rpdpcl |
⊢ ( 0 . _ 0 _ 0 _ 0 1 ) ∈ ℝ+ |
158 |
157
|
a1i |
⊢ ( 𝜑 → ( 0 . _ 0 _ 0 _ 0 1 ) ∈ ℝ+ ) |
159 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
160 |
159 105
|
deccl |
⊢ ; 2 7 ∈ ℕ0 |
161 |
104 160
|
nn0expcli |
⊢ ( ; 1 0 ↑ ; 2 7 ) ∈ ℕ0 |
162 |
161
|
nn0rei |
⊢ ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ |
163 |
162
|
a1i |
⊢ ( 𝜑 → ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ ) |
164 |
161
|
nn0ge0i |
⊢ 0 ≤ ( ; 1 0 ↑ ; 2 7 ) |
165 |
164
|
a1i |
⊢ ( 𝜑 → 0 ≤ ( ; 1 0 ↑ ; 2 7 ) ) |
166 |
163 165
|
resqrtcld |
⊢ ( 𝜑 → ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ∈ ℝ ) |
167 |
|
expmul |
⊢ ( ( ; 1 0 ∈ ℂ ∧ 7 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( ; 1 0 ↑ ( 7 · 2 ) ) = ( ( ; 1 0 ↑ 7 ) ↑ 2 ) ) |
168 |
121 105 159 167
|
mp3an |
⊢ ( ; 1 0 ↑ ( 7 · 2 ) ) = ( ( ; 1 0 ↑ 7 ) ↑ 2 ) |
169 |
|
7t2e14 |
⊢ ( 7 · 2 ) = ; 1 4 |
170 |
169
|
oveq2i |
⊢ ( ; 1 0 ↑ ( 7 · 2 ) ) = ( ; 1 0 ↑ ; 1 4 ) |
171 |
168 170
|
eqtr3i |
⊢ ( ( ; 1 0 ↑ 7 ) ↑ 2 ) = ( ; 1 0 ↑ ; 1 4 ) |
172 |
171
|
fveq2i |
⊢ ( √ ‘ ( ( ; 1 0 ↑ 7 ) ↑ 2 ) ) = ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) |
173 |
|
expgt0 |
⊢ ( ( ; 1 0 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < ; 1 0 ) → 0 < ( ; 1 0 ↑ 7 ) ) |
174 |
110 152 122 173
|
mp3an |
⊢ 0 < ( ; 1 0 ↑ 7 ) |
175 |
39 107 174
|
ltleii |
⊢ 0 ≤ ( ; 1 0 ↑ 7 ) |
176 |
|
sqrtsq |
⊢ ( ( ( ; 1 0 ↑ 7 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ 7 ) ) → ( √ ‘ ( ( ; 1 0 ↑ 7 ) ↑ 2 ) ) = ( ; 1 0 ↑ 7 ) ) |
177 |
107 175 176
|
mp2an |
⊢ ( √ ‘ ( ( ; 1 0 ↑ 7 ) ↑ 2 ) ) = ( ; 1 0 ↑ 7 ) |
178 |
172 177
|
eqtr3i |
⊢ ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) = ( ; 1 0 ↑ 7 ) |
179 |
17 129
|
deccl |
⊢ ; 1 4 ∈ ℕ0 |
180 |
179
|
nn0zi |
⊢ ; 1 4 ∈ ℤ |
181 |
160
|
nn0zi |
⊢ ; 2 7 ∈ ℤ |
182 |
110 180 181
|
3pm3.2i |
⊢ ( ; 1 0 ∈ ℝ ∧ ; 1 4 ∈ ℤ ∧ ; 2 7 ∈ ℤ ) |
183 |
|
4lt10 |
⊢ 4 < ; 1 0 |
184 |
|
1lt2 |
⊢ 1 < 2 |
185 |
17 159 129 105 183 184
|
decltc |
⊢ ; 1 4 < ; 2 7 |
186 |
114 185
|
pm3.2i |
⊢ ( 1 < ; 1 0 ∧ ; 1 4 < ; 2 7 ) |
187 |
|
ltexp2a |
⊢ ( ( ( ; 1 0 ∈ ℝ ∧ ; 1 4 ∈ ℤ ∧ ; 2 7 ∈ ℤ ) ∧ ( 1 < ; 1 0 ∧ ; 1 4 < ; 2 7 ) ) → ( ; 1 0 ↑ ; 1 4 ) < ( ; 1 0 ↑ ; 2 7 ) ) |
188 |
182 186 187
|
mp2an |
⊢ ( ; 1 0 ↑ ; 1 4 ) < ( ; 1 0 ↑ ; 2 7 ) |
189 |
104 179
|
nn0expcli |
⊢ ( ; 1 0 ↑ ; 1 4 ) ∈ ℕ0 |
190 |
189
|
nn0rei |
⊢ ( ; 1 0 ↑ ; 1 4 ) ∈ ℝ |
191 |
|
expgt0 |
⊢ ( ( ; 1 0 ∈ ℝ ∧ ; 1 4 ∈ ℤ ∧ 0 < ; 1 0 ) → 0 < ( ; 1 0 ↑ ; 1 4 ) ) |
192 |
110 180 122 191
|
mp3an |
⊢ 0 < ( ; 1 0 ↑ ; 1 4 ) |
193 |
39 190 192
|
ltleii |
⊢ 0 ≤ ( ; 1 0 ↑ ; 1 4 ) |
194 |
190 193
|
pm3.2i |
⊢ ( ( ; 1 0 ↑ ; 1 4 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ ; 1 4 ) ) |
195 |
162 164
|
pm3.2i |
⊢ ( ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ ; 2 7 ) ) |
196 |
|
sqrtlt |
⊢ ( ( ( ( ; 1 0 ↑ ; 1 4 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ ; 1 4 ) ) ∧ ( ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ ; 2 7 ) ) ) → ( ( ; 1 0 ↑ ; 1 4 ) < ( ; 1 0 ↑ ; 2 7 ) ↔ ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) |
197 |
194 195 196
|
mp2an |
⊢ ( ( ; 1 0 ↑ ; 1 4 ) < ( ; 1 0 ↑ ; 2 7 ) ↔ ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) |
198 |
188 197
|
mpbi |
⊢ ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) |
199 |
178 198
|
eqbrtrri |
⊢ ( ; 1 0 ↑ 7 ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) |
200 |
199
|
a1i |
⊢ ( 𝜑 → ( ; 1 0 ↑ 7 ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) |
201 |
163 165 33 35
|
sqrtled |
⊢ ( 𝜑 → ( ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ↔ ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ≤ ( √ ‘ 𝑁 ) ) ) |
202 |
2 201
|
mpbid |
⊢ ( 𝜑 → ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ≤ ( √ ‘ 𝑁 ) ) |
203 |
108 166 36 200 202
|
ltletrd |
⊢ ( 𝜑 → ( ; 1 0 ↑ 7 ) < ( √ ‘ 𝑁 ) ) |
204 |
108 36 158 203
|
ltmul2dd |
⊢ ( 𝜑 → ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( ; 1 0 ↑ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) ) |
205 |
101 109 53 155 204
|
lttrd |
⊢ ( 𝜑 → 1 < ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) ) |
206 |
16 101 53 103 205
|
lttrd |
⊢ ( 𝜑 → ( log ‘ 2 ) < ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) ) |
207 |
13 16 37 53 100 206
|
lt2addd |
⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) + ( log ‘ 2 ) ) < ( ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) + ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) ) ) |
208 |
|
nfv |
⊢ Ⅎ 𝑖 𝜑 |
209 |
|
nfcv |
⊢ Ⅎ 𝑖 ( log ‘ 2 ) |
210 |
|
2prm |
⊢ 2 ∈ ℙ |
211 |
210
|
a1i |
⊢ ( 𝜑 → 2 ∈ ℙ ) |
212 |
|
elndif |
⊢ ( 2 ∈ ℙ → ¬ 2 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) |
213 |
211 212
|
syl |
⊢ ( 𝜑 → ¬ 2 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) |
214 |
|
fveq2 |
⊢ ( 𝑖 = 2 → ( Λ ‘ 𝑖 ) = ( Λ ‘ 2 ) ) |
215 |
|
vmaprm |
⊢ ( 2 ∈ ℙ → ( Λ ‘ 2 ) = ( log ‘ 2 ) ) |
216 |
210 215
|
ax-mp |
⊢ ( Λ ‘ 2 ) = ( log ‘ 2 ) |
217 |
214 216
|
eqtrdi |
⊢ ( 𝑖 = 2 → ( Λ ‘ 𝑖 ) = ( log ‘ 2 ) ) |
218 |
|
2cnd |
⊢ ( 𝜑 → 2 ∈ ℂ ) |
219 |
|
2ne0 |
⊢ 2 ≠ 0 |
220 |
219
|
a1i |
⊢ ( 𝜑 → 2 ≠ 0 ) |
221 |
218 220
|
logcld |
⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℂ ) |
222 |
208 209 5 211 213 77 217 221
|
fsumsplitsn |
⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) + ( log ‘ 2 ) ) ) |
223 |
147 14
|
rpdp2cl |
⊢ _ 6 2 ∈ ℝ+ |
224 |
159 223
|
rpdp2cl |
⊢ _ 2 _ 6 2 ∈ ℝ+ |
225 |
|
3rp |
⊢ 3 ∈ ℝ+ |
226 |
147 225
|
rpdp2cl |
⊢ _ 6 3 ∈ ℝ+ |
227 |
159 226
|
rpdp2cl |
⊢ _ 2 _ 6 3 ∈ ℝ+ |
228 |
|
1p0e1 |
⊢ ( 1 + 0 ) = 1 |
229 |
|
4cn |
⊢ 4 ∈ ℂ |
230 |
229
|
addid1i |
⊢ ( 4 + 0 ) = 4 |
231 |
|
2cn |
⊢ 2 ∈ ℂ |
232 |
231
|
addid1i |
⊢ ( 2 + 0 ) = 2 |
233 |
|
3nn0 |
⊢ 3 ∈ ℕ0 |
234 |
|
eqid |
⊢ ; 6 2 = ; 6 2 |
235 |
|
eqid |
⊢ ; 0 1 = ; 0 1 |
236 |
|
6cn |
⊢ 6 ∈ ℂ |
237 |
236
|
addid1i |
⊢ ( 6 + 0 ) = 6 |
238 |
|
2p1e3 |
⊢ ( 2 + 1 ) = 3 |
239 |
147 159 38 17 234 235 237 238
|
decadd |
⊢ ( ; 6 2 + ; 0 1 ) = ; 6 3 |
240 |
147 159 38 17 147 233 239
|
dpadd |
⊢ ( ( 6 . 2 ) + ( 0 . 1 ) ) = ( 6 . 3 ) |
241 |
147 14 38 136 147 225 159 38 232 240
|
dpadd2 |
⊢ ( ( 2 . _ 6 2 ) + ( 0 . _ 0 1 ) ) = ( 2 . _ 6 3 ) |
242 |
159 223 38 145 159 226 129 38 230 241
|
dpadd2 |
⊢ ( ( 4 . _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 1 ) ) = ( 4 . _ 2 _ 6 3 ) |
243 |
129 224 38 150 129 227 17 38 228 242
|
dpadd2 |
⊢ ( ( 1 . _ 4 _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 _ 0 1 ) ) = ( 1 . _ 4 _ 2 _ 6 3 ) |
244 |
243
|
oveq1i |
⊢ ( ( ( 1 . _ 4 _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 _ 0 1 ) ) · ( √ ‘ 𝑁 ) ) = ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( √ ‘ 𝑁 ) ) |
245 |
32
|
recnd |
⊢ ( 𝜑 → ( 1 . _ 4 _ 2 _ 6 2 ) ∈ ℂ ) |
246 |
52
|
recnd |
⊢ ( 𝜑 → ( 0 . _ 0 _ 0 _ 0 1 ) ∈ ℂ ) |
247 |
36
|
recnd |
⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℂ ) |
248 |
245 246 247
|
adddird |
⊢ ( 𝜑 → ( ( ( 1 . _ 4 _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 _ 0 1 ) ) · ( √ ‘ 𝑁 ) ) = ( ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) + ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) ) ) |
249 |
244 248
|
eqtr3id |
⊢ ( 𝜑 → ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( √ ‘ 𝑁 ) ) = ( ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑁 ) ) + ( ( 0 . _ 0 _ 0 _ 0 1 ) · ( √ ‘ 𝑁 ) ) ) ) |
250 |
207 222 249
|
3brtr4d |
⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) < ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( √ ‘ 𝑁 ) ) ) |