| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lgamgulm.r |
⊢ ( 𝜑 → 𝑅 ∈ ℕ ) |
| 2 |
|
lgamgulm.u |
⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) } |
| 3 |
|
lgamgulm.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
| 4 |
|
lgamgulm.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) |
| 5 |
|
lgamgulm.l |
⊢ ( 𝜑 → ( 2 · 𝑅 ) ≤ 𝑁 ) |
| 6 |
|
1elunit |
⊢ 1 ∈ ( 0 [,] 1 ) |
| 7 |
|
0elunit |
⊢ 0 ∈ ( 0 [,] 1 ) |
| 8 |
|
0red |
⊢ ( 𝜑 → 0 ∈ ℝ ) |
| 9 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
| 10 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
| 11 |
10
|
subcn |
⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) |
| 12 |
11
|
a1i |
⊢ ( 𝜑 → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ) |
| 13 |
1 2
|
lgamgulmlem1 |
⊢ ( 𝜑 → 𝑈 ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) |
| 14 |
13 4
|
sseldd |
⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) |
| 15 |
14
|
eldifad |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
| 16 |
3
|
nnred |
⊢ ( 𝜑 → 𝑁 ∈ ℝ ) |
| 17 |
16
|
recnd |
⊢ ( 𝜑 → 𝑁 ∈ ℂ ) |
| 18 |
3
|
nnne0d |
⊢ ( 𝜑 → 𝑁 ≠ 0 ) |
| 19 |
15 17 18
|
divcld |
⊢ ( 𝜑 → ( 𝐴 / 𝑁 ) ∈ ℂ ) |
| 20 |
|
unitssre |
⊢ ( 0 [,] 1 ) ⊆ ℝ |
| 21 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
| 22 |
20 21
|
sstri |
⊢ ( 0 [,] 1 ) ⊆ ℂ |
| 23 |
22
|
a1i |
⊢ ( 𝜑 → ( 0 [,] 1 ) ⊆ ℂ ) |
| 24 |
|
ssidd |
⊢ ( 𝜑 → ℂ ⊆ ℂ ) |
| 25 |
|
cncfmptc |
⊢ ( ( ( 𝐴 / 𝑁 ) ∈ ℂ ∧ ( 0 [,] 1 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( 𝐴 / 𝑁 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) |
| 26 |
19 23 24 25
|
syl3anc |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( 𝐴 / 𝑁 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) |
| 27 |
|
cncfmptid |
⊢ ( ( ( 0 [,] 1 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ 𝑡 ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) |
| 28 |
22 24 27
|
sylancr |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ 𝑡 ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) |
| 29 |
26 28
|
mulcncf |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) |
| 30 |
|
eqid |
⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) ) |
| 31 |
30
|
logcn |
⊢ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ ) |
| 32 |
31
|
a1i |
⊢ ( 𝜑 → ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ ) ) |
| 33 |
|
cncff |
⊢ ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ ) → ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) : ( ℂ ∖ ( -∞ (,] 0 ) ) ⟶ ℂ ) |
| 34 |
32 33
|
syl |
⊢ ( 𝜑 → ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) : ( ℂ ∖ ( -∞ (,] 0 ) ) ⟶ ℂ ) |
| 35 |
19
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝐴 / 𝑁 ) ∈ ℂ ) |
| 36 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑡 ∈ ( 0 [,] 1 ) ) |
| 37 |
20 36
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑡 ∈ ℝ ) |
| 38 |
37
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑡 ∈ ℂ ) |
| 39 |
35 38
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝐴 / 𝑁 ) · 𝑡 ) ∈ ℂ ) |
| 40 |
|
1cnd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 1 ∈ ℂ ) |
| 41 |
39 40
|
addcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℂ ) |
| 42 |
|
rere |
⊢ ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℝ → ( ℜ ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) = ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) |
| 43 |
42
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ∧ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℝ ) → ( ℜ ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) = ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) |
| 44 |
41
|
recld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ℜ ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ∈ ℝ ) |
| 45 |
39
|
recld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ∈ ℝ ) |
| 46 |
45
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ∈ ℂ ) |
| 47 |
46
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ∈ ℝ ) |
| 48 |
39
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ∈ ℝ ) |
| 49 |
|
1red |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 1 ∈ ℝ ) |
| 50 |
|
absrele |
⊢ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) ∈ ℂ → ( abs ‘ ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ≤ ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) |
| 51 |
39 50
|
syl |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ≤ ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) |
| 52 |
49
|
rehalfcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 1 / 2 ) ∈ ℝ ) |
| 53 |
1
|
nnred |
⊢ ( 𝜑 → 𝑅 ∈ ℝ ) |
| 54 |
53
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑅 ∈ ℝ ) |
| 55 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑁 ∈ ℕ ) |
| 56 |
54 55
|
nndivred |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝑅 / 𝑁 ) ∈ ℝ ) |
| 57 |
19
|
abscld |
⊢ ( 𝜑 → ( abs ‘ ( 𝐴 / 𝑁 ) ) ∈ ℝ ) |
| 58 |
57
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( 𝐴 / 𝑁 ) ) ∈ ℝ ) |
| 59 |
35
|
absge0d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 0 ≤ ( abs ‘ ( 𝐴 / 𝑁 ) ) ) |
| 60 |
|
elicc01 |
⊢ ( 𝑡 ∈ ( 0 [,] 1 ) ↔ ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1 ) ) |
| 61 |
60
|
simp2bi |
⊢ ( 𝑡 ∈ ( 0 [,] 1 ) → 0 ≤ 𝑡 ) |
| 62 |
61
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 0 ≤ 𝑡 ) |
| 63 |
15 17 18
|
absdivd |
⊢ ( 𝜑 → ( abs ‘ ( 𝐴 / 𝑁 ) ) = ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝑁 ) ) ) |
| 64 |
3
|
nnrpd |
⊢ ( 𝜑 → 𝑁 ∈ ℝ+ ) |
| 65 |
64
|
rpge0d |
⊢ ( 𝜑 → 0 ≤ 𝑁 ) |
| 66 |
16 65
|
absidd |
⊢ ( 𝜑 → ( abs ‘ 𝑁 ) = 𝑁 ) |
| 67 |
66
|
oveq2d |
⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝑁 ) ) = ( ( abs ‘ 𝐴 ) / 𝑁 ) ) |
| 68 |
63 67
|
eqtr2d |
⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) / 𝑁 ) = ( abs ‘ ( 𝐴 / 𝑁 ) ) ) |
| 69 |
15
|
abscld |
⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ ) |
| 70 |
|
fveq2 |
⊢ ( 𝑥 = 𝐴 → ( abs ‘ 𝑥 ) = ( abs ‘ 𝐴 ) ) |
| 71 |
70
|
breq1d |
⊢ ( 𝑥 = 𝐴 → ( ( abs ‘ 𝑥 ) ≤ 𝑅 ↔ ( abs ‘ 𝐴 ) ≤ 𝑅 ) ) |
| 72 |
|
fvoveq1 |
⊢ ( 𝑥 = 𝐴 → ( abs ‘ ( 𝑥 + 𝑘 ) ) = ( abs ‘ ( 𝐴 + 𝑘 ) ) ) |
| 73 |
72
|
breq2d |
⊢ ( 𝑥 = 𝐴 → ( ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) ) |
| 74 |
73
|
ralbidv |
⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) ) |
| 75 |
71 74
|
anbi12d |
⊢ ( 𝑥 = 𝐴 → ( ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ↔ ( ( abs ‘ 𝐴 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) ) ) |
| 76 |
75 2
|
elrab2 |
⊢ ( 𝐴 ∈ 𝑈 ↔ ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) ) ) |
| 77 |
76
|
simprbi |
⊢ ( 𝐴 ∈ 𝑈 → ( ( abs ‘ 𝐴 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) ) |
| 78 |
4 77
|
syl |
⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) ) |
| 79 |
78
|
simpld |
⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ≤ 𝑅 ) |
| 80 |
69 53 64 79
|
lediv1dd |
⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) / 𝑁 ) ≤ ( 𝑅 / 𝑁 ) ) |
| 81 |
68 80
|
eqbrtrrd |
⊢ ( 𝜑 → ( abs ‘ ( 𝐴 / 𝑁 ) ) ≤ ( 𝑅 / 𝑁 ) ) |
| 82 |
81
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( 𝐴 / 𝑁 ) ) ≤ ( 𝑅 / 𝑁 ) ) |
| 83 |
60
|
simp3bi |
⊢ ( 𝑡 ∈ ( 0 [,] 1 ) → 𝑡 ≤ 1 ) |
| 84 |
83
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑡 ≤ 1 ) |
| 85 |
58 56 37 49 59 62 82 84
|
lemul12ad |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( abs ‘ ( 𝐴 / 𝑁 ) ) · 𝑡 ) ≤ ( ( 𝑅 / 𝑁 ) · 1 ) ) |
| 86 |
35 38
|
absmuld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) = ( ( abs ‘ ( 𝐴 / 𝑁 ) ) · ( abs ‘ 𝑡 ) ) ) |
| 87 |
37 62
|
absidd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( abs ‘ 𝑡 ) = 𝑡 ) |
| 88 |
87
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( abs ‘ ( 𝐴 / 𝑁 ) ) · ( abs ‘ 𝑡 ) ) = ( ( abs ‘ ( 𝐴 / 𝑁 ) ) · 𝑡 ) ) |
| 89 |
86 88
|
eqtr2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( abs ‘ ( 𝐴 / 𝑁 ) ) · 𝑡 ) = ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) |
| 90 |
56
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝑅 / 𝑁 ) ∈ ℂ ) |
| 91 |
90
|
mulridd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑅 / 𝑁 ) · 1 ) = ( 𝑅 / 𝑁 ) ) |
| 92 |
85 89 91
|
3brtr3d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ≤ ( 𝑅 / 𝑁 ) ) |
| 93 |
|
2rp |
⊢ 2 ∈ ℝ+ |
| 94 |
93
|
a1i |
⊢ ( 𝜑 → 2 ∈ ℝ+ ) |
| 95 |
53 16 94
|
lemuldiv2d |
⊢ ( 𝜑 → ( ( 2 · 𝑅 ) ≤ 𝑁 ↔ 𝑅 ≤ ( 𝑁 / 2 ) ) ) |
| 96 |
5 95
|
mpbid |
⊢ ( 𝜑 → 𝑅 ≤ ( 𝑁 / 2 ) ) |
| 97 |
|
2cnd |
⊢ ( 𝜑 → 2 ∈ ℂ ) |
| 98 |
|
2ne0 |
⊢ 2 ≠ 0 |
| 99 |
98
|
a1i |
⊢ ( 𝜑 → 2 ≠ 0 ) |
| 100 |
17 97 99
|
divrecd |
⊢ ( 𝜑 → ( 𝑁 / 2 ) = ( 𝑁 · ( 1 / 2 ) ) ) |
| 101 |
96 100
|
breqtrd |
⊢ ( 𝜑 → 𝑅 ≤ ( 𝑁 · ( 1 / 2 ) ) ) |
| 102 |
9
|
rehalfcld |
⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ ) |
| 103 |
53 102 64
|
ledivmuld |
⊢ ( 𝜑 → ( ( 𝑅 / 𝑁 ) ≤ ( 1 / 2 ) ↔ 𝑅 ≤ ( 𝑁 · ( 1 / 2 ) ) ) ) |
| 104 |
101 103
|
mpbird |
⊢ ( 𝜑 → ( 𝑅 / 𝑁 ) ≤ ( 1 / 2 ) ) |
| 105 |
104
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝑅 / 𝑁 ) ≤ ( 1 / 2 ) ) |
| 106 |
48 56 52 92 105
|
letrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ≤ ( 1 / 2 ) ) |
| 107 |
|
halflt1 |
⊢ ( 1 / 2 ) < 1 |
| 108 |
107
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 1 / 2 ) < 1 ) |
| 109 |
48 52 49 106 108
|
lelttrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) < 1 ) |
| 110 |
47 48 49 51 109
|
lelttrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( abs ‘ ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) < 1 ) |
| 111 |
45 49
|
absltd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( abs ‘ ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) < 1 ↔ ( - 1 < ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ∧ ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) < 1 ) ) ) |
| 112 |
110 111
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( - 1 < ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ∧ ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) < 1 ) ) |
| 113 |
112
|
simpld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → - 1 < ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) |
| 114 |
49
|
renegcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → - 1 ∈ ℝ ) |
| 115 |
114 45
|
posdifd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( - 1 < ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ↔ 0 < ( ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) − - 1 ) ) ) |
| 116 |
113 115
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 0 < ( ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) − - 1 ) ) |
| 117 |
46 40
|
subnegd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) − - 1 ) = ( ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) + 1 ) ) |
| 118 |
116 117
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 0 < ( ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) + 1 ) ) |
| 119 |
39 40
|
readdd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ℜ ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) = ( ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) + ( ℜ ‘ 1 ) ) ) |
| 120 |
|
re1 |
⊢ ( ℜ ‘ 1 ) = 1 |
| 121 |
120
|
oveq2i |
⊢ ( ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) + ( ℜ ‘ 1 ) ) = ( ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) + 1 ) |
| 122 |
119 121
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ℜ ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) = ( ( ℜ ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) + 1 ) ) |
| 123 |
118 122
|
breqtrrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 0 < ( ℜ ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) |
| 124 |
44 123
|
elrpd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ℜ ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ∈ ℝ+ ) |
| 125 |
124
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ∧ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℝ ) → ( ℜ ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ∈ ℝ+ ) |
| 126 |
43 125
|
eqeltrrd |
⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ∧ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℝ ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℝ+ ) |
| 127 |
126
|
ex |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℝ → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℝ+ ) ) |
| 128 |
30
|
ellogdm |
⊢ ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↔ ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℂ ∧ ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℝ → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℝ+ ) ) ) |
| 129 |
41 127 128
|
sylanbrc |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) |
| 130 |
34 129
|
cofmpt |
⊢ ( 𝜑 → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∘ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) |
| 131 |
129
|
fvresd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) = ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) |
| 132 |
131
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) |
| 133 |
130 132
|
eqtrd |
⊢ ( 𝜑 → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∘ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) |
| 134 |
129
|
fmpttd |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) : ( 0 [,] 1 ) ⟶ ( ℂ ∖ ( -∞ (,] 0 ) ) ) |
| 135 |
|
difss |
⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ |
| 136 |
10
|
addcn |
⊢ + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) |
| 137 |
136
|
a1i |
⊢ ( 𝜑 → + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ) |
| 138 |
|
1cnd |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
| 139 |
|
cncfmptc |
⊢ ( ( 1 ∈ ℂ ∧ ( 0 [,] 1 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ 1 ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) |
| 140 |
138 23 24 139
|
syl3anc |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ 1 ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) |
| 141 |
10 137 29 140
|
cncfmpt2f |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) |
| 142 |
|
cncfcdm |
⊢ ( ( ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ↔ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) : ( 0 [,] 1 ) ⟶ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) |
| 143 |
135 141 142
|
sylancr |
⊢ ( 𝜑 → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ↔ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) : ( 0 [,] 1 ) ⟶ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) |
| 144 |
134 143
|
mpbird |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) |
| 145 |
144 32
|
cncfco |
⊢ ( 𝜑 → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∘ ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) |
| 146 |
133 145
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) |
| 147 |
10 12 29 146
|
cncfmpt2f |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) |
| 148 |
21
|
a1i |
⊢ ( 𝜑 → ℝ ⊆ ℂ ) |
| 149 |
20
|
a1i |
⊢ ( 𝜑 → ( 0 [,] 1 ) ⊆ ℝ ) |
| 150 |
30
|
logdmn0 |
⊢ ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ≠ 0 ) |
| 151 |
129 150
|
syl |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ≠ 0 ) |
| 152 |
41 151
|
logcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ∈ ℂ ) |
| 153 |
39 152
|
subcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ∈ ℂ ) |
| 154 |
|
tgioo4 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
| 155 |
|
0re |
⊢ 0 ∈ ℝ |
| 156 |
|
iccntr |
⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 0 [,] 1 ) ) = ( 0 (,) 1 ) ) |
| 157 |
155 9 156
|
sylancr |
⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 0 [,] 1 ) ) = ( 0 (,) 1 ) ) |
| 158 |
148 149 153 154 10 157
|
dvmptntr |
⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) = ( ℝ D ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ) |
| 159 |
|
reelprrecn |
⊢ ℝ ∈ { ℝ , ℂ } |
| 160 |
159
|
a1i |
⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } ) |
| 161 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝐴 ∈ ℂ ) |
| 162 |
17
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ℂ ) |
| 163 |
18
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑁 ≠ 0 ) |
| 164 |
161 162 163
|
divcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝐴 / 𝑁 ) ∈ ℂ ) |
| 165 |
|
ioossicc |
⊢ ( 0 (,) 1 ) ⊆ ( 0 [,] 1 ) |
| 166 |
165
|
sseli |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → 𝑡 ∈ ( 0 [,] 1 ) ) |
| 167 |
166 38
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ℂ ) |
| 168 |
164 167
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝐴 / 𝑁 ) · 𝑡 ) ∈ ℂ ) |
| 169 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝐴 ∈ ℂ ) |
| 170 |
17
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑁 ∈ ℂ ) |
| 171 |
18
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑁 ≠ 0 ) |
| 172 |
169 170 171
|
divcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝐴 / 𝑁 ) ∈ ℂ ) |
| 173 |
148
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℂ ) |
| 174 |
172 173
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( ( 𝐴 / 𝑁 ) · 𝑡 ) ∈ ℂ ) |
| 175 |
|
1cnd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 1 ∈ ℂ ) |
| 176 |
160
|
dvmptid |
⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ℝ ↦ 𝑡 ) ) = ( 𝑡 ∈ ℝ ↦ 1 ) ) |
| 177 |
160 173 175 176 19
|
dvmptcmul |
⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ℝ ↦ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( 𝐴 / 𝑁 ) · 1 ) ) ) |
| 178 |
19
|
mulridd |
⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) · 1 ) = ( 𝐴 / 𝑁 ) ) |
| 179 |
178
|
mpteq2dv |
⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( ( 𝐴 / 𝑁 ) · 1 ) ) = ( 𝑡 ∈ ℝ ↦ ( 𝐴 / 𝑁 ) ) ) |
| 180 |
177 179
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ℝ ↦ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( 𝐴 / 𝑁 ) ) ) |
| 181 |
165 149
|
sstrid |
⊢ ( 𝜑 → ( 0 (,) 1 ) ⊆ ℝ ) |
| 182 |
|
retop |
⊢ ( topGen ‘ ran (,) ) ∈ Top |
| 183 |
|
iooretop |
⊢ ( 0 (,) 1 ) ∈ ( topGen ‘ ran (,) ) |
| 184 |
|
isopn3i |
⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 0 (,) 1 ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 0 (,) 1 ) ) = ( 0 (,) 1 ) ) |
| 185 |
182 183 184
|
mp2an |
⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 0 (,) 1 ) ) = ( 0 (,) 1 ) |
| 186 |
185
|
a1i |
⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 0 (,) 1 ) ) = ( 0 (,) 1 ) ) |
| 187 |
160 174 172 180 181 154 10 186
|
dvmptres2 |
⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( 𝐴 / 𝑁 ) ) ) |
| 188 |
166 152
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ∈ ℂ ) |
| 189 |
|
1cnd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 1 ∈ ℂ ) |
| 190 |
168 189
|
addcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℂ ) |
| 191 |
166 151
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ≠ 0 ) |
| 192 |
190 191
|
reccld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ∈ ℂ ) |
| 193 |
192 164
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ∈ ℂ ) |
| 194 |
|
cnelprrecn |
⊢ ℂ ∈ { ℝ , ℂ } |
| 195 |
194
|
a1i |
⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } ) |
| 196 |
166 129
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) |
| 197 |
|
eldifi |
⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝑦 ∈ ℂ ) |
| 198 |
197
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → 𝑦 ∈ ℂ ) |
| 199 |
30
|
logdmn0 |
⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝑦 ≠ 0 ) |
| 200 |
199
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → 𝑦 ≠ 0 ) |
| 201 |
198 200
|
logcld |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( log ‘ 𝑦 ) ∈ ℂ ) |
| 202 |
198 200
|
reccld |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( 1 / 𝑦 ) ∈ ℂ ) |
| 203 |
174 175
|
addcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ∈ ℂ ) |
| 204 |
|
0cnd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 0 ∈ ℂ ) |
| 205 |
160 138
|
dvmptc |
⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ℝ ↦ 1 ) ) = ( 𝑡 ∈ ℝ ↦ 0 ) ) |
| 206 |
160 174 172 180 175 204 205
|
dvmptadd |
⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ℝ ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( 𝐴 / 𝑁 ) + 0 ) ) ) |
| 207 |
19
|
addridd |
⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) + 0 ) = ( 𝐴 / 𝑁 ) ) |
| 208 |
207
|
mpteq2dv |
⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( ( 𝐴 / 𝑁 ) + 0 ) ) = ( 𝑡 ∈ ℝ ↦ ( 𝐴 / 𝑁 ) ) ) |
| 209 |
206 208
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ℝ ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( 𝐴 / 𝑁 ) ) ) |
| 210 |
160 203 172 209 181 154 10 186
|
dvmptres2 |
⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( 𝐴 / 𝑁 ) ) ) |
| 211 |
34
|
feqmptd |
⊢ ( 𝜑 → ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ‘ 𝑦 ) ) ) |
| 212 |
|
fvres |
⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ‘ 𝑦 ) = ( log ‘ 𝑦 ) ) |
| 213 |
212
|
mpteq2ia |
⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ‘ 𝑦 ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) |
| 214 |
211 213
|
eqtr2di |
⊢ ( 𝜑 → ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) = ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) |
| 215 |
214
|
oveq2d |
⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) ) = ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) ) |
| 216 |
30
|
dvlog |
⊢ ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑦 ) ) |
| 217 |
215 216
|
eqtrdi |
⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑦 ) ) ) |
| 218 |
|
fveq2 |
⊢ ( 𝑦 = ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) → ( log ‘ 𝑦 ) = ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) |
| 219 |
|
oveq2 |
⊢ ( 𝑦 = ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) → ( 1 / 𝑦 ) = ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) |
| 220 |
160 195 196 164 201 202 210 217 218 219
|
dvmptco |
⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) = ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) |
| 221 |
160 168 164 187 188 193 220
|
dvmptsub |
⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) = ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ) |
| 222 |
158 221
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) = ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ) |
| 223 |
222
|
dmeqd |
⊢ ( 𝜑 → dom ( ℝ D ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) = dom ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ) |
| 224 |
|
ovex |
⊢ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ∈ V |
| 225 |
|
eqid |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) = ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) |
| 226 |
224 225
|
dmmpti |
⊢ dom ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) = ( 0 (,) 1 ) |
| 227 |
223 226
|
eqtrdi |
⊢ ( 𝜑 → dom ( ℝ D ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) = ( 0 (,) 1 ) ) |
| 228 |
|
2re |
⊢ 2 ∈ ℝ |
| 229 |
228
|
a1i |
⊢ ( 𝜑 → 2 ∈ ℝ ) |
| 230 |
229 53
|
remulcld |
⊢ ( 𝜑 → ( 2 · 𝑅 ) ∈ ℝ ) |
| 231 |
1
|
nnrpd |
⊢ ( 𝜑 → 𝑅 ∈ ℝ+ ) |
| 232 |
53 231
|
ltaddrpd |
⊢ ( 𝜑 → 𝑅 < ( 𝑅 + 𝑅 ) ) |
| 233 |
53
|
recnd |
⊢ ( 𝜑 → 𝑅 ∈ ℂ ) |
| 234 |
233
|
2timesd |
⊢ ( 𝜑 → ( 2 · 𝑅 ) = ( 𝑅 + 𝑅 ) ) |
| 235 |
232 234
|
breqtrrd |
⊢ ( 𝜑 → 𝑅 < ( 2 · 𝑅 ) ) |
| 236 |
53 230 16 235 5
|
ltletrd |
⊢ ( 𝜑 → 𝑅 < 𝑁 ) |
| 237 |
|
difrp |
⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑅 < 𝑁 ↔ ( 𝑁 − 𝑅 ) ∈ ℝ+ ) ) |
| 238 |
53 16 237
|
syl2anc |
⊢ ( 𝜑 → ( 𝑅 < 𝑁 ↔ ( 𝑁 − 𝑅 ) ∈ ℝ+ ) ) |
| 239 |
236 238
|
mpbid |
⊢ ( 𝜑 → ( 𝑁 − 𝑅 ) ∈ ℝ+ ) |
| 240 |
239
|
rprecred |
⊢ ( 𝜑 → ( 1 / ( 𝑁 − 𝑅 ) ) ∈ ℝ ) |
| 241 |
3
|
nnrecred |
⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℝ ) |
| 242 |
240 241
|
resubcld |
⊢ ( 𝜑 → ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ∈ ℝ ) |
| 243 |
53 242
|
remulcld |
⊢ ( 𝜑 → ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ∈ ℝ ) |
| 244 |
222
|
fveq1d |
⊢ ( 𝜑 → ( ( ℝ D ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ‘ 𝑦 ) = ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑦 ) ) |
| 245 |
244
|
fveq2d |
⊢ ( 𝜑 → ( abs ‘ ( ( ℝ D ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ‘ 𝑦 ) ) = ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑦 ) ) ) |
| 246 |
245
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( ℝ D ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ‘ 𝑦 ) ) = ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑦 ) ) ) |
| 247 |
|
nfv |
⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑦 ∈ ( 0 (,) 1 ) ) |
| 248 |
|
nfcv |
⊢ Ⅎ 𝑡 abs |
| 249 |
|
nffvmpt1 |
⊢ Ⅎ 𝑡 ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑦 ) |
| 250 |
248 249
|
nffv |
⊢ Ⅎ 𝑡 ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑦 ) ) |
| 251 |
|
nfcv |
⊢ Ⅎ 𝑡 ≤ |
| 252 |
|
nfcv |
⊢ Ⅎ 𝑡 ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) |
| 253 |
250 251 252
|
nfbr |
⊢ Ⅎ 𝑡 ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑦 ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) |
| 254 |
247 253
|
nfim |
⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ 𝑦 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑦 ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) |
| 255 |
|
eleq1w |
⊢ ( 𝑡 = 𝑦 → ( 𝑡 ∈ ( 0 (,) 1 ) ↔ 𝑦 ∈ ( 0 (,) 1 ) ) ) |
| 256 |
255
|
anbi2d |
⊢ ( 𝑡 = 𝑦 → ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) ↔ ( 𝜑 ∧ 𝑦 ∈ ( 0 (,) 1 ) ) ) ) |
| 257 |
|
2fveq3 |
⊢ ( 𝑡 = 𝑦 → ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑡 ) ) = ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑦 ) ) ) |
| 258 |
257
|
breq1d |
⊢ ( 𝑡 = 𝑦 → ( ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑡 ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ↔ ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑦 ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) ) |
| 259 |
256 258
|
imbi12d |
⊢ ( 𝑡 = 𝑦 → ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑡 ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑦 ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) ) ) |
| 260 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ( 0 (,) 1 ) ) |
| 261 |
225
|
fvmpt2 |
⊢ ( ( 𝑡 ∈ ( 0 (,) 1 ) ∧ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ∈ V ) → ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑡 ) = ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) |
| 262 |
260 224 261
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑡 ) = ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) |
| 263 |
262
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑡 ) ) = ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ) |
| 264 |
164 189 192
|
subdid |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝐴 / 𝑁 ) · ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) = ( ( ( 𝐴 / 𝑁 ) · 1 ) − ( ( 𝐴 / 𝑁 ) · ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) |
| 265 |
164
|
mulridd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝐴 / 𝑁 ) · 1 ) = ( 𝐴 / 𝑁 ) ) |
| 266 |
164 192
|
mulcomd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝐴 / 𝑁 ) · ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) |
| 267 |
265 266
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( 𝐴 / 𝑁 ) · 1 ) − ( ( 𝐴 / 𝑁 ) · ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) = ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) |
| 268 |
264 267
|
eqtr2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) = ( ( 𝐴 / 𝑁 ) · ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) |
| 269 |
268
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) = ( abs ‘ ( ( 𝐴 / 𝑁 ) · ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ) |
| 270 |
161 162 163
|
absdivd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 𝐴 / 𝑁 ) ) = ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝑁 ) ) ) |
| 271 |
16
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ℝ ) |
| 272 |
65
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 0 ≤ 𝑁 ) |
| 273 |
271 272
|
absidd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ 𝑁 ) = 𝑁 ) |
| 274 |
273
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝑁 ) ) = ( ( abs ‘ 𝐴 ) / 𝑁 ) ) |
| 275 |
270 274
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 𝐴 / 𝑁 ) ) = ( ( abs ‘ 𝐴 ) / 𝑁 ) ) |
| 276 |
275
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( abs ‘ ( 𝐴 / 𝑁 ) ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) = ( ( ( abs ‘ 𝐴 ) / 𝑁 ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ) |
| 277 |
189 192
|
subcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ∈ ℂ ) |
| 278 |
164 277
|
absmuld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( 𝐴 / 𝑁 ) · ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) = ( ( abs ‘ ( 𝐴 / 𝑁 ) ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ) |
| 279 |
69
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ ) |
| 280 |
279
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ 𝐴 ) ∈ ℂ ) |
| 281 |
277
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ∈ ℝ ) |
| 282 |
281
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ∈ ℂ ) |
| 283 |
280 282 162 163
|
div23d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( abs ‘ 𝐴 ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) / 𝑁 ) = ( ( ( abs ‘ 𝐴 ) / 𝑁 ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ) |
| 284 |
276 278 283
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( 𝐴 / 𝑁 ) · ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) = ( ( ( abs ‘ 𝐴 ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) / 𝑁 ) ) |
| 285 |
263 269 284
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑡 ) ) = ( ( ( abs ‘ 𝐴 ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) / 𝑁 ) ) |
| 286 |
53
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑅 ∈ ℝ ) |
| 287 |
240
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / ( 𝑁 − 𝑅 ) ) ∈ ℝ ) |
| 288 |
241
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / 𝑁 ) ∈ ℝ ) |
| 289 |
287 288
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ∈ ℝ ) |
| 290 |
271 289
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ∈ ℝ ) |
| 291 |
15
|
absge0d |
⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝐴 ) ) |
| 292 |
291
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 0 ≤ ( abs ‘ 𝐴 ) ) |
| 293 |
277
|
absge0d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 0 ≤ ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) |
| 294 |
79
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ 𝐴 ) ≤ 𝑅 ) |
| 295 |
239
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 − 𝑅 ) ∈ ℝ+ ) |
| 296 |
231
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑅 ∈ ℝ+ ) |
| 297 |
295 296
|
rpdivcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 − 𝑅 ) / 𝑅 ) ∈ ℝ+ ) |
| 298 |
14
|
dmgmn0 |
⊢ ( 𝜑 → 𝐴 ≠ 0 ) |
| 299 |
298
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝐴 ≠ 0 ) |
| 300 |
161 162 299 163
|
divne0d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝐴 / 𝑁 ) ≠ 0 ) |
| 301 |
|
eliooord |
⊢ ( 𝑡 ∈ ( 0 (,) 1 ) → ( 0 < 𝑡 ∧ 𝑡 < 1 ) ) |
| 302 |
301
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 0 < 𝑡 ∧ 𝑡 < 1 ) ) |
| 303 |
302
|
simpld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 0 < 𝑡 ) |
| 304 |
303
|
gt0ne0d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ≠ 0 ) |
| 305 |
164 167 300 304
|
mulne0d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝐴 / 𝑁 ) · 𝑡 ) ≠ 0 ) |
| 306 |
168 305
|
reccld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ∈ ℂ ) |
| 307 |
189 306
|
addcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ∈ ℂ ) |
| 308 |
168 189 168 305
|
divdird |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) = ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) |
| 309 |
168 305
|
dividd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) = 1 ) |
| 310 |
309
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) |
| 311 |
308 310
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) = ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) |
| 312 |
190 168 191 305
|
divne0d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ≠ 0 ) |
| 313 |
311 312
|
eqnetrrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ≠ 0 ) |
| 314 |
307 313
|
absrpcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ∈ ℝ+ ) |
| 315 |
|
1red |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 1 ∈ ℝ ) |
| 316 |
|
0le1 |
⊢ 0 ≤ 1 |
| 317 |
316
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 0 ≤ 1 ) |
| 318 |
297
|
rpred |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 − 𝑅 ) / 𝑅 ) ∈ ℝ ) |
| 319 |
306
|
negcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ∈ ℂ ) |
| 320 |
319
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ∈ ℝ ) |
| 321 |
320 315
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( abs ‘ - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) − 1 ) ∈ ℝ ) |
| 322 |
307
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ∈ ℝ ) |
| 323 |
233
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑅 ∈ ℂ ) |
| 324 |
296
|
rpne0d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑅 ≠ 0 ) |
| 325 |
162 323 323 324
|
divsubdird |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 − 𝑅 ) / 𝑅 ) = ( ( 𝑁 / 𝑅 ) − ( 𝑅 / 𝑅 ) ) ) |
| 326 |
323 324
|
dividd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑅 / 𝑅 ) = 1 ) |
| 327 |
326
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 / 𝑅 ) − ( 𝑅 / 𝑅 ) ) = ( ( 𝑁 / 𝑅 ) − 1 ) ) |
| 328 |
325 327
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 − 𝑅 ) / 𝑅 ) = ( ( 𝑁 / 𝑅 ) − 1 ) ) |
| 329 |
271 296
|
rerpdivcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 / 𝑅 ) ∈ ℝ ) |
| 330 |
323 162 324 163
|
recdivd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / ( 𝑅 / 𝑁 ) ) = ( 𝑁 / 𝑅 ) ) |
| 331 |
166 92
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ≤ ( 𝑅 / 𝑁 ) ) |
| 332 |
168 305
|
absrpcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ∈ ℝ+ ) |
| 333 |
64
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ℝ+ ) |
| 334 |
296 333
|
rpdivcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑅 / 𝑁 ) ∈ ℝ+ ) |
| 335 |
332 334
|
lerecd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ≤ ( 𝑅 / 𝑁 ) ↔ ( 1 / ( 𝑅 / 𝑁 ) ) ≤ ( 1 / ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) |
| 336 |
331 335
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / ( 𝑅 / 𝑁 ) ) ≤ ( 1 / ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) |
| 337 |
330 336
|
eqbrtrrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 / 𝑅 ) ≤ ( 1 / ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) |
| 338 |
306
|
absnegd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( abs ‘ ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) |
| 339 |
189 168 305
|
absdivd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( ( abs ‘ 1 ) / ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) |
| 340 |
|
abs1 |
⊢ ( abs ‘ 1 ) = 1 |
| 341 |
340
|
oveq1i |
⊢ ( ( abs ‘ 1 ) / ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( 1 / ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) |
| 342 |
339 341
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( 1 / ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) |
| 343 |
338 342
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( 1 / ( abs ‘ ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) |
| 344 |
337 343
|
breqtrrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 / 𝑅 ) ≤ ( abs ‘ - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) |
| 345 |
329 320 315 344
|
lesub1dd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 / 𝑅 ) − 1 ) ≤ ( ( abs ‘ - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) − 1 ) ) |
| 346 |
328 345
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 − 𝑅 ) / 𝑅 ) ≤ ( ( abs ‘ - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) − 1 ) ) |
| 347 |
340
|
oveq2i |
⊢ ( ( abs ‘ - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) − ( abs ‘ 1 ) ) = ( ( abs ‘ - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) − 1 ) |
| 348 |
319 189
|
abs2difd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( abs ‘ - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) − ( abs ‘ 1 ) ) ≤ ( abs ‘ ( - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) − 1 ) ) ) |
| 349 |
347 348
|
eqbrtrrid |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( abs ‘ - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) − 1 ) ≤ ( abs ‘ ( - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) − 1 ) ) ) |
| 350 |
189 306
|
addcomd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) + 1 ) ) |
| 351 |
350
|
negeqd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → - ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = - ( ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) + 1 ) ) |
| 352 |
306 189
|
negdi2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → - ( ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) + 1 ) = ( - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) − 1 ) ) |
| 353 |
351 352
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → - ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) − 1 ) ) |
| 354 |
353
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ - ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) = ( abs ‘ ( - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) − 1 ) ) ) |
| 355 |
307
|
absnegd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ - ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) = ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) |
| 356 |
354 355
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) − 1 ) ) = ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) |
| 357 |
349 356
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( abs ‘ - ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) − 1 ) ≤ ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) |
| 358 |
318 321 322 346 357
|
letrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 − 𝑅 ) / 𝑅 ) ≤ ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) |
| 359 |
297 314 315 317 358
|
lediv2ad |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) ≤ ( 1 / ( ( 𝑁 − 𝑅 ) / 𝑅 ) ) ) |
| 360 |
17 233
|
subcld |
⊢ ( 𝜑 → ( 𝑁 − 𝑅 ) ∈ ℂ ) |
| 361 |
360
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 − 𝑅 ) ∈ ℂ ) |
| 362 |
53 236
|
gtned |
⊢ ( 𝜑 → 𝑁 ≠ 𝑅 ) |
| 363 |
17 233 362
|
subne0d |
⊢ ( 𝜑 → ( 𝑁 − 𝑅 ) ≠ 0 ) |
| 364 |
363
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 − 𝑅 ) ≠ 0 ) |
| 365 |
361 323 364 324
|
recdivd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / ( ( 𝑁 − 𝑅 ) / 𝑅 ) ) = ( 𝑅 / ( 𝑁 − 𝑅 ) ) ) |
| 366 |
162 323
|
nncand |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 − ( 𝑁 − 𝑅 ) ) = 𝑅 ) |
| 367 |
366
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 − ( 𝑁 − 𝑅 ) ) / ( 𝑁 − 𝑅 ) ) = ( 𝑅 / ( 𝑁 − 𝑅 ) ) ) |
| 368 |
162 361 361 364
|
divsubdird |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 − ( 𝑁 − 𝑅 ) ) / ( 𝑁 − 𝑅 ) ) = ( ( 𝑁 / ( 𝑁 − 𝑅 ) ) − ( ( 𝑁 − 𝑅 ) / ( 𝑁 − 𝑅 ) ) ) ) |
| 369 |
367 368
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑅 / ( 𝑁 − 𝑅 ) ) = ( ( 𝑁 / ( 𝑁 − 𝑅 ) ) − ( ( 𝑁 − 𝑅 ) / ( 𝑁 − 𝑅 ) ) ) ) |
| 370 |
361 364
|
dividd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 − 𝑅 ) / ( 𝑁 − 𝑅 ) ) = 1 ) |
| 371 |
370
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 / ( 𝑁 − 𝑅 ) ) − ( ( 𝑁 − 𝑅 ) / ( 𝑁 − 𝑅 ) ) ) = ( ( 𝑁 / ( 𝑁 − 𝑅 ) ) − 1 ) ) |
| 372 |
365 369 371
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / ( ( 𝑁 − 𝑅 ) / 𝑅 ) ) = ( ( 𝑁 / ( 𝑁 − 𝑅 ) ) − 1 ) ) |
| 373 |
359 372
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) ≤ ( ( 𝑁 / ( 𝑁 − 𝑅 ) ) − 1 ) ) |
| 374 |
190 189 190 191
|
divsubdird |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) − 1 ) / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) = ( ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) |
| 375 |
168 189
|
pncand |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) − 1 ) = ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) |
| 376 |
375
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) − 1 ) / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) = ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) |
| 377 |
190 191
|
dividd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) = 1 ) |
| 378 |
377
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) |
| 379 |
374 376 378
|
3eqtr3rd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) |
| 380 |
190 168 191 305
|
recdivd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) |
| 381 |
311
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / ( ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) = ( 1 / ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) |
| 382 |
379 380 381
|
3eqtr2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = ( 1 / ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) |
| 383 |
382
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) = ( abs ‘ ( 1 / ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) ) |
| 384 |
189 307 313
|
absdivd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 1 / ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) = ( ( abs ‘ 1 ) / ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) ) |
| 385 |
340
|
oveq1i |
⊢ ( ( abs ‘ 1 ) / ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) = ( 1 / ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) |
| 386 |
384 385
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 1 / ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) = ( 1 / ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) ) |
| 387 |
383 386
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) = ( 1 / ( abs ‘ ( 1 + ( 1 / ( ( 𝐴 / 𝑁 ) · 𝑡 ) ) ) ) ) ) |
| 388 |
360 363
|
reccld |
⊢ ( 𝜑 → ( 1 / ( 𝑁 − 𝑅 ) ) ∈ ℂ ) |
| 389 |
388
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / ( 𝑁 − 𝑅 ) ) ∈ ℂ ) |
| 390 |
241
|
recnd |
⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℂ ) |
| 391 |
390
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 / 𝑁 ) ∈ ℂ ) |
| 392 |
162 389 391
|
subdid |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) = ( ( 𝑁 · ( 1 / ( 𝑁 − 𝑅 ) ) ) − ( 𝑁 · ( 1 / 𝑁 ) ) ) ) |
| 393 |
162 361 364
|
divrecd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 / ( 𝑁 − 𝑅 ) ) = ( 𝑁 · ( 1 / ( 𝑁 − 𝑅 ) ) ) ) |
| 394 |
393
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 · ( 1 / ( 𝑁 − 𝑅 ) ) ) = ( 𝑁 / ( 𝑁 − 𝑅 ) ) ) |
| 395 |
162 163
|
recidd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 · ( 1 / 𝑁 ) ) = 1 ) |
| 396 |
394 395
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑁 · ( 1 / ( 𝑁 − 𝑅 ) ) ) − ( 𝑁 · ( 1 / 𝑁 ) ) ) = ( ( 𝑁 / ( 𝑁 − 𝑅 ) ) − 1 ) ) |
| 397 |
392 396
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑁 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) = ( ( 𝑁 / ( 𝑁 − 𝑅 ) ) − 1 ) ) |
| 398 |
373 387 397
|
3brtr4d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ≤ ( 𝑁 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) |
| 399 |
279 286 281 290 292 293 294 398
|
lemul12ad |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( abs ‘ 𝐴 ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ≤ ( 𝑅 · ( 𝑁 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) ) |
| 400 |
242
|
recnd |
⊢ ( 𝜑 → ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ∈ ℂ ) |
| 401 |
400
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ∈ ℂ ) |
| 402 |
323 162 401
|
mul12d |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑅 · ( 𝑁 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) = ( 𝑁 · ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) ) |
| 403 |
399 402
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( abs ‘ 𝐴 ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ≤ ( 𝑁 · ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) ) |
| 404 |
279 281
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( abs ‘ 𝐴 ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ∈ ℝ ) |
| 405 |
243
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ∈ ℝ ) |
| 406 |
404 405 333
|
ledivmuld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( ( abs ‘ 𝐴 ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) / 𝑁 ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ↔ ( ( abs ‘ 𝐴 ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ≤ ( 𝑁 · ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) ) ) |
| 407 |
403 406
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( abs ‘ 𝐴 ) · ( abs ‘ ( 1 − ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) / 𝑁 ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) |
| 408 |
285 407
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑡 ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) |
| 409 |
254 259 408
|
chvarfv |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( 𝑡 ∈ ( 0 (,) 1 ) ↦ ( ( 𝐴 / 𝑁 ) − ( ( 1 / ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) · ( 𝐴 / 𝑁 ) ) ) ) ‘ 𝑦 ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) |
| 410 |
246 409
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 (,) 1 ) ) → ( abs ‘ ( ( ℝ D ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) ‘ 𝑦 ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) |
| 411 |
8 9 147 227 243 410
|
dvlip |
⊢ ( ( 𝜑 ∧ ( 1 ∈ ( 0 [,] 1 ) ∧ 0 ∈ ( 0 [,] 1 ) ) ) → ( abs ‘ ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ‘ 1 ) − ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ‘ 0 ) ) ) ≤ ( ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) · ( abs ‘ ( 1 − 0 ) ) ) ) |
| 412 |
6 7 411
|
mpanr12 |
⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ‘ 1 ) − ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ‘ 0 ) ) ) ≤ ( ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) · ( abs ‘ ( 1 − 0 ) ) ) ) |
| 413 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) = ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ) |
| 414 |
|
oveq2 |
⊢ ( 𝑡 = 1 → ( ( 𝐴 / 𝑁 ) · 𝑡 ) = ( ( 𝐴 / 𝑁 ) · 1 ) ) |
| 415 |
414 178
|
sylan9eqr |
⊢ ( ( 𝜑 ∧ 𝑡 = 1 ) → ( ( 𝐴 / 𝑁 ) · 𝑡 ) = ( 𝐴 / 𝑁 ) ) |
| 416 |
415
|
fvoveq1d |
⊢ ( ( 𝜑 ∧ 𝑡 = 1 ) → ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) = ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) |
| 417 |
415 416
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑡 = 1 ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) |
| 418 |
6
|
a1i |
⊢ ( 𝜑 → 1 ∈ ( 0 [,] 1 ) ) |
| 419 |
|
ovexd |
⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ∈ V ) |
| 420 |
413 417 418 419
|
fvmptd |
⊢ ( 𝜑 → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ‘ 1 ) = ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) |
| 421 |
|
oveq2 |
⊢ ( 𝑡 = 0 → ( ( 𝐴 / 𝑁 ) · 𝑡 ) = ( ( 𝐴 / 𝑁 ) · 0 ) ) |
| 422 |
19
|
mul01d |
⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) · 0 ) = 0 ) |
| 423 |
421 422
|
sylan9eqr |
⊢ ( ( 𝜑 ∧ 𝑡 = 0 ) → ( ( 𝐴 / 𝑁 ) · 𝑡 ) = 0 ) |
| 424 |
423
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑡 = 0 ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) = ( 0 + 1 ) ) |
| 425 |
|
0p1e1 |
⊢ ( 0 + 1 ) = 1 |
| 426 |
424 425
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑡 = 0 ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) = 1 ) |
| 427 |
426
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑡 = 0 ) → ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) = ( log ‘ 1 ) ) |
| 428 |
|
log1 |
⊢ ( log ‘ 1 ) = 0 |
| 429 |
427 428
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑡 = 0 ) → ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) = 0 ) |
| 430 |
423 429
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑡 = 0 ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = ( 0 − 0 ) ) |
| 431 |
|
0m0e0 |
⊢ ( 0 − 0 ) = 0 |
| 432 |
430 431
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑡 = 0 ) → ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) = 0 ) |
| 433 |
7
|
a1i |
⊢ ( 𝜑 → 0 ∈ ( 0 [,] 1 ) ) |
| 434 |
413 432 433 433
|
fvmptd |
⊢ ( 𝜑 → ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ‘ 0 ) = 0 ) |
| 435 |
420 434
|
oveq12d |
⊢ ( 𝜑 → ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ‘ 1 ) − ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ‘ 0 ) ) = ( ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) − 0 ) ) |
| 436 |
19 138
|
addcld |
⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) + 1 ) ∈ ℂ ) |
| 437 |
14 3
|
dmgmdivn0 |
⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) + 1 ) ≠ 0 ) |
| 438 |
436 437
|
logcld |
⊢ ( 𝜑 → ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ∈ ℂ ) |
| 439 |
19 438
|
subcld |
⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ∈ ℂ ) |
| 440 |
439
|
subid1d |
⊢ ( 𝜑 → ( ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) − 0 ) = ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) |
| 441 |
435 440
|
eqtr2d |
⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) = ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ‘ 1 ) − ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ‘ 0 ) ) ) |
| 442 |
441
|
fveq2d |
⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) = ( abs ‘ ( ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ‘ 1 ) − ( ( 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) − ( log ‘ ( ( ( 𝐴 / 𝑁 ) · 𝑡 ) + 1 ) ) ) ) ‘ 0 ) ) ) ) |
| 443 |
|
1m0e1 |
⊢ ( 1 − 0 ) = 1 |
| 444 |
443
|
fveq2i |
⊢ ( abs ‘ ( 1 − 0 ) ) = ( abs ‘ 1 ) |
| 445 |
444 340
|
eqtri |
⊢ ( abs ‘ ( 1 − 0 ) ) = 1 |
| 446 |
445
|
oveq2i |
⊢ ( ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) · ( abs ‘ ( 1 − 0 ) ) ) = ( ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) · 1 ) |
| 447 |
233 400
|
mulcld |
⊢ ( 𝜑 → ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ∈ ℂ ) |
| 448 |
447
|
mulridd |
⊢ ( 𝜑 → ( ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) · 1 ) = ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) |
| 449 |
446 448
|
eqtr2id |
⊢ ( 𝜑 → ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) = ( ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) · ( abs ‘ ( 1 − 0 ) ) ) ) |
| 450 |
412 442 449
|
3brtr4d |
⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) |