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 31888
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 2806 . 2 (ℤ𝑀) = (ℤ𝑀)
2 sinccvg.5 . . 3 (𝜑𝑀 ∈ ℕ)
32nnzd 11747 . 2 (𝜑𝑀 ∈ ℤ)
4 sinccvg.2 . . . 4 (𝜑𝐹 ⇝ 0)
5 sinccvg.4 . . . . . 6 𝐻 = (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3)))
65funmpt2 6140 . . . . 5 Fun 𝐻
7 sinccvg.1 . . . . . 6 (𝜑𝐹:ℕ⟶(ℝ ∖ {0}))
8 nnex 11311 . . . . . 6 ℕ ∈ V
9 fex 6714 . . . . . 6 ((𝐹:ℕ⟶(ℝ ∖ {0}) ∧ ℕ ∈ V) → 𝐹 ∈ V)
107, 8, 9sylancl 576 . . . . 5 (𝜑𝐹 ∈ V)
11 cofunexg 7360 . . . . 5 ((Fun 𝐻𝐹 ∈ V) → (𝐻𝐹) ∈ V)
126, 10, 11sylancr 577 . . . 4 (𝜑 → (𝐻𝐹) ∈ V)
137adantr 468 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → 𝐹:ℕ⟶(ℝ ∖ {0}))
14 eluznn 11977 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ)
152, 14sylan 571 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ)
1613, 15ffvelrnd 6582 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ (ℝ ∖ {0}))
17 eldifsn 4508 . . . . . . 7 ((𝐹𝑘) ∈ (ℝ ∖ {0}) ↔ ((𝐹𝑘) ∈ ℝ ∧ (𝐹𝑘) ≠ 0))
1816, 17sylib 209 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐹𝑘) ∈ ℝ ∧ (𝐹𝑘) ≠ 0))
1918simpld 484 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℝ)
2019recnd 10353 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℂ)
21 ax-1cn 10279 . . . . . 6 1 ∈ ℂ
22 sqcl 13148 . . . . . . 7 (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
23 3cn 11379 . . . . . . . 8 3 ∈ ℂ
24 3ne0 11398 . . . . . . . 8 3 ≠ 0
25 divcl 10976 . . . . . . . 8 (((𝑥↑2) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → ((𝑥↑2) / 3) ∈ ℂ)
2623, 24, 25mp3an23 1570 . . . . . . 7 ((𝑥↑2) ∈ ℂ → ((𝑥↑2) / 3) ∈ ℂ)
2722, 26syl 17 . . . . . 6 (𝑥 ∈ ℂ → ((𝑥↑2) / 3) ∈ ℂ)
28 subcl 10565 . . . . . 6 ((1 ∈ ℂ ∧ ((𝑥↑2) / 3) ∈ ℂ) → (1 − ((𝑥↑2) / 3)) ∈ ℂ)
2921, 27, 28sylancr 577 . . . . 5 (𝑥 ∈ ℂ → (1 − ((𝑥↑2) / 3)) ∈ ℂ)
305, 29fmpti 6604 . . . 4 𝐻:ℂ⟶ℂ
31 eqid 2806 . . . . . . . . . 10 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
3231cnfldtopon 22799 . . . . . . . . 9 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
3332a1i 11 . . . . . . . 8 (⊤ → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
34 1cnd 10320 . . . . . . . . 9 (⊤ → 1 ∈ ℂ)
3533, 33, 34cnmptc 21679 . . . . . . . 8 (⊤ → (𝑥 ∈ ℂ ↦ 1) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
3631sqcn 22890 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
3736a1i 11 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
3831divccn 22889 . . . . . . . . . . 11 ((3 ∈ ℂ ∧ 3 ≠ 0) → (𝑦 ∈ ℂ ↦ (𝑦 / 3)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
3923, 24, 38mp2an 675 . . . . . . . . . 10 (𝑦 ∈ ℂ ↦ (𝑦 / 3)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
4039a1i 11 . . . . . . . . 9 (⊤ → (𝑦 ∈ ℂ ↦ (𝑦 / 3)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
41 oveq1 6881 . . . . . . . . 9 (𝑦 = (𝑥↑2) → (𝑦 / 3) = ((𝑥↑2) / 3))
4233, 37, 33, 40, 41cnmpt11 21680 . . . . . . . 8 (⊤ → (𝑥 ∈ ℂ ↦ ((𝑥↑2) / 3)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
4331subcn 22882 . . . . . . . . 9 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
4443a1i 11 . . . . . . . 8 (⊤ → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
4533, 35, 42, 44cnmpt12f 21683 . . . . . . 7 (⊤ → (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3))) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
4645mptru 1645 . . . . . 6 (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3))) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
4731cncfcn1 22926 . . . . . 6 (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
4846, 5, 473eltr4i 2898 . . . . 5 𝐻 ∈ (ℂ–cn→ℂ)
49 cncfi 22910 . . . . 5 ((𝐻 ∈ (ℂ–cn→ℂ) ∧ 0 ∈ ℂ ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤 ∈ ℂ ((abs‘(𝑤 − 0)) < 𝑧 → (abs‘((𝐻𝑤) − (𝐻‘0))) < 𝑦))
5048, 49mp3an1 1565 . . . 4 ((0 ∈ ℂ ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤 ∈ ℂ ((abs‘(𝑤 − 0)) < 𝑧 → (abs‘((𝐻𝑤) − (𝐻‘0))) < 𝑦))
51 fvco3 6496 . . . . . 6 ((𝐹:ℕ⟶(ℝ ∖ {0}) ∧ 𝑘 ∈ ℕ) → ((𝐻𝐹)‘𝑘) = (𝐻‘(𝐹𝑘)))
527, 51sylan 571 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝐻𝐹)‘𝑘) = (𝐻‘(𝐹𝑘)))
5315, 52syldan 581 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐻𝐹)‘𝑘) = (𝐻‘(𝐹𝑘)))
541, 4, 12, 3, 20, 30, 50, 53climcn1lem 14556 . . 3 (𝜑 → (𝐻𝐹) ⇝ (𝐻‘0))
55 0cn 10317 . . . 4 0 ∈ ℂ
56 sq0i 13179 . . . . . . . . 9 (𝑥 = 0 → (𝑥↑2) = 0)
5756oveq1d 6889 . . . . . . . 8 (𝑥 = 0 → ((𝑥↑2) / 3) = (0 / 3))
5823, 24div0i 11044 . . . . . . . 8 (0 / 3) = 0
5957, 58syl6eq 2856 . . . . . . 7 (𝑥 = 0 → ((𝑥↑2) / 3) = 0)
6059oveq2d 6890 . . . . . 6 (𝑥 = 0 → (1 − ((𝑥↑2) / 3)) = (1 − 0))
61 1m0e1 11413 . . . . . 6 (1 − 0) = 1
6260, 61syl6eq 2856 . . . . 5 (𝑥 = 0 → (1 − ((𝑥↑2) / 3)) = 1)
63 1ex 10321 . . . . 5 1 ∈ V
6462, 5, 63fvmpt 6503 . . . 4 (0 ∈ ℂ → (𝐻‘0) = 1)
6555, 64ax-mp 5 . . 3 (𝐻‘0) = 1
6654, 65syl6breq 4885 . 2 (𝜑 → (𝐻𝐹) ⇝ 1)
67 sinccvg.3 . . . 4 𝐺 = (𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥))
6867funmpt2 6140 . . 3 Fun 𝐺
69 cofunexg 7360 . . 3 ((Fun 𝐺𝐹 ∈ V) → (𝐺𝐹) ∈ V)
7068, 10, 69sylancr 577 . 2 (𝜑 → (𝐺𝐹) ∈ V)
71 oveq1 6881 . . . . . . . 8 (𝑥 = (𝐹𝑘) → (𝑥↑2) = ((𝐹𝑘)↑2))
7271oveq1d 6889 . . . . . . 7 (𝑥 = (𝐹𝑘) → ((𝑥↑2) / 3) = (((𝐹𝑘)↑2) / 3))
7372oveq2d 6890 . . . . . 6 (𝑥 = (𝐹𝑘) → (1 − ((𝑥↑2) / 3)) = (1 − (((𝐹𝑘)↑2) / 3)))
74 ovex 6906 . . . . . 6 (1 − (((𝐹𝑘)↑2) / 3)) ∈ V
7573, 5, 74fvmpt 6503 . . . . 5 ((𝐹𝑘) ∈ ℂ → (𝐻‘(𝐹𝑘)) = (1 − (((𝐹𝑘)↑2) / 3)))
7620, 75syl 17 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐻‘(𝐹𝑘)) = (1 − (((𝐹𝑘)↑2) / 3)))
7753, 76eqtrd 2840 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐻𝐹)‘𝑘) = (1 − (((𝐹𝑘)↑2) / 3)))
78 1re 10325 . . . 4 1 ∈ ℝ
7919resqcld 13258 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐹𝑘)↑2) ∈ ℝ)
80 3nn 11463 . . . . 5 3 ∈ ℕ
81 nndivre 11342 . . . . 5 ((((𝐹𝑘)↑2) ∈ ℝ ∧ 3 ∈ ℕ) → (((𝐹𝑘)↑2) / 3) ∈ ℝ)
8279, 80, 81sylancl 576 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((𝐹𝑘)↑2) / 3) ∈ ℝ)
83 resubcl 10630 . . . 4 ((1 ∈ ℝ ∧ (((𝐹𝑘)↑2) / 3) ∈ ℝ) → (1 − (((𝐹𝑘)↑2) / 3)) ∈ ℝ)
8478, 82, 83sylancr 577 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → (1 − (((𝐹𝑘)↑2) / 3)) ∈ ℝ)
8577, 84eqeltrd 2885 . 2 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐻𝐹)‘𝑘) ∈ ℝ)
86 fvco3 6496 . . . . . 6 ((𝐹:ℕ⟶(ℝ ∖ {0}) ∧ 𝑘 ∈ ℕ) → ((𝐺𝐹)‘𝑘) = (𝐺‘(𝐹𝑘)))
877, 86sylan 571 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝐺𝐹)‘𝑘) = (𝐺‘(𝐹𝑘)))
8815, 87syldan 581 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐺𝐹)‘𝑘) = (𝐺‘(𝐹𝑘)))
89 fveq2 6408 . . . . . . 7 (𝑥 = (𝐹𝑘) → (sin‘𝑥) = (sin‘(𝐹𝑘)))
90 id 22 . . . . . . 7 (𝑥 = (𝐹𝑘) → 𝑥 = (𝐹𝑘))
9189, 90oveq12d 6892 . . . . . 6 (𝑥 = (𝐹𝑘) → ((sin‘𝑥) / 𝑥) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
92 ovex 6906 . . . . . 6 ((sin‘(𝐹𝑘)) / (𝐹𝑘)) ∈ V
9391, 67, 92fvmpt 6503 . . . . 5 ((𝐹𝑘) ∈ (ℝ ∖ {0}) → (𝐺‘(𝐹𝑘)) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
9416, 93syl 17 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺‘(𝐹𝑘)) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
9588, 94eqtrd 2840 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐺𝐹)‘𝑘) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
9619resincld 15093 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (sin‘(𝐹𝑘)) ∈ ℝ)
9718simprd 485 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ≠ 0)
9896, 19, 97redivcld 11138 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘(𝐹𝑘)) / (𝐹𝑘)) ∈ ℝ)
9995, 98eqeltrd 2885 . 2 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐺𝐹)‘𝑘) ∈ ℝ)
100 1cnd 10320 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → 1 ∈ ℂ)
10182recnd 10353 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((𝐹𝑘)↑2) / 3) ∈ ℂ)
10220abscld 14398 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) ∈ ℝ)
103102recnd 10353 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) ∈ ℂ)
104100, 101, 103subdird 10772 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((1 − (((𝐹𝑘)↑2) / 3)) · (abs‘(𝐹𝑘))) = ((1 · (abs‘(𝐹𝑘))) − ((((𝐹𝑘)↑2) / 3) · (abs‘(𝐹𝑘)))))
105103mulid2d 10343 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → (1 · (abs‘(𝐹𝑘))) = (abs‘(𝐹𝑘)))
106 df-3 11365 . . . . . . . . . . . . 13 3 = (2 + 1)
107106oveq2i 6885 . . . . . . . . . . . 12 ((abs‘(𝐹𝑘))↑3) = ((abs‘(𝐹𝑘))↑(2 + 1))
108 2nn0 11576 . . . . . . . . . . . . . 14 2 ∈ ℕ0
109 expp1 13090 . . . . . . . . . . . . . 14 (((abs‘(𝐹𝑘)) ∈ ℂ ∧ 2 ∈ ℕ0) → ((abs‘(𝐹𝑘))↑(2 + 1)) = (((abs‘(𝐹𝑘))↑2) · (abs‘(𝐹𝑘))))
110103, 108, 109sylancl 576 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘))↑(2 + 1)) = (((abs‘(𝐹𝑘))↑2) · (abs‘(𝐹𝑘))))
111 absresq 14265 . . . . . . . . . . . . . . 15 ((𝐹𝑘) ∈ ℝ → ((abs‘(𝐹𝑘))↑2) = ((𝐹𝑘)↑2))
11219, 111syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘))↑2) = ((𝐹𝑘)↑2))
113112oveq1d 6889 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((abs‘(𝐹𝑘))↑2) · (abs‘(𝐹𝑘))) = (((𝐹𝑘)↑2) · (abs‘(𝐹𝑘))))
114110, 113eqtrd 2840 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘))↑(2 + 1)) = (((𝐹𝑘)↑2) · (abs‘(𝐹𝑘))))
115107, 114syl5eq 2852 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘))↑3) = (((𝐹𝑘)↑2) · (abs‘(𝐹𝑘))))
116115oveq1d 6889 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((abs‘(𝐹𝑘))↑3) / 3) = ((((𝐹𝑘)↑2) · (abs‘(𝐹𝑘))) / 3))
11779recnd 10353 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐹𝑘)↑2) ∈ ℂ)
11823a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → 3 ∈ ℂ)
11924a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → 3 ≠ 0)
120117, 103, 118, 119div23d 11123 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((((𝐹𝑘)↑2) · (abs‘(𝐹𝑘))) / 3) = ((((𝐹𝑘)↑2) / 3) · (abs‘(𝐹𝑘))))
121116, 120eqtr2d 2841 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((((𝐹𝑘)↑2) / 3) · (abs‘(𝐹𝑘))) = (((abs‘(𝐹𝑘))↑3) / 3))
122105, 121oveq12d 6892 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((1 · (abs‘(𝐹𝑘))) − ((((𝐹𝑘)↑2) / 3) · (abs‘(𝐹𝑘)))) = ((abs‘(𝐹𝑘)) − (((abs‘(𝐹𝑘))↑3) / 3)))
123104, 122eqtrd 2840 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((1 − (((𝐹𝑘)↑2) / 3)) · (abs‘(𝐹𝑘))) = ((abs‘(𝐹𝑘)) − (((abs‘(𝐹𝑘))↑3) / 3)))
12420, 97absrpcld 14410 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) ∈ ℝ+)
125124rpgt0d 12089 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ𝑀)) → 0 < (abs‘(𝐹𝑘)))
126 sinccvg.6 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) < 1)
127 ltle 10411 . . . . . . . . . . . 12 (((abs‘(𝐹𝑘)) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘(𝐹𝑘)) < 1 → (abs‘(𝐹𝑘)) ≤ 1))
128102, 78, 127sylancl 576 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘)) < 1 → (abs‘(𝐹𝑘)) ≤ 1))
129126, 128mpd 15 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) ≤ 1)
130 0xr 10371 . . . . . . . . . . 11 0 ∈ ℝ*
131 elioc2 12454 . . . . . . . . . . 11 ((0 ∈ ℝ* ∧ 1 ∈ ℝ) → ((abs‘(𝐹𝑘)) ∈ (0(,]1) ↔ ((abs‘(𝐹𝑘)) ∈ ℝ ∧ 0 < (abs‘(𝐹𝑘)) ∧ (abs‘(𝐹𝑘)) ≤ 1)))
132130, 78, 131mp2an 675 . . . . . . . . . 10 ((abs‘(𝐹𝑘)) ∈ (0(,]1) ↔ ((abs‘(𝐹𝑘)) ∈ ℝ ∧ 0 < (abs‘(𝐹𝑘)) ∧ (abs‘(𝐹𝑘)) ≤ 1))
133102, 125, 129, 132syl3anbrc 1436 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹𝑘)) ∈ (0(,]1))
134 sin01bnd 15135 . . . . . . . . 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 484 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘)) − (((abs‘(𝐹𝑘))↑3) / 3)) < (sin‘(abs‘(𝐹𝑘))))
137123, 136eqbrtrd 4866 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((1 − (((𝐹𝑘)↑2) / 3)) · (abs‘(𝐹𝑘))) < (sin‘(abs‘(𝐹𝑘))))
138102resincld 15093 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → (sin‘(abs‘(𝐹𝑘))) ∈ ℝ)
13984, 138, 124ltmuldivd 12133 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((1 − (((𝐹𝑘)↑2) / 3)) · (abs‘(𝐹𝑘))) < (sin‘(abs‘(𝐹𝑘))) ↔ (1 − (((𝐹𝑘)↑2) / 3)) < ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘)))))
140137, 139mpbid 223 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → (1 − (((𝐹𝑘)↑2) / 3)) < ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))))
141 fveq2 6408 . . . . . . . 8 ((abs‘(𝐹𝑘)) = (𝐹𝑘) → (sin‘(abs‘(𝐹𝑘))) = (sin‘(𝐹𝑘)))
142 id 22 . . . . . . . 8 ((abs‘(𝐹𝑘)) = (𝐹𝑘) → (abs‘(𝐹𝑘)) = (𝐹𝑘))
143141, 142oveq12d 6892 . . . . . . 7 ((abs‘(𝐹𝑘)) = (𝐹𝑘) → ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
144143a1i 11 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘)) = (𝐹𝑘) → ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) = ((sin‘(𝐹𝑘)) / (𝐹𝑘))))
145 sinneg 15096 . . . . . . . . . 10 ((𝐹𝑘) ∈ ℂ → (sin‘-(𝐹𝑘)) = -(sin‘(𝐹𝑘)))
14620, 145syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → (sin‘-(𝐹𝑘)) = -(sin‘(𝐹𝑘)))
147146oveq1d 6889 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘-(𝐹𝑘)) / -(𝐹𝑘)) = (-(sin‘(𝐹𝑘)) / -(𝐹𝑘)))
14896recnd 10353 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑀)) → (sin‘(𝐹𝑘)) ∈ ℂ)
149148, 20, 97div2negd 11101 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑀)) → (-(sin‘(𝐹𝑘)) / -(𝐹𝑘)) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
150147, 149eqtrd 2840 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘-(𝐹𝑘)) / -(𝐹𝑘)) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
151 fveq2 6408 . . . . . . . . 9 ((abs‘(𝐹𝑘)) = -(𝐹𝑘) → (sin‘(abs‘(𝐹𝑘))) = (sin‘-(𝐹𝑘)))
152 id 22 . . . . . . . . 9 ((abs‘(𝐹𝑘)) = -(𝐹𝑘) → (abs‘(𝐹𝑘)) = -(𝐹𝑘))
153151, 152oveq12d 6892 . . . . . . . 8 ((abs‘(𝐹𝑘)) = -(𝐹𝑘) → ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) = ((sin‘-(𝐹𝑘)) / -(𝐹𝑘)))
154153eqeq1d 2808 . . . . . . 7 ((abs‘(𝐹𝑘)) = -(𝐹𝑘) → (((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)) ↔ ((sin‘-(𝐹𝑘)) / -(𝐹𝑘)) = ((sin‘(𝐹𝑘)) / (𝐹𝑘))))
155150, 154syl5ibrcom 238 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘)) = -(𝐹𝑘) → ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) = ((sin‘(𝐹𝑘)) / (𝐹𝑘))))
15619absord 14377 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘)) = (𝐹𝑘) ∨ (abs‘(𝐹𝑘)) = -(𝐹𝑘)))
157144, 155, 156mpjaod 878 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) = ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
158140, 157breqtrd 4870 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (1 − (((𝐹𝑘)↑2) / 3)) < ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
15984, 98, 158ltled 10470 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → (1 − (((𝐹𝑘)↑2) / 3)) ≤ ((sin‘(𝐹𝑘)) / (𝐹𝑘)))
160159, 77, 953brtr4d 4876 . 2 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐻𝐹)‘𝑘) ≤ ((𝐺𝐹)‘𝑘))
16178a1i 11 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → 1 ∈ ℝ)
162135simprd 485 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → (sin‘(abs‘(𝐹𝑘))) < (abs‘(𝐹𝑘)))
163103mulid1d 10342 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((abs‘(𝐹𝑘)) · 1) = (abs‘(𝐹𝑘)))
164162, 163breqtrrd 4872 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (sin‘(abs‘(𝐹𝑘))) < ((abs‘(𝐹𝑘)) · 1))
165138, 161, 124ltdivmuld 12137 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) < 1 ↔ (sin‘(abs‘(𝐹𝑘))) < ((abs‘(𝐹𝑘)) · 1)))
166164, 165mpbird 248 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘(abs‘(𝐹𝑘))) / (abs‘(𝐹𝑘))) < 1)
167157, 166eqbrtrrd 4868 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘(𝐹𝑘)) / (𝐹𝑘)) < 1)
16898, 161, 167ltled 10470 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((sin‘(𝐹𝑘)) / (𝐹𝑘)) ≤ 1)
16995, 168eqbrtrd 4866 . 2 ((𝜑𝑘 ∈ (ℤ𝑀)) → ((𝐺𝐹)‘𝑘) ≤ 1)
1701, 3, 66, 70, 85, 99, 160, 169climsqz 14594 1 (𝜑 → (𝐺𝐹) ⇝ 1)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wtru 1638  wcel 2156  wne 2978  wral 3096  wrex 3097  Vcvv 3391  cdif 3766  {csn 4370   class class class wbr 4844  cmpt 4923  ccom 5315  Fun wfun 6095  wf 6097  cfv 6101  (class class class)co 6874  cc 10219  cr 10220  0cc0 10221  1c1 10222   + caddc 10224   · cmul 10226  *cxr 10358   < clt 10359  cle 10360  cmin 10551  -cneg 10552   / cdiv 10969  cn 11305  2c2 11356  3c3 11357  0cn0 11559  cuz 11904  +crp 12046  (,]cioc 12394  cexp 13083  abscabs 14197  cli 14438  sincsin 15014  TopOpenctopn 16287  fldccnfld 19954  TopOnctopon 20928   Cn ccn 21242   ×t ctx 21577  cnccncf 22892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-inf2 8785  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298  ax-pre-sup 10299  ax-addf 10300  ax-mulf 10301
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-isom 6110  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-of 7127  df-om 7296  df-1st 7398  df-2nd 7399  df-supp 7530  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-2o 7797  df-oadd 7800  df-er 7979  df-map 8094  df-pm 8095  df-ixp 8146  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-fsupp 8515  df-fi 8556  df-sup 8587  df-inf 8588  df-oi 8654  df-card 9048  df-cda 9275  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-div 10970  df-nn 11306  df-2 11364  df-3 11365  df-4 11366  df-5 11367  df-6 11368  df-7 11369  df-8 11370  df-9 11371  df-n0 11560  df-z 11644  df-dec 11760  df-uz 11905  df-q 12008  df-rp 12047  df-xneg 12162  df-xadd 12163  df-xmul 12164  df-ioc 12398  df-ico 12399  df-icc 12400  df-fz 12550  df-fzo 12690  df-fl 12817  df-seq 13025  df-exp 13084  df-fac 13281  df-hash 13338  df-shft 14030  df-cj 14062  df-re 14063  df-im 14064  df-sqrt 14198  df-abs 14199  df-limsup 14425  df-clim 14442  df-rlim 14443  df-sum 14640  df-ef 15018  df-sin 15020  df-struct 16070  df-ndx 16071  df-slot 16072  df-base 16074  df-sets 16075  df-ress 16076  df-plusg 16166  df-mulr 16167  df-starv 16168  df-sca 16169  df-vsca 16170  df-ip 16171  df-tset 16172  df-ple 16173  df-ds 16175  df-unif 16176  df-hom 16177  df-cco 16178  df-rest 16288  df-topn 16289  df-0g 16307  df-gsum 16308  df-topgen 16309  df-pt 16310  df-prds 16313  df-xrs 16367  df-qtop 16372  df-imas 16373  df-xps 16375  df-mre 16451  df-mrc 16452  df-acs 16454  df-mgm 17447  df-sgrp 17489  df-mnd 17500  df-submnd 17541  df-mulg 17746  df-cntz 17951  df-cmn 18396  df-psmet 19946  df-xmet 19947  df-met 19948  df-bl 19949  df-mopn 19950  df-cnfld 19955  df-top 20912  df-topon 20929  df-topsp 20951  df-bases 20964  df-cn 21245  df-cnp 21246  df-tx 21579  df-hmeo 21772  df-xms 22338  df-ms 22339  df-tms 22340  df-cncf 22894
This theorem is referenced by:  sinccvg  31889
  Copyright terms: Public domain W3C validator