Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smflimlem4 Structured version   Visualization version   GIF version

Theorem smflimlem4 40315
 Description: Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
smflimlem4.1 (𝜑𝑀 ∈ ℤ)
smflimlem4.2 𝑍 = (ℤ𝑀)
smflimlem4.3 (𝜑𝑆 ∈ SAlg)
smflimlem4.4 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
smflimlem4.5 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
smflimlem4.6 𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
smflimlem4.7 (𝜑𝐴 ∈ ℝ)
smflimlem4.8 𝑃 = (𝑚𝑍, 𝑘 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
smflimlem4.9 𝐻 = (𝑚𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))
smflimlem4.10 𝐼 = 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)
smflimlem4.11 ((𝜑𝑟 ∈ ran 𝑃) → (𝐶𝑟) ∈ 𝑟)
Assertion
Ref Expression
smflimlem4 (𝜑 → (𝐷𝐼) ⊆ {𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴})
Distinct variable groups:   𝐴,𝑘,𝑚,𝑠   𝑥,𝐴,𝑘,𝑚   𝐶,𝑘,𝑚,𝑠   𝐶,𝑟,𝑘   𝐷,𝑘,𝑚,𝑛,𝑥   𝐷,𝑟,𝑥   𝑘,𝐹,𝑚,𝑛,𝑥   𝐹,𝑠   𝑚,𝐺   𝑘,𝐻,𝑚,𝑛   𝑘,𝐼,𝑚,𝑥   𝐼,𝑟   𝑚,𝑀   𝑃,𝑘,𝑚,𝑠   𝑃,𝑟   𝑆,𝑘,𝑚,𝑠   𝑘,𝑍,𝑚,𝑛,𝑥   𝜑,𝑘,𝑚,𝑛,𝑥   𝜑,𝑟
Allowed substitution hints:   𝜑(𝑠)   𝐴(𝑛,𝑟)   𝐶(𝑥,𝑛)   𝐷(𝑠)   𝑃(𝑥,𝑛)   𝑆(𝑥,𝑛,𝑟)   𝐹(𝑟)   𝐺(𝑥,𝑘,𝑛,𝑠,𝑟)   𝐻(𝑥,𝑠,𝑟)   𝐼(𝑛,𝑠)   𝑀(𝑥,𝑘,𝑛,𝑠,𝑟)   𝑍(𝑠,𝑟)

