Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. 2
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
2 | | sinccvg.5 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℕ) |
3 | 2 | nnzd 12526 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
4 | | sinccvg.2 |
. . . 4
⊢ (𝜑 → 𝐹 ⇝ 0) |
5 | | sinccvg.4 |
. . . . . 6
⊢ 𝐻 = (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3))) |
6 | 5 | funmpt2 6540 |
. . . . 5
⊢ Fun 𝐻 |
7 | | sinccvg.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ∖
{0})) |
8 | | nnex 12159 |
. . . . . 6
⊢ ℕ
∈ V |
9 | | fex 7176 |
. . . . . 6
⊢ ((𝐹:ℕ⟶(ℝ ∖
{0}) ∧ ℕ ∈ V) → 𝐹 ∈ V) |
10 | 7, 8, 9 | sylancl 586 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ V) |
11 | | cofunexg 7881 |
. . . . 5
⊢ ((Fun
𝐻 ∧ 𝐹 ∈ V) → (𝐻 ∘ 𝐹) ∈ V) |
12 | 6, 10, 11 | sylancr 587 |
. . . 4
⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ V) |
13 | 7 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝐹:ℕ⟶(ℝ ∖
{0})) |
14 | | eluznn 12843 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑀)) → 𝑘 ∈ ℕ) |
15 | 2, 14 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ) |
16 | 13, 15 | ffvelcdmd 7036 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ (ℝ ∖
{0})) |
17 | | eldifsn 4747 |
. . . . . . 7
⊢ ((𝐹‘𝑘) ∈ (ℝ ∖ {0}) ↔ ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) ≠ 0)) |
18 | 16, 17 | sylib 217 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) ≠ 0)) |
19 | 18 | simpld 495 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℝ) |
20 | 19 | recnd 11183 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
21 | | ax-1cn 11109 |
. . . . . 6
⊢ 1 ∈
ℂ |
22 | | sqcl 14023 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈
ℂ) |
23 | | 3cn 12234 |
. . . . . . . 8
⊢ 3 ∈
ℂ |
24 | | 3ne0 12259 |
. . . . . . . 8
⊢ 3 ≠
0 |
25 | | divcl 11819 |
. . . . . . . 8
⊢ (((𝑥↑2) ∈ ℂ ∧ 3
∈ ℂ ∧ 3 ≠ 0) → ((𝑥↑2) / 3) ∈
ℂ) |
26 | 23, 24, 25 | mp3an23 1453 |
. . . . . . 7
⊢ ((𝑥↑2) ∈ ℂ →
((𝑥↑2) / 3) ∈
ℂ) |
27 | 22, 26 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) / 3) ∈
ℂ) |
28 | | subcl 11400 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ ((𝑥↑2) / 3) ∈ ℂ) → (1
− ((𝑥↑2) / 3))
∈ ℂ) |
29 | 21, 27, 28 | sylancr 587 |
. . . . 5
⊢ (𝑥 ∈ ℂ → (1
− ((𝑥↑2) / 3))
∈ ℂ) |
30 | 5, 29 | fmpti 7060 |
. . . 4
⊢ 𝐻:ℂ⟶ℂ |
31 | | eqid 2736 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
32 | 31 | cnfldtopon 24146 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
33 | 32 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
34 | | 1cnd 11150 |
. . . . . . . . 9
⊢ (⊤
→ 1 ∈ ℂ) |
35 | 33, 33, 34 | cnmptc 23013 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ 1) ∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
36 | 31 | sqcn 24237 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
37 | 36 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ (𝑥↑2)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
38 | 31 | divccn 24236 |
. . . . . . . . . . 11
⊢ ((3
∈ ℂ ∧ 3 ≠ 0) → (𝑦 ∈ ℂ ↦ (𝑦 / 3)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
39 | 23, 24, 38 | mp2an 690 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ ↦ (𝑦 / 3)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
40 | 39 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (𝑦 ∈ ℂ
↦ (𝑦 / 3)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
41 | | oveq1 7364 |
. . . . . . . . 9
⊢ (𝑦 = (𝑥↑2) → (𝑦 / 3) = ((𝑥↑2) / 3)) |
42 | 33, 37, 33, 40, 41 | cnmpt11 23014 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ ((𝑥↑2) / 3))
∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
43 | 31 | subcn 24229 |
. . . . . . . . 9
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
44 | 43 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ − ∈ (((TopOpen‘ℂfld)
×t (TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
45 | 33, 35, 42, 44 | cnmpt12f 23017 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ (1 − ((𝑥↑2) / 3))) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
46 | 45 | mptru 1548 |
. . . . . 6
⊢ (𝑥 ∈ ℂ ↦ (1
− ((𝑥↑2) / 3)))
∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
47 | 31 | cncfcn1 24274 |
. . . . . 6
⊢
(ℂ–cn→ℂ) =
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
48 | 46, 5, 47 | 3eltr4i 2851 |
. . . . 5
⊢ 𝐻 ∈ (ℂ–cn→ℂ) |
49 | | cncfi 24257 |
. . . . 5
⊢ ((𝐻 ∈ (ℂ–cn→ℂ) ∧ 0 ∈ ℂ ∧
𝑦 ∈
ℝ+) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℂ
((abs‘(𝑤 − 0))
< 𝑧 →
(abs‘((𝐻‘𝑤) − (𝐻‘0))) < 𝑦)) |
50 | 48, 49 | mp3an1 1448 |
. . . 4
⊢ ((0
∈ ℂ ∧ 𝑦
∈ ℝ+) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℂ
((abs‘(𝑤 − 0))
< 𝑧 →
(abs‘((𝐻‘𝑤) − (𝐻‘0))) < 𝑦)) |
51 | | fvco3 6940 |
. . . . . 6
⊢ ((𝐹:ℕ⟶(ℝ ∖
{0}) ∧ 𝑘 ∈
ℕ) → ((𝐻 ∘
𝐹)‘𝑘) = (𝐻‘(𝐹‘𝑘))) |
52 | 7, 51 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐻 ∘ 𝐹)‘𝑘) = (𝐻‘(𝐹‘𝑘))) |
53 | 15, 52 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐻 ∘ 𝐹)‘𝑘) = (𝐻‘(𝐹‘𝑘))) |
54 | 1, 4, 12, 3, 20, 30, 50, 53 | climcn1lem 15485 |
. . 3
⊢ (𝜑 → (𝐻 ∘ 𝐹) ⇝ (𝐻‘0)) |
55 | | 0cn 11147 |
. . . 4
⊢ 0 ∈
ℂ |
56 | | sq0i 14097 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥↑2) = 0) |
57 | 56 | oveq1d 7372 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑥↑2) / 3) = (0 / 3)) |
58 | 23, 24 | div0i 11889 |
. . . . . . . 8
⊢ (0 / 3) =
0 |
59 | 57, 58 | eqtrdi 2792 |
. . . . . . 7
⊢ (𝑥 = 0 → ((𝑥↑2) / 3) = 0) |
60 | 59 | oveq2d 7373 |
. . . . . 6
⊢ (𝑥 = 0 → (1 − ((𝑥↑2) / 3)) = (1 −
0)) |
61 | | 1m0e1 12274 |
. . . . . 6
⊢ (1
− 0) = 1 |
62 | 60, 61 | eqtrdi 2792 |
. . . . 5
⊢ (𝑥 = 0 → (1 − ((𝑥↑2) / 3)) =
1) |
63 | | 1ex 11151 |
. . . . 5
⊢ 1 ∈
V |
64 | 62, 5, 63 | fvmpt 6948 |
. . . 4
⊢ (0 ∈
ℂ → (𝐻‘0)
= 1) |
65 | 55, 64 | ax-mp 5 |
. . 3
⊢ (𝐻‘0) = 1 |
66 | 54, 65 | breqtrdi 5146 |
. 2
⊢ (𝜑 → (𝐻 ∘ 𝐹) ⇝ 1) |
67 | | sinccvg.3 |
. . . 4
⊢ 𝐺 = (𝑥 ∈ (ℝ ∖ {0}) ↦
((sin‘𝑥) / 𝑥)) |
68 | 67 | funmpt2 6540 |
. . 3
⊢ Fun 𝐺 |
69 | | cofunexg 7881 |
. . 3
⊢ ((Fun
𝐺 ∧ 𝐹 ∈ V) → (𝐺 ∘ 𝐹) ∈ V) |
70 | 68, 10, 69 | sylancr 587 |
. 2
⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ V) |
71 | | oveq1 7364 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑘) → (𝑥↑2) = ((𝐹‘𝑘)↑2)) |
72 | 71 | oveq1d 7372 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑘) → ((𝑥↑2) / 3) = (((𝐹‘𝑘)↑2) / 3)) |
73 | 72 | oveq2d 7373 |
. . . . . 6
⊢ (𝑥 = (𝐹‘𝑘) → (1 − ((𝑥↑2) / 3)) = (1 − (((𝐹‘𝑘)↑2) / 3))) |
74 | | ovex 7390 |
. . . . . 6
⊢ (1
− (((𝐹‘𝑘)↑2) / 3)) ∈
V |
75 | 73, 5, 74 | fvmpt 6948 |
. . . . 5
⊢ ((𝐹‘𝑘) ∈ ℂ → (𝐻‘(𝐹‘𝑘)) = (1 − (((𝐹‘𝑘)↑2) / 3))) |
76 | 20, 75 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘(𝐹‘𝑘)) = (1 − (((𝐹‘𝑘)↑2) / 3))) |
77 | 53, 76 | eqtrd 2776 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐻 ∘ 𝐹)‘𝑘) = (1 − (((𝐹‘𝑘)↑2) / 3))) |
78 | | 1re 11155 |
. . . 4
⊢ 1 ∈
ℝ |
79 | 19 | resqcld 14030 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐹‘𝑘)↑2) ∈ ℝ) |
80 | | 3nn 12232 |
. . . . 5
⊢ 3 ∈
ℕ |
81 | | nndivre 12194 |
. . . . 5
⊢ ((((𝐹‘𝑘)↑2) ∈ ℝ ∧ 3 ∈
ℕ) → (((𝐹‘𝑘)↑2) / 3) ∈
ℝ) |
82 | 79, 80, 81 | sylancl 586 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (((𝐹‘𝑘)↑2) / 3) ∈
ℝ) |
83 | | resubcl 11465 |
. . . 4
⊢ ((1
∈ ℝ ∧ (((𝐹‘𝑘)↑2) / 3) ∈ ℝ) → (1
− (((𝐹‘𝑘)↑2) / 3)) ∈
ℝ) |
84 | 78, 82, 83 | sylancr 587 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (1 − (((𝐹‘𝑘)↑2) / 3)) ∈
ℝ) |
85 | 77, 84 | eqeltrd 2838 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐻 ∘ 𝐹)‘𝑘) ∈ ℝ) |
86 | | fvco3 6940 |
. . . . . 6
⊢ ((𝐹:ℕ⟶(ℝ ∖
{0}) ∧ 𝑘 ∈
ℕ) → ((𝐺 ∘
𝐹)‘𝑘) = (𝐺‘(𝐹‘𝑘))) |
87 | 7, 86 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐺 ∘ 𝐹)‘𝑘) = (𝐺‘(𝐹‘𝑘))) |
88 | 15, 87 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐺 ∘ 𝐹)‘𝑘) = (𝐺‘(𝐹‘𝑘))) |
89 | | fveq2 6842 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑘) → (sin‘𝑥) = (sin‘(𝐹‘𝑘))) |
90 | | id 22 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑘) → 𝑥 = (𝐹‘𝑘)) |
91 | 89, 90 | oveq12d 7375 |
. . . . . 6
⊢ (𝑥 = (𝐹‘𝑘) → ((sin‘𝑥) / 𝑥) = ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘))) |
92 | | ovex 7390 |
. . . . . 6
⊢
((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘)) ∈ V |
93 | 91, 67, 92 | fvmpt 6948 |
. . . . 5
⊢ ((𝐹‘𝑘) ∈ (ℝ ∖ {0}) → (𝐺‘(𝐹‘𝑘)) = ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘))) |
94 | 16, 93 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘(𝐹‘𝑘)) = ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘))) |
95 | 88, 94 | eqtrd 2776 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐺 ∘ 𝐹)‘𝑘) = ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘))) |
96 | 19 | resincld 16025 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (sin‘(𝐹‘𝑘)) ∈ ℝ) |
97 | 18 | simprd 496 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ≠ 0) |
98 | 96, 19, 97 | redivcld 11983 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘)) ∈ ℝ) |
99 | 95, 98 | eqeltrd 2838 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐺 ∘ 𝐹)‘𝑘) ∈ ℝ) |
100 | | 1cnd 11150 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 1 ∈
ℂ) |
101 | 82 | recnd 11183 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (((𝐹‘𝑘)↑2) / 3) ∈
ℂ) |
102 | 20 | abscld 15321 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘𝑘)) ∈ ℝ) |
103 | 102 | recnd 11183 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘𝑘)) ∈ ℂ) |
104 | 100, 101,
103 | subdird 11612 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((1 − (((𝐹‘𝑘)↑2) / 3)) · (abs‘(𝐹‘𝑘))) = ((1 · (abs‘(𝐹‘𝑘))) − ((((𝐹‘𝑘)↑2) / 3) · (abs‘(𝐹‘𝑘))))) |
105 | 103 | mulid2d 11173 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (1 ·
(abs‘(𝐹‘𝑘))) = (abs‘(𝐹‘𝑘))) |
106 | | df-3 12217 |
. . . . . . . . . . . . 13
⊢ 3 = (2 +
1) |
107 | 106 | oveq2i 7368 |
. . . . . . . . . . . 12
⊢
((abs‘(𝐹‘𝑘))↑3) = ((abs‘(𝐹‘𝑘))↑(2 + 1)) |
108 | | 2nn0 12430 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 |
109 | | expp1 13974 |
. . . . . . . . . . . . . 14
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℂ ∧ 2 ∈
ℕ0) → ((abs‘(𝐹‘𝑘))↑(2 + 1)) = (((abs‘(𝐹‘𝑘))↑2) · (abs‘(𝐹‘𝑘)))) |
110 | 103, 108,
109 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((abs‘(𝐹‘𝑘))↑(2 + 1)) = (((abs‘(𝐹‘𝑘))↑2) · (abs‘(𝐹‘𝑘)))) |
111 | | absresq 15187 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑘) ∈ ℝ → ((abs‘(𝐹‘𝑘))↑2) = ((𝐹‘𝑘)↑2)) |
112 | 19, 111 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((abs‘(𝐹‘𝑘))↑2) = ((𝐹‘𝑘)↑2)) |
113 | 112 | oveq1d 7372 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (((abs‘(𝐹‘𝑘))↑2) · (abs‘(𝐹‘𝑘))) = (((𝐹‘𝑘)↑2) · (abs‘(𝐹‘𝑘)))) |
114 | 110, 113 | eqtrd 2776 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((abs‘(𝐹‘𝑘))↑(2 + 1)) = (((𝐹‘𝑘)↑2) · (abs‘(𝐹‘𝑘)))) |
115 | 107, 114 | eqtrid 2788 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((abs‘(𝐹‘𝑘))↑3) = (((𝐹‘𝑘)↑2) · (abs‘(𝐹‘𝑘)))) |
116 | 115 | oveq1d 7372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (((abs‘(𝐹‘𝑘))↑3) / 3) = ((((𝐹‘𝑘)↑2) · (abs‘(𝐹‘𝑘))) / 3)) |
117 | 79 | recnd 11183 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐹‘𝑘)↑2) ∈ ℂ) |
118 | 23 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 3 ∈
ℂ) |
119 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 3 ≠
0) |
120 | 117, 103,
118, 119 | div23d 11968 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((((𝐹‘𝑘)↑2) · (abs‘(𝐹‘𝑘))) / 3) = ((((𝐹‘𝑘)↑2) / 3) · (abs‘(𝐹‘𝑘)))) |
121 | 116, 120 | eqtr2d 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((((𝐹‘𝑘)↑2) / 3) · (abs‘(𝐹‘𝑘))) = (((abs‘(𝐹‘𝑘))↑3) / 3)) |
122 | 105, 121 | oveq12d 7375 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((1 ·
(abs‘(𝐹‘𝑘))) − ((((𝐹‘𝑘)↑2) / 3) · (abs‘(𝐹‘𝑘)))) = ((abs‘(𝐹‘𝑘)) − (((abs‘(𝐹‘𝑘))↑3) / 3))) |
123 | 104, 122 | eqtrd 2776 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((1 − (((𝐹‘𝑘)↑2) / 3)) · (abs‘(𝐹‘𝑘))) = ((abs‘(𝐹‘𝑘)) − (((abs‘(𝐹‘𝑘))↑3) / 3))) |
124 | 20, 97 | absrpcld 15333 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘𝑘)) ∈
ℝ+) |
125 | 124 | rpgt0d 12960 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 0 <
(abs‘(𝐹‘𝑘))) |
126 | | sinccvg.6 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘𝑘)) < 1) |
127 | | ltle 11243 |
. . . . . . . . . . . 12
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((abs‘(𝐹‘𝑘)) < 1 → (abs‘(𝐹‘𝑘)) ≤ 1)) |
128 | 102, 78, 127 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((abs‘(𝐹‘𝑘)) < 1 → (abs‘(𝐹‘𝑘)) ≤ 1)) |
129 | 126, 128 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘𝑘)) ≤ 1) |
130 | | 0xr 11202 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
131 | | elioc2 13327 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → ((abs‘(𝐹‘𝑘)) ∈ (0(,]1) ↔ ((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 0 <
(abs‘(𝐹‘𝑘)) ∧ (abs‘(𝐹‘𝑘)) ≤ 1))) |
132 | 130, 78, 131 | mp2an 690 |
. . . . . . . . . 10
⊢
((abs‘(𝐹‘𝑘)) ∈ (0(,]1) ↔ ((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 0 <
(abs‘(𝐹‘𝑘)) ∧ (abs‘(𝐹‘𝑘)) ≤ 1)) |
133 | 102, 125,
129, 132 | syl3anbrc 1343 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘𝑘)) ∈ (0(,]1)) |
134 | | sin01bnd 16067 |
. . . . . . . . 9
⊢
((abs‘(𝐹‘𝑘)) ∈ (0(,]1) → (((abs‘(𝐹‘𝑘)) − (((abs‘(𝐹‘𝑘))↑3) / 3)) <
(sin‘(abs‘(𝐹‘𝑘))) ∧ (sin‘(abs‘(𝐹‘𝑘))) < (abs‘(𝐹‘𝑘)))) |
135 | 133, 134 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (((abs‘(𝐹‘𝑘)) − (((abs‘(𝐹‘𝑘))↑3) / 3)) <
(sin‘(abs‘(𝐹‘𝑘))) ∧ (sin‘(abs‘(𝐹‘𝑘))) < (abs‘(𝐹‘𝑘)))) |
136 | 135 | simpld 495 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((abs‘(𝐹‘𝑘)) − (((abs‘(𝐹‘𝑘))↑3) / 3)) <
(sin‘(abs‘(𝐹‘𝑘)))) |
137 | 123, 136 | eqbrtrd 5127 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((1 − (((𝐹‘𝑘)↑2) / 3)) · (abs‘(𝐹‘𝑘))) < (sin‘(abs‘(𝐹‘𝑘)))) |
138 | 102 | resincld 16025 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) →
(sin‘(abs‘(𝐹‘𝑘))) ∈ ℝ) |
139 | 84, 138, 124 | ltmuldivd 13004 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (((1 − (((𝐹‘𝑘)↑2) / 3)) · (abs‘(𝐹‘𝑘))) < (sin‘(abs‘(𝐹‘𝑘))) ↔ (1 − (((𝐹‘𝑘)↑2) / 3)) <
((sin‘(abs‘(𝐹‘𝑘))) / (abs‘(𝐹‘𝑘))))) |
140 | 137, 139 | mpbid 231 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (1 − (((𝐹‘𝑘)↑2) / 3)) <
((sin‘(abs‘(𝐹‘𝑘))) / (abs‘(𝐹‘𝑘)))) |
141 | | fveq2 6842 |
. . . . . . . 8
⊢
((abs‘(𝐹‘𝑘)) = (𝐹‘𝑘) → (sin‘(abs‘(𝐹‘𝑘))) = (sin‘(𝐹‘𝑘))) |
142 | | id 22 |
. . . . . . . 8
⊢
((abs‘(𝐹‘𝑘)) = (𝐹‘𝑘) → (abs‘(𝐹‘𝑘)) = (𝐹‘𝑘)) |
143 | 141, 142 | oveq12d 7375 |
. . . . . . 7
⊢
((abs‘(𝐹‘𝑘)) = (𝐹‘𝑘) → ((sin‘(abs‘(𝐹‘𝑘))) / (abs‘(𝐹‘𝑘))) = ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘))) |
144 | 143 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((abs‘(𝐹‘𝑘)) = (𝐹‘𝑘) → ((sin‘(abs‘(𝐹‘𝑘))) / (abs‘(𝐹‘𝑘))) = ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘)))) |
145 | | sinneg 16028 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑘) ∈ ℂ → (sin‘-(𝐹‘𝑘)) = -(sin‘(𝐹‘𝑘))) |
146 | 20, 145 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (sin‘-(𝐹‘𝑘)) = -(sin‘(𝐹‘𝑘))) |
147 | 146 | oveq1d 7372 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((sin‘-(𝐹‘𝑘)) / -(𝐹‘𝑘)) = (-(sin‘(𝐹‘𝑘)) / -(𝐹‘𝑘))) |
148 | 96 | recnd 11183 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (sin‘(𝐹‘𝑘)) ∈ ℂ) |
149 | 148, 20, 97 | div2negd 11946 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (-(sin‘(𝐹‘𝑘)) / -(𝐹‘𝑘)) = ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘))) |
150 | 147, 149 | eqtrd 2776 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((sin‘-(𝐹‘𝑘)) / -(𝐹‘𝑘)) = ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘))) |
151 | | fveq2 6842 |
. . . . . . . . 9
⊢
((abs‘(𝐹‘𝑘)) = -(𝐹‘𝑘) → (sin‘(abs‘(𝐹‘𝑘))) = (sin‘-(𝐹‘𝑘))) |
152 | | id 22 |
. . . . . . . . 9
⊢
((abs‘(𝐹‘𝑘)) = -(𝐹‘𝑘) → (abs‘(𝐹‘𝑘)) = -(𝐹‘𝑘)) |
153 | 151, 152 | oveq12d 7375 |
. . . . . . . 8
⊢
((abs‘(𝐹‘𝑘)) = -(𝐹‘𝑘) → ((sin‘(abs‘(𝐹‘𝑘))) / (abs‘(𝐹‘𝑘))) = ((sin‘-(𝐹‘𝑘)) / -(𝐹‘𝑘))) |
154 | 153 | eqeq1d 2738 |
. . . . . . 7
⊢
((abs‘(𝐹‘𝑘)) = -(𝐹‘𝑘) → (((sin‘(abs‘(𝐹‘𝑘))) / (abs‘(𝐹‘𝑘))) = ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘)) ↔ ((sin‘-(𝐹‘𝑘)) / -(𝐹‘𝑘)) = ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘)))) |
155 | 150, 154 | syl5ibrcom 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((abs‘(𝐹‘𝑘)) = -(𝐹‘𝑘) → ((sin‘(abs‘(𝐹‘𝑘))) / (abs‘(𝐹‘𝑘))) = ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘)))) |
156 | 19 | absord 15300 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((abs‘(𝐹‘𝑘)) = (𝐹‘𝑘) ∨ (abs‘(𝐹‘𝑘)) = -(𝐹‘𝑘))) |
157 | 144, 155,
156 | mpjaod 858 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) →
((sin‘(abs‘(𝐹‘𝑘))) / (abs‘(𝐹‘𝑘))) = ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘))) |
158 | 140, 157 | breqtrd 5131 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (1 − (((𝐹‘𝑘)↑2) / 3)) < ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘))) |
159 | 84, 98, 158 | ltled 11303 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (1 − (((𝐹‘𝑘)↑2) / 3)) ≤ ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘))) |
160 | 159, 77, 95 | 3brtr4d 5137 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐻 ∘ 𝐹)‘𝑘) ≤ ((𝐺 ∘ 𝐹)‘𝑘)) |
161 | 78 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 1 ∈
ℝ) |
162 | 135 | simprd 496 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) →
(sin‘(abs‘(𝐹‘𝑘))) < (abs‘(𝐹‘𝑘))) |
163 | 103 | mulid1d 11172 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((abs‘(𝐹‘𝑘)) · 1) = (abs‘(𝐹‘𝑘))) |
164 | 162, 163 | breqtrrd 5133 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) →
(sin‘(abs‘(𝐹‘𝑘))) < ((abs‘(𝐹‘𝑘)) · 1)) |
165 | 138, 161,
124 | ltdivmuld 13008 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) →
(((sin‘(abs‘(𝐹‘𝑘))) / (abs‘(𝐹‘𝑘))) < 1 ↔
(sin‘(abs‘(𝐹‘𝑘))) < ((abs‘(𝐹‘𝑘)) · 1))) |
166 | 164, 165 | mpbird 256 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) →
((sin‘(abs‘(𝐹‘𝑘))) / (abs‘(𝐹‘𝑘))) < 1) |
167 | 157, 166 | eqbrtrrd 5129 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘)) < 1) |
168 | 98, 161, 167 | ltled 11303 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((sin‘(𝐹‘𝑘)) / (𝐹‘𝑘)) ≤ 1) |
169 | 95, 168 | eqbrtrd 5127 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐺 ∘ 𝐹)‘𝑘) ≤ 1) |
170 | 1, 3, 66, 70, 85, 99, 160, 169 | climsqz 15523 |
1
⊢ (𝜑 → (𝐺 ∘ 𝐹) ⇝ 1) |