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

Theorem smflimlem4 45005
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 4188 . . 3 (𝐷𝐼) ⊆ 𝐷
21a1i 11 . 2 (𝜑 → (𝐷𝐼) ⊆ 𝐷)
32sselda 3944 . . . . . . 7 ((𝜑𝑥 ∈ (𝐷𝐼)) → 𝑥𝐷)
4 smflimlem4.6 . . . . . . . . . 10 𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
54a1i 11 . . . . . . . . 9 (𝜑𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))))
6 nfv 1917 . . . . . . . . . . 11 𝑚(𝜑𝑥𝐷)
7 nfcv 2907 . . . . . . . . . . 11 𝑚𝐹
8 nfcv 2907 . . . . . . . . . . 11 𝑧𝐹
9 smflimlem4.2 . . . . . . . . . . 11 𝑍 = (ℤ𝑀)
10 smflimlem4.3 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ SAlg)
1110adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑚𝑍) → 𝑆 ∈ SAlg)
12 smflimlem4.4 . . . . . . . . . . . . . 14 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
1312ffvelcdmda 7035 . . . . . . . . . . . . 13 ((𝜑𝑚𝑍) → (𝐹𝑚) ∈ (SMblFn‘𝑆))
14 eqid 2736 . . . . . . . . . . . . 13 dom (𝐹𝑚) = dom (𝐹𝑚)
1511, 13, 14smff 44963 . . . . . . . . . . . 12 ((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
1615adantlr 713 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
17 smflimlem4.5 . . . . . . . . . . . 12 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
18 fveq2 6842 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑚)‘𝑧))
1918mpteq2dv 5207 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑧)))
2019eleq1d 2822 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑧)) ∈ dom ⇝ ))
2120cbvrabv 3417 . . . . . . . . . . . 12 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑧 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑧)) ∈ dom ⇝ }
2217, 21eqtri 2764 . . . . . . . . . . 11 𝐷 = {𝑧 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑧)) ∈ dom ⇝ }
23 simpr 485 . . . . . . . . . . 11 ((𝜑𝑥𝐷) → 𝑥𝐷)
246, 7, 8, 9, 16, 22, 23fnlimfvre 43905 . . . . . . . . . 10 ((𝜑𝑥𝐷) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
2524elexd 3465 . . . . . . . . 9 ((𝜑𝑥𝐷) → ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ V)
265, 25fvmpt2d 6961 . . . . . . . 8 ((𝜑𝑥𝐷) → (𝐺𝑥) = ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
2726, 24eqeltrd 2838 . . . . . . 7 ((𝜑𝑥𝐷) → (𝐺𝑥) ∈ ℝ)
283, 27syldan 591 . . . . . 6 ((𝜑𝑥 ∈ (𝐷𝐼)) → (𝐺𝑥) ∈ ℝ)
2928adantr 481 . . . . 5 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝐺𝑥) ∈ ℝ)
30 smflimlem4.7 . . . . . . . 8 (𝜑𝐴 ∈ ℝ)
3130adantr 481 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → 𝐴 ∈ ℝ)
32 rpre 12923 . . . . . . . 8 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
3332adantl 482 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
3431, 33readdcld 11184 . . . . . 6 ((𝜑𝑦 ∈ ℝ+) → (𝐴 + 𝑦) ∈ ℝ)
3534adantlr 713 . . . . 5 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝐴 + 𝑦) ∈ ℝ)
36 nfv 1917 . . . . . . . 8 𝑚((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+)
37 rphalfcl 12942 . . . . . . . . . . 11 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
38 rpgtrecnn 43604 . . . . . . . . . . 11 ((𝑦 / 2) ∈ ℝ+ → ∃𝑘 ∈ ℕ (1 / 𝑘) < (𝑦 / 2))
3937, 38syl 17 . . . . . . . . . 10 (𝑦 ∈ ℝ+ → ∃𝑘 ∈ ℕ (1 / 𝑘) < (𝑦 / 2))
4039adantl 482 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ∃𝑘 ∈ ℕ (1 / 𝑘) < (𝑦 / 2))
4110ad4antr 730 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → 𝑆 ∈ SAlg)
4213adantlr 713 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑚𝑍) → (𝐹𝑚) ∈ (SMblFn‘𝑆))
4342ad5ant15 757 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) ∧ 𝑚𝑍) → (𝐹𝑚) ∈ (SMblFn‘𝑆))
4430adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐷𝐼)) → 𝐴 ∈ ℝ)
4544ad3antrrr 728 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → 𝐴 ∈ ℝ)
46 smflimlem4.8 . . . . . . . . . . . 12 𝑃 = (𝑚𝑍, 𝑘 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))})
47 nfcv 2907 . . . . . . . . . . . . 13 𝑘𝑍
48 nfcv 2907 . . . . . . . . . . . . 13 𝑗𝑍
49 nfcv 2907 . . . . . . . . . . . . 13 𝑗{𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}
50 nfcv 2907 . . . . . . . . . . . . 13 𝑘{𝑠𝑆 ∣ {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))}
5118breq1d 5115 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)) ↔ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑘))))
5251cbvrabv 3417 . . . . . . . . . . . . . . . . 17 {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑘))}
5352a1i 11 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑗 → {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑘))})
54 oveq2 7365 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → (1 / 𝑘) = (1 / 𝑗))
5554oveq2d 7373 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → (𝐴 + (1 / 𝑘)) = (𝐴 + (1 / 𝑗)))
5655breq2d 5117 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑗 → (((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑘)) ↔ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))))
5756rabbidv 3415 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑗 → {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑘))} = {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))})
5853, 57eqtrd 2776 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))})
5958eqeq1d 2738 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ({𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚)) ↔ {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))))
6059rabbidv 3415 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))} = {𝑠𝑆 ∣ {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))})
6147, 48, 49, 50, 60cbvmpo2 43297 . . . . . . . . . . . 12 (𝑚𝑍, 𝑘 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑥 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹𝑚))}) = (𝑚𝑍, 𝑗 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))})
6246, 61eqtri 2764 . . . . . . . . . . 11 𝑃 = (𝑚𝑍, 𝑗 ∈ ℕ ↦ {𝑠𝑆 ∣ {𝑧 ∈ dom (𝐹𝑚) ∣ ((𝐹𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹𝑚))})
63 smflimlem4.9 . . . . . . . . . . . 12 𝐻 = (𝑚𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))
64 nfcv 2907 . . . . . . . . . . . . 13 𝑗(𝐶‘(𝑚𝑃𝑘))
65 nfcv 2907 . . . . . . . . . . . . 13 𝑘(𝐶‘(𝑚𝑃𝑗))
66 oveq2 7365 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (𝑚𝑃𝑘) = (𝑚𝑃𝑗))
6766fveq2d 6846 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (𝐶‘(𝑚𝑃𝑘)) = (𝐶‘(𝑚𝑃𝑗)))
6847, 48, 64, 65, 67cbvmpo2 43297 . . . . . . . . . . . 12 (𝑚𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘))) = (𝑚𝑍, 𝑗 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑗)))
6963, 68eqtri 2764 . . . . . . . . . . 11 𝐻 = (𝑚𝑍, 𝑗 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑗)))
70 smflimlem4.10 . . . . . . . . . . . 12 𝐼 = 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘)
71 simpll 765 . . . . . . . . . . . . . . . 16 (((𝑘 = 𝑗𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑘 = 𝑗)
7271oveq2d 7373 . . . . . . . . . . . . . . 15 (((𝑘 = 𝑗𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → (𝑚𝐻𝑘) = (𝑚𝐻𝑗))
7372iineq2dv 4979 . . . . . . . . . . . . . 14 ((𝑘 = 𝑗𝑛𝑍) → 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) = 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑗))
7473iuneq2dv 4978 . . . . . . . . . . . . 13 (𝑘 = 𝑗 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) = 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑗))
7574cbviinv 5001 . . . . . . . . . . . 12 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑘) = 𝑗 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑗)
7670, 75eqtri 2764 . . . . . . . . . . 11 𝐼 = 𝑗 ∈ ℕ 𝑛𝑍 𝑚 ∈ (ℤ𝑛)(𝑚𝐻𝑗)
77 smflimlem4.11 . . . . . . . . . . . . 13 ((𝜑𝑟 ∈ ran 𝑃) → (𝐶𝑟) ∈ 𝑟)
7877adantlr 713 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑟 ∈ ran 𝑃) → (𝐶𝑟) ∈ 𝑟)
7978ad5ant15 757 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) ∧ 𝑟 ∈ ran 𝑃) → (𝐶𝑟) ∈ 𝑟)
80 simp-4r 782 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → 𝑥 ∈ (𝐷𝐼))
81 simplr 767 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → 𝑘 ∈ ℕ)
8237ad3antlr 729 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → (𝑦 / 2) ∈ ℝ+)
83 simpr 485 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → (1 / 𝑘) < (𝑦 / 2))
849, 41, 43, 22, 45, 62, 69, 76, 79, 80, 81, 82, 83smflimlem3 45004 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 / 𝑘) < (𝑦 / 2)) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(𝑥 ∈ dom (𝐹𝑖) ∧ ((𝐹𝑖)‘𝑥) < (𝐴 + (𝑦 / 2))))
8584rexlimdva2 3154 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (∃𝑘 ∈ ℕ (1 / 𝑘) < (𝑦 / 2) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(𝑥 ∈ dom (𝐹𝑖) ∧ ((𝐹𝑖)‘𝑥) < (𝐴 + (𝑦 / 2)))))
8640, 85mpd 15 . . . . . . . 8 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(𝑥 ∈ dom (𝐹𝑖) ∧ ((𝐹𝑖)‘𝑥) < (𝐴 + (𝑦 / 2))))
87 nfv 1917 . . . . . . . . . 10 𝑖((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+)
88 nfcv 2907 . . . . . . . . . 10 𝑖𝐹
89 nfcv 2907 . . . . . . . . . 10 𝑥𝐹
90 smflimlem4.1 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
9190ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → 𝑀 ∈ ℤ)
92 eleq1w 2820 . . . . . . . . . . . . . 14 (𝑚 = 𝑖 → (𝑚𝑍𝑖𝑍))
9392anbi2d 629 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → ((𝜑𝑚𝑍) ↔ (𝜑𝑖𝑍)))
94 fveq2 6842 . . . . . . . . . . . . . 14 (𝑚 = 𝑖 → (𝐹𝑚) = (𝐹𝑖))
9594dmeqd 5861 . . . . . . . . . . . . . 14 (𝑚 = 𝑖 → dom (𝐹𝑚) = dom (𝐹𝑖))
9694, 95feq12d 6656 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → ((𝐹𝑚):dom (𝐹𝑚)⟶ℝ ↔ (𝐹𝑖):dom (𝐹𝑖)⟶ℝ))
9793, 96imbi12d 344 . . . . . . . . . . . 12 (𝑚 = 𝑖 → (((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ) ↔ ((𝜑𝑖𝑍) → (𝐹𝑖):dom (𝐹𝑖)⟶ℝ)))
9897, 15chvarvv 2002 . . . . . . . . . . 11 ((𝜑𝑖𝑍) → (𝐹𝑖):dom (𝐹𝑖)⟶ℝ)
9998ad4ant14 750 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑖𝑍) → (𝐹𝑖):dom (𝐹𝑖)⟶ℝ)
100 fveq2 6842 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑙 → (𝐹𝑚) = (𝐹𝑙))
101100dmeqd 5861 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑙 → dom (𝐹𝑚) = dom (𝐹𝑙))
102101cbviinv 5001 . . . . . . . . . . . . . . 15 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙)
103102a1i 11 . . . . . . . . . . . . . 14 (𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙))
104103iuneq2i 4975 . . . . . . . . . . . . 13 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑛𝑍 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙)
105 fveq2 6842 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → (ℤ𝑛) = (ℤ𝑚))
106105iineq1d 43290 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙) = 𝑙 ∈ (ℤ𝑚)dom (𝐹𝑙))
107 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑖 → (𝐹𝑙) = (𝐹𝑖))
108107dmeqd 5861 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑖 → dom (𝐹𝑙) = dom (𝐹𝑖))
109108cbviinv 5001 . . . . . . . . . . . . . . . 16 𝑙 ∈ (ℤ𝑚)dom (𝐹𝑙) = 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖)
110109a1i 11 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 𝑙 ∈ (ℤ𝑚)dom (𝐹𝑙) = 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖))
111106, 110eqtrd 2776 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙) = 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖))
112111cbviunv 5000 . . . . . . . . . . . . 13 𝑛𝑍 𝑙 ∈ (ℤ𝑛)dom (𝐹𝑙) = 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖)
113104, 112eqtri 2764 . . . . . . . . . . . 12 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) = 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖)
114113rabeqi 3420 . . . . . . . . . . 11 {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑥 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ }
115 fveq2 6842 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑚 → (𝐹𝑖) = (𝐹𝑚))
116115fveq1d 6844 . . . . . . . . . . . . . . 15 (𝑖 = 𝑚 → ((𝐹𝑖)‘𝑥) = ((𝐹𝑚)‘𝑥))
117116cbvmptv 5218 . . . . . . . . . . . . . 14 (𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))
118117eqcomi 2745 . . . . . . . . . . . . 13 (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥))
119118eleq1i 2828 . . . . . . . . . . . 12 ((𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥)) ∈ dom ⇝ )
120119rabbii 3413 . . . . . . . . . . 11 {𝑥 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖) ∣ (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑥 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖) ∣ (𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥)) ∈ dom ⇝ }
12117, 114, 1203eqtri 2768 . . . . . . . . . 10 𝐷 = {𝑥 𝑚𝑍 𝑖 ∈ (ℤ𝑚)dom (𝐹𝑖) ∣ (𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥)) ∈ dom ⇝ }
122118fveq2i 6845 . . . . . . . . . . . 12 ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥)))
123122mpteq2i 5210 . . . . . . . . . . 11 (𝑥𝐷 ↦ ( ⇝ ‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))) = (𝑥𝐷 ↦ ( ⇝ ‘(𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥))))
1244, 123eqtri 2764 . . . . . . . . . 10 𝐺 = (𝑥𝐷 ↦ ( ⇝ ‘(𝑖𝑍 ↦ ((𝐹𝑖)‘𝑥))))
1253adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → 𝑥𝐷)
12637adantl 482 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ+)
12787, 88, 89, 91, 9, 99, 121, 124, 125, 126fnlimabslt 43910 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2)))
12829adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → (𝐺𝑥) ∈ ℝ)
129 simpr 485 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → ((𝐹𝑖)‘𝑥) ∈ ℝ)
130128, 129resubcld 11583 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → ((𝐺𝑥) − ((𝐹𝑖)‘𝑥)) ∈ ℝ)
131130adantrr 715 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → ((𝐺𝑥) − ((𝐹𝑖)‘𝑥)) ∈ ℝ)
132130recnd 11183 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → ((𝐺𝑥) − ((𝐹𝑖)‘𝑥)) ∈ ℂ)
133132abscld 15321 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))) ∈ ℝ)
134133adantrr 715 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))) ∈ ℝ)
13532rehalfcld 12400 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ)
136135ad2antlr 725 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (𝑦 / 2) ∈ ℝ)
137131leabsd 15299 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → ((𝐺𝑥) − ((𝐹𝑖)‘𝑥)) ≤ (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))))
13828recnd 11183 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (𝐷𝐼)) → (𝐺𝑥) ∈ ℂ)
139138adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → (𝐺𝑥) ∈ ℂ)
140 recn 11141 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑖)‘𝑥) ∈ ℝ → ((𝐹𝑖)‘𝑥) ∈ ℂ)
141140adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → ((𝐹𝑖)‘𝑥) ∈ ℂ)
142139, 141abssubd 15338 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ ((𝐹𝑖)‘𝑥) ∈ ℝ) → (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))) = (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))))
143142adantrr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))) = (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))))
144 simprr 771 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))
145143, 144eqbrtrd 5127 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))) < (𝑦 / 2))
146145adantlr 713 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (abs‘((𝐺𝑥) − ((𝐹𝑖)‘𝑥))) < (𝑦 / 2))
147131, 134, 136, 137, 146lelttrd 11313 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → ((𝐺𝑥) − ((𝐹𝑖)‘𝑥)) < (𝑦 / 2))
14829adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (𝐺𝑥) ∈ ℝ)
149 simprl 769 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → ((𝐹𝑖)‘𝑥) ∈ ℝ)
150148, 149, 136ltsubadd2d 11753 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (((𝐺𝑥) − ((𝐹𝑖)‘𝑥)) < (𝑦 / 2) ↔ (𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2))))
151147, 150mpbid 231 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2))) → (𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2)))
152151ex 413 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ((((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2)) → (𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2))))
153152ad2antrr 724 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ 𝑖 ∈ (ℤ𝑚)) → ((((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2)) → (𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2))))
154153ralimdva 3164 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) → (∀𝑖 ∈ (ℤ𝑚)(((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2)) → ∀𝑖 ∈ (ℤ𝑚)(𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2))))
155154ex 413 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝑚𝑍 → (∀𝑖 ∈ (ℤ𝑚)(((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2)) → ∀𝑖 ∈ (ℤ𝑚)(𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2)))))
15636, 155reximdai 3244 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(((𝐹𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹𝑖)‘𝑥) − (𝐺𝑥))) < (𝑦 / 2)) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2))))
157127, 156mpd 15 . . . . . . . 8 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ∃𝑚𝑍𝑖 ∈ (ℤ𝑚)(𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2)))
158115dmeqd 5861 . . . . . . . . . 10 (𝑖 = 𝑚 → dom (𝐹𝑖) = dom (𝐹𝑚))
159158eleq2d 2823 . . . . . . . . 9 (𝑖 = 𝑚 → (𝑥 ∈ dom (𝐹𝑖) ↔ 𝑥 ∈ dom (𝐹𝑚)))
160116breq1d 5115 . . . . . . . . 9 (𝑖 = 𝑚 → (((𝐹𝑖)‘𝑥) < (𝐴 + (𝑦 / 2)) ↔ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))))
161159, 160anbi12d 631 . . . . . . . 8 (𝑖 = 𝑚 → ((𝑥 ∈ dom (𝐹𝑖) ∧ ((𝐹𝑖)‘𝑥) < (𝐴 + (𝑦 / 2))) ↔ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))))
162116oveq1d 7372 . . . . . . . . 9 (𝑖 = 𝑚 → (((𝐹𝑖)‘𝑥) + (𝑦 / 2)) = (((𝐹𝑚)‘𝑥) + (𝑦 / 2)))
163162breq2d 5117 . . . . . . . 8 (𝑖 = 𝑚 → ((𝐺𝑥) < (((𝐹𝑖)‘𝑥) + (𝑦 / 2)) ↔ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))))
16436, 9, 86, 157, 161, 163rexanuz3 43296 . . . . . . 7 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ∃𝑚𝑍 ((𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))))
165 df-3an 1089 . . . . . . . . 9 ((𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))) ↔ ((𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))))
166 3ancomb 1099 . . . . . . . . 9 ((𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))) ↔ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))))
167165, 166bitr3i 276 . . . . . . . 8 (((𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))) ↔ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))))
168167rexbii 3097 . . . . . . 7 (∃𝑚𝑍 ((𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2))) ↔ ∃𝑚𝑍 (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))))
169164, 168sylib 217 . . . . . 6 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → ∃𝑚𝑍 (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))))
17029ad2antrr 724 . . . . . . . . 9 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐺𝑥) ∈ ℝ)
171153adant3 1132 . . . . . . . . . . . . . 14 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
172 simp3 1138 . . . . . . . . . . . . . 14 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → 𝑥 ∈ dom (𝐹𝑚))
173171, 172ffvelcdmd 7036 . . . . . . . . . . . . 13 ((𝜑𝑚𝑍𝑥 ∈ dom (𝐹𝑚)) → ((𝐹𝑚)‘𝑥) ∈ ℝ)
174173ad4ant134 1174 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ 𝑥 ∈ dom (𝐹𝑚)) → ((𝐹𝑚)‘𝑥) ∈ ℝ)
175 simpllr 774 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ 𝑥 ∈ dom (𝐹𝑚)) → 𝑦 ∈ ℝ+)
176175, 135syl 17 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ 𝑥 ∈ dom (𝐹𝑚)) → (𝑦 / 2) ∈ ℝ)
177174, 176readdcld 11184 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ 𝑥 ∈ dom (𝐹𝑚)) → (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∈ ℝ)
178177adantl3r 748 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ 𝑥 ∈ dom (𝐹𝑚)) → (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∈ ℝ)
1791783ad2antr1 1188 . . . . . . . . 9 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∈ ℝ)
180 rehalfcl 12379 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ → (𝑦 / 2) ∈ ℝ)
18133, 180syl 17 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ)
18231, 181jca 512 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ+) → (𝐴 ∈ ℝ ∧ (𝑦 / 2) ∈ ℝ))
183 readdcl 11134 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ (𝑦 / 2) ∈ ℝ) → (𝐴 + (𝑦 / 2)) ∈ ℝ)
184182, 183syl 17 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → (𝐴 + (𝑦 / 2)) ∈ ℝ)
185184, 181readdcld 11184 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) ∈ ℝ)
186185ad5ant13 755 . . . . . . . . 9 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) ∈ ℝ)
187 simpr2 1195 . . . . . . . . 9 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)))
188174adantrr 715 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → ((𝐹𝑚)‘𝑥) ∈ ℝ)
189184ad2antrr 724 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐴 + (𝑦 / 2)) ∈ ℝ)
190176adantrr 715 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝑦 / 2) ∈ ℝ)
191 simprr 771 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))
192188, 189, 190, 191ltadd1dd 11766 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) < ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)))
193192adantl3r 748 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) < ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)))
1941933adantr2 1170 . . . . . . . . 9 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) < ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)))
195170, 179, 186, 187, 194lttrd 11316 . . . . . . . 8 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐺𝑥) < ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)))
19631recnd 11183 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → 𝐴 ∈ ℂ)
197181recnd 11183 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℂ)
198196, 197, 197addassd 11177 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) = (𝐴 + ((𝑦 / 2) + (𝑦 / 2))))
19932recnd 11183 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+𝑦 ∈ ℂ)
200 2halves 12381 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ → ((𝑦 / 2) + (𝑦 / 2)) = 𝑦)
201199, 200syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ℝ+ → ((𝑦 / 2) + (𝑦 / 2)) = 𝑦)
202201oveq2d 7373 . . . . . . . . . . 11 (𝑦 ∈ ℝ+ → (𝐴 + ((𝑦 / 2) + (𝑦 / 2))) = (𝐴 + 𝑦))
203202adantl 482 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ+) → (𝐴 + ((𝑦 / 2) + (𝑦 / 2))) = (𝐴 + 𝑦))
204198, 203eqtrd 2776 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ+) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) = (𝐴 + 𝑦))
205204ad5ant13 755 . . . . . . . 8 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) = (𝐴 + 𝑦))
206195, 205breqtrd 5131 . . . . . . 7 (((((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚𝑍) ∧ (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐺𝑥) < (𝐴 + 𝑦))
207206rexlimdva2 3154 . . . . . 6 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (∃𝑚𝑍 (𝑥 ∈ dom (𝐹𝑚) ∧ (𝐺𝑥) < (((𝐹𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) → (𝐺𝑥) < (𝐴 + 𝑦)))
208169, 207mpd 15 . . . . 5 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝐺𝑥) < (𝐴 + 𝑦))
20929, 35, 208ltled 11303 . . . 4 (((𝜑𝑥 ∈ (𝐷𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝐺𝑥) ≤ (𝐴 + 𝑦))
210209ralrimiva 3143 . . 3 ((𝜑𝑥 ∈ (𝐷𝐼)) → ∀𝑦 ∈ ℝ+ (𝐺𝑥) ≤ (𝐴 + 𝑦))
211 alrple 13125 . . . 4 (((𝐺𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝐺𝑥) ≤ 𝐴 ↔ ∀𝑦 ∈ ℝ+ (𝐺𝑥) ≤ (𝐴 + 𝑦)))
21228, 44, 211syl2anc 584 . . 3 ((𝜑𝑥 ∈ (𝐷𝐼)) → ((𝐺𝑥) ≤ 𝐴 ↔ ∀𝑦 ∈ ℝ+ (𝐺𝑥) ≤ (𝐴 + 𝑦)))
213210, 212mpbird 256 . 2 ((𝜑𝑥 ∈ (𝐷𝐼)) → (𝐺𝑥) ≤ 𝐴)
2142, 213ssrabdv 4031 1 (𝜑 → (𝐷𝐼) ⊆ {𝑥𝐷 ∣ (𝐺𝑥) ≤ 𝐴})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  cin 3909  wss 3910   ciun 4954   ciin 4955   class class class wbr 5105  cmpt 5188  dom cdm 5633  ran crn 5634  wf 6492  cfv 6496  (class class class)co 7357  cmpo 7359  cc 11049  cr 11050  1c1 11052   + caddc 11054   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  cn 12153  2c2 12208  cz 12499  cuz 12763  +crp 12915  abscabs 15119  cli 15366  SAlgcsalg 44539  SMblFncsmblfn 44926
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-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
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-op 4593  df-uni 4866  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-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-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-sup 9378  df-inf 9379  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-n0 12414  df-z 12500  df-uz 12764  df-q 12874  df-rp 12916  df-ioo 13268  df-ico 13270  df-fl 13697  df-seq 13907  df-exp 13968  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-rlim 15371  df-smblfn 44927
This theorem is referenced by:  smflimlem5  45006
  Copyright terms: Public domain W3C validator