Proof of Theorem smflimlem4
Dummy variables 𝑖 𝑗 𝑧 𝑦 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 3816 . . 3 (𝐷𝐼) ⊆ 𝐷
21a1i 11 . 2 (𝜑 → (𝐷𝐼) ⊆ 𝐷)
32sselda 3587 . . . . . . 7 ((𝜑𝑥 ∈ (𝐷𝐼)) → 𝑥𝐷)
4 smflimlem4.6 . . . . . . . . . 10 𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
54a1i 11 . . . . . . . . 9 (𝜑𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))))
6 nfv 1840 . . . . . . . . . . 11 𝑚(𝜑𝑥𝐷)
7 nfcv 2761 . . . . . . . . . . 11 𝑚𝐹
8 nfcv 2761 . . . . . . . . . . 11 𝑧𝐹
9 smflimlem4.2 . . . . . . . . . . 11 𝑍 = (ℤ𝑀)
10 smflimlem4.3 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ SAlg)
1110adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑚𝑍) → 𝑆 ∈ SAlg)
12 smflimlem4.4 . . . . . . . . . . . . . 14 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
1312ffvelrnda 6320 . . . . . . . . . . . . 13 ((𝜑𝑚𝑍) → (𝐹𝑚) ∈ (SMblFn‘𝑆))
14 eqid 2621 . . . . . . . . . . . . 13 dom (𝐹𝑚) = dom (𝐹𝑚)
1511, 13, 14smff 40274 . . . . . . . . . . . 12 ((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
1615adantlr 750 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
17 smflimlem4.5 . . . . . . . . . . . 12 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
18 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑚)‘𝑧))
1918mpteq2dv 4710 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑧)))
2019eleq1d 2683 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑧)) ∈ dom ⇝ ))
2120cbvrabv 3188 . . . . . . . . . . . 12 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑧 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑧)) ∈ dom ⇝ }
2217, 21eqtri 2643 . . . . . . . . . . 11 𝐷 = {𝑧 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑧)) ∈ dom ⇝ }
23 simpr 477 . . . . . . . . . . 11 ((𝜑𝑥𝐷) → 𝑥𝐷)
246, 7, 8, 9, 16, 22, 23fnlimfvre 39338 . . . . . . . . . 10 ((𝜑𝑥𝐷) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
2524elexd 3203 . . . . . . . . 9 ((𝜑𝑥𝐷) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ V)
265, 25fvmpt2d 6255 . . . . . . . 8 ((𝜑𝑥𝐷) → (𝐺𝑥) = ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
2726, 24eqeltrd 2698 . . . . . . 7 ((𝜑𝑥𝐷) → (𝐺𝑥) ∈ ℝ)
283, 27syldan 487 . . . . . 6 ((𝜑𝑥 ∈ (𝐷𝐼)) → (𝐺𝑥) ∈ ℝ)
2928adantr 481 . . . . 5 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝐺𝑥) ∈ ℝ)
30 smflimlem4.7 . . . . . . . 8 (𝜑𝐴 ∈ ℝ)
3130adantr 481 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → 𝐴 ∈ ℝ)
32 rpre 11791 . . . . . . . 8 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
3332adantl 482 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
3431, 33readdcld 10021 . . . . . 6 ((𝜑𝑦 ∈ ℝ+) → (𝐴 + 𝑦) ∈ ℝ)
3534adantlr 750 . . . . 5 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝐴 + 𝑦) ∈ ℝ)
36 nfv 1840 . . . . . . . 8 𝑚((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+)
37 rphalfcl 11810 . . . . . . . . . . 11 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
38 rpgtrecnn 39092 . . . . . . . . . . 11 ((𝑦 / 2) ∈ ℝ+ → ∃𝑘 ∈ ℕ (1 / 𝑘) < (𝑦 / 2))
3937, 38syl 17 . . . . . . . . . 10 (𝑦 ∈ ℝ+ → ∃𝑘 ∈ ℕ (1 / 𝑘) < (𝑦 / 2))
4039adantl 482 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ∃𝑘 ∈ ℕ (1 / 𝑘) < (𝑦 / 2))
4110ad4antr 767 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → 𝑆 ∈ SAlg)
4213adantlr 750 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑚𝑍) → (𝐹𝑚) ∈ (SMblFn‘𝑆))
4342ad5ant15 1300 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) ∧ 𝑚𝑍) → (𝐹𝑚) ∈ (SMblFn‘𝑆))
4430adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐷𝐼)) → 𝐴 ∈ ℝ)
4544ad3antrrr 765 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → 𝐴 ∈ ℝ)
46 smflimlem4.8 . . . . . . . . . . . . 13 𝑃 = (𝑚𝑍, 𝑘 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
47 nfcv 2761 . . . . . . . . . . . . . 14 𝑘𝑍
48 nfcv 2761 . . . . . . . . . . . . . 14 𝑗𝑍
49 nfcv 2761 . . . . . . . . . . . . . 14 𝑗{𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}
50 nfcv 2761 . . . . . . . . . . . . . 14 𝑘{𝑠𝑆 ∣ {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))}
5118breq1d 4628 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → (((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)) ↔ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑘))))
5251cbvrabv 3188 . . . . . . . . . . . . . . . . . 18 {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑘))}
5352a1i 11 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑗 → {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑘))})
54 oveq2 6618 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → (1 / 𝑘) = (1 / 𝑗))
5554oveq2d 6626 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → (𝐴 + (1 / 𝑘)) = (𝐴 + (1 / 𝑗)))
5655breq2d 4630 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → (((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑘)) ↔ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))))
5756rabbidv 3180 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑗 → {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑘))} = {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))})
5853, 57eqtrd 2655 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑗 → {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))})
5958eqeq1d 2623 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ({𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚)) ↔ {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))))
6059rabbidv 3180 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} = {𝑠𝑆 ∣ {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))})
6147, 48, 49, 50, 60cbvmpt22 38795 . . . . . . . . . . . . 13 (𝑚𝑍, 𝑘 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}) = (𝑚𝑍, 𝑗 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))})
6246, 61eqtri 2643 . . . . . . . . . . . 12 𝑃 = (𝑚𝑍, 𝑗 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))})
63 smflimlem4.9 . . . . . . . . . . . . 13 𝐻 = (𝑚𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))
64 nfcv 2761 . . . . . . . . . . . . . 14 𝑗(𝐶‘(𝑚𝑃𝑘))
65 nfcv 2761 . . . . . . . . . . . . . 14 𝑘(𝐶‘(𝑚𝑃𝑗))
66 oveq2 6618 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝑚𝑃𝑘) = (𝑚𝑃𝑗))
6766fveq2d 6157 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (𝐶‘(𝑚𝑃𝑘)) = (𝐶‘(𝑚𝑃𝑗)))
6847, 48, 64, 65, 67cbvmpt22 38795 . . . . . . . . . . . . 13 (𝑚𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘))) = (𝑚𝑍, 𝑗 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑗)))
6963, 68eqtri 2643 . . . . . . . . . . . 12 𝐻 = (𝑚𝑍, 𝑗 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑗)))
70 smflimlem4.10 . . . . . . . . . . . . 13 𝐼 = 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)
71 simpll 789 . . . . . . . . . . . . . . . . 17 (((𝑘 = 𝑗𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑘 = 𝑗)
7271oveq2d 6626 . . . . . . . . . . . . . . . 16 (((𝑘 = 𝑗𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → (𝑚𝐻𝑘) = (𝑚𝐻𝑗))
7372iineq2dv 4514 . . . . . . . . . . . . . . 15 ((𝑘 = 𝑗𝑛𝑍) → 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) = 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑗))
7473iuneq2dv 4513 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) = 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑗))
7574cbviinv 4531 . . . . . . . . . . . . 13 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) = 𝑗 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑗)
7670, 75eqtri 2643 . . . . . . . . . . . 12 𝐼 = 𝑗 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑗)
77 smflimlem4.11 . . . . . . . . . . . . . 14 ((𝜑𝑟 ∈ ran 𝑃) → (𝐶𝑟) ∈ 𝑟)
7877adantlr 750 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑟 ∈ ran 𝑃) → (𝐶𝑟) ∈ 𝑟)
7978ad5ant15 1300 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) ∧ 𝑟 ∈ ran 𝑃) → (𝐶𝑟) ∈ 𝑟)
80 simp-4r 806 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → 𝑥 ∈ (𝐷𝐼))
81 simplr 791 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → 𝑘 ∈ ℕ)
8237ad3antlr 766 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → (𝑦 / 2) ∈ ℝ+)
83 simpr 477 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → (1 / 𝑘) < (𝑦 / 2))
849, 41, 43, 22, 45, 62, 69, 76, 79, 80, 81, 82, 83smflimlem3 40314 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(𝑥 ∈ dom (𝐹𝑖) ∧ ((𝐹𝑖)‘𝑥) < (𝐴 + (𝑦 / 2))))
8584exp31 629 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝑘 ∈ ℕ → ((1 / 𝑘) < (𝑦 / 2) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(𝑥 ∈ dom (𝐹𝑖) ∧ ((𝐹𝑖)‘𝑥) < (𝐴 + (𝑦 / 2))))))
8685rexlimdv 3024 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (∃𝑘 ∈ ℕ (1 / 𝑘) < (𝑦 / 2) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(𝑥 ∈ dom (𝐹𝑖) ∧ ((𝐹𝑖)‘𝑥) < (𝐴 + (𝑦 / 2)))))
8740, 86mpd 15 . . . . . . . 8 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(𝑥 ∈ dom (𝐹𝑖) ∧ ((𝐹𝑖)‘𝑥) < (𝐴 + (𝑦 / 2))))
88 nfv 1840 . . . . . . . . . 10 𝑖((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+)
89 nfcv 2761 . . . . . . . . . 10 𝑖𝐹
90 nfcv 2761 . . . . . . . . . 10 𝑥𝐹
91 smflimlem4.1 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
9291ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → 𝑀 ∈ ℤ)
93 eleq1 2686 . . . . . . . . . . . . . 14 (𝑚 = 𝑖 → (𝑚𝑍𝑖𝑍))
9493anbi2d 739 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → ((𝜑𝑚𝑍) ↔ (𝜑𝑖𝑍)))
95 fveq2 6153 . . . . . . . . . . . . . 14 (𝑚 = 𝑖 → (𝐹𝑚) = (𝐹𝑖))
9695dmeqd 5291 . . . . . . . . . . . . . 14 (𝑚 = 𝑖 → dom (𝐹𝑚) = dom (𝐹𝑖))
9795, 96feq12d 5995 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → ((𝐹𝑚):dom (𝐹𝑚)⟶ℝ ↔ (𝐹𝑖):dom (𝐹𝑖)⟶ℝ))
9894, 97imbi12d 334 . . . . . . . . . . . 12 (𝑚 = 𝑖 → (((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ) ↔ ((𝜑𝑖𝑍) → (𝐹𝑖):dom (𝐹𝑖)⟶ℝ)))
9998, 15chvarv 2262 . . . . . . . . . . 11 ((𝜑𝑖𝑍) → (𝐹𝑖):dom (𝐹𝑖)⟶ℝ)
10099ad4ant14 1290 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑖𝑍) → (𝐹𝑖):dom (𝐹𝑖)⟶ℝ)
101 fveq2 6153 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑙 → (𝐹𝑚) = (𝐹𝑙))
102101dmeqd 5291 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑙 → dom (𝐹𝑚) = dom (𝐹𝑙))
103102cbviinv 4531 . . . . . . . . . . . . . . 15 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙)
104103a1i 11 . . . . . . . . . . . . . 14 (𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙))
105104iuneq2i 4510 . . . . . . . . . . . . 13 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑛𝑍 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙)
106 fveq2 6153 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → (ℤ𝑛) = (ℤ𝑚))
107106iineq1d 38785 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙) = 𝑙 ∈ (ℤ𝑚)dom (𝐹𝑙))
108 fveq2 6153 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑖 → (𝐹𝑙) = (𝐹𝑖))
109108dmeqd 5291 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑖 → dom (𝐹𝑙) = dom (𝐹𝑖))
110109cbviinv 4531 . . . . . . . . . . . . . . . 16 𝑙 ∈ (ℤ𝑚)dom (𝐹𝑙) = 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖)
111110a1i 11 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 𝑙 ∈ (ℤ𝑚)dom (𝐹𝑙) = 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖))
112107, 111eqtrd 2655 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙) = 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖))
113112cbviunv 4530 . . . . . . . . . . . . 13 𝑛𝑍 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙) = 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖)
114105, 113eqtri 2643 . . . . . . . . . . . 12 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖)
115114rabeqi 38821 . . . . . . . . . . 11 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑥 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
116 fveq2 6153 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑚 → (𝐹𝑖) = (𝐹𝑚))
117116fveq1d 6155 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑚 → ((𝐹𝑖)‘𝑥) = ((𝐹𝑚)‘𝑥))
118117cbvmptv 4715 . . . . . . . . . . . . . . 15 (𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))
119118eqcomi 2630 . . . . . . . . . . . . . 14 (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥))
120119eleq1i 2689 . . . . . . . . . . . . 13 ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥)) ∈ dom ⇝ )
121120a1i 11 . . . . . . . . . . . 12 (𝑥 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖) → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥)) ∈ dom ⇝ ))
122121rabbiia 3176 . . . . . . . . . . 11 {𝑥 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑥 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖) ∣ (𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥)) ∈ dom ⇝ }
12317, 115, 1223eqtri 2647 . . . . . . . . . 10 𝐷 = {𝑥 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖) ∣ (𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥)) ∈ dom ⇝ }
124119fveq2i 6156 . . . . . . . . . . . 12 ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥)))
125124mpteq2i 4706 . . . . . . . . . . 11 (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))) = (𝑥𝐷 ↦ ( ⇝ ‘(𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥))))
1264, 125eqtri 2643 . . . . . . . . . 10 𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥))))
1273adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → 𝑥𝐷)
12837adantl 482 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ+)
12988, 89, 90, 92, 9, 100, 123, 126, 127, 128fnlimabslt 39343 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2)))
13029adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → (𝐺𝑥) ∈ ℝ)
131 simpr 477 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → ((𝐹𝑖)‘𝑥) ∈ ℝ)
132130, 131resubcld 10410 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → ((𝐺𝑥) − ((𝐹𝑖)‘𝑥)) ∈ ℝ)
133132adantrr 752 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → ((𝐺𝑥) − ((𝐹𝑖)‘𝑥)) ∈ ℝ)
134132recnd 10020 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → ((𝐺𝑥) − ((𝐹𝑖)‘𝑥)) ∈ ℂ)
135134abscld 14117 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))) ∈ ℝ)
136135adantrr 752 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))) ∈ ℝ)
13732rehalfcld 11231 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ)
138137ad2antlr 762 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (𝑦 / 2) ∈ ℝ)
139133leabsd 14095 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → ((𝐺𝑥) − ((𝐹𝑖)‘𝑥)) ≤ (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))))
14028recnd 10020 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (𝐷𝐼)) → (𝐺𝑥) ∈ ℂ)
141140adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → (𝐺𝑥) ∈ ℂ)
142 recn 9978 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑖)‘𝑥) ∈ ℝ → ((𝐹𝑖)‘𝑥) ∈ ℂ)
143142adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → ((𝐹𝑖)‘𝑥) ∈ ℂ)
144141, 143abssubd 14134 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))) = (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))))
145144adantrr 752 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))) = (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))))
146 simprr 795 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))
147145, 146eqbrtrd 4640 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))) < (𝑦 / 2))
148147adantlr 750 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))) < (𝑦 / 2))
149133, 136, 138, 139, 148lelttrd 10147 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → ((𝐺𝑥) − ((𝐹𝑖)‘𝑥)) < (𝑦 / 2))
15029adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (𝐺𝑥) ∈ ℝ)
151 simprl 793 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → ((𝐹𝑖)‘𝑥) ∈ ℝ)
152150, 151, 138ltsubadd2d 10577 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (((𝐺𝑥) − ((𝐹𝑖)‘𝑥)) < (𝑦 / 2) ↔ (𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2))))
153149, 152mpbid 222 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2)))
154153ex 450 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ((((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2)) → (𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2))))
155154ad2antrr 761 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ 𝑖 ∈ (ℤ𝑚)) → ((((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2)) → (𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2))))
156155ralimdva 2957 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) → (∀𝑖 ∈ (ℤ𝑚)(((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2)) → ∀𝑖 ∈ (ℤ𝑚)(𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2))))
157156ex 450 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝑚𝑍 → (∀𝑖 ∈ (ℤ𝑚)(((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2)) → ∀𝑖 ∈ (ℤ𝑚)(𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2)))))
15836, 157reximdai 3007 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2)) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2))))
159129, 158mpd 15 . . . . . . . 8 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2)))
160116dmeqd 5291 . . . . . . . . . 10 (𝑖 = 𝑚 → dom (𝐹𝑖) = dom (𝐹𝑚))
161160eleq2d 2684 . . . . . . . . 9 (𝑖 = 𝑚 → (𝑥 ∈ dom (𝐹𝑖) ↔ 𝑥 ∈ dom (𝐹𝑚)))
162117breq1d 4628 . . . . . . . . 9 (𝑖 = 𝑚 → (((𝐹𝑖)‘𝑥) < (𝐴 + (𝑦 / 2)) ↔ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))))
163161, 162anbi12d 746 . . . . . . . 8 (𝑖 = 𝑚 → ((𝑥 ∈ dom (𝐹𝑖) ∧ ((𝐹𝑖)‘𝑥) < (𝐴 + (𝑦 / 2))) ↔ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))))
164117oveq1d 6625 . . . . . . . . 9 (𝑖 = 𝑚 → (((𝐹𝑖)‘𝑥) + (𝑦 / 2)) = (((𝐹𝑚)‘𝑥) + (𝑦 / 2)))
165164breq2d 4630 . . . . . . . 8 (𝑖 = 𝑚 → ((𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2)) ↔ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))))
16636, 9, 87, 159, 163, 165rexanuz3 38793 . . . . . . 7 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ∃𝑚𝑍 ((𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))))
167 df-3an 1038 . . . . . . . . 9 ((𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))) ↔ ((𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))))
168 3ancomb 1045 . . . . . . . . 9 ((𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))) ↔ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))))
169167, 168bitr3i 266 . . . . . . . 8 (((𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))) ↔ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))))
170169rexbii 3035 . . . . . . 7 (∃𝑚𝑍 ((𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))) ↔ ∃𝑚𝑍 (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))))
171166, 170sylib 208 . . . . . 6 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ∃𝑚𝑍 (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))))
17229ad2antrr 761 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐺𝑥) ∈ ℝ)
173153adant3 1079 . . . . . . . . . . . . . . 15 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
174 simp3 1061 . . . . . . . . . . . . . . 15 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → 𝑥 ∈ dom (𝐹𝑚))
175173, 174ffvelrnd 6321 . . . . . . . . . . . . . 14 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → ((𝐹𝑚)‘𝑥) ∈ ℝ)
176175ad4ant134 1293 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ 𝑥 ∈ dom (𝐹𝑚)) → ((𝐹𝑚)‘𝑥) ∈ ℝ)
177 simpllr 798 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ 𝑥 ∈ dom (𝐹𝑚)) → 𝑦 ∈ ℝ+)
178177, 137syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ 𝑥 ∈ dom (𝐹𝑚)) → (𝑦 / 2) ∈ ℝ)
179176, 178readdcld 10021 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ 𝑥 ∈ dom (𝐹𝑚)) → (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∈ ℝ)
180179adantlllr 38717 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ 𝑥 ∈ dom (𝐹𝑚)) → (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∈ ℝ)
1811803ad2antr1 1224 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∈ ℝ)
182 rehalfcl 11210 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ → (𝑦 / 2) ∈ ℝ)
18333, 182syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ)
18431, 183jca 554 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ+) → (𝐴 ∈ ℝ ∧ (𝑦 / 2) ∈ ℝ))
185 readdcl 9971 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ (𝑦 / 2) ∈ ℝ) → (𝐴 + (𝑦 / 2)) ∈ ℝ)
186184, 185syl 17 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ+) → (𝐴 + (𝑦 / 2)) ∈ ℝ)
187186, 183readdcld 10021 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) ∈ ℝ)
188187ad5ant13 1298 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) ∈ ℝ)
189 simpr2 1066 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)))
190176adantrr 752 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → ((𝐹𝑚)‘𝑥) ∈ ℝ)
191186ad2antrr 761 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐴 + (𝑦 / 2)) ∈ ℝ)
192178adantrr 752 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝑦 / 2) ∈ ℝ)
193 simprr 795 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))
194190, 191, 192, 193ltadd1dd 10590 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) < ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)))
195194adantlllr 38717 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) < ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)))
1961953adantr2 1219 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) < ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)))
197172, 181, 188, 189, 196lttrd 10150 . . . . . . . . 9 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐺𝑥) < ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)))
19831recnd 10020 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ+) → 𝐴 ∈ ℂ)
199183recnd 10020 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℂ)
200198, 199, 199addassd 10014 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) = (𝐴 + ((𝑦 / 2) + (𝑦 / 2))))
20132recnd 10020 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+𝑦 ∈ ℂ)
202 2halves 11212 . . . . . . . . . . . . . 14 (𝑦 ∈ ℂ → ((𝑦 / 2) + (𝑦 / 2)) = 𝑦)
203201, 202syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+ → ((𝑦 / 2) + (𝑦 / 2)) = 𝑦)
204203oveq2d 6626 . . . . . . . . . . . 12 (𝑦 ∈ ℝ+ → (𝐴 + ((𝑦 / 2) + (𝑦 / 2))) = (𝐴 + 𝑦))
205204adantl 482 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → (𝐴 + ((𝑦 / 2) + (𝑦 / 2))) = (𝐴 + 𝑦))
206200, 205eqtrd 2655 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) = (𝐴 + 𝑦))
207206ad5ant13 1298 . . . . . . . . 9 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) = (𝐴 + 𝑦))
208197, 207breqtrd 4644 . . . . . . . 8 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐺𝑥) < (𝐴 + 𝑦))
209208exp31 629 . . . . . . 7 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝑚𝑍 → ((𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) → (𝐺𝑥) < (𝐴 + 𝑦))))
210209rexlimdv 3024 . . . . . 6 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (∃𝑚𝑍 (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) → (𝐺𝑥) < (𝐴 + 𝑦)))
211171, 210mpd 15 . . . . 5 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝐺𝑥) < (𝐴 + 𝑦))
21229, 35, 211ltled 10137 . . . 4 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝐺𝑥) ≤ (𝐴 + 𝑦))
213212ralrimiva 2961 . . 3 ((𝜑𝑥 ∈ (𝐷𝐼)) → ∀𝑦 ∈ ℝ+ (𝐺𝑥) ≤ (𝐴 + 𝑦))
214 alrple 11988 . . . 4 (((𝐺𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝐺𝑥) ≤ 𝐴 ↔ ∀𝑦 ∈ ℝ+ (𝐺𝑥) ≤ (𝐴 + 𝑦)))
21528, 44, 214syl2anc 692 . . 3 ((𝜑𝑥 ∈ (𝐷𝐼)) → ((𝐺𝑥) ≤ 𝐴 ↔ ∀𝑦 ∈ ℝ+ (𝐺𝑥) ≤ (𝐴 + 𝑦)))
216213, 215mpbird 247 . 2 ((𝜑𝑥 ∈ (𝐷𝐼)) → (𝐺𝑥) ≤ 𝐴)
2172, 216ssrabdv 3665 1 (𝜑 → (𝐷𝐼) ⊆ {𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908  {crab 2911  Vcvv 3189   ∩ cin 3558   ⊆ wss 3559  ∪ ciun 4490  ∩ ciin 4491   class class class wbr 4618   ↦ cmpt 4678  dom cdm 5079  ran crn 5080  ⟶wf 5848  ‘cfv 5852  (class class class)co 6610   ↦ cmpt2 6612  ℂcc 9886  ℝcr 9887  1c1 9889   + caddc 9891   < clt 10026   ≤ cle 10027   − cmin 10218   / cdiv 10636  ℕcn 10972  2c2 11022  ℤcz 11329  ℤ≥cuz 11639  ℝ+crp 11784  abscabs 13916   ⇝ cli 14157  SAlgcsalg 39861  SMblFncsmblfn 40242 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-er 7694  df-pm 7812  df-en 7908  df-dom 7909  df-sdom 7910  df-sup 8300  df-inf 8301  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-n0 11245  df-z 11330  df-uz 11640  df-q 11741  df-rp 11785  df-ioo 12129  df-ico 12131  df-fl 12541  df-seq 12750  df-exp 12809  df-cj 13781  df-re 13782  df-im 13783  df-sqrt 13917  df-abs 13918  df-clim 14161  df-rlim 14162  df-smblfn 40243 This theorem is referenced by:  smflimlem5  40316
 Copyright terms: Public domain W3C validator