Step | Hyp | Ref
| Expression |
1 | | 1elunit 12162 |
. . 3
⊢ 1 ∈
(0[,]1) |
2 | | 0elunit 12161 |
. . 3
⊢ 0 ∈
(0[,]1) |
3 | | 0red 9920 |
. . . 4
⊢ (𝜑 → 0 ∈
ℝ) |
4 | | 1red 9934 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
5 | | eqid 2610 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
6 | 5 | subcn 22477 |
. . . . . 6
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
7 | 6 | a1i 11 |
. . . . 5
⊢ (𝜑 → − ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
8 | | lgamgulm.r |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℕ) |
9 | | lgamgulm.u |
. . . . . . . . . . 11
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} |
10 | 8, 9 | lgamgulmlem1 24555 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
11 | | lgamgulm.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
12 | 10, 11 | sseldd 3569 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
13 | 12 | eldifad 3552 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
14 | | lgamgulm.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
15 | 14 | nnred 10912 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
16 | 15 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℂ) |
17 | 14 | nnne0d 10942 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ≠ 0) |
18 | 13, 16, 17 | divcld 10680 |
. . . . . . 7
⊢ (𝜑 → (𝐴 / 𝑁) ∈ ℂ) |
19 | | unitssre 12190 |
. . . . . . . . 9
⊢ (0[,]1)
⊆ ℝ |
20 | | ax-resscn 9872 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
21 | 19, 20 | sstri 3577 |
. . . . . . . 8
⊢ (0[,]1)
⊆ ℂ |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0[,]1) ⊆
ℂ) |
23 | | ssid 3587 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
24 | 23 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ⊆
ℂ) |
25 | | cncfmptc 22522 |
. . . . . . 7
⊢ (((𝐴 / 𝑁) ∈ ℂ ∧ (0[,]1) ⊆
ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ (𝐴 / 𝑁)) ∈ ((0[,]1)–cn→ℂ)) |
26 | 18, 22, 24, 25 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (𝐴 / 𝑁)) ∈ ((0[,]1)–cn→ℂ)) |
27 | | cncfmptid 22523 |
. . . . . . 7
⊢ (((0[,]1)
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ)) |
28 | 21, 24, 27 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ)) |
29 | 26, 28 | mulcncf 23023 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ ((𝐴 / 𝑁) · 𝑡)) ∈ ((0[,]1)–cn→ℂ)) |
30 | 18 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (𝐴 / 𝑁) ∈ ℂ) |
31 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1)) |
32 | 19, 31 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℝ) |
33 | 32 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℂ) |
34 | 30, 33 | mulcld 9939 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((𝐴 / 𝑁) · 𝑡) ∈ ℂ) |
35 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 1 ∈
ℂ) |
36 | 34, 35 | addcld 9938 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ) |
37 | | rere 13710 |
. . . . . . . . . . . 12
⊢ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ →
(ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (((𝐴 / 𝑁) · 𝑡) + 1)) |
38 | 37 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (0[,]1)) ∧ (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ) →
(ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (((𝐴 / 𝑁) · 𝑡) + 1)) |
39 | 36 | recld 13782 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) →
(ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℝ) |
40 | 34 | recld 13782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∈ ℝ) |
41 | 40 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∈ ℂ) |
42 | 41 | abscld 14023 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) →
(abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) ∈ ℝ) |
43 | 34 | abscld 14023 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ∈ ℝ) |
44 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 1 ∈
ℝ) |
45 | | absrele 13896 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 / 𝑁) · 𝑡) ∈ ℂ →
(abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) ≤ (abs‘((𝐴 / 𝑁) · 𝑡))) |
46 | 34, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) →
(abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) ≤ (abs‘((𝐴 / 𝑁) · 𝑡))) |
47 | 44 | rehalfcld 11156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (1 / 2) ∈
ℝ) |
48 | 8 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑅 ∈ ℝ) |
49 | 48 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 𝑅 ∈ ℝ) |
50 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 𝑁 ∈ ℕ) |
51 | 49, 50 | nndivred 10946 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (𝑅 / 𝑁) ∈ ℝ) |
52 | 18 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (abs‘(𝐴 / 𝑁)) ∈ ℝ) |
53 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘(𝐴 / 𝑁)) ∈ ℝ) |
54 | 30 | absge0d 14031 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 0 ≤
(abs‘(𝐴 / 𝑁))) |
55 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ∈
ℝ |
56 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℝ |
57 | 55, 56 | elicc2i 12110 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤
𝑡 ∧ 𝑡 ≤ 1)) |
58 | 57 | simp2bi 1070 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 ∈ (0[,]1) → 0 ≤
𝑡) |
59 | 58 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 0 ≤ 𝑡) |
60 | 13, 16, 17 | absdivd 14042 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (abs‘(𝐴 / 𝑁)) = ((abs‘𝐴) / (abs‘𝑁))) |
61 | 14 | nnrpd 11746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
62 | 61 | rpge0d 11752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 0 ≤ 𝑁) |
63 | 15, 62 | absidd 14009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (abs‘𝑁) = 𝑁) |
64 | 63 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((abs‘𝐴) / (abs‘𝑁)) = ((abs‘𝐴) / 𝑁)) |
65 | 60, 64 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((abs‘𝐴) / 𝑁) = (abs‘(𝐴 / 𝑁))) |
66 | 13 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ) |
67 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 = 𝐴 → (abs‘𝑥) = (abs‘𝐴)) |
68 | 67 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 = 𝐴 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝐴) ≤ 𝑅)) |
69 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 = 𝐴 → (𝑥 + 𝑘) = (𝐴 + 𝑘)) |
70 | 69 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 = 𝐴 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝐴 + 𝑘))) |
71 | 70 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 = 𝐴 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘)))) |
72 | 71 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 = 𝐴 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘)))) |
73 | 68, 72 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = 𝐴 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))) |
74 | 73, 9 | elrab2 3333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐴 ∈ 𝑈 ↔ (𝐴 ∈ ℂ ∧ ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))) |
75 | 74 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴 ∈ 𝑈 → ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘)))) |
76 | 11, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘)))) |
77 | 76 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (abs‘𝐴) ≤ 𝑅) |
78 | 66, 48, 61, 77 | lediv1dd 11806 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((abs‘𝐴) / 𝑁) ≤ (𝑅 / 𝑁)) |
79 | 65, 78 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (abs‘(𝐴 / 𝑁)) ≤ (𝑅 / 𝑁)) |
80 | 79 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘(𝐴 / 𝑁)) ≤ (𝑅 / 𝑁)) |
81 | 57 | simp3bi 1071 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 ∈ (0[,]1) → 𝑡 ≤ 1) |
82 | 81 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ≤ 1) |
83 | 53, 51, 32, 44, 54, 59, 80, 82 | lemul12ad 10845 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((abs‘(𝐴 / 𝑁)) · 𝑡) ≤ ((𝑅 / 𝑁) · 1)) |
84 | 30, 33 | absmuld 14041 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) = ((abs‘(𝐴 / 𝑁)) · (abs‘𝑡))) |
85 | 32, 59 | absidd 14009 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘𝑡) = 𝑡) |
86 | 85 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((abs‘(𝐴 / 𝑁)) · (abs‘𝑡)) = ((abs‘(𝐴 / 𝑁)) · 𝑡)) |
87 | 84, 86 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((abs‘(𝐴 / 𝑁)) · 𝑡) = (abs‘((𝐴 / 𝑁) · 𝑡))) |
88 | 51 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (𝑅 / 𝑁) ∈ ℂ) |
89 | 88 | mulid1d 9936 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((𝑅 / 𝑁) · 1) = (𝑅 / 𝑁)) |
90 | 83, 87, 89 | 3brtr3d 4614 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (𝑅 / 𝑁)) |
91 | | lgamgulm.l |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁) |
92 | | 2rp 11713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℝ+ |
93 | 92 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 2 ∈
ℝ+) |
94 | 48, 15, 93 | lemuldiv2d 11798 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((2 · 𝑅) ≤ 𝑁 ↔ 𝑅 ≤ (𝑁 / 2))) |
95 | 91, 94 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑅 ≤ (𝑁 / 2)) |
96 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 2 ∈
ℂ) |
97 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ≠
0 |
98 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 2 ≠ 0) |
99 | 16, 96, 98 | divrecd 10683 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2))) |
100 | 95, 99 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑅 ≤ (𝑁 · (1 / 2))) |
101 | 4 | rehalfcld 11156 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
102 | 48, 101, 61 | ledivmuld 11801 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑅 / 𝑁) ≤ (1 / 2) ↔ 𝑅 ≤ (𝑁 · (1 / 2)))) |
103 | 100, 102 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑅 / 𝑁) ≤ (1 / 2)) |
104 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (𝑅 / 𝑁) ≤ (1 / 2)) |
105 | 43, 51, 47, 90, 104 | letrd 10073 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (1 / 2)) |
106 | | halflt1 11127 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 / 2)
< 1 |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (1 / 2) <
1) |
108 | 43, 47, 44, 105, 107 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) < 1) |
109 | 42, 43, 44, 46, 108 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) →
(abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) < 1) |
110 | 40, 44 | absltd 14016 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) →
((abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) < 1 ↔ (-1 <
(ℜ‘((𝐴 / 𝑁) · 𝑡)) ∧ (ℜ‘((𝐴 / 𝑁) · 𝑡)) < 1))) |
111 | 109, 110 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (-1 <
(ℜ‘((𝐴 / 𝑁) · 𝑡)) ∧ (ℜ‘((𝐴 / 𝑁) · 𝑡)) < 1)) |
112 | 111 | simpld 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → -1 <
(ℜ‘((𝐴 / 𝑁) · 𝑡))) |
113 | 44 | renegcld 10336 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → -1 ∈
ℝ) |
114 | 113, 40 | posdifd 10493 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (-1 <
(ℜ‘((𝐴 / 𝑁) · 𝑡)) ↔ 0 < ((ℜ‘((𝐴 / 𝑁) · 𝑡)) − -1))) |
115 | 112, 114 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 0 <
((ℜ‘((𝐴 / 𝑁) · 𝑡)) − -1)) |
116 | 41, 35 | subnegd 10278 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) →
((ℜ‘((𝐴 / 𝑁) · 𝑡)) − -1) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1)) |
117 | 115, 116 | breqtrd 4609 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 0 <
((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1)) |
118 | 34, 35 | readdd 13802 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) →
(ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + (ℜ‘1))) |
119 | | re1 13742 |
. . . . . . . . . . . . . . . 16
⊢
(ℜ‘1) = 1 |
120 | 119 | oveq2i 6560 |
. . . . . . . . . . . . . . 15
⊢
((ℜ‘((𝐴 /
𝑁) · 𝑡)) + (ℜ‘1)) =
((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1) |
121 | 118, 120 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) →
(ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1)) |
122 | 117, 121 | breqtrrd 4611 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 0 <
(ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1))) |
123 | 39, 122 | elrpd 11745 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) →
(ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈
ℝ+) |
124 | 123 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (0[,]1)) ∧ (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ) →
(ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈
ℝ+) |
125 | 38, 124 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (0[,]1)) ∧ (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈
ℝ+) |
126 | 125 | ex 449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ → (((𝐴 / 𝑁) · 𝑡) + 1) ∈
ℝ+)) |
127 | | eqid 2610 |
. . . . . . . . . 10
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
128 | 127 | ellogdm 24185 |
. . . . . . . . 9
⊢ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖
(-∞(,]0)) ↔ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ ∧ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ → (((𝐴 / 𝑁) · 𝑡) + 1) ∈
ℝ+))) |
129 | 36, 126, 128 | sylanbrc 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖
(-∞(,]0))) |
130 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) = (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) |
131 | 127 | logcn 24193 |
. . . . . . . . . . 11
⊢ (log
↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖
(-∞(,]0))–cn→ℂ) |
132 | 131 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (log ↾ (ℂ
∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)) |
133 | | cncff 22504 |
. . . . . . . . . 10
⊢ ((log
↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖
(-∞(,]0))–cn→ℂ)
→ (log ↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖
(-∞(,]0))⟶ℂ) |
134 | 132, 133 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (log ↾ (ℂ
∖ (-∞(,]0))):(ℂ ∖
(-∞(,]0))⟶ℂ) |
135 | 134 | feqmptd 6159 |
. . . . . . . 8
⊢ (𝜑 → (log ↾ (ℂ
∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦))) |
136 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = (((𝐴 / 𝑁) · 𝑡) + 1) → ((log ↾ (ℂ ∖
(-∞(,]0)))‘𝑦) =
((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1))) |
137 | 129, 130,
135, 136 | fmptco 6303 |
. . . . . . 7
⊢ (𝜑 → ((log ↾ (ℂ
∖ (-∞(,]0))) ∘ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0[,]1) ↦ ((log ↾
(ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1)))) |
138 | | fvres 6117 |
. . . . . . . . 9
⊢ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖
(-∞(,]0)) → ((log ↾ (ℂ ∖
(-∞(,]0)))‘(((𝐴
/ 𝑁) · 𝑡) + 1)) = (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) |
139 | 129, 138 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((log ↾
(ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) |
140 | 139 | mpteq2dva 4672 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ ((log ↾
(ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0[,]1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) |
141 | 137, 140 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → ((log ↾ (ℂ
∖ (-∞(,]0))) ∘ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0[,]1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) |
142 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) = (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) |
143 | 129, 142 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)):(0[,]1)⟶(ℂ ∖
(-∞(,]0))) |
144 | | difss 3699 |
. . . . . . . . 9
⊢ (ℂ
∖ (-∞(,]0)) ⊆ ℂ |
145 | 5 | addcn 22476 |
. . . . . . . . . . 11
⊢ + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
146 | 145 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
147 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℂ) |
148 | | cncfmptc 22522 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ)
→ (𝑡 ∈ (0[,]1)
↦ 1) ∈ ((0[,]1)–cn→ℂ)) |
149 | 147, 22, 24, 148 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ 1) ∈
((0[,]1)–cn→ℂ)) |
150 | 5, 146, 29, 149 | cncfmpt2f 22525 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→ℂ)) |
151 | | cncffvrn 22509 |
. . . . . . . . 9
⊢
(((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→ℂ)) → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)):(0[,]1)⟶(ℂ ∖
(-∞(,]0)))) |
152 | 144, 150,
151 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)):(0[,]1)⟶(ℂ ∖
(-∞(,]0)))) |
153 | 143, 152 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→(ℂ ∖
(-∞(,]0)))) |
154 | 153, 132 | cncfco 22518 |
. . . . . 6
⊢ (𝜑 → ((log ↾ (ℂ
∖ (-∞(,]0))) ∘ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ((0[,]1)–cn→ℂ)) |
155 | 141, 154 | eqeltrrd 2689 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ((0[,]1)–cn→ℂ)) |
156 | 5, 7, 29, 155 | cncfmpt2f 22525 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) ∈ ((0[,]1)–cn→ℂ)) |
157 | 20 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ⊆
ℂ) |
158 | 19 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (0[,]1) ⊆
ℝ) |
159 | 127 | logdmn0 24186 |
. . . . . . . . . . 11
⊢ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖
(-∞(,]0)) → (((𝐴
/ 𝑁) · 𝑡) + 1) ≠ 0) |
160 | 129, 159 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ≠ 0) |
161 | 36, 160 | logcld 24121 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℂ) |
162 | 34, 161 | subcld 10271 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ℂ) |
163 | 5 | tgioo2 22414 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
164 | | iccntr 22432 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ) → ((int‘(topGen‘ran
(,)))‘(0[,]1)) = (0(,)1)) |
165 | 55, 4, 164 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1)) |
166 | 157, 158,
162, 163, 5, 165 | dvmptntr 23540 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (ℝ D (𝑡 ∈ (0(,)1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))) |
167 | | reelprrecn 9907 |
. . . . . . . . 9
⊢ ℝ
∈ {ℝ, ℂ} |
168 | 167 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
169 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝐴 ∈ ℂ) |
170 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑁 ∈ ℂ) |
171 | 17 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑁 ≠ 0) |
172 | 169, 170,
171 | divcld 10680 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝐴 / 𝑁) ∈ ℂ) |
173 | | ioossicc 12130 |
. . . . . . . . . . 11
⊢ (0(,)1)
⊆ (0[,]1) |
174 | 173 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈
(0[,]1)) |
175 | 174, 33 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ) |
176 | 172, 175 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · 𝑡) ∈ ℂ) |
177 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝐴 ∈ ℂ) |
178 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑁 ∈ ℂ) |
179 | 17 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑁 ≠ 0) |
180 | 177, 178,
179 | divcld 10680 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝐴 / 𝑁) ∈ ℂ) |
181 | 157 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ) |
182 | 180, 181 | mulcld 9939 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ((𝐴 / 𝑁) · 𝑡) ∈ ℂ) |
183 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 1 ∈
ℂ) |
184 | 168 | dvmptid 23526 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1)) |
185 | 168, 181,
183, 184, 18 | dvmptcmul 23533 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 𝑡))) = (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 1))) |
186 | 18 | mulid1d 9936 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 / 𝑁) · 1) = (𝐴 / 𝑁)) |
187 | 186 | mpteq2dv 4673 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 1)) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁))) |
188 | 185, 187 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 𝑡))) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁))) |
189 | 173, 158 | syl5ss 3579 |
. . . . . . . . 9
⊢ (𝜑 → (0(,)1) ⊆
ℝ) |
190 | | retop 22375 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) ∈ Top |
191 | | iooretop 22379 |
. . . . . . . . . . 11
⊢ (0(,)1)
∈ (topGen‘ran (,)) |
192 | | isopn3i 20696 |
. . . . . . . . . . 11
⊢
(((topGen‘ran (,)) ∈ Top ∧ (0(,)1) ∈
(topGen‘ran (,))) → ((int‘(topGen‘ran
(,)))‘(0(,)1)) = (0(,)1)) |
193 | 190, 191,
192 | mp2an 704 |
. . . . . . . . . 10
⊢
((int‘(topGen‘ran (,)))‘(0(,)1)) =
(0(,)1) |
194 | 193 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(0(,)1)) = (0(,)1)) |
195 | 168, 182,
180, 188, 189, 163, 5, 194 | dvmptres2 23531 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (𝐴 / 𝑁))) |
196 | 174, 161 | sylan2 490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℂ) |
197 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 1 ∈
ℂ) |
198 | 176, 197 | addcld 9938 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ) |
199 | 174, 160 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ≠ 0) |
200 | 198, 199 | reccld 10673 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℂ) |
201 | 200, 172 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)) ∈ ℂ) |
202 | | cnelprrecn 9908 |
. . . . . . . . . 10
⊢ ℂ
∈ {ℝ, ℂ} |
203 | 202 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
204 | 174, 129 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖
(-∞(,]0))) |
205 | | eldifi 3694 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
∈ ℂ) |
206 | 205 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0)))
→ 𝑦 ∈
ℂ) |
207 | 127 | logdmn0 24186 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
≠ 0) |
208 | 207 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0)))
→ 𝑦 ≠
0) |
209 | 206, 208 | logcld 24121 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0)))
→ (log‘𝑦) ∈
ℂ) |
210 | 206, 208 | reccld 10673 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0)))
→ (1 / 𝑦) ∈
ℂ) |
211 | 182, 183 | addcld 9938 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ) |
212 | | 0cnd 9912 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 0 ∈
ℂ) |
213 | 168, 147 | dvmptc 23527 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 1)) =
(𝑡 ∈ ℝ ↦
0)) |
214 | 168, 182,
180, 188, 183, 212, 213 | dvmptadd 23529 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) + 0))) |
215 | 18 | addid1d 10115 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 / 𝑁) + 0) = (𝐴 / 𝑁)) |
216 | 215 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) + 0)) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁))) |
217 | 214, 216 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁))) |
218 | 168, 211,
180, 217, 189, 163, 5, 194 | dvmptres2 23531 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0(,)1) ↦ (𝐴 / 𝑁))) |
219 | | fvres 6117 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → ((log ↾ (ℂ ∖
(-∞(,]0)))‘𝑦) =
(log‘𝑦)) |
220 | 219 | mpteq2ia 4668 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) ↦ ((log ↾ (ℂ ∖
(-∞(,]0)))‘𝑦))
= (𝑦 ∈ (ℂ
∖ (-∞(,]0)) ↦ (log‘𝑦)) |
221 | 135, 220 | syl6req 2661 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (log‘𝑦)) =
(log ↾ (ℂ ∖ (-∞(,]0)))) |
222 | 221 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂ D (𝑦 ∈ (ℂ ∖
(-∞(,]0)) ↦ (log‘𝑦))) = (ℂ D (log ↾ (ℂ
∖ (-∞(,]0))))) |
223 | 127 | dvlog 24197 |
. . . . . . . . . 10
⊢ (ℂ
D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦)) |
224 | 222, 223 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝜑 → (ℂ D (𝑦 ∈ (ℂ ∖
(-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦))) |
225 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = (((𝐴 / 𝑁) · 𝑡) + 1) → (log‘𝑦) = (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) |
226 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑦 = (((𝐴 / 𝑁) · 𝑡) + 1) → (1 / 𝑦) = (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) |
227 | 168, 203,
204, 172, 209, 210, 218, 224, 225, 226 | dvmptco 23541 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦
(log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) = (𝑡 ∈ (0(,)1) ↦ ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) |
228 | 168, 176,
172, 195, 196, 201, 227 | dvmptsub 23536 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))) |
229 | 166, 228 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))) |
230 | 229 | dmeqd 5248 |
. . . . 5
⊢ (𝜑 → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = dom (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))) |
231 | | ovex 6577 |
. . . . . 6
⊢ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) ∈ V |
232 | | eqid 2610 |
. . . . . 6
⊢ (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) = (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) |
233 | 231, 232 | dmmpti 5936 |
. . . . 5
⊢ dom
(𝑡 ∈ (0(,)1) ↦
((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) = (0(,)1) |
234 | 230, 233 | syl6eq 2660 |
. . . 4
⊢ (𝜑 → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (0(,)1)) |
235 | | 2re 10967 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
236 | 235 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℝ) |
237 | 236, 48 | remulcld 9949 |
. . . . . . . . 9
⊢ (𝜑 → (2 · 𝑅) ∈
ℝ) |
238 | 8 | nnrpd 11746 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
239 | 48, 238 | ltaddrpd 11781 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 < (𝑅 + 𝑅)) |
240 | 48 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℂ) |
241 | 240 | 2timesd 11152 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑅) = (𝑅 + 𝑅)) |
242 | 239, 241 | breqtrrd 4611 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 < (2 · 𝑅)) |
243 | 48, 237, 15, 242, 91 | ltletrd 10076 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 < 𝑁) |
244 | | difrp 11744 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑅 < 𝑁 ↔ (𝑁 − 𝑅) ∈
ℝ+)) |
245 | 48, 15, 244 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 < 𝑁 ↔ (𝑁 − 𝑅) ∈
ℝ+)) |
246 | 243, 245 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → (𝑁 − 𝑅) ∈
ℝ+) |
247 | 246 | rprecred 11759 |
. . . . . 6
⊢ (𝜑 → (1 / (𝑁 − 𝑅)) ∈ ℝ) |
248 | 14 | nnrecred 10943 |
. . . . . 6
⊢ (𝜑 → (1 / 𝑁) ∈ ℝ) |
249 | 247, 248 | resubcld 10337 |
. . . . 5
⊢ (𝜑 → ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)) ∈ ℝ) |
250 | 48, 249 | remulcld 9949 |
. . . 4
⊢ (𝜑 → (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ∈ ℝ) |
251 | 229 | fveq1d 6105 |
. . . . . . 7
⊢ (𝜑 → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦) = ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) |
252 | 251 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (abs‘((ℝ D
(𝑡 ∈ (0[,]1) ↦
(((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦)) = (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦))) |
253 | 252 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (0(,)1)) → (abs‘((ℝ
D (𝑡 ∈ (0[,]1) ↦
(((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦)) = (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦))) |
254 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑡(𝜑 ∧ 𝑦 ∈ (0(,)1)) |
255 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑡abs |
256 | | nffvmpt1 6111 |
. . . . . . . . 9
⊢
Ⅎ𝑡((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦) |
257 | 255, 256 | nffv 6110 |
. . . . . . . 8
⊢
Ⅎ𝑡(abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) |
258 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑡
≤ |
259 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) |
260 | 257, 258,
259 | nfbr 4629 |
. . . . . . 7
⊢
Ⅎ𝑡(abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) |
261 | 254, 260 | nfim 1813 |
. . . . . 6
⊢
Ⅎ𝑡((𝜑 ∧ 𝑦 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) |
262 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑡 = 𝑦 → (𝑡 ∈ (0(,)1) ↔ 𝑦 ∈ (0(,)1))) |
263 | 262 | anbi2d 736 |
. . . . . . 7
⊢ (𝑡 = 𝑦 → ((𝜑 ∧ 𝑡 ∈ (0(,)1)) ↔ (𝜑 ∧ 𝑦 ∈ (0(,)1)))) |
264 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑡 = 𝑦 → ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡) = ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) |
265 | 264 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑡 = 𝑦 → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) = (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦))) |
266 | 265 | breq1d 4593 |
. . . . . . 7
⊢ (𝑡 = 𝑦 → ((abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ↔ (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))) |
267 | 263, 266 | imbi12d 333 |
. . . . . 6
⊢ (𝑡 = 𝑦 → (((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) ↔ ((𝜑 ∧ 𝑦 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))))) |
268 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0(,)1)) |
269 | 232 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ (0(,)1) ∧ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) ∈ V) → ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡) = ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) |
270 | 268, 231,
269 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡) = ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) |
271 | 270 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) = (abs‘((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))) |
272 | 172, 197,
200 | subdid 10365 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = (((𝐴 / 𝑁) · 1) − ((𝐴 / 𝑁) · (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) |
273 | 172 | mulid1d 9936 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · 1) = (𝐴 / 𝑁)) |
274 | 172, 200 | mulcomd 9940 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) |
275 | 273, 274 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 1) − ((𝐴 / 𝑁) · (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) |
276 | 272, 275 | eqtr2d 2645 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) = ((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) |
277 | 276 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) = (abs‘((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))))) |
278 | 169, 170,
171 | absdivd 14042 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(𝐴 / 𝑁)) = ((abs‘𝐴) / (abs‘𝑁))) |
279 | 15 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑁 ∈ ℝ) |
280 | 62 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 0 ≤ 𝑁) |
281 | 279, 280 | absidd 14009 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘𝑁) = 𝑁) |
282 | 281 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘𝐴) / (abs‘𝑁)) = ((abs‘𝐴) / 𝑁)) |
283 | 278, 282 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(𝐴 / 𝑁)) = ((abs‘𝐴) / 𝑁)) |
284 | 283 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘(𝐴 / 𝑁)) · (abs‘(1 − (1 /
(((𝐴 / 𝑁) · 𝑡) + 1))))) = (((abs‘𝐴) / 𝑁) · (abs‘(1 − (1 /
(((𝐴 / 𝑁) · 𝑡) + 1)))))) |
285 | 197, 200 | subcld 10271 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 − (1 /
(((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ℂ) |
286 | 172, 285 | absmuld 14041 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) = ((abs‘(𝐴 / 𝑁)) · (abs‘(1 − (1 /
(((𝐴 / 𝑁) · 𝑡) + 1)))))) |
287 | 66 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘𝐴) ∈
ℝ) |
288 | 287 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘𝐴) ∈
ℂ) |
289 | 285 | abscld 14023 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 −
(1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) ∈ ℝ) |
290 | 289 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 −
(1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) ∈ ℂ) |
291 | 288, 290,
170, 171 | div23d 10717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((abs‘𝐴) · (abs‘(1 −
(1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁) = (((abs‘𝐴) / 𝑁) · (abs‘(1 − (1 /
(((𝐴 / 𝑁) · 𝑡) + 1)))))) |
292 | 284, 286,
291 | 3eqtr4d 2654 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) = (((abs‘𝐴) · (abs‘(1 − (1 /
(((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁)) |
293 | 271, 277,
292 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) = (((abs‘𝐴) · (abs‘(1 − (1 /
(((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁)) |
294 | 48 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑅 ∈ ℝ) |
295 | 247 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (𝑁 − 𝑅)) ∈ ℝ) |
296 | 248 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / 𝑁) ∈
ℝ) |
297 | 295, 296 | resubcld 10337 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)) ∈ ℝ) |
298 | 279, 297 | remulcld 9949 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ∈ ℝ) |
299 | 13 | absge0d 14031 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ (abs‘𝐴)) |
300 | 299 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 0 ≤
(abs‘𝐴)) |
301 | 285 | absge0d 14031 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 0 ≤ (abs‘(1
− (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) |
302 | 77 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘𝐴) ≤ 𝑅) |
303 | 246 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 − 𝑅) ∈
ℝ+) |
304 | 238 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑅 ∈
ℝ+) |
305 | 303, 304 | rpdivcld 11765 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / 𝑅) ∈
ℝ+) |
306 | 12 | dmgmn0 24552 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ≠ 0) |
307 | 306 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝐴 ≠ 0) |
308 | 169, 170,
307, 171 | divne0d 10696 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝐴 / 𝑁) ≠ 0) |
309 | | eliooord 12104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ (0(,)1) → (0 <
𝑡 ∧ 𝑡 < 1)) |
310 | 309 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (0 < 𝑡 ∧ 𝑡 < 1)) |
311 | 310 | simpld 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 0 < 𝑡) |
312 | 311 | gt0ne0d 10471 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ≠ 0) |
313 | 172, 175,
308, 312 | mulne0d 10558 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · 𝑡) ≠ 0) |
314 | 176, 313 | reccld 10673 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / ((𝐴 / 𝑁) · 𝑡)) ∈ ℂ) |
315 | 197, 314 | addcld 9938 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 + (1 / ((𝐴 / 𝑁) · 𝑡))) ∈ ℂ) |
316 | 176, 197,
176, 313 | divdird 10718 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡)) = ((((𝐴 / 𝑁) · 𝑡) / ((𝐴 / 𝑁) · 𝑡)) + (1 / ((𝐴 / 𝑁) · 𝑡)))) |
317 | 176, 313 | dividd 10678 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) / ((𝐴 / 𝑁) · 𝑡)) = 1) |
318 | 317 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) / ((𝐴 / 𝑁) · 𝑡)) + (1 / ((𝐴 / 𝑁) · 𝑡))) = (1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) |
319 | 316, 318 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡)) = (1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) |
320 | 198, 176,
199, 313 | divne0d 10696 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡)) ≠ 0) |
321 | 319, 320 | eqnetrrd 2850 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 + (1 / ((𝐴 / 𝑁) · 𝑡))) ≠ 0) |
322 | 315, 321 | absrpcld 14035 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 + (1 /
((𝐴 / 𝑁) · 𝑡)))) ∈
ℝ+) |
323 | | 1red 9934 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 1 ∈
ℝ) |
324 | | 0le1 10430 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
1 |
325 | 324 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 0 ≤
1) |
326 | 305 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / 𝑅) ∈ ℝ) |
327 | 314 | negcld 10258 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → -(1 / ((𝐴 / 𝑁) · 𝑡)) ∈ ℂ) |
328 | 327 | abscld 14023 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘-(1 /
((𝐴 / 𝑁) · 𝑡))) ∈ ℝ) |
329 | 328, 323 | resubcld 10337 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘-(1 /
((𝐴 / 𝑁) · 𝑡))) − 1) ∈
ℝ) |
330 | 315 | abscld 14023 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 + (1 /
((𝐴 / 𝑁) · 𝑡)))) ∈ ℝ) |
331 | 240 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑅 ∈ ℂ) |
332 | 304 | rpne0d 11753 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑅 ≠ 0) |
333 | 170, 331,
331, 332 | divsubdird 10719 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / 𝑅) = ((𝑁 / 𝑅) − (𝑅 / 𝑅))) |
334 | 331, 332 | dividd 10678 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑅 / 𝑅) = 1) |
335 | 334 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 / 𝑅) − (𝑅 / 𝑅)) = ((𝑁 / 𝑅) − 1)) |
336 | 333, 335 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / 𝑅) = ((𝑁 / 𝑅) − 1)) |
337 | 279, 304 | rerpdivcld 11779 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 / 𝑅) ∈ ℝ) |
338 | 331, 170,
332, 171 | recdivd 10697 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (𝑅 / 𝑁)) = (𝑁 / 𝑅)) |
339 | 174, 90 | sylan2 490 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (𝑅 / 𝑁)) |
340 | 176, 313 | absrpcld 14035 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ∈
ℝ+) |
341 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑁 ∈
ℝ+) |
342 | 304, 341 | rpdivcld 11765 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑅 / 𝑁) ∈
ℝ+) |
343 | 340, 342 | lerecd 11767 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (𝑅 / 𝑁) ↔ (1 / (𝑅 / 𝑁)) ≤ (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))) |
344 | 339, 343 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (𝑅 / 𝑁)) ≤ (1 / (abs‘((𝐴 / 𝑁) · 𝑡)))) |
345 | 338, 344 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 / 𝑅) ≤ (1 / (abs‘((𝐴 / 𝑁) · 𝑡)))) |
346 | 314 | absnegd 14036 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘-(1 /
((𝐴 / 𝑁) · 𝑡))) = (abs‘(1 / ((𝐴 / 𝑁) · 𝑡)))) |
347 | 197, 176,
313 | absdivd 14042 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 /
((𝐴 / 𝑁) · 𝑡))) = ((abs‘1) / (abs‘((𝐴 / 𝑁) · 𝑡)))) |
348 | | abs1 13885 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(abs‘1) = 1 |
349 | 348 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . 19
⊢
((abs‘1) / (abs‘((𝐴 / 𝑁) · 𝑡))) = (1 / (abs‘((𝐴 / 𝑁) · 𝑡))) |
350 | 347, 349 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 /
((𝐴 / 𝑁) · 𝑡))) = (1 / (abs‘((𝐴 / 𝑁) · 𝑡)))) |
351 | 346, 350 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘-(1 /
((𝐴 / 𝑁) · 𝑡))) = (1 / (abs‘((𝐴 / 𝑁) · 𝑡)))) |
352 | 345, 351 | breqtrrd 4611 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 / 𝑅) ≤ (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡)))) |
353 | 337, 328,
323, 352 | lesub1dd 10522 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 / 𝑅) − 1) ≤ ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1)) |
354 | 336, 353 | eqbrtrd 4605 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / 𝑅) ≤ ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1)) |
355 | 348 | oveq2i 6560 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − (abs‘1)) = ((abs‘-(1
/ ((𝐴 / 𝑁) · 𝑡))) − 1) |
356 | 327, 197 | abs2difd 14044 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘-(1 /
((𝐴 / 𝑁) · 𝑡))) − (abs‘1)) ≤
(abs‘(-(1 / ((𝐴 /
𝑁) · 𝑡)) − 1))) |
357 | 355, 356 | syl5eqbrr 4619 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘-(1 /
((𝐴 / 𝑁) · 𝑡))) − 1) ≤ (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1))) |
358 | 197, 314 | addcomd 10117 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 + (1 / ((𝐴 / 𝑁) · 𝑡))) = ((1 / ((𝐴 / 𝑁) · 𝑡)) + 1)) |
359 | 358 | negeqd 10154 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → -(1 + (1 / ((𝐴 / 𝑁) · 𝑡))) = -((1 / ((𝐴 / 𝑁) · 𝑡)) + 1)) |
360 | 314, 197 | negdi2d 10285 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → -((1 / ((𝐴 / 𝑁) · 𝑡)) + 1) = (-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)) |
361 | 359, 360 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → -(1 + (1 / ((𝐴 / 𝑁) · 𝑡))) = (-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)) |
362 | 361 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘-(1 + (1 /
((𝐴 / 𝑁) · 𝑡)))) = (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1))) |
363 | 315 | absnegd 14036 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘-(1 + (1 /
((𝐴 / 𝑁) · 𝑡)))) = (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) |
364 | 362, 363 | eqtr3d 2646 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(-(1 /
((𝐴 / 𝑁) · 𝑡)) − 1)) = (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) |
365 | 357, 364 | breqtrd 4609 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘-(1 /
((𝐴 / 𝑁) · 𝑡))) − 1) ≤ (abs‘(1 + (1 /
((𝐴 / 𝑁) · 𝑡))))) |
366 | 326, 329,
330, 354, 365 | letrd 10073 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / 𝑅) ≤ (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) |
367 | 305, 322,
323, 325, 366 | lediv2ad 11770 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (abs‘(1 +
(1 / ((𝐴 / 𝑁) · 𝑡))))) ≤ (1 / ((𝑁 − 𝑅) / 𝑅))) |
368 | 16, 240 | subcld 10271 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − 𝑅) ∈ ℂ) |
369 | 368 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 − 𝑅) ∈ ℂ) |
370 | 48, 243 | gtned 10051 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ≠ 𝑅) |
371 | 16, 240, 370 | subne0d 10280 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − 𝑅) ≠ 0) |
372 | 371 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 − 𝑅) ≠ 0) |
373 | 369, 331,
372, 332 | recdivd 10697 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / ((𝑁 − 𝑅) / 𝑅)) = (𝑅 / (𝑁 − 𝑅))) |
374 | 170, 331 | nncand 10276 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 − (𝑁 − 𝑅)) = 𝑅) |
375 | 374 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − (𝑁 − 𝑅)) / (𝑁 − 𝑅)) = (𝑅 / (𝑁 − 𝑅))) |
376 | 170, 369,
369, 372 | divsubdird 10719 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − (𝑁 − 𝑅)) / (𝑁 − 𝑅)) = ((𝑁 / (𝑁 − 𝑅)) − ((𝑁 − 𝑅) / (𝑁 − 𝑅)))) |
377 | 375, 376 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑅 / (𝑁 − 𝑅)) = ((𝑁 / (𝑁 − 𝑅)) − ((𝑁 − 𝑅) / (𝑁 − 𝑅)))) |
378 | 369, 372 | dividd 10678 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / (𝑁 − 𝑅)) = 1) |
379 | 378 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 / (𝑁 − 𝑅)) − ((𝑁 − 𝑅) / (𝑁 − 𝑅))) = ((𝑁 / (𝑁 − 𝑅)) − 1)) |
380 | 373, 377,
379 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / ((𝑁 − 𝑅) / 𝑅)) = ((𝑁 / (𝑁 − 𝑅)) − 1)) |
381 | 367, 380 | breqtrd 4609 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (abs‘(1 +
(1 / ((𝐴 / 𝑁) · 𝑡))))) ≤ ((𝑁 / (𝑁 − 𝑅)) − 1)) |
382 | 198, 197,
198, 199 | divsubdird 10719 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((((𝐴 / 𝑁) · 𝑡) + 1) − 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) = (((((𝐴 / 𝑁) · 𝑡) + 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) |
383 | 176, 197 | pncand 10272 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) − 1) = ((𝐴 / 𝑁) · 𝑡)) |
384 | 383 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((((𝐴 / 𝑁) · 𝑡) + 1) − 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) = (((𝐴 / 𝑁) · 𝑡) / (((𝐴 / 𝑁) · 𝑡) + 1))) |
385 | 198, 199 | dividd 10678 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) = 1) |
386 | 385 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((((𝐴 / 𝑁) · 𝑡) + 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) |
387 | 382, 384,
386 | 3eqtr3rd 2653 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 − (1 /
(((𝐴 / 𝑁) · 𝑡) + 1))) = (((𝐴 / 𝑁) · 𝑡) / (((𝐴 / 𝑁) · 𝑡) + 1))) |
388 | 198, 176,
199, 313 | recdivd 10697 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡))) = (((𝐴 / 𝑁) · 𝑡) / (((𝐴 / 𝑁) · 𝑡) + 1))) |
389 | 319 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡))) = (1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) |
390 | 387, 388,
389 | 3eqtr2d 2650 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 − (1 /
(((𝐴 / 𝑁) · 𝑡) + 1))) = (1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) |
391 | 390 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 −
(1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = (abs‘(1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))) |
392 | 197, 315,
321 | absdivd 14042 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 / (1 +
(1 / ((𝐴 / 𝑁) · 𝑡))))) = ((abs‘1) / (abs‘(1 + (1 /
((𝐴 / 𝑁) · 𝑡)))))) |
393 | 348 | oveq1i 6559 |
. . . . . . . . . . . . 13
⊢
((abs‘1) / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) = (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) |
394 | 392, 393 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 / (1 +
(1 / ((𝐴 / 𝑁) · 𝑡))))) = (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))) |
395 | 391, 394 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 −
(1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))) |
396 | 368, 371 | reccld 10673 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 / (𝑁 − 𝑅)) ∈ ℂ) |
397 | 396 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (𝑁 − 𝑅)) ∈ ℂ) |
398 | 248 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 / 𝑁) ∈ ℂ) |
399 | 398 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / 𝑁) ∈
ℂ) |
400 | 170, 397,
399 | subdid 10365 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) = ((𝑁 · (1 / (𝑁 − 𝑅))) − (𝑁 · (1 / 𝑁)))) |
401 | 170, 369,
372 | divrecd 10683 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 / (𝑁 − 𝑅)) = (𝑁 · (1 / (𝑁 − 𝑅)))) |
402 | 401 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 · (1 / (𝑁 − 𝑅))) = (𝑁 / (𝑁 − 𝑅))) |
403 | 170, 171 | recidd 10675 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 · (1 / 𝑁)) = 1) |
404 | 402, 403 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 · (1 / (𝑁 − 𝑅))) − (𝑁 · (1 / 𝑁))) = ((𝑁 / (𝑁 − 𝑅)) − 1)) |
405 | 400, 404 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) = ((𝑁 / (𝑁 − 𝑅)) − 1)) |
406 | 381, 395,
405 | 3brtr4d 4615 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 −
(1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) ≤ (𝑁 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) |
407 | 287, 294,
289, 298, 300, 301, 302, 406 | lemul12ad 10845 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘𝐴) · (abs‘(1 −
(1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ≤ (𝑅 · (𝑁 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))) |
408 | 249 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)) ∈ ℂ) |
409 | 408 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)) ∈ ℂ) |
410 | 331, 170,
409 | mul12d 10124 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑅 · (𝑁 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) = (𝑁 · (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))) |
411 | 407, 410 | breqtrd 4609 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘𝐴) · (abs‘(1 −
(1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ≤ (𝑁 · (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))) |
412 | 287, 289 | remulcld 9949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘𝐴) · (abs‘(1 −
(1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ∈ ℝ) |
413 | 250 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ∈ ℝ) |
414 | 412, 413,
341 | ledivmuld 11801 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((abs‘𝐴) · (abs‘(1 −
(1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ↔ ((abs‘𝐴) · (abs‘(1 − (1 /
(((𝐴 / 𝑁) · 𝑡) + 1))))) ≤ (𝑁 · (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))))) |
415 | 411, 414 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((abs‘𝐴) · (abs‘(1 −
(1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) |
416 | 293, 415 | eqbrtrd 4605 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) |
417 | 261, 267,
416 | chvar 2250 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) |
418 | 253, 417 | eqbrtrd 4605 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (0(,)1)) → (abs‘((ℝ
D (𝑡 ∈ (0[,]1) ↦
(((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) |
419 | 3, 4, 156, 234, 250, 418 | dvlip 23560 |
. . 3
⊢ ((𝜑 ∧ (1 ∈ (0[,]1) ∧ 0
∈ (0[,]1))) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0))) ≤ ((𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) · (abs‘(1 −
0)))) |
420 | 1, 2, 419 | mpanr12 717 |
. 2
⊢ (𝜑 → (abs‘(((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0))) ≤ ((𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) · (abs‘(1 −
0)))) |
421 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) = (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) |
422 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑡 = 1 → ((𝐴 / 𝑁) · 𝑡) = ((𝐴 / 𝑁) · 1)) |
423 | 422, 186 | sylan9eqr 2666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 = 1) → ((𝐴 / 𝑁) · 𝑡) = (𝐴 / 𝑁)) |
424 | 423 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 = 1) → (((𝐴 / 𝑁) · 𝑡) + 1) = ((𝐴 / 𝑁) + 1)) |
425 | 424 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 = 1) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘((𝐴 / 𝑁) + 1))) |
426 | 423, 425 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 = 1) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) = ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) |
427 | 1 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 1 ∈
(0[,]1)) |
428 | | ovex 6577 |
. . . . . . 7
⊢ ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) ∈ V |
429 | 428 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) ∈ V) |
430 | 421, 426,
427, 429 | fvmptd 6197 |
. . . . 5
⊢ (𝜑 → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) = ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) |
431 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑡 = 0 → ((𝐴 / 𝑁) · 𝑡) = ((𝐴 / 𝑁) · 0)) |
432 | 18 | mul01d 10114 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 / 𝑁) · 0) = 0) |
433 | 431, 432 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 = 0) → ((𝐴 / 𝑁) · 𝑡) = 0) |
434 | 433 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) + 1) = (0 + 1)) |
435 | | 0p1e1 11009 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
436 | 434, 435 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) + 1) = 1) |
437 | 436 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 = 0) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘1)) |
438 | | log1 24136 |
. . . . . . . . 9
⊢
(log‘1) = 0 |
439 | 437, 438 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 = 0) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) = 0) |
440 | 433, 439 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) = (0 − 0)) |
441 | | 0m0e0 11007 |
. . . . . . 7
⊢ (0
− 0) = 0 |
442 | 440, 441 | syl6eq 2660 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) = 0) |
443 | 2 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈
(0[,]1)) |
444 | 421, 442,
443, 443 | fvmptd 6197 |
. . . . 5
⊢ (𝜑 → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0) = 0) |
445 | 430, 444 | oveq12d 6567 |
. . . 4
⊢ (𝜑 → (((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0)) = (((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) − 0)) |
446 | 18, 147 | addcld 9938 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 / 𝑁) + 1) ∈ ℂ) |
447 | 12, 14 | dmgmdivn0 24554 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 / 𝑁) + 1) ≠ 0) |
448 | 446, 447 | logcld 24121 |
. . . . . 6
⊢ (𝜑 → (log‘((𝐴 / 𝑁) + 1)) ∈ ℂ) |
449 | 18, 448 | subcld 10271 |
. . . . 5
⊢ (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) ∈ ℂ) |
450 | 449 | subid1d 10260 |
. . . 4
⊢ (𝜑 → (((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) − 0) = ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) |
451 | 445, 450 | eqtr2d 2645 |
. . 3
⊢ (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) = (((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0))) |
452 | 451 | fveq2d 6107 |
. 2
⊢ (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) = (abs‘(((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0)))) |
453 | | 1m0e1 11008 |
. . . . . 6
⊢ (1
− 0) = 1 |
454 | 453 | fveq2i 6106 |
. . . . 5
⊢
(abs‘(1 − 0)) = (abs‘1) |
455 | 454, 348 | eqtri 2632 |
. . . 4
⊢
(abs‘(1 − 0)) = 1 |
456 | 455 | oveq2i 6560 |
. . 3
⊢ ((𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))) =
((𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) · 1) |
457 | 240, 408 | mulcld 9939 |
. . . 4
⊢ (𝜑 → (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ∈ ℂ) |
458 | 457 | mulid1d 9936 |
. . 3
⊢ (𝜑 → ((𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) · 1) = (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) |
459 | 456, 458 | syl5req 2657 |
. 2
⊢ (𝜑 → (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) = ((𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) · (abs‘(1 −
0)))) |
460 | 420, 452,
459 | 3brtr4d 4615 |
1
⊢ (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) |