Users' Mathboxes Mathbox for Paul Chapman < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sinccvglem Structured version   Visualization version   GIF version

Theorem sinccvglem 34260
Description: ((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Revised by Mario Carneiro, 21-May-2014.)
Hypotheses
Ref Expression
sinccvg.1 (𝜑𝐹:ℕ⟶(ℝ ∖ {0}))
sinccvg.2 (𝜑𝐹 ⇝ 0)
sinccvg.3 𝐺 = (𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥))
sinccvg.4 𝐻 = (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3)))
sinccvg.5 (𝜑𝑀 ∈ ℕ)
sinccvg.6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) < 1)
Assertion
Ref Expression
sinccvglem (𝜑 → (𝐺𝐹) ⇝ 1)
Distinct variable groups:   𝑥,𝑘,𝐹   𝑘,𝐻   𝑘,𝑀   𝜑,𝑘   𝑘,𝐺
Allowed substitution hints:   𝜑(𝑥)   𝐺(𝑥)   𝐻(𝑥)   𝑀(𝑥)

Proof of Theorem sinccvglem
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2736 . 2 (ℤ𝑀) = (ℤ𝑀)
2 sinccvg.5 . . 3 (𝜑𝑀 ∈ ℕ)
32nnzd 12526 . 2 (𝜑𝑀 ∈ ℤ)
4 sinccvg.2 . . . 4 (𝜑𝐹 ⇝ 0)
5 sinccvg.4 . . . . . 6 𝐻 = (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3)))
65funmpt2 6540 . . . . 5 Fun 𝐻
7 sinccvg.1 . . . . . 6 (𝜑𝐹:ℕ⟶(ℝ ∖ {0}))
8 nnex 12159 . . . . . 6 ℕ ∈ V
9 fex 7176 . . . . . 6 ((𝐹:ℕ⟶(ℝ ∖ {0}) ∧ ℕ ∈ V) → 𝐹 ∈ V)
107, 8, 9sylancl 586 . . . . 5 (𝜑𝐹 ∈ V)
11 cofunexg 7881 . . . . 5 ((Fun 𝐻𝐹 ∈ V) → (𝐻𝐹) ∈ V)
126, 10, 11sylancr 587 . . . 4 (𝜑 → (𝐻𝐹) ∈ V)
137adantr 481 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → 𝐹:ℕ⟶(ℝ ∖ {0}))
14 eluznn 12843 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ)
152, 14sylan 580 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ)
1613, 15ffvelcdmd 7036 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ (ℝ ∖ {0}))
17 eldifsn 4747 . . . . . . 7 ((𝐹𝑘) ∈ (ℝ ∖ {0}) ↔ ((𝐹𝑘) ∈ ℝ ∧ (𝐹𝑘) ≠ 0))
1816, 17sylib 217 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐹𝑘) ∈ ℝ ∧ (𝐹𝑘) ≠ 0))
1918simpld 495 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℝ)
2019recnd 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) ∈ ℂ)
2623, 24, 25mp3an23 1453 . . . . . . 7 ((𝑥↑2) ∈ ℂ → ((𝑥↑2) / 3) ∈ ℂ)
2722, 26syl 17 . . . . . 6 (𝑥 ∈ ℂ → ((𝑥↑2) / 3) ∈ ℂ)
28 subcl 11400 . . . . . 6 ((1 ∈ ℂ ∧ ((𝑥↑2) / 3) ∈ ℂ) → (1 − ((𝑥↑2) / 3)) ∈ ℂ)
2921, 27, 28sylancr 587 . . . . 5 (𝑥 ∈ ℂ → (1 − ((𝑥↑2) / 3)) ∈ ℂ)
305, 29fmpti 7060 . . . 4 𝐻:ℂ⟶ℂ
31 eqid 2736 . . . . . . . . . 10 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
3231cnfldtopon 24146 . . . . . . . . 9 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
3332a1i 11 . . . . . . . 8 (⊤ → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
34 1cnd 11150 . . . . . . . . 9 (⊤ → 1 ∈ ℂ)
3533, 33, 34cnmptc 23013 . . . . . . . 8 (⊤ → (𝑥 ∈ ℂ ↦ 1) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
3631sqcn 24237 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
3736a1i 11 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
3831divccn 24236 . . . . . . . . . . 11 ((3 ∈ ℂ ∧ 3 ≠ 0) → (𝑦 ∈ ℂ ↦ (𝑦 / 3)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
3923, 24, 38mp2an 690 . . . . . . . . . 10 (𝑦 ∈ ℂ ↦ (𝑦 / 3)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
4039a1i 11 . . . . . . . . 9 (⊤ → (𝑦 ∈ ℂ ↦ (𝑦 / 3)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
41 oveq1 7364 . . . . . . . . 9 (𝑦 = (𝑥↑2) → (𝑦 / 3) = ((𝑥↑2) / 3))
4233, 37, 33, 40, 41cnmpt11 23014 . . . . . . . 8 (⊤ → (𝑥 ∈ ℂ ↦ ((𝑥↑2) / 3)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
4331subcn 24229 . . . . . . . . 9 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
4443a1i 11 . . . . . . . 8 (⊤ → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
4533, 35, 42, 44cnmpt12f 23017 . . . . . . 7 (⊤ → (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3))) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
4645mptru 1548 . . . . . 6 (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3))) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
4731cncfcn1 24274 . . . . . 6 (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
4846, 5, 473eltr4i 2851 . . . . 5 𝐻 ∈ (ℂ–cn→ℂ)
49 cncfi 24257 . . . . 5 ((𝐻 ∈ (ℂ–cn→ℂ) ∧ 0 ∈ ℂ ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤 ∈ ℂ ((abs‘(𝑤 − 0)) < 𝑧 → (abs‘((𝐻𝑤) − (𝐻‘0))) < 𝑦))
5048, 49mp3an1 1448 . . . 4 ((0 ∈ ℂ ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤 ∈ ℂ ((abs‘(𝑤 − 0)) < 𝑧 → (abs‘((𝐻𝑤) − (𝐻‘0))) < 𝑦))
51 fvco3 6940 . . . . . 6 ((𝐹:ℕ⟶(ℝ ∖ {0}) ∧ 𝑘 ∈ ℕ) → ((𝐻𝐹)‘𝑘) = (𝐻‘(𝐹𝑘)))
527, 51sylan 580 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝐻𝐹)‘𝑘) = (𝐻‘(𝐹𝑘)))
5315, 52syldan 591 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐻𝐹)‘𝑘) = (𝐻‘(𝐹𝑘)))
541, 4, 12, 3, 20, 30, 50, 53climcn1lem 15485 . . 3 (𝜑 → (𝐻𝐹) ⇝ (𝐻‘0))
55 0cn 11147 . . . 4 0 ∈ ℂ
56 sq0i 14097 . . . . . . . . 9 (𝑥 = 0 → (𝑥↑2) = 0)
5756oveq1d 7372 . . . . . . . 8 (𝑥 = 0 → ((𝑥↑2) / 3) = (0 / 3))
5823, 24div0i 11889 . . . . . . . 8 (0 / 3) = 0
5957, 58eqtrdi 2792 . . . . . . 7 (𝑥 = 0 → ((𝑥↑2) / 3) = 0)
6059oveq2d 7373 . . . . . 6 (𝑥 = 0 → (1 − ((𝑥↑2) / 3)) = (1 − 0))
61 1m0e1 12274 . . . . . 6 (1 − 0) = 1
6260, 61eqtrdi 2792 . . . . 5 (𝑥 = 0 → (1 − ((𝑥↑2) / 3)) = 1)
63 1ex 11151 . . . . 5 1 ∈ V
6462, 5, 63fvmpt 6948 . . . 4 (0 ∈ ℂ → (𝐻‘0) = 1)
6555, 64ax-mp 5 . . 3 (𝐻‘0) = 1
6654, 65breqtrdi 5146 . 2 (𝜑 → (𝐻𝐹) ⇝ 1)
67 sinccvg.3 . . . 4 𝐺 = (𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥))
6867funmpt2 6540 . . 3 Fun 𝐺
69 cofunexg 7881 . . 3 ((Fun 𝐺𝐹 ∈ V) → (𝐺𝐹) ∈ V)
7068, 10, 69sylancr 587 . 2 (𝜑 → (𝐺𝐹) ∈ V)
71 oveq1 7364 . . . . . . . 8 (𝑥 = (𝐹𝑘) → (𝑥↑2) = ((𝐹𝑘)↑2))
7271oveq1d 7372 . . . . . . 7 (𝑥 = (𝐹𝑘) → ((𝑥↑2) / 3) = (((𝐹𝑘)↑2) / 3))
7372oveq2d 7373 . . . . . 6 (𝑥 = (𝐹𝑘) → (1 − ((𝑥↑2) / 3)) = (1 − (((𝐹𝑘)↑2) / 3)))
74 ovex 7390 . . . . . 6 (1 − (((𝐹𝑘)↑2) / 3)) ∈ V
7573, 5, 74fvmpt 6948 . . . . 5 ((𝐹𝑘) ∈ ℂ → (𝐻‘(𝐹𝑘)) = (1 − (((𝐹𝑘)↑2) / 3)))
7620, 75syl 17 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐻‘(𝐹𝑘)) = (1 − (((𝐹𝑘)↑2) / 3)))
7753, 76eqtrd 2776 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐻𝐹)‘𝑘) = (1 − (((𝐹𝑘)↑2) / 3)))
78 1re 11155 . . . 4 1 ∈ ℝ
7919resqcld 14030 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐹𝑘)↑2) ∈ ℝ)
80 3nn 12232 . . . . 5 3 ∈ ℕ
81 nndivre 12194 . . . . 5 ((((𝐹𝑘)↑2) ∈ ℝ ∧ 3 ∈ ℕ) → (((𝐹𝑘)↑2) / 3) ∈ ℝ)
8279, 80, 81sylancl 586 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((𝐹𝑘)↑2) / 3) ∈ ℝ)
83 resubcl 11465 . . . 4 ((1 ∈ ℝ ∧ (((𝐹𝑘)↑2) / 3) ∈ ℝ) → (1 − (((𝐹𝑘)↑2) / 3)) ∈ ℝ)
8478, 82, 83sylancr 587 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → (1 − (((𝐹𝑘)↑2) / 3)) ∈ ℝ)
8577, 84eqeltrd 2838 . 2 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐻𝐹)‘𝑘) ∈ ℝ)
86 fvco3 6940 . . . . . 6 ((𝐹:ℕ⟶(ℝ ∖ {0}) ∧ 𝑘 ∈ ℕ) → ((𝐺𝐹)‘𝑘) = (𝐺‘(𝐹𝑘)))
877, 86sylan 580 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝐺𝐹)‘𝑘) = (𝐺‘(𝐹𝑘)))
8815, 87syldan 591 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐺𝐹)‘𝑘) = (𝐺‘(𝐹𝑘)))
89 fveq2 6842 . . . . . . 7 (𝑥 = (𝐹𝑘) → (sin‘𝑥) = (sin‘(𝐹𝑘)))
90 id 22 . . . . . . 7 (𝑥 = (𝐹𝑘) → 𝑥 = (𝐹𝑘))
9189, 90oveq12d 7375 . . . . . 6 (𝑥 = (𝐹𝑘) → ((sin‘𝑥) / 𝑥) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
92 ovex 7390 . . . . . 6 ((sin‘(𝐹𝑘)) / (𝐹𝑘)) ∈ V
9391, 67, 92fvmpt 6948 . . . . 5 ((𝐹𝑘) ∈ (ℝ ∖ {0}) → (𝐺‘(𝐹𝑘)) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
9416, 93syl 17 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺‘(𝐹𝑘)) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
9588, 94eqtrd 2776 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐺𝐹)‘𝑘) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
9619resincld 16025 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (sin‘(𝐹𝑘)) ∈ ℝ)
9718simprd 496 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ≠ 0)
9896, 19, 97redivcld 11983 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘(𝐹𝑘)) / (𝐹𝑘)) ∈ ℝ)
9995, 98eqeltrd 2838 . 2 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐺𝐹)‘𝑘) ∈ ℝ)
100 1cnd 11150 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → 1 ∈ ℂ)
10182recnd 11183 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((𝐹𝑘)↑2) / 3) ∈ ℂ)
10220abscld 15321 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) ∈ ℝ)
103102recnd 11183 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) ∈ ℂ)
104100, 101, 103subdird 11612 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((1 − (((𝐹𝑘)↑2) / 3)) · (abs‘(𝐹𝑘))) = ((1 · (abs‘(𝐹𝑘))) − ((((𝐹𝑘)↑2) / 3) · (abs‘(𝐹𝑘)))))
105103mulid2d 11173 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → (1 · (abs‘(𝐹𝑘))) = (abs‘(𝐹𝑘)))
106 df-3 12217 . . . . . . . . . . . . 13 3 = (2 + 1)
107106oveq2i 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‘(𝐹𝑘))))
110103, 108, 109sylancl 586 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘))↑(2 + 1)) = (((abs‘(𝐹𝑘))↑2) · (abs‘(𝐹𝑘))))
111 absresq 15187 . . . . . . . . . . . . . . 15 ((𝐹𝑘) ∈ ℝ → ((abs‘(𝐹𝑘))↑2) = ((𝐹𝑘)↑2))
11219, 111syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘))↑2) = ((𝐹𝑘)↑2))
113112oveq1d 7372 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((abs‘(𝐹𝑘))↑2) · (abs‘(𝐹𝑘))) = (((𝐹𝑘)↑2) · (abs‘(𝐹𝑘))))
114110, 113eqtrd 2776 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘))↑(2 + 1)) = (((𝐹𝑘)↑2) · (abs‘(𝐹𝑘))))
115107, 114eqtrid 2788 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘))↑3) = (((𝐹𝑘)↑2) · (abs‘(𝐹𝑘))))
116115oveq1d 7372 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((abs‘(𝐹𝑘))↑3) / 3) = ((((𝐹𝑘)↑2) · (abs‘(𝐹𝑘))) / 3))
11779recnd 11183 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐹𝑘)↑2) ∈ ℂ)
11823a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → 3 ∈ ℂ)
11924a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → 3 ≠ 0)
120117, 103, 118, 119div23d 11968 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((((𝐹𝑘)↑2) · (abs‘(𝐹𝑘))) / 3) = ((((𝐹𝑘)↑2) / 3) · (abs‘(𝐹𝑘))))
121116, 120eqtr2d 2777 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((((𝐹𝑘)↑2) / 3) · (abs‘(𝐹𝑘))) = (((abs‘(𝐹𝑘))↑3) / 3))
122105, 121oveq12d 7375 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((1 · (abs‘(𝐹𝑘))) − ((((𝐹𝑘)↑2) / 3) · (abs‘(𝐹𝑘)))) = ((abs‘(𝐹𝑘)) − (((abs‘(𝐹𝑘))↑3) / 3)))
123104, 122eqtrd 2776 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((1 − (((𝐹𝑘)↑2) / 3)) · (abs‘(𝐹𝑘))) = ((abs‘(𝐹𝑘)) − (((abs‘(𝐹𝑘))↑3) / 3)))
12420, 97absrpcld 15333 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) ∈ ℝ+)
125124rpgt0d 12960 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ𝑀)) → 0 < (abs‘(𝐹𝑘)))
126 sinccvg.6 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) < 1)
127 ltle 11243 . . . . . . . . . . . 12 (((abs‘(𝐹𝑘)) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘(𝐹𝑘)) < 1 → (abs‘(𝐹𝑘)) ≤ 1))
128102, 78, 127sylancl 586 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘)) < 1 → (abs‘(𝐹𝑘)) ≤ 1))
129126, 128mpd 15 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) ≤ 1)
130 0xr 11202 . . . . . . . . . . 11 0 ∈ ℝ*
131 elioc2 13327 . . . . . . . . . . 11 ((0 ∈ ℝ* ∧ 1 ∈ ℝ) → ((abs‘(𝐹𝑘)) ∈ (0(,]1) ↔ ((abs‘(𝐹𝑘)) ∈ ℝ ∧ 0 < (abs‘(𝐹𝑘)) ∧ (abs‘(𝐹𝑘)) ≤ 1)))
132130, 78, 131mp2an 690 . . . . . . . . . 10 ((abs‘(𝐹𝑘)) ∈ (0(,]1) ↔ ((abs‘(𝐹𝑘)) ∈ ℝ ∧ 0 < (abs‘(𝐹𝑘)) ∧ (abs‘(𝐹𝑘)) ≤ 1))
133102, 125, 129, 132syl3anbrc 1343 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) ∈ (0(,]1))
134 sin01bnd 16067 . . . . . . . . 9 ((abs‘(𝐹𝑘)) ∈ (0(,]1) → (((abs‘(𝐹𝑘)) − (((abs‘(𝐹𝑘))↑3) / 3)) < (sin‘(abs‘(𝐹𝑘))) ∧ (sin‘(abs‘(𝐹𝑘))) < (abs‘(𝐹𝑘))))
135133, 134syl 17 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((abs‘(𝐹𝑘)) − (((abs‘(𝐹𝑘))↑3) / 3)) < (sin‘(abs‘(𝐹𝑘))) ∧ (sin‘(abs‘(𝐹𝑘))) < (abs‘(𝐹𝑘))))
136135simpld 495 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘)) − (((abs‘(𝐹𝑘))↑3) / 3)) < (sin‘(abs‘(𝐹𝑘))))
137123, 136eqbrtrd 5127 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((1 − (((𝐹𝑘)↑2) / 3)) · (abs‘(𝐹𝑘))) < (sin‘(abs‘(𝐹𝑘))))
138102resincld 16025 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → (sin‘(abs‘(𝐹𝑘))) ∈ ℝ)
13984, 138, 124ltmuldivd 13004 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((1 − (((𝐹𝑘)↑2) / 3)) · (abs‘(𝐹𝑘))) < (sin‘(abs‘(𝐹𝑘))) ↔ (1 − (((𝐹𝑘)↑2) / 3)) < ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘)))))
140137, 139mpbid 231 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → (1 − (((𝐹𝑘)↑2) / 3)) < ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))))
141 fveq2 6842 . . . . . . . 8 ((abs‘(𝐹𝑘)) = (𝐹𝑘) → (sin‘(abs‘(𝐹𝑘))) = (sin‘(𝐹𝑘)))
142 id 22 . . . . . . . 8 ((abs‘(𝐹𝑘)) = (𝐹𝑘) → (abs‘(𝐹𝑘)) = (𝐹𝑘))
143141, 142oveq12d 7375 . . . . . . 7 ((abs‘(𝐹𝑘)) = (𝐹𝑘) → ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
144143a1i 11 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘)) = (𝐹𝑘) → ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) = ((sin‘(𝐹𝑘)) / (𝐹𝑘))))
145 sinneg 16028 . . . . . . . . . 10 ((𝐹𝑘) ∈ ℂ → (sin‘-(𝐹𝑘)) = -(sin‘(𝐹𝑘)))
14620, 145syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → (sin‘-(𝐹𝑘)) = -(sin‘(𝐹𝑘)))
147146oveq1d 7372 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘-(𝐹𝑘)) / -(𝐹𝑘)) = (-(sin‘(𝐹𝑘)) / -(𝐹𝑘)))
14896recnd 11183 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → (sin‘(𝐹𝑘)) ∈ ℂ)
149148, 20, 97div2negd 11946 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → (-(sin‘(𝐹𝑘)) / -(𝐹𝑘)) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
150147, 149eqtrd 2776 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘-(𝐹𝑘)) / -(𝐹𝑘)) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
151 fveq2 6842 . . . . . . . . 9 ((abs‘(𝐹𝑘)) = -(𝐹𝑘) → (sin‘(abs‘(𝐹𝑘))) = (sin‘-(𝐹𝑘)))
152 id 22 . . . . . . . . 9 ((abs‘(𝐹𝑘)) = -(𝐹𝑘) → (abs‘(𝐹𝑘)) = -(𝐹𝑘))
153151, 152oveq12d 7375 . . . . . . . 8 ((abs‘(𝐹𝑘)) = -(𝐹𝑘) → ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) = ((sin‘-(𝐹𝑘)) / -(𝐹𝑘)))
154153eqeq1d 2738 . . . . . . 7 ((abs‘(𝐹𝑘)) = -(𝐹𝑘) → (((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)) ↔ ((sin‘-(𝐹𝑘)) / -(𝐹𝑘)) = ((sin‘(𝐹𝑘)) / (𝐹𝑘))))
155150, 154syl5ibrcom 246 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘)) = -(𝐹𝑘) → ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) = ((sin‘(𝐹𝑘)) / (𝐹𝑘))))
15619absord 15300 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘)) = (𝐹𝑘) ∨ (abs‘(𝐹𝑘)) = -(𝐹𝑘)))
157144, 155, 156mpjaod 858 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
158140, 157breqtrd 5131 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (1 − (((𝐹𝑘)↑2) / 3)) < ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
15984, 98, 158ltled 11303 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → (1 − (((𝐹𝑘)↑2) / 3)) ≤ ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
160159, 77, 953brtr4d 5137 . 2 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐻𝐹)‘𝑘) ≤ ((𝐺𝐹)‘𝑘))
16178a1i 11 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → 1 ∈ ℝ)
162135simprd 496 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → (sin‘(abs‘(𝐹𝑘))) < (abs‘(𝐹𝑘)))
163103mulid1d 11172 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘)) · 1) = (abs‘(𝐹𝑘)))
164162, 163breqtrrd 5133 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (sin‘(abs‘(𝐹𝑘))) < ((abs‘(𝐹𝑘)) · 1))
165138, 161, 124ltdivmuld 13008 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) < 1 ↔ (sin‘(abs‘(𝐹𝑘))) < ((abs‘(𝐹𝑘)) · 1)))
166164, 165mpbird 256 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) < 1)
167157, 166eqbrtrrd 5129 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘(𝐹𝑘)) / (𝐹𝑘)) < 1)
16898, 161, 167ltled 11303 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘(𝐹𝑘)) / (𝐹𝑘)) ≤ 1)
16995, 168eqbrtrd 5127 . 2 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐺𝐹)‘𝑘) ≤ 1)
1701, 3, 66, 70, 85, 99, 160, 169climsqz 15523 1 (𝜑 → (𝐺𝐹) ⇝ 1)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wtru 1542  wcel 2106  wne 2943  wral 3064  wrex 3073  Vcvv 3445  cdif 3907  {csn 4586   class class class wbr 5105  cmpt 5188  ccom 5637  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  *cxr 11188   < clt 11189  cle 11190  cmin 11385  -cneg 11386   / cdiv 11812  cn 12153  2c2 12208  3c3 12209  0cn0 12413  cuz 12763  +crp 12915  (,]cioc 13265  cexp 13967  abscabs 15119  cli 15366  sincsin 15946  TopOpenctopn 17303  fldccnfld 20796  TopOnctopon 22259   Cn ccn 22575   ×t ctx 22911  cnccncf 24239
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioc 13269  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-seq 13907  df-exp 13968  df-fac 14174  df-hash 14231  df-shft 14952  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-ef 15950  df-sin 15952  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cn 22578  df-cnp 22579  df-tx 22913  df-hmeo 23106  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241
This theorem is referenced by:  sinccvg  34261
  Copyright terms: Public domain W3C validator