Step | Hyp | Ref
| Expression |
1 | | inss1 3833 |
. . 3
⊢ (𝐷 ∩ 𝐼) ⊆ 𝐷 |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → (𝐷 ∩ 𝐼) ⊆ 𝐷) |
3 | 2 | sselda 3603 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) → 𝑥 ∈ 𝐷) |
4 | | smflimlem4.6 |
. . . . . . . . . 10
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
5 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))) |
6 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚(𝜑 ∧ 𝑥 ∈ 𝐷) |
7 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚𝐹 |
8 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧𝐹 |
9 | | smflimlem4.2 |
. . . . . . . . . . 11
⊢ 𝑍 =
(ℤ≥‘𝑀) |
10 | | smflimlem4.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ SAlg) |
11 | 10 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑆 ∈ SAlg) |
12 | | smflimlem4.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
13 | 12 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
14 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) |
15 | 11, 13, 14 | smff 40941 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
16 | 15 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
17 | | smflimlem4.5 |
. . . . . . . . . . . 12
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
18 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑧)) |
19 | 18 | mpteq2dv 4745 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑧))) |
20 | 19 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑧)) ∈ dom ⇝ )) |
21 | 20 | cbvrabv 3199 |
. . . . . . . . . . . 12
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑧 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑧)) ∈ dom ⇝ } |
22 | 17, 21 | eqtri 2644 |
. . . . . . . . . . 11
⊢ 𝐷 = {𝑧 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑧)) ∈ dom ⇝ } |
23 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷) |
24 | 6, 7, 8, 9, 16, 22, 23 | fnlimfvre 39906 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) |
25 | 24 | elexd 3214 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ V) |
26 | 5, 25 | fvmpt2d 6293 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐺‘𝑥) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) |
27 | 26, 24 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐺‘𝑥) ∈ ℝ) |
28 | 3, 27 | syldan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) → (𝐺‘𝑥) ∈ ℝ) |
29 | 28 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝐺‘𝑥) ∈ ℝ) |
30 | | smflimlem4.7 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
31 | 30 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐴 ∈
ℝ) |
32 | | rpre 11839 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
33 | 32 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ) |
34 | 31, 33 | readdcld 10069 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝐴 + 𝑦) ∈ ℝ) |
35 | 34 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝐴 + 𝑦) ∈ ℝ) |
36 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑚((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) |
37 | | rphalfcl 11858 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ+) |
38 | | rpgtrecnn 39597 |
. . . . . . . . . . 11
⊢ ((𝑦 / 2) ∈ ℝ+
→ ∃𝑘 ∈
ℕ (1 / 𝑘) < (𝑦 / 2)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ+
→ ∃𝑘 ∈
ℕ (1 / 𝑘) < (𝑦 / 2)) |
40 | 39 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) →
∃𝑘 ∈ ℕ (1
/ 𝑘) < (𝑦 / 2)) |
41 | 10 | ad4antr 768 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 /
𝑘) < (𝑦 / 2)) → 𝑆 ∈ SAlg) |
42 | 13 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
43 | 42 | ad5ant15 1303 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 /
𝑘) < (𝑦 / 2)) ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
44 | 30 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) → 𝐴 ∈ ℝ) |
45 | 44 | ad3antrrr 766 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 /
𝑘) < (𝑦 / 2)) → 𝐴 ∈ ℝ) |
46 | | smflimlem4.8 |
. . . . . . . . . . . . 13
⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
47 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘𝑍 |
48 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗𝑍 |
49 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗{𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} |
50 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘{𝑠 ∈ 𝑆 ∣ {𝑧 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚))} |
51 | 18 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → (((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘)) ↔ ((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑘)))) |
52 | 51 | cbvrabv 3199 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = {𝑧 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑘))} |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑗 → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = {𝑧 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑘))}) |
54 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑗 → (1 / 𝑘) = (1 / 𝑗)) |
55 | 54 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑗 → (𝐴 + (1 / 𝑘)) = (𝐴 + (1 / 𝑗))) |
56 | 55 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑗 → (((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑘)) ↔ ((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑗)))) |
57 | 56 | rabbidv 3189 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑗 → {𝑧 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑘))} = {𝑧 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))}) |
58 | 53, 57 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑗 → {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = {𝑧 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))}) |
59 | 58 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → ({𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚)) ↔ {𝑧 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚)))) |
60 | 59 | rabbidv 3189 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))} = {𝑠 ∈ 𝑆 ∣ {𝑧 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
61 | 47, 48, 49, 50, 60 | cbvmpt22 39277 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) = (𝑚 ∈ 𝑍, 𝑗 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑧 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
62 | 46, 61 | eqtri 2644 |
. . . . . . . . . . . 12
⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑗 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑧 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑧) < (𝐴 + (1 / 𝑗))} = (𝑠 ∩ dom (𝐹‘𝑚))}) |
63 | | smflimlem4.9 |
. . . . . . . . . . . . 13
⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘))) |
64 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗(𝐶‘(𝑚𝑃𝑘)) |
65 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝐶‘(𝑚𝑃𝑗)) |
66 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → (𝑚𝑃𝑘) = (𝑚𝑃𝑗)) |
67 | 66 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → (𝐶‘(𝑚𝑃𝑘)) = (𝐶‘(𝑚𝑃𝑗))) |
68 | 47, 48, 64, 65, 67 | cbvmpt22 39277 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘))) = (𝑚 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑗))) |
69 | 63, 68 | eqtri 2644 |
. . . . . . . . . . . 12
⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑗 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑗))) |
70 | | smflimlem4.10 |
. . . . . . . . . . . . 13
⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) |
71 | | simpll 790 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 = 𝑗 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑘 = 𝑗) |
72 | 71 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 = 𝑗 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝑚𝐻𝑘) = (𝑚𝐻𝑗)) |
73 | 72 | iineq2dv 4543 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 = 𝑗 ∧ 𝑛 ∈ 𝑍) → ∩
𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) = ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑗)) |
74 | 73 | iuneq2dv 4542 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑗)) |
75 | 74 | cbviinv 4560 |
. . . . . . . . . . . . 13
⊢ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑘) = ∩ 𝑗 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑗) |
76 | 70, 75 | eqtri 2644 |
. . . . . . . . . . . 12
⊢ 𝐼 = ∩ 𝑗 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)(𝑚𝐻𝑗) |
77 | | smflimlem4.11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟) |
78 | 77 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟) |
79 | 78 | ad5ant15 1303 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 /
𝑘) < (𝑦 / 2)) ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟) |
80 | | simp-4r 807 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 /
𝑘) < (𝑦 / 2)) → 𝑥 ∈ (𝐷 ∩ 𝐼)) |
81 | | simplr 792 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 /
𝑘) < (𝑦 / 2)) → 𝑘 ∈ ℕ) |
82 | 37 | ad3antlr 767 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 /
𝑘) < (𝑦 / 2)) → (𝑦 / 2) ∈
ℝ+) |
83 | | simpr 477 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 /
𝑘) < (𝑦 / 2)) → (1 / 𝑘) < (𝑦 / 2)) |
84 | 9, 41, 43, 22, 45, 62, 69, 76, 79, 80, 81, 82, 83 | smflimlem3 40981 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ (1 /
𝑘) < (𝑦 / 2)) → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)(𝑥 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (𝑦 / 2)))) |
85 | 84 | exp31 630 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝑘 ∈ ℕ → ((1 /
𝑘) < (𝑦 / 2) → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)(𝑥 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (𝑦 / 2)))))) |
86 | 85 | rexlimdv 3030 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) →
(∃𝑘 ∈ ℕ (1
/ 𝑘) < (𝑦 / 2) → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)(𝑥 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (𝑦 / 2))))) |
87 | 40, 86 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) →
∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)(𝑥 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (𝑦 / 2)))) |
88 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑖((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) |
89 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑖𝐹 |
90 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐹 |
91 | | smflimlem4.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
92 | 91 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) → 𝑀 ∈
ℤ) |
93 | | eleq1 2689 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑖 → (𝑚 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍)) |
94 | 93 | anbi2d 740 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑖 → ((𝜑 ∧ 𝑚 ∈ 𝑍) ↔ (𝜑 ∧ 𝑖 ∈ 𝑍))) |
95 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑖 → (𝐹‘𝑚) = (𝐹‘𝑖)) |
96 | 95 | dmeqd 5326 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑖 → dom (𝐹‘𝑚) = dom (𝐹‘𝑖)) |
97 | 95, 96 | feq12d 6033 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑖 → ((𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ ↔ (𝐹‘𝑖):dom (𝐹‘𝑖)⟶ℝ)) |
98 | 94, 97 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑖 → (((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖):dom (𝐹‘𝑖)⟶ℝ))) |
99 | 98, 15 | chvarv 2263 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖):dom (𝐹‘𝑖)⟶ℝ) |
100 | 99 | ad4ant14 1293 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖):dom (𝐹‘𝑖)⟶ℝ) |
101 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑙 → (𝐹‘𝑚) = (𝐹‘𝑙)) |
102 | 101 | dmeqd 5326 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑙 → dom (𝐹‘𝑚) = dom (𝐹‘𝑙)) |
103 | 102 | cbviinv 4560 |
. . . . . . . . . . . . . . 15
⊢ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑙 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑙) |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∩ 𝑙 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑙)) |
105 | 104 | iuneq2i 4539 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑙) |
106 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑚)) |
107 | 106 | iineq1d 39267 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ∩
𝑙 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑙) = ∩ 𝑙 ∈
(ℤ≥‘𝑚)dom (𝐹‘𝑙)) |
108 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑖 → (𝐹‘𝑙) = (𝐹‘𝑖)) |
109 | 108 | dmeqd 5326 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑖 → dom (𝐹‘𝑙) = dom (𝐹‘𝑖)) |
110 | 109 | cbviinv 4560 |
. . . . . . . . . . . . . . . 16
⊢ ∩ 𝑙 ∈ (ℤ≥‘𝑚)dom (𝐹‘𝑙) = ∩ 𝑖 ∈
(ℤ≥‘𝑚)dom (𝐹‘𝑖) |
111 | 110 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ∩
𝑙 ∈
(ℤ≥‘𝑚)dom (𝐹‘𝑙) = ∩ 𝑖 ∈
(ℤ≥‘𝑚)dom (𝐹‘𝑖)) |
112 | 107, 111 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ∩
𝑙 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑙) = ∩ 𝑖 ∈
(ℤ≥‘𝑚)dom (𝐹‘𝑖)) |
113 | 112 | cbviunv 4559 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑙 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑙) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑚)dom (𝐹‘𝑖) |
114 | 105, 113 | eqtri 2644 |
. . . . . . . . . . . 12
⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑚)dom (𝐹‘𝑖) |
115 | 114 | rabeqi 3193 |
. . . . . . . . . . 11
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑥 ∈ ∪
𝑚 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑚)dom (𝐹‘𝑖) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } |
116 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑚 → (𝐹‘𝑖) = (𝐹‘𝑚)) |
117 | 116 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑚 → ((𝐹‘𝑖)‘𝑥) = ((𝐹‘𝑚)‘𝑥)) |
118 | 117 | cbvmptv 4750 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ 𝑍 ↦ ((𝐹‘𝑖)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) |
119 | 118 | eqcomi 2631 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑖 ∈ 𝑍 ↦ ((𝐹‘𝑖)‘𝑥)) |
120 | 119 | eleq1i 2692 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑖 ∈ 𝑍 ↦ ((𝐹‘𝑖)‘𝑥)) ∈ dom ⇝ ) |
121 | 120 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑚)dom (𝐹‘𝑖) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ ↔ (𝑖 ∈ 𝑍 ↦ ((𝐹‘𝑖)‘𝑥)) ∈ dom ⇝ )) |
122 | 121 | rabbiia 3185 |
. . . . . . . . . . 11
⊢ {𝑥 ∈ ∪ 𝑚 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑚)dom (𝐹‘𝑖) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑥 ∈ ∪
𝑚 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑚)dom (𝐹‘𝑖) ∣ (𝑖 ∈ 𝑍 ↦ ((𝐹‘𝑖)‘𝑥)) ∈ dom ⇝ } |
123 | 17, 115, 122 | 3eqtri 2648 |
. . . . . . . . . 10
⊢ 𝐷 = {𝑥 ∈ ∪
𝑚 ∈ 𝑍 ∩ 𝑖 ∈
(ℤ≥‘𝑚)dom (𝐹‘𝑖) ∣ (𝑖 ∈ 𝑍 ↦ ((𝐹‘𝑖)‘𝑥)) ∈ dom ⇝ } |
124 | 119 | fveq2i 6194 |
. . . . . . . . . . . 12
⊢ ( ⇝
‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = ( ⇝ ‘(𝑖 ∈ 𝑍 ↦ ((𝐹‘𝑖)‘𝑥))) |
125 | 124 | mpteq2i 4741 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑖 ∈ 𝑍 ↦ ((𝐹‘𝑖)‘𝑥)))) |
126 | 4, 125 | eqtri 2644 |
. . . . . . . . . 10
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑖 ∈ 𝑍 ↦ ((𝐹‘𝑖)‘𝑥)))) |
127 | 3 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) → 𝑥 ∈ 𝐷) |
128 | 37 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈
ℝ+) |
129 | 88, 89, 90, 92, 9, 100, 123, 126, 127, 128 | fnlimabslt 39911 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) →
∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)(((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) |
130 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹‘𝑖)‘𝑥) ∈ ℝ) → (𝐺‘𝑥) ∈ ℝ) |
131 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹‘𝑖)‘𝑥) ∈ ℝ) → ((𝐹‘𝑖)‘𝑥) ∈ ℝ) |
132 | 130, 131 | resubcld 10458 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹‘𝑖)‘𝑥) ∈ ℝ) → ((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥)) ∈ ℝ) |
133 | 132 | adantrr 753 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → ((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥)) ∈ ℝ) |
134 | 132 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹‘𝑖)‘𝑥) ∈ ℝ) → ((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥)) ∈ ℂ) |
135 | 134 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ ((𝐹‘𝑖)‘𝑥) ∈ ℝ) → (abs‘((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥))) ∈ ℝ) |
136 | 135 | adantrr 753 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → (abs‘((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥))) ∈ ℝ) |
137 | 32 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ) |
138 | 137 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → (𝑦 / 2) ∈ ℝ) |
139 | 133 | leabsd 14153 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → ((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥)) ≤ (abs‘((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥)))) |
140 | 28 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) → (𝐺‘𝑥) ∈ ℂ) |
141 | 140 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ ((𝐹‘𝑖)‘𝑥) ∈ ℝ) → (𝐺‘𝑥) ∈ ℂ) |
142 | | recn 10026 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹‘𝑖)‘𝑥) ∈ ℝ → ((𝐹‘𝑖)‘𝑥) ∈ ℂ) |
143 | 142 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ ((𝐹‘𝑖)‘𝑥) ∈ ℝ) → ((𝐹‘𝑖)‘𝑥) ∈ ℂ) |
144 | 141, 143 | abssubd 14192 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ ((𝐹‘𝑖)‘𝑥) ∈ ℝ) → (abs‘((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥))) = (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥)))) |
145 | 144 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → (abs‘((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥))) = (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥)))) |
146 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2)) |
147 | 145, 146 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → (abs‘((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥))) < (𝑦 / 2)) |
148 | 147 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → (abs‘((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥))) < (𝑦 / 2)) |
149 | 133, 136,
138, 139, 148 | lelttrd 10195 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → ((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥)) < (𝑦 / 2)) |
150 | 29 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → (𝐺‘𝑥) ∈ ℝ) |
151 | | simprl 794 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → ((𝐹‘𝑖)‘𝑥) ∈ ℝ) |
152 | 150, 151,
138 | ltsubadd2d 10625 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → (((𝐺‘𝑥) − ((𝐹‘𝑖)‘𝑥)) < (𝑦 / 2) ↔ (𝐺‘𝑥) < (((𝐹‘𝑖)‘𝑥) + (𝑦 / 2)))) |
153 | 149, 152 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ (((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2))) → (𝐺‘𝑥) < (((𝐹‘𝑖)‘𝑥) + (𝑦 / 2))) |
154 | 153 | ex 450 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) → ((((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2)) → (𝐺‘𝑥) < (((𝐹‘𝑖)‘𝑥) + (𝑦 / 2)))) |
155 | 154 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → ((((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2)) → (𝐺‘𝑥) < (((𝐹‘𝑖)‘𝑥) + (𝑦 / 2)))) |
156 | 155 | ralimdva 2962 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) → (∀𝑖 ∈ (ℤ≥‘𝑚)(((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2)) → ∀𝑖 ∈ (ℤ≥‘𝑚)(𝐺‘𝑥) < (((𝐹‘𝑖)‘𝑥) + (𝑦 / 2)))) |
157 | 156 | ex 450 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝑚 ∈ 𝑍 → (∀𝑖 ∈ (ℤ≥‘𝑚)(((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2)) → ∀𝑖 ∈ (ℤ≥‘𝑚)(𝐺‘𝑥) < (((𝐹‘𝑖)‘𝑥) + (𝑦 / 2))))) |
158 | 36, 157 | reximdai 3012 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) →
(∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)(((𝐹‘𝑖)‘𝑥) ∈ ℝ ∧ (abs‘(((𝐹‘𝑖)‘𝑥) − (𝐺‘𝑥))) < (𝑦 / 2)) → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)(𝐺‘𝑥) < (((𝐹‘𝑖)‘𝑥) + (𝑦 / 2)))) |
159 | 129, 158 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) →
∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)(𝐺‘𝑥) < (((𝐹‘𝑖)‘𝑥) + (𝑦 / 2))) |
160 | 116 | dmeqd 5326 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑚 → dom (𝐹‘𝑖) = dom (𝐹‘𝑚)) |
161 | 160 | eleq2d 2687 |
. . . . . . . . 9
⊢ (𝑖 = 𝑚 → (𝑥 ∈ dom (𝐹‘𝑖) ↔ 𝑥 ∈ dom (𝐹‘𝑚))) |
162 | 117 | breq1d 4663 |
. . . . . . . . 9
⊢ (𝑖 = 𝑚 → (((𝐹‘𝑖)‘𝑥) < (𝐴 + (𝑦 / 2)) ↔ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) |
163 | 161, 162 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑖 = 𝑚 → ((𝑥 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑥) < (𝐴 + (𝑦 / 2))) ↔ (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))))) |
164 | 117 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑖 = 𝑚 → (((𝐹‘𝑖)‘𝑥) + (𝑦 / 2)) = (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2))) |
165 | 164 | breq2d 4665 |
. . . . . . . 8
⊢ (𝑖 = 𝑚 → ((𝐺‘𝑥) < (((𝐹‘𝑖)‘𝑥) + (𝑦 / 2)) ↔ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)))) |
166 | 36, 9, 87, 159, 163, 165 | rexanuz3 39275 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) →
∃𝑚 ∈ 𝑍 ((𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)))) |
167 | | df-3an 1039 |
. . . . . . . . 9
⊢ ((𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2))) ↔ ((𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)))) |
168 | | 3ancomb 1047 |
. . . . . . . . 9
⊢ ((𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2))) ↔ (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) |
169 | 167, 168 | bitr3i 266 |
. . . . . . . 8
⊢ (((𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2))) ↔ (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) |
170 | 169 | rexbii 3041 |
. . . . . . 7
⊢
(∃𝑚 ∈
𝑍 ((𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2))) ↔ ∃𝑚 ∈ 𝑍 (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) |
171 | 166, 170 | sylib 208 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) →
∃𝑚 ∈ 𝑍 (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) |
172 | 29 | ad2antrr 762 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐺‘𝑥) ∈ ℝ) |
173 | 15 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) |
174 | | simp3 1063 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → 𝑥 ∈ dom (𝐹‘𝑚)) |
175 | 173, 174 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ) |
176 | 175 | ad4ant134 1296 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ) |
177 | | simpllr 799 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → 𝑦 ∈ ℝ+) |
178 | 177, 137 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → (𝑦 / 2) ∈ ℝ) |
179 | 176, 178 | readdcld 10069 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∈ ℝ) |
180 | 179 | adantlllr 39199 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∈ ℝ) |
181 | 180 | 3ad2antr1 1226 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∈ ℝ) |
182 | | rehalfcl 11258 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ → (𝑦 / 2) ∈
ℝ) |
183 | 33, 182 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈
ℝ) |
184 | 31, 183 | jca 554 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝐴 ∈ ℝ ∧ (𝑦 / 2) ∈
ℝ)) |
185 | | readdcl 10019 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ (𝑦 / 2) ∈ ℝ) →
(𝐴 + (𝑦 / 2)) ∈ ℝ) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝐴 + (𝑦 / 2)) ∈ ℝ) |
187 | 186, 183 | readdcld 10069 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) ∈ ℝ) |
188 | 187 | ad5ant13 1301 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) ∈ ℝ) |
189 | | simpr2 1068 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2))) |
190 | 176 | adantrr 753 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ) |
191 | 186 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐴 + (𝑦 / 2)) ∈ ℝ) |
192 | 178 | adantrr 753 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝑦 / 2) ∈ ℝ) |
193 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) |
194 | 190, 191,
192, 193 | ltadd1dd 10638 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) < ((𝐴 + (𝑦 / 2)) + (𝑦 / 2))) |
195 | 194 | adantlllr 39199 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) < ((𝐴 + (𝑦 / 2)) + (𝑦 / 2))) |
196 | 195 | 3adantr2 1221 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) < ((𝐴 + (𝑦 / 2)) + (𝑦 / 2))) |
197 | 172, 181,
188, 189, 196 | lttrd 10198 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐺‘𝑥) < ((𝐴 + (𝑦 / 2)) + (𝑦 / 2))) |
198 | 31 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐴 ∈
ℂ) |
199 | 183 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈
ℂ) |
200 | 198, 199,
199 | addassd 10062 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) = (𝐴 + ((𝑦 / 2) + (𝑦 / 2)))) |
201 | 32 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
202 | | 2halves 11260 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℂ → ((𝑦 / 2) + (𝑦 / 2)) = 𝑦) |
203 | 201, 202 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ+
→ ((𝑦 / 2) + (𝑦 / 2)) = 𝑦) |
204 | 203 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ+
→ (𝐴 + ((𝑦 / 2) + (𝑦 / 2))) = (𝐴 + 𝑦)) |
205 | 204 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝐴 + ((𝑦 / 2) + (𝑦 / 2))) = (𝐴 + 𝑦)) |
206 | 200, 205 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) = (𝐴 + 𝑦)) |
207 | 206 | ad5ant13 1301 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → ((𝐴 + (𝑦 / 2)) + (𝑦 / 2)) = (𝐴 + 𝑦)) |
208 | 197, 207 | breqtrd 4679 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑚 ∈ 𝑍) ∧ (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2)))) → (𝐺‘𝑥) < (𝐴 + 𝑦)) |
209 | 208 | exp31 630 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝑚 ∈ 𝑍 → ((𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) → (𝐺‘𝑥) < (𝐴 + 𝑦)))) |
210 | 209 | rexlimdv 3030 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) →
(∃𝑚 ∈ 𝑍 (𝑥 ∈ dom (𝐹‘𝑚) ∧ (𝐺‘𝑥) < (((𝐹‘𝑚)‘𝑥) + (𝑦 / 2)) ∧ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (𝑦 / 2))) → (𝐺‘𝑥) < (𝐴 + 𝑦))) |
211 | 171, 210 | mpd 15 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝐺‘𝑥) < (𝐴 + 𝑦)) |
212 | 29, 35, 211 | ltled 10185 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) ∧ 𝑦 ∈ ℝ+) → (𝐺‘𝑥) ≤ (𝐴 + 𝑦)) |
213 | 212 | ralrimiva 2966 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) → ∀𝑦 ∈ ℝ+ (𝐺‘𝑥) ≤ (𝐴 + 𝑦)) |
214 | | alrple 12037 |
. . . 4
⊢ (((𝐺‘𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝐺‘𝑥) ≤ 𝐴 ↔ ∀𝑦 ∈ ℝ+ (𝐺‘𝑥) ≤ (𝐴 + 𝑦))) |
215 | 28, 44, 214 | syl2anc 693 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) → ((𝐺‘𝑥) ≤ 𝐴 ↔ ∀𝑦 ∈ ℝ+ (𝐺‘𝑥) ≤ (𝐴 + 𝑦))) |
216 | 213, 215 | mpbird 247 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∩ 𝐼)) → (𝐺‘𝑥) ≤ 𝐴) |
217 | 2, 216 | ssrabdv 3681 |
1
⊢ (𝜑 → (𝐷 ∩ 𝐼) ⊆ {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴}) |