MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iscau3 Structured version   Visualization version   GIF version

Theorem iscau3 23552
Description: Express the Cauchy sequence property in the more conventional three-quantifier form. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.)
Hypotheses
Ref Expression
iscau3.2 𝑍 = (ℤ𝑀)
iscau3.3 (𝜑𝐷 ∈ (∞Met‘𝑋))
iscau3.4 (𝜑𝑀 ∈ ℤ)
Assertion
Ref Expression
iscau3 (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))))
Distinct variable groups:   𝑗,𝑘,𝑚,𝑥,𝐷   𝑗,𝐹,𝑘,𝑚,𝑥   𝜑,𝑗,𝑘,𝑥   𝑗,𝑋,𝑘,𝑚,𝑥   𝑗,𝑀   𝑗,𝑍,𝑘,𝑥
Allowed substitution hints:   𝜑(𝑚)   𝑀(𝑥,𝑘,𝑚)   𝑍(𝑚)

Proof of Theorem iscau3
StepHypRef Expression
1 iscau3.3 . . 3 (𝜑𝐷 ∈ (∞Met‘𝑋))
2 iscau2 23551 . . 3 (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥))))
31, 2syl 17 . 2 (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥))))
41adantr 481 . . . . . 6 ((𝜑𝐹 ∈ (𝑋pm ℂ)) → 𝐷 ∈ (∞Met‘𝑋))
5 ssid 3905 . . . . . . 7 ℤ ⊆ ℤ
6 simpr 485 . . . . . . 7 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) → (𝐹𝑘) ∈ 𝑋)
7 eleq1 2868 . . . . . . 7 ((𝐹𝑘) = (𝐹𝑗) → ((𝐹𝑘) ∈ 𝑋 ↔ (𝐹𝑗) ∈ 𝑋))
8 eleq1 2868 . . . . . . 7 ((𝐹𝑘) = (𝐹𝑚) → ((𝐹𝑘) ∈ 𝑋 ↔ (𝐹𝑚) ∈ 𝑋))
9 xmetsym 22628 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹𝑗) ∈ 𝑋 ∧ (𝐹𝑘) ∈ 𝑋) → ((𝐹𝑗)𝐷(𝐹𝑘)) = ((𝐹𝑘)𝐷(𝐹𝑗)))
109fveq2d 6534 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹𝑗) ∈ 𝑋 ∧ (𝐹𝑘) ∈ 𝑋) → ( I ‘((𝐹𝑗)𝐷(𝐹𝑘))) = ( I ‘((𝐹𝑘)𝐷(𝐹𝑗))))
11 xmetsym 22628 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹𝑚) ∈ 𝑋 ∧ (𝐹𝑗) ∈ 𝑋) → ((𝐹𝑚)𝐷(𝐹𝑗)) = ((𝐹𝑗)𝐷(𝐹𝑚)))
1211fveq2d 6534 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹𝑚) ∈ 𝑋 ∧ (𝐹𝑗) ∈ 𝑋) → ( I ‘((𝐹𝑚)𝐷(𝐹𝑗))) = ( I ‘((𝐹𝑗)𝐷(𝐹𝑚))))
13 simp1 1127 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → 𝐷 ∈ (∞Met‘𝑋))
14 simp2l 1190 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → (𝐹𝑘) ∈ 𝑋)
15 simp3l 1192 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → (𝐹𝑗) ∈ 𝑋)
16 xmetcl 22612 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑗) ∈ 𝑋) → ((𝐹𝑘)𝐷(𝐹𝑗)) ∈ ℝ*)
1713, 14, 15, 16syl3anc 1362 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((𝐹𝑘)𝐷(𝐹𝑗)) ∈ ℝ*)
18 simp2r 1191 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → (𝐹𝑚) ∈ 𝑋)
19 xmetcl 22612 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹𝑗) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) → ((𝐹𝑗)𝐷(𝐹𝑚)) ∈ ℝ*)
2013, 15, 18, 19syl3anc 1362 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((𝐹𝑗)𝐷(𝐹𝑚)) ∈ ℝ*)
21 simp3r 1193 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → 𝑥 ∈ ℝ)
2221rehalfcld 11721 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → (𝑥 / 2) ∈ ℝ)
2322rexrd 10526 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → (𝑥 / 2) ∈ ℝ*)
24 xlt2add 12492 . . . . . . . . . 10 (((((𝐹𝑘)𝐷(𝐹𝑗)) ∈ ℝ* ∧ ((𝐹𝑗)𝐷(𝐹𝑚)) ∈ ℝ*) ∧ ((𝑥 / 2) ∈ ℝ* ∧ (𝑥 / 2) ∈ ℝ*)) → ((((𝐹𝑘)𝐷(𝐹𝑗)) < (𝑥 / 2) ∧ ((𝐹𝑗)𝐷(𝐹𝑚)) < (𝑥 / 2)) → (((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))) < ((𝑥 / 2) +𝑒 (𝑥 / 2))))
2517, 20, 23, 23, 24syl22anc 835 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((((𝐹𝑘)𝐷(𝐹𝑗)) < (𝑥 / 2) ∧ ((𝐹𝑗)𝐷(𝐹𝑚)) < (𝑥 / 2)) → (((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))) < ((𝑥 / 2) +𝑒 (𝑥 / 2))))
2622, 22rexaddd 12466 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((𝑥 / 2) +𝑒 (𝑥 / 2)) = ((𝑥 / 2) + (𝑥 / 2)))
2721recnd 10504 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → 𝑥 ∈ ℂ)
28272halvesd 11720 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥)
2926, 28eqtrd 2829 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((𝑥 / 2) +𝑒 (𝑥 / 2)) = 𝑥)
3029breq2d 4968 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))) < ((𝑥 / 2) +𝑒 (𝑥 / 2)) ↔ (((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))) < 𝑥))
31 xmettri 22632 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋 ∧ (𝐹𝑗) ∈ 𝑋)) → ((𝐹𝑘)𝐷(𝐹𝑚)) ≤ (((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))))
3213, 14, 18, 15, 31syl13anc 1363 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((𝐹𝑘)𝐷(𝐹𝑚)) ≤ (((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))))
33 xmetcl 22612 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) → ((𝐹𝑘)𝐷(𝐹𝑚)) ∈ ℝ*)
3413, 14, 18, 33syl3anc 1362 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((𝐹𝑘)𝐷(𝐹𝑚)) ∈ ℝ*)
3517, 20xaddcld 12533 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → (((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))) ∈ ℝ*)
3621rexrd 10526 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → 𝑥 ∈ ℝ*)
37 xrlelttr 12388 . . . . . . . . . . . 12 ((((𝐹𝑘)𝐷(𝐹𝑚)) ∈ ℝ* ∧ (((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))) ∈ ℝ*𝑥 ∈ ℝ*) → ((((𝐹𝑘)𝐷(𝐹𝑚)) ≤ (((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))) ∧ (((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))) < 𝑥) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
3834, 35, 36, 37syl3anc 1362 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((((𝐹𝑘)𝐷(𝐹𝑚)) ≤ (((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))) ∧ (((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))) < 𝑥) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
3932, 38mpand 691 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))) < 𝑥 → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
4030, 39sylbid 241 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((((𝐹𝑘)𝐷(𝐹𝑗)) +𝑒 ((𝐹𝑗)𝐷(𝐹𝑚))) < ((𝑥 / 2) +𝑒 (𝑥 / 2)) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
4125, 40syld 47 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((((𝐹𝑘)𝐷(𝐹𝑗)) < (𝑥 / 2) ∧ ((𝐹𝑗)𝐷(𝐹𝑚)) < (𝑥 / 2)) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
42 ovex 7039 . . . . . . . . . . 11 ((𝐹𝑘)𝐷(𝐹𝑗)) ∈ V
43 fvi 6599 . . . . . . . . . . 11 (((𝐹𝑘)𝐷(𝐹𝑗)) ∈ V → ( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) = ((𝐹𝑘)𝐷(𝐹𝑗)))
4442, 43ax-mp 5 . . . . . . . . . 10 ( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) = ((𝐹𝑘)𝐷(𝐹𝑗))
4544breq1i 4963 . . . . . . . . 9 (( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) ↔ ((𝐹𝑘)𝐷(𝐹𝑗)) < (𝑥 / 2))
46 ovex 7039 . . . . . . . . . . 11 ((𝐹𝑗)𝐷(𝐹𝑚)) ∈ V
47 fvi 6599 . . . . . . . . . . 11 (((𝐹𝑗)𝐷(𝐹𝑚)) ∈ V → ( I ‘((𝐹𝑗)𝐷(𝐹𝑚))) = ((𝐹𝑗)𝐷(𝐹𝑚)))
4846, 47ax-mp 5 . . . . . . . . . 10 ( I ‘((𝐹𝑗)𝐷(𝐹𝑚))) = ((𝐹𝑗)𝐷(𝐹𝑚))
4948breq1i 4963 . . . . . . . . 9 (( I ‘((𝐹𝑗)𝐷(𝐹𝑚))) < (𝑥 / 2) ↔ ((𝐹𝑗)𝐷(𝐹𝑚)) < (𝑥 / 2))
5045, 49anbi12i 626 . . . . . . . 8 ((( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) ∧ ( I ‘((𝐹𝑗)𝐷(𝐹𝑚))) < (𝑥 / 2)) ↔ (((𝐹𝑘)𝐷(𝐹𝑗)) < (𝑥 / 2) ∧ ((𝐹𝑗)𝐷(𝐹𝑚)) < (𝑥 / 2)))
51 ovex 7039 . . . . . . . . . 10 ((𝐹𝑘)𝐷(𝐹𝑚)) ∈ V
52 fvi 6599 . . . . . . . . . 10 (((𝐹𝑘)𝐷(𝐹𝑚)) ∈ V → ( I ‘((𝐹𝑘)𝐷(𝐹𝑚))) = ((𝐹𝑘)𝐷(𝐹𝑚)))
5351, 52ax-mp 5 . . . . . . . . 9 ( I ‘((𝐹𝑘)𝐷(𝐹𝑚))) = ((𝐹𝑘)𝐷(𝐹𝑚))
5453breq1i 4963 . . . . . . . 8 (( I ‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥 ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)
5541, 50, 543imtr4g 297 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑚) ∈ 𝑋) ∧ ((𝐹𝑗) ∈ 𝑋𝑥 ∈ ℝ)) → ((( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) < (𝑥 / 2) ∧ ( I ‘((𝐹𝑗)𝐷(𝐹𝑚))) < (𝑥 / 2)) → ( I ‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥))
565, 6, 7, 8, 10, 12, 55cau3lem 14536 . . . . . 6 (𝐷 ∈ (∞Met‘𝑋) → (∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)( I ‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
574, 56syl 17 . . . . 5 ((𝜑𝐹 ∈ (𝑋pm ℂ)) → (∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)( I ‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥)))
5844breq1i 4963 . . . . . . . . . 10 (( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥 ↔ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥)
5958anbi2i 622 . . . . . . . . 9 (((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥))
60 df-3an 1080 . . . . . . . . 9 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥) ↔ ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥))
6159, 60bitr4i 279 . . . . . . . 8 (((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥))
6261ralbii 3130 . . . . . . 7 (∀𝑘 ∈ (ℤ𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥))
6362rexbii 3209 . . . . . 6 (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥))
6463ralbii 3130 . . . . 5 (∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ( I ‘((𝐹𝑘)𝐷(𝐹𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥))
6554ralbii 3130 . . . . . . . . . 10 (∀𝑚 ∈ (ℤ𝑘)( I ‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥 ↔ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)
6665anbi2i 622 . . . . . . . . 9 (((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)( I ‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥) ↔ ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
67 df-3an 1080 . . . . . . . . 9 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
6866, 67bitr4i 279 . . . . . . . 8 (((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)( I ‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥) ↔ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
6968ralbii 3130 . . . . . . 7 (∀𝑘 ∈ (ℤ𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)( I ‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
7069rexbii 3209 . . . . . 6 (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)( I ‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
7170ralbii 3130 . . . . 5 (∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)( I ‘((𝐹𝑘)𝐷(𝐹𝑚))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
7257, 64, 713bitr3g 314 . . . 4 ((𝜑𝐹 ∈ (𝑋pm ℂ)) → (∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
73 iscau3.4 . . . . . . 7 (𝜑𝑀 ∈ ℤ)
7473adantr 481 . . . . . 6 ((𝜑𝐹 ∈ (𝑋pm ℂ)) → 𝑀 ∈ ℤ)
75 iscau3.2 . . . . . . 7 𝑍 = (ℤ𝑀)
7675rexuz3 14530 . . . . . 6 (𝑀 ∈ ℤ → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
7774, 76syl 17 . . . . 5 ((𝜑𝐹 ∈ (𝑋pm ℂ)) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
7877ralbidv 3162 . . . 4 ((𝜑𝐹 ∈ (𝑋pm ℂ)) → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
7972, 78bitr4d 283 . . 3 ((𝜑𝐹 ∈ (𝑋pm ℂ)) → (∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
8079pm5.32da 579 . 2 (𝜑 → ((𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑥)) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))))
813, 80bitrd 280 1 (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1078   = wceq 1520  wcel 2079  wral 3103  wrex 3104  Vcvv 3432   class class class wbr 4956   I cid 5339  dom cdm 5435  cfv 6217  (class class class)co 7007  pm cpm 8248  cc 10370  cr 10371   + caddc 10375  *cxr 10509   < clt 10510  cle 10511   / cdiv 11134  2c2 11529  cz 11818  cuz 12082  +crp 12228   +𝑒 cxad 12344  ∞Metcxmet 20200  Cauccau 23527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-cnex 10428  ax-resscn 10429  ax-1cn 10430  ax-icn 10431  ax-addcl 10432  ax-addrcl 10433  ax-mulcl 10434  ax-mulrcl 10435  ax-mulcom 10436  ax-addass 10437  ax-mulass 10438  ax-distr 10439  ax-i2m1 10440  ax-1ne0 10441  ax-1rid 10442  ax-rnegex 10443  ax-rrecex 10444  ax-cnre 10445  ax-pre-lttri 10446  ax-pre-lttrn 10447  ax-pre-ltadd 10448  ax-pre-mulgt0 10449
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-iun 4821  df-br 4957  df-opab 5019  df-mpt 5036  df-id 5340  df-po 5354  df-so 5355  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-riota 6968  df-ov 7010  df-oprab 7011  df-mpo 7012  df-1st 7536  df-2nd 7537  df-er 8130  df-map 8249  df-pm 8250  df-en 8348  df-dom 8349  df-sdom 8350  df-pnf 10512  df-mnf 10513  df-xr 10514  df-ltxr 10515  df-le 10516  df-sub 10708  df-neg 10709  df-div 11135  df-2 11537  df-z 11819  df-uz 12083  df-rp 12229  df-xneg 12346  df-xadd 12347  df-psmet 20207  df-xmet 20208  df-bl 20210  df-cau 23530
This theorem is referenced by:  iscau4  23553  caucfil  23557  cmetcaulem  23562  heibor1lem  34565
  Copyright terms: Public domain W3C validator