Metamath Proof Explorer


Theorem smflimlem4

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 D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses 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 smflimlem4 ( 𝜑 → ( 𝐷𝐼 ) ⊆ { 𝑥𝐷 ∣ ( 𝐺𝑥 ) ≤ 𝐴 } )

Proof

Step Hyp Ref Expression
1 smflimlem4.1 ( 𝜑𝑀 ∈ ℤ )
2 smflimlem4.2 𝑍 = ( ℤ𝑀 )
3 smflimlem4.3 ( 𝜑𝑆 ∈ SAlg )
4 smflimlem4.4 ( 𝜑𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5 smflimlem4.5 𝐷 = { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
6 smflimlem4.6 𝐺 = ( 𝑥𝐷 ↦ ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ) )
7 smflimlem4.7 ( 𝜑𝐴 ∈ ℝ )
8 smflimlem4.8 𝑃 = ( 𝑚𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠𝑆 ∣ { 𝑥 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } )
9 smflimlem4.9 𝐻 = ( 𝑚𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
10 smflimlem4.10 𝐼 = 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) ( 𝑚 𝐻 𝑘 )
11 smflimlem4.11 ( ( 𝜑𝑟 ∈ ran 𝑃 ) → ( 𝐶𝑟 ) ∈ 𝑟 )
12 inss1 ( 𝐷𝐼 ) ⊆ 𝐷
13 12 a1i ( 𝜑 → ( 𝐷𝐼 ) ⊆ 𝐷 )
14 13 sselda ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) → 𝑥𝐷 )
15 6 a1i ( 𝜑𝐺 = ( 𝑥𝐷 ↦ ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ) ) )
16 nfv 𝑚 ( 𝜑𝑥𝐷 )
17 nfcv 𝑚 𝐹
18 nfcv 𝑧 𝐹
19 3 adantr ( ( 𝜑𝑚𝑍 ) → 𝑆 ∈ SAlg )
20 4 ffvelrnda ( ( 𝜑𝑚𝑍 ) → ( 𝐹𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
21 eqid dom ( 𝐹𝑚 ) = dom ( 𝐹𝑚 )
22 19 20 21 smff ( ( 𝜑𝑚𝑍 ) → ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ )
23 22 adantlr ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑚𝑍 ) → ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ )
24 fveq2 ( 𝑥 = 𝑧 → ( ( 𝐹𝑚 ) ‘ 𝑥 ) = ( ( 𝐹𝑚 ) ‘ 𝑧 ) )
25 24 mpteq2dv ( 𝑥 = 𝑧 → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) )
26 25 eleq1d ( 𝑥 = 𝑧 → ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) ∈ dom ⇝ ) )
27 26 cbvrabv { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑧 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) ∈ dom ⇝ }
28 5 27 eqtri 𝐷 = { 𝑧 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) ∈ dom ⇝ }
29 simpr ( ( 𝜑𝑥𝐷 ) → 𝑥𝐷 )
30 16 17 18 2 23 28 29 fnlimfvre ( ( 𝜑𝑥𝐷 ) → ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
31 30 elexd ( ( 𝜑𝑥𝐷 ) → ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ) ∈ V )
32 15 31 fvmpt2d ( ( 𝜑𝑥𝐷 ) → ( 𝐺𝑥 ) = ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ) )
33 32 30 eqeltrd ( ( 𝜑𝑥𝐷 ) → ( 𝐺𝑥 ) ∈ ℝ )
34 14 33 syldan ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) → ( 𝐺𝑥 ) ∈ ℝ )
35 34 adantr ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐺𝑥 ) ∈ ℝ )
36 7 adantr ( ( 𝜑𝑦 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
37 rpre ( 𝑦 ∈ ℝ+𝑦 ∈ ℝ )
38 37 adantl ( ( 𝜑𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ )
39 36 38 readdcld ( ( 𝜑𝑦 ∈ ℝ+ ) → ( 𝐴 + 𝑦 ) ∈ ℝ )
40 39 adantlr ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐴 + 𝑦 ) ∈ ℝ )
41 nfv 𝑚 ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ )
42 rphalfcl ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ+ )
43 rpgtrecnn ( ( 𝑦 / 2 ) ∈ ℝ+ → ∃ 𝑘 ∈ ℕ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) )
44 42 43 syl ( 𝑦 ∈ ℝ+ → ∃ 𝑘 ∈ ℕ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) )
45 44 adantl ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑘 ∈ ℕ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) )
46 3 ad4antr ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → 𝑆 ∈ SAlg )
47 20 adantlr ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑚𝑍 ) → ( 𝐹𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
48 47 ad5ant15 ( ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) ∧ 𝑚𝑍 ) → ( 𝐹𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
49 7 adantr ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) → 𝐴 ∈ ℝ )
50 49 ad3antrrr ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → 𝐴 ∈ ℝ )
51 nfcv 𝑘 𝑍
52 nfcv 𝑗 𝑍
53 nfcv 𝑗 { 𝑠𝑆 ∣ { 𝑥 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) }
54 nfcv 𝑘 { 𝑠𝑆 ∣ { 𝑧 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) }
55 24 breq1d ( 𝑥 = 𝑧 → ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ↔ ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) )
56 55 cbvrabv { 𝑥 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = { 𝑧 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑘 ) ) }
57 56 a1i ( 𝑘 = 𝑗 → { 𝑥 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = { 𝑧 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } )
58 oveq2 ( 𝑘 = 𝑗 → ( 1 / 𝑘 ) = ( 1 / 𝑗 ) )
59 58 oveq2d ( 𝑘 = 𝑗 → ( 𝐴 + ( 1 / 𝑘 ) ) = ( 𝐴 + ( 1 / 𝑗 ) ) )
60 59 breq2d ( 𝑘 = 𝑗 → ( ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ↔ ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) ) )
61 60 rabbidv ( 𝑘 = 𝑗 → { 𝑧 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = { 𝑧 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } )
62 57 61 eqtrd ( 𝑘 = 𝑗 → { 𝑥 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = { 𝑧 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } )
63 62 eqeq1d ( 𝑘 = 𝑗 → ( { 𝑥 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) ↔ { 𝑧 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) ) )
64 63 rabbidv ( 𝑘 = 𝑗 → { 𝑠𝑆 ∣ { 𝑥 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } = { 𝑠𝑆 ∣ { 𝑧 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } )
65 51 52 53 54 64 cbvmpo2 ( 𝑚𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠𝑆 ∣ { 𝑥 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) = ( 𝑚𝑍 , 𝑗 ∈ ℕ ↦ { 𝑠𝑆 ∣ { 𝑧 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } )
66 8 65 eqtri 𝑃 = ( 𝑚𝑍 , 𝑗 ∈ ℕ ↦ { 𝑠𝑆 ∣ { 𝑧 ∈ dom ( 𝐹𝑚 ) ∣ ( ( 𝐹𝑚 ) ‘ 𝑧 ) < ( 𝐴 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } )
67 nfcv 𝑗 ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) )
68 nfcv 𝑘 ( 𝐶 ‘ ( 𝑚 𝑃 𝑗 ) )
69 oveq2 ( 𝑘 = 𝑗 → ( 𝑚 𝑃 𝑘 ) = ( 𝑚 𝑃 𝑗 ) )
70 69 fveq2d ( 𝑘 = 𝑗 → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑗 ) ) )
71 51 52 67 68 70 cbvmpo2 ( 𝑚𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ) = ( 𝑚𝑍 , 𝑗 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑗 ) ) )
72 9 71 eqtri 𝐻 = ( 𝑚𝑍 , 𝑗 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑗 ) ) )
73 simpll ( ( ( 𝑘 = 𝑗𝑛𝑍 ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → 𝑘 = 𝑗 )
74 73 oveq2d ( ( ( 𝑘 = 𝑗𝑛𝑍 ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → ( 𝑚 𝐻 𝑘 ) = ( 𝑚 𝐻 𝑗 ) )
75 74 iineq2dv ( ( 𝑘 = 𝑗𝑛𝑍 ) → 𝑚 ∈ ( ℤ𝑛 ) ( 𝑚 𝐻 𝑘 ) = 𝑚 ∈ ( ℤ𝑛 ) ( 𝑚 𝐻 𝑗 ) )
76 75 iuneq2dv ( 𝑘 = 𝑗 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) ( 𝑚 𝐻 𝑘 ) = 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) ( 𝑚 𝐻 𝑗 ) )
77 76 cbviinv 𝑘 ∈ ℕ 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) ( 𝑚 𝐻 𝑘 ) = 𝑗 ∈ ℕ 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) ( 𝑚 𝐻 𝑗 )
78 10 77 eqtri 𝐼 = 𝑗 ∈ ℕ 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) ( 𝑚 𝐻 𝑗 )
79 11 adantlr ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶𝑟 ) ∈ 𝑟 )
80 79 ad5ant15 ( ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶𝑟 ) ∈ 𝑟 )
81 simp-4r ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → 𝑥 ∈ ( 𝐷𝐼 ) )
82 simplr ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → 𝑘 ∈ ℕ )
83 42 ad3antlr ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → ( 𝑦 / 2 ) ∈ ℝ+ )
84 simpr ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → ( 1 / 𝑘 ) < ( 𝑦 / 2 ) )
85 2 46 48 28 50 66 72 78 80 81 82 83 84 smflimlem3 ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) ∧ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) ) → ∃ 𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( 𝑥 ∈ dom ( 𝐹𝑖 ) ∧ ( ( 𝐹𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
86 85 rexlimdva2 ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑘 ∈ ℕ ( 1 / 𝑘 ) < ( 𝑦 / 2 ) → ∃ 𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( 𝑥 ∈ dom ( 𝐹𝑖 ) ∧ ( ( 𝐹𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) )
87 45 86 mpd ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( 𝑥 ∈ dom ( 𝐹𝑖 ) ∧ ( ( 𝐹𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
88 nfv 𝑖 ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ )
89 nfcv 𝑖 𝐹
90 nfcv 𝑥 𝐹
91 1 ad2antrr ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
92 eleq1w ( 𝑚 = 𝑖 → ( 𝑚𝑍𝑖𝑍 ) )
93 92 anbi2d ( 𝑚 = 𝑖 → ( ( 𝜑𝑚𝑍 ) ↔ ( 𝜑𝑖𝑍 ) ) )
94 fveq2 ( 𝑚 = 𝑖 → ( 𝐹𝑚 ) = ( 𝐹𝑖 ) )
95 94 dmeqd ( 𝑚 = 𝑖 → dom ( 𝐹𝑚 ) = dom ( 𝐹𝑖 ) )
96 94 95 feq12d ( 𝑚 = 𝑖 → ( ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ ↔ ( 𝐹𝑖 ) : dom ( 𝐹𝑖 ) ⟶ ℝ ) )
97 93 96 imbi12d ( 𝑚 = 𝑖 → ( ( ( 𝜑𝑚𝑍 ) → ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ ) ↔ ( ( 𝜑𝑖𝑍 ) → ( 𝐹𝑖 ) : dom ( 𝐹𝑖 ) ⟶ ℝ ) ) )
98 97 22 chvarvv ( ( 𝜑𝑖𝑍 ) → ( 𝐹𝑖 ) : dom ( 𝐹𝑖 ) ⟶ ℝ )
99 98 ad4ant14 ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑖𝑍 ) → ( 𝐹𝑖 ) : dom ( 𝐹𝑖 ) ⟶ ℝ )
100 fveq2 ( 𝑚 = 𝑙 → ( 𝐹𝑚 ) = ( 𝐹𝑙 ) )
101 100 dmeqd ( 𝑚 = 𝑙 → dom ( 𝐹𝑚 ) = dom ( 𝐹𝑙 ) )
102 101 cbviinv 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) = 𝑙 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑙 )
103 102 a1i ( 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) = 𝑙 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑙 ) )
104 103 iuneq2i 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) = 𝑛𝑍 𝑙 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑙 )
105 fveq2 ( 𝑛 = 𝑚 → ( ℤ𝑛 ) = ( ℤ𝑚 ) )
106 105 iineq1d ( 𝑛 = 𝑚 𝑙 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑙 ) = 𝑙 ∈ ( ℤ𝑚 ) dom ( 𝐹𝑙 ) )
107 fveq2 ( 𝑙 = 𝑖 → ( 𝐹𝑙 ) = ( 𝐹𝑖 ) )
108 107 dmeqd ( 𝑙 = 𝑖 → dom ( 𝐹𝑙 ) = dom ( 𝐹𝑖 ) )
109 108 cbviinv 𝑙 ∈ ( ℤ𝑚 ) dom ( 𝐹𝑙 ) = 𝑖 ∈ ( ℤ𝑚 ) dom ( 𝐹𝑖 )
110 109 a1i ( 𝑛 = 𝑚 𝑙 ∈ ( ℤ𝑚 ) dom ( 𝐹𝑙 ) = 𝑖 ∈ ( ℤ𝑚 ) dom ( 𝐹𝑖 ) )
111 106 110 eqtrd ( 𝑛 = 𝑚 𝑙 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑙 ) = 𝑖 ∈ ( ℤ𝑚 ) dom ( 𝐹𝑖 ) )
112 111 cbviunv 𝑛𝑍 𝑙 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑙 ) = 𝑚𝑍 𝑖 ∈ ( ℤ𝑚 ) dom ( 𝐹𝑖 )
113 104 112 eqtri 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) = 𝑚𝑍 𝑖 ∈ ( ℤ𝑚 ) dom ( 𝐹𝑖 )
114 113 rabeqi { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑥 𝑚𝑍 𝑖 ∈ ( ℤ𝑚 ) dom ( 𝐹𝑖 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
115 fveq2 ( 𝑖 = 𝑚 → ( 𝐹𝑖 ) = ( 𝐹𝑚 ) )
116 115 fveq1d ( 𝑖 = 𝑚 → ( ( 𝐹𝑖 ) ‘ 𝑥 ) = ( ( 𝐹𝑚 ) ‘ 𝑥 ) )
117 116 cbvmptv ( 𝑖𝑍 ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) )
118 117 eqcomi ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) = ( 𝑖𝑍 ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) )
119 118 eleq1i ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑖𝑍 ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
120 119 rabbii { 𝑥 𝑚𝑍 𝑖 ∈ ( ℤ𝑚 ) dom ( 𝐹𝑖 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑥 𝑚𝑍 𝑖 ∈ ( ℤ𝑚 ) dom ( 𝐹𝑖 ) ∣ ( 𝑖𝑍 ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
121 5 114 120 3eqtri 𝐷 = { 𝑥 𝑚𝑍 𝑖 ∈ ( ℤ𝑚 ) dom ( 𝐹𝑖 ) ∣ ( 𝑖𝑍 ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
122 118 fveq2i ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑖𝑍 ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) )
123 122 mpteq2i ( 𝑥𝐷 ↦ ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑥𝐷 ↦ ( ⇝ ‘ ( 𝑖𝑍 ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ) )
124 6 123 eqtri 𝐺 = ( 𝑥𝐷 ↦ ( ⇝ ‘ ( 𝑖𝑍 ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ) )
125 14 adantr ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝑥𝐷 )
126 42 adantl ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) ∈ ℝ+ )
127 88 89 90 91 2 99 121 124 125 126 fnlimabslt ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) )
128 35 adantr ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( 𝐺𝑥 ) ∈ ℝ )
129 simpr ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ )
130 128 129 resubcld ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ∈ ℝ )
131 130 adantrr ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ∈ ℝ )
132 130 recnd ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ∈ ℂ )
133 132 abscld ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( abs ‘ ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ) ∈ ℝ )
134 133 adantrr ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ) ∈ ℝ )
135 37 rehalfcld ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ )
136 135 ad2antlr ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( 𝑦 / 2 ) ∈ ℝ )
137 131 leabsd ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ) )
138 34 recnd ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) → ( 𝐺𝑥 ) ∈ ℂ )
139 138 adantr ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( 𝐺𝑥 ) ∈ ℂ )
140 recn ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ → ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℂ )
141 140 adantl ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℂ )
142 139 141 abssubd ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ) → ( abs ‘ ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ) = ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) )
143 142 adantrr ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ) = ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) )
144 simprr ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) )
145 143 144 eqbrtrd ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) )
146 145 adantlr ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) )
147 131 134 136 137 146 lelttrd ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) < ( 𝑦 / 2 ) )
148 35 adantr ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( 𝐺𝑥 ) ∈ ℝ )
149 simprl ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ )
150 148 149 136 ltsubadd2d ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( ( ( 𝐺𝑥 ) − ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) < ( 𝑦 / 2 ) ↔ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
151 147 150 mpbid ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( 𝐺𝑥 ) < ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) )
152 151 ex ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ( 𝐺𝑥 ) < ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
153 152 ad2antrr ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ 𝑖 ∈ ( ℤ𝑚 ) ) → ( ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ( 𝐺𝑥 ) < ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
154 153 ralimdva ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) → ( ∀ 𝑖 ∈ ( ℤ𝑚 ) ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ∀ 𝑖 ∈ ( ℤ𝑚 ) ( 𝐺𝑥 ) < ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
155 154 ex ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑚𝑍 → ( ∀ 𝑖 ∈ ( ℤ𝑚 ) ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ∀ 𝑖 ∈ ( ℤ𝑚 ) ( 𝐺𝑥 ) < ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) ) )
156 41 155 reximdai ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) − ( 𝐺𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ∃ 𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( 𝐺𝑥 ) < ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
157 127 156 mpd ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑚𝑍𝑖 ∈ ( ℤ𝑚 ) ( 𝐺𝑥 ) < ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) )
158 115 dmeqd ( 𝑖 = 𝑚 → dom ( 𝐹𝑖 ) = dom ( 𝐹𝑚 ) )
159 158 eleq2d ( 𝑖 = 𝑚 → ( 𝑥 ∈ dom ( 𝐹𝑖 ) ↔ 𝑥 ∈ dom ( 𝐹𝑚 ) ) )
160 116 breq1d ( 𝑖 = 𝑚 → ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ↔ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
161 159 160 anbi12d ( 𝑖 = 𝑚 → ( ( 𝑥 ∈ dom ( 𝐹𝑖 ) ∧ ( ( 𝐹𝑖 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ↔ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) )
162 116 oveq1d ( 𝑖 = 𝑚 → ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) = ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) )
163 162 breq2d ( 𝑖 = 𝑚 → ( ( 𝐺𝑥 ) < ( ( ( 𝐹𝑖 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ↔ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
164 41 2 87 157 161 163 rexanuz3 ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑚𝑍 ( ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
165 df-3an ( ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) ↔ ( ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) )
166 3ancomb ( ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) ↔ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
167 165 166 bitr3i ( ( ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) ↔ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
168 167 rexbii ( ∃ 𝑚𝑍 ( ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ) ↔ ∃ 𝑚𝑍 ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
169 164 168 sylib ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑚𝑍 ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) )
170 35 ad2antrr ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( 𝐺𝑥 ) ∈ ℝ )
171 22 3adant3 ( ( 𝜑𝑚𝑍𝑥 ∈ dom ( 𝐹𝑚 ) ) → ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ )
172 simp3 ( ( 𝜑𝑚𝑍𝑥 ∈ dom ( 𝐹𝑚 ) ) → 𝑥 ∈ dom ( 𝐹𝑚 ) )
173 171 172 ffvelrnd ( ( 𝜑𝑚𝑍𝑥 ∈ dom ( 𝐹𝑚 ) ) → ( ( 𝐹𝑚 ) ‘ 𝑥 ) ∈ ℝ )
174 173 ad4ant134 ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ 𝑥 ∈ dom ( 𝐹𝑚 ) ) → ( ( 𝐹𝑚 ) ‘ 𝑥 ) ∈ ℝ )
175 simpllr ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ 𝑥 ∈ dom ( 𝐹𝑚 ) ) → 𝑦 ∈ ℝ+ )
176 175 135 syl ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ 𝑥 ∈ dom ( 𝐹𝑚 ) ) → ( 𝑦 / 2 ) ∈ ℝ )
177 174 176 readdcld ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ 𝑥 ∈ dom ( 𝐹𝑚 ) ) → ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∈ ℝ )
178 177 adantl3r ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ 𝑥 ∈ dom ( 𝐹𝑚 ) ) → ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∈ ℝ )
179 178 3ad2antr1 ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∈ ℝ )
180 rehalfcl ( 𝑦 ∈ ℝ → ( 𝑦 / 2 ) ∈ ℝ )
181 38 180 syl ( ( 𝜑𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) ∈ ℝ )
182 36 181 jca ( ( 𝜑𝑦 ∈ ℝ+ ) → ( 𝐴 ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ ) )
183 readdcl ( ( 𝐴 ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ ) → ( 𝐴 + ( 𝑦 / 2 ) ) ∈ ℝ )
184 182 183 syl ( ( 𝜑𝑦 ∈ ℝ+ ) → ( 𝐴 + ( 𝑦 / 2 ) ) ∈ ℝ )
185 184 181 readdcld ( ( 𝜑𝑦 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) ∈ ℝ )
186 185 ad5ant13 ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) ∈ ℝ )
187 simpr2 ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) )
188 174 adantrr ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( 𝐹𝑚 ) ‘ 𝑥 ) ∈ ℝ )
189 184 ad2antrr ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( 𝐴 + ( 𝑦 / 2 ) ) ∈ ℝ )
190 176 adantrr ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( 𝑦 / 2 ) ∈ ℝ )
191 simprr ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) )
192 188 189 190 191 ltadd1dd ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) < ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) )
193 192 adantl3r ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) < ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) )
194 193 3adantr2 ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) < ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) )
195 170 179 186 187 194 lttrd ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( 𝐺𝑥 ) < ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) )
196 36 recnd ( ( 𝜑𝑦 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
197 181 recnd ( ( 𝜑𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) ∈ ℂ )
198 196 197 197 addassd ( ( 𝜑𝑦 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) = ( 𝐴 + ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) )
199 37 recnd ( 𝑦 ∈ ℝ+𝑦 ∈ ℂ )
200 2halves ( 𝑦 ∈ ℂ → ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) = 𝑦 )
201 199 200 syl ( 𝑦 ∈ ℝ+ → ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) = 𝑦 )
202 201 oveq2d ( 𝑦 ∈ ℝ+ → ( 𝐴 + ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) = ( 𝐴 + 𝑦 ) )
203 202 adantl ( ( 𝜑𝑦 ∈ ℝ+ ) → ( 𝐴 + ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) = ( 𝐴 + 𝑦 ) )
204 198 203 eqtrd ( ( 𝜑𝑦 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) = ( 𝐴 + 𝑦 ) )
205 204 ad5ant13 ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( ( 𝐴 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) = ( 𝐴 + 𝑦 ) )
206 195 205 breqtrd ( ( ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑚𝑍 ) ∧ ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) ) → ( 𝐺𝑥 ) < ( 𝐴 + 𝑦 ) )
207 206 rexlimdva2 ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑚𝑍 ( 𝑥 ∈ dom ( 𝐹𝑚 ) ∧ ( 𝐺𝑥 ) < ( ( ( 𝐹𝑚 ) ‘ 𝑥 ) + ( 𝑦 / 2 ) ) ∧ ( ( 𝐹𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 𝑦 / 2 ) ) ) → ( 𝐺𝑥 ) < ( 𝐴 + 𝑦 ) ) )
208 169 207 mpd ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐺𝑥 ) < ( 𝐴 + 𝑦 ) )
209 35 40 208 ltled ( ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐺𝑥 ) ≤ ( 𝐴 + 𝑦 ) )
210 209 ralrimiva ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) → ∀ 𝑦 ∈ ℝ+ ( 𝐺𝑥 ) ≤ ( 𝐴 + 𝑦 ) )
211 alrple ( ( ( 𝐺𝑥 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐺𝑥 ) ≤ 𝐴 ↔ ∀ 𝑦 ∈ ℝ+ ( 𝐺𝑥 ) ≤ ( 𝐴 + 𝑦 ) ) )
212 34 49 211 syl2anc ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) → ( ( 𝐺𝑥 ) ≤ 𝐴 ↔ ∀ 𝑦 ∈ ℝ+ ( 𝐺𝑥 ) ≤ ( 𝐴 + 𝑦 ) ) )
213 210 212 mpbird ( ( 𝜑𝑥 ∈ ( 𝐷𝐼 ) ) → ( 𝐺𝑥 ) ≤ 𝐴 )
214 13 213 ssrabdv ( 𝜑 → ( 𝐷𝐼 ) ⊆ { 𝑥𝐷 ∣ ( 𝐺𝑥 ) ≤ 𝐴 } )