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 |
⊢ ( 𝜑 → ( 𝐷 ∩ 𝐼 ) ⊆ { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ) |