Proof of Theorem iscau3
Step | Hyp | Ref
| Expression |
1 | | iscau3.3 |
. . 3
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
2 | | iscau2 22883 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)))) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)))) |
4 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋 ↑pm ℂ)) →
𝐷 ∈
(∞Met‘𝑋)) |
5 | | ssid 3587 |
. . . . . . 7
⊢ ℤ
⊆ ℤ |
6 | | simpr 476 |
. . . . . . 7
⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) → (𝐹‘𝑘) ∈ 𝑋) |
7 | | eleq1 2676 |
. . . . . . 7
⊢ ((𝐹‘𝑘) = (𝐹‘𝑗) → ((𝐹‘𝑘) ∈ 𝑋 ↔ (𝐹‘𝑗) ∈ 𝑋)) |
8 | | eleq1 2676 |
. . . . . . 7
⊢ ((𝐹‘𝑘) = (𝐹‘𝑚) → ((𝐹‘𝑘) ∈ 𝑋 ↔ (𝐹‘𝑚) ∈ 𝑋)) |
9 | | xmetsym 21962 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹‘𝑗) ∈ 𝑋 ∧ (𝐹‘𝑘) ∈ 𝑋) → ((𝐹‘𝑗)𝐷(𝐹‘𝑘)) = ((𝐹‘𝑘)𝐷(𝐹‘𝑗))) |
10 | 9 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹‘𝑗) ∈ 𝑋 ∧ (𝐹‘𝑘) ∈ 𝑋) → ( I ‘((𝐹‘𝑗)𝐷(𝐹‘𝑘))) = ( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑗)))) |
11 | | xmetsym 21962 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹‘𝑚) ∈ 𝑋 ∧ (𝐹‘𝑗) ∈ 𝑋) → ((𝐹‘𝑚)𝐷(𝐹‘𝑗)) = ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) |
12 | 11 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹‘𝑚) ∈ 𝑋 ∧ (𝐹‘𝑗) ∈ 𝑋) → ( I ‘((𝐹‘𝑚)𝐷(𝐹‘𝑗))) = ( I ‘((𝐹‘𝑗)𝐷(𝐹‘𝑚)))) |
13 | | simp1 1054 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → 𝐷 ∈ (∞Met‘𝑋)) |
14 | | simp2l 1080 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → (𝐹‘𝑘) ∈ 𝑋) |
15 | | simp3l 1082 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → (𝐹‘𝑗) ∈ 𝑋) |
16 | | xmetcl 21946 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑗) ∈ 𝑋) → ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) ∈
ℝ*) |
17 | 13, 14, 15, 16 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) ∈
ℝ*) |
18 | | simp2r 1081 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → (𝐹‘𝑚) ∈ 𝑋) |
19 | | xmetcl 21946 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹‘𝑗) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) → ((𝐹‘𝑗)𝐷(𝐹‘𝑚)) ∈
ℝ*) |
20 | 13, 15, 18, 19 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((𝐹‘𝑗)𝐷(𝐹‘𝑚)) ∈
ℝ*) |
21 | | simp3r 1083 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → 𝑥 ∈ ℝ) |
22 | 21 | rehalfcld 11156 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → (𝑥 / 2) ∈ ℝ) |
23 | 22 | rexrd 9968 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → (𝑥 / 2) ∈
ℝ*) |
24 | | xlt2add 11962 |
. . . . . . . . . 10
⊢
(((((𝐹‘𝑘)𝐷(𝐹‘𝑗)) ∈ ℝ* ∧ ((𝐹‘𝑗)𝐷(𝐹‘𝑚)) ∈ ℝ*) ∧ ((𝑥 / 2) ∈ ℝ*
∧ (𝑥 / 2) ∈
ℝ*)) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < (𝑥 / 2) ∧ ((𝐹‘𝑗)𝐷(𝐹‘𝑚)) < (𝑥 / 2)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < ((𝑥 / 2) +𝑒 (𝑥 / 2)))) |
25 | 17, 20, 23, 23, 24 | syl22anc 1319 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < (𝑥 / 2) ∧ ((𝐹‘𝑗)𝐷(𝐹‘𝑚)) < (𝑥 / 2)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < ((𝑥 / 2) +𝑒 (𝑥 / 2)))) |
26 | | rexadd 11937 |
. . . . . . . . . . . . 13
⊢ (((𝑥 / 2) ∈ ℝ ∧
(𝑥 / 2) ∈ ℝ)
→ ((𝑥 / 2)
+𝑒 (𝑥 /
2)) = ((𝑥 / 2) + (𝑥 / 2))) |
27 | 22, 22, 26 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((𝑥 / 2) +𝑒 (𝑥 / 2)) = ((𝑥 / 2) + (𝑥 / 2))) |
28 | 21 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → 𝑥 ∈ ℂ) |
29 | 28 | 2halvesd 11155 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥) |
30 | 27, 29 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((𝑥 / 2) +𝑒 (𝑥 / 2)) = 𝑥) |
31 | 30 | breq2d 4595 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < ((𝑥 / 2) +𝑒 (𝑥 / 2)) ↔ (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < 𝑥)) |
32 | | xmettri 21966 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋 ∧ (𝐹‘𝑗) ∈ 𝑋)) → ((𝐹‘𝑘)𝐷(𝐹‘𝑚)) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚)))) |
33 | 13, 14, 18, 15, 32 | syl13anc 1320 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((𝐹‘𝑘)𝐷(𝐹‘𝑚)) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚)))) |
34 | | xmetcl 21946 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) → ((𝐹‘𝑘)𝐷(𝐹‘𝑚)) ∈
ℝ*) |
35 | 13, 14, 18, 34 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((𝐹‘𝑘)𝐷(𝐹‘𝑚)) ∈
ℝ*) |
36 | 17, 20 | xaddcld 12003 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) ∈
ℝ*) |
37 | 21 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → 𝑥 ∈ ℝ*) |
38 | | xrlelttr 11863 |
. . . . . . . . . . . 12
⊢ ((((𝐹‘𝑘)𝐷(𝐹‘𝑚)) ∈ ℝ* ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) ∈ ℝ* ∧ 𝑥 ∈ ℝ*)
→ ((((𝐹‘𝑘)𝐷(𝐹‘𝑚)) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < 𝑥) → ((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)) |
39 | 35, 36, 37, 38 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑚)) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < 𝑥) → ((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)) |
40 | 33, 39 | mpand 707 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < 𝑥 → ((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)) |
41 | 31, 40 | sylbid 229 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑗)) +𝑒 ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < ((𝑥 / 2) +𝑒 (𝑥 / 2)) → ((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)) |
42 | 25, 41 | syld 46 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < (𝑥 / 2) ∧ ((𝐹‘𝑗)𝐷(𝐹‘𝑚)) < (𝑥 / 2)) → ((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)) |
43 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) ∈ V |
44 | | fvi 6165 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) ∈ V → ( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) = ((𝐹‘𝑘)𝐷(𝐹‘𝑗))) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . . . 10
⊢ ( I
‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) = ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) |
46 | 45 | breq1i 4590 |
. . . . . . . . 9
⊢ (( I
‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < (𝑥 / 2) ↔ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < (𝑥 / 2)) |
47 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑗)𝐷(𝐹‘𝑚)) ∈ V |
48 | | fvi 6165 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑗)𝐷(𝐹‘𝑚)) ∈ V → ( I ‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))) = ((𝐹‘𝑗)𝐷(𝐹‘𝑚))) |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . . 10
⊢ ( I
‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))) = ((𝐹‘𝑗)𝐷(𝐹‘𝑚)) |
50 | 49 | breq1i 4590 |
. . . . . . . . 9
⊢ (( I
‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < (𝑥 / 2) ↔ ((𝐹‘𝑗)𝐷(𝐹‘𝑚)) < (𝑥 / 2)) |
51 | 46, 50 | anbi12i 729 |
. . . . . . . 8
⊢ ((( I
‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < (𝑥 / 2) ∧ ( I ‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < (𝑥 / 2)) ↔ (((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < (𝑥 / 2) ∧ ((𝐹‘𝑗)𝐷(𝐹‘𝑚)) < (𝑥 / 2))) |
52 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑘)𝐷(𝐹‘𝑚)) ∈ V |
53 | | fvi 6165 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑘)𝐷(𝐹‘𝑚)) ∈ V → ( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) = ((𝐹‘𝑘)𝐷(𝐹‘𝑚))) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . 9
⊢ ( I
‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) = ((𝐹‘𝑘)𝐷(𝐹‘𝑚)) |
55 | 54 | breq1i 4590 |
. . . . . . . 8
⊢ (( I
‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥 ↔ ((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥) |
56 | 42, 51, 55 | 3imtr4g 284 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑚) ∈ 𝑋) ∧ ((𝐹‘𝑗) ∈ 𝑋 ∧ 𝑥 ∈ ℝ)) → ((( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < (𝑥 / 2) ∧ ( I ‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < (𝑥 / 2)) → ( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥)) |
57 | 5, 6, 7, 8, 10, 12, 56 | cau3lem 13942 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥))) |
58 | 4, 57 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋 ↑pm ℂ)) →
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥))) |
59 | 45 | breq1i 4590 |
. . . . . . . . . 10
⊢ (( I
‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥 ↔ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥) |
60 | 59 | anbi2i 726 |
. . . . . . . . 9
⊢ (((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)) |
61 | | df-3an 1033 |
. . . . . . . . 9
⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥) ↔ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)) |
62 | 60, 61 | bitr4i 266 |
. . . . . . . 8
⊢ (((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)) |
63 | 62 | ralbii 2963 |
. . . . . . 7
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)) |
64 | 63 | rexbii 3023 |
. . . . . 6
⊢
(∃𝑗 ∈
ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)) |
65 | 64 | ralbii 2963 |
. . . . 5
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)) |
66 | 55 | ralbii 2963 |
. . . . . . . . . 10
⊢
(∀𝑚 ∈
(ℤ≥‘𝑘)( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥 ↔ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥) |
67 | 66 | anbi2i 726 |
. . . . . . . . 9
⊢ (((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥) ↔ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)) |
68 | | df-3an 1033 |
. . . . . . . . 9
⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥) ↔ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)) |
69 | 67, 68 | bitr4i 266 |
. . . . . . . 8
⊢ (((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥) ↔ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)) |
70 | 69 | ralbii 2963 |
. . . . . . 7
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥) ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)) |
71 | 70 | rexbii 3023 |
. . . . . 6
⊢
(∃𝑗 ∈
ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)) |
72 | 71 | ralbii 2963 |
. . . . 5
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)( I ‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)) |
73 | 58, 65, 72 | 3bitr3g 301 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋 ↑pm ℂ)) →
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥))) |
74 | | iscau3.4 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
75 | 74 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋 ↑pm ℂ)) →
𝑀 ∈
ℤ) |
76 | | iscau3.2 |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
77 | 76 | rexuz3 13936 |
. . . . . 6
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥))) |
78 | 75, 77 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋 ↑pm ℂ)) →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥))) |
79 | 78 | ralbidv 2969 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋 ↑pm ℂ)) →
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥))) |
80 | 73, 79 | bitr4d 270 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋 ↑pm ℂ)) →
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥))) |
81 | 80 | pm5.32da 671 |
. 2
⊢ (𝜑 → ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)))) |
82 | 3, 81 | bitrd 267 |
1
⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)))) |