| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | iscmet3.3 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 2 |  | iscmet3.1 | . . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 3 | 2 | iscmet3lem3 25324 | . . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑟 ∈ ℝ+)
→ ∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑟) | 
| 4 | 1, 3 | sylan 580 | . . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑟) | 
| 5 | 2 | r19.2uz 15390 | . . . . 5
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑟 → ∃𝑘 ∈ 𝑍 ((1 / 2)↑𝑘) < 𝑟) | 
| 6 | 4, 5 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑘 ∈ 𝑍 ((1 / 2)↑𝑘) < 𝑟) | 
| 7 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑆‘𝑛) = (𝑆‘𝑘)) | 
| 8 | 7 | eleq2d 2827 | . . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑘) ∈ (𝑆‘𝑛) ↔ (𝐹‘𝑘) ∈ (𝑆‘𝑘))) | 
| 9 |  | iscmet3.10 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛)) | 
| 10 | 9 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛)) | 
| 11 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑘 ∈ 𝑍) | 
| 12 | 11 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → 𝑘 ∈ 𝑍) | 
| 13 |  | rsp 3247 | . . . . . . . . . . 11
⊢
(∀𝑘 ∈
𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛) → (𝑘 ∈ 𝑍 → ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛))) | 
| 14 | 10, 12, 13 | sylc 65 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛)) | 
| 15 | 12, 2 | eleqtrdi 2851 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → 𝑘 ∈ (ℤ≥‘𝑀)) | 
| 16 |  | eluzfz2 13572 | . . . . . . . . . . 11
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ (𝑀...𝑘)) | 
| 17 | 15, 16 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → 𝑘 ∈ (𝑀...𝑘)) | 
| 18 | 8, 14, 17 | rspcdva 3623 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑘) ∈ (𝑆‘𝑘)) | 
| 19 | 7 | eleq2d 2827 | . . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑗) ∈ (𝑆‘𝑛) ↔ (𝐹‘𝑗) ∈ (𝑆‘𝑘))) | 
| 20 |  | oveq2 7439 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝑀...𝑘) = (𝑀...𝑗)) | 
| 21 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗)) | 
| 22 | 21 | eleq1d 2826 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) ∈ (𝑆‘𝑛) ↔ (𝐹‘𝑗) ∈ (𝑆‘𝑛))) | 
| 23 | 20, 22 | raleqbidv 3346 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → (∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛) ↔ ∀𝑛 ∈ (𝑀...𝑗)(𝐹‘𝑗) ∈ (𝑆‘𝑛))) | 
| 24 | 2 | uztrn2 12897 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ 𝑍) | 
| 25 | 24 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → 𝑗 ∈ 𝑍) | 
| 26 | 23, 10, 25 | rspcdva 3623 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → ∀𝑛 ∈ (𝑀...𝑗)(𝐹‘𝑗) ∈ (𝑆‘𝑛)) | 
| 27 |  | simprr 773 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → 𝑗 ∈ (ℤ≥‘𝑘)) | 
| 28 |  | elfzuzb 13558 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (𝑀...𝑗) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑘))) | 
| 29 | 15, 27, 28 | sylanbrc 583 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → 𝑘 ∈ (𝑀...𝑗)) | 
| 30 | 19, 26, 29 | rspcdva 3623 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑗) ∈ (𝑆‘𝑘)) | 
| 31 |  | iscmet3.9 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) | 
| 32 | 31 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) | 
| 33 |  | eluzelz 12888 | . . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) | 
| 34 | 33, 2 | eleq2s 2859 | . . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) | 
| 35 | 34 | ad2antrl 728 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → 𝑘 ∈ ℤ) | 
| 36 |  | rsp 3247 | . . . . . . . . . 10
⊢
(∀𝑘 ∈
ℤ ∀𝑢 ∈
(𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘) → (𝑘 ∈ ℤ → ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))) | 
| 37 | 32, 35, 36 | sylc 65 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) | 
| 38 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑢 = (𝐹‘𝑘) → (𝑢𝐷𝑣) = ((𝐹‘𝑘)𝐷𝑣)) | 
| 39 | 38 | breq1d 5153 | . . . . . . . . . 10
⊢ (𝑢 = (𝐹‘𝑘) → ((𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ((𝐹‘𝑘)𝐷𝑣) < ((1 / 2)↑𝑘))) | 
| 40 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑣 = (𝐹‘𝑗) → ((𝐹‘𝑘)𝐷𝑣) = ((𝐹‘𝑘)𝐷(𝐹‘𝑗))) | 
| 41 | 40 | breq1d 5153 | . . . . . . . . . 10
⊢ (𝑣 = (𝐹‘𝑗) → (((𝐹‘𝑘)𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < ((1 / 2)↑𝑘))) | 
| 42 | 39, 41 | rspc2va 3634 | . . . . . . . . 9
⊢ ((((𝐹‘𝑘) ∈ (𝑆‘𝑘) ∧ (𝐹‘𝑗) ∈ (𝑆‘𝑘)) ∧ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) → ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < ((1 / 2)↑𝑘)) | 
| 43 | 18, 30, 37, 42 | syl21anc 838 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < ((1 / 2)↑𝑘)) | 
| 44 |  | iscmet3.4 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) | 
| 45 | 44 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → 𝐷 ∈ (Met‘𝑋)) | 
| 46 |  | iscmet3.6 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝑍⟶𝑋) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝐹:𝑍⟶𝑋) | 
| 48 |  | ffvelcdm 7101 | . . . . . . . . . . 11
⊢ ((𝐹:𝑍⟶𝑋 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑋) | 
| 49 | 47, 11, 48 | syl2an 596 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑘) ∈ 𝑋) | 
| 50 |  | ffvelcdm 7101 | . . . . . . . . . . 11
⊢ ((𝐹:𝑍⟶𝑋 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ∈ 𝑋) | 
| 51 | 47, 24, 50 | syl2an 596 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑗) ∈ 𝑋) | 
| 52 |  | metcl 24342 | . . . . . . . . . 10
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑗) ∈ 𝑋) → ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) ∈ ℝ) | 
| 53 | 45, 49, 51, 52 | syl3anc 1373 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) ∈ ℝ) | 
| 54 |  | 1rp 13038 | . . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ | 
| 55 |  | rphalfcl 13062 | . . . . . . . . . . . 12
⊢ (1 ∈
ℝ+ → (1 / 2) ∈ ℝ+) | 
| 56 | 54, 55 | ax-mp 5 | . . . . . . . . . . 11
⊢ (1 / 2)
∈ ℝ+ | 
| 57 |  | rpexpcl 14121 | . . . . . . . . . . 11
⊢ (((1 / 2)
∈ ℝ+ ∧ 𝑘 ∈ ℤ) → ((1 / 2)↑𝑘) ∈
ℝ+) | 
| 58 | 56, 35, 57 | sylancr 587 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → ((1 / 2)↑𝑘) ∈
ℝ+) | 
| 59 | 58 | rpred 13077 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → ((1 / 2)↑𝑘) ∈
ℝ) | 
| 60 |  | rpre 13043 | . . . . . . . . . 10
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) | 
| 61 | 60 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℝ) | 
| 62 |  | lttr 11337 | . . . . . . . . 9
⊢ ((((𝐹‘𝑘)𝐷(𝐹‘𝑗)) ∈ ℝ ∧ ((1 / 2)↑𝑘) ∈ ℝ ∧ 𝑟 ∈ ℝ) →
((((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < ((1 / 2)↑𝑘) ∧ ((1 / 2)↑𝑘) < 𝑟) → ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑟)) | 
| 63 | 53, 59, 61, 62 | syl3anc 1373 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < ((1 / 2)↑𝑘) ∧ ((1 / 2)↑𝑘) < 𝑟) → ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑟)) | 
| 64 | 43, 63 | mpand 695 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘))) → (((1 / 2)↑𝑘) < 𝑟 → ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑟)) | 
| 65 | 64 | anassrs 467 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((1 / 2)↑𝑘) < 𝑟 → ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑟)) | 
| 66 | 65 | ralrimdva 3154 | . . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (((1 / 2)↑𝑘) < 𝑟 → ∀𝑗 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑟)) | 
| 67 | 66 | reximdva 3168 | . . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑘 ∈ 𝑍 ((1 / 2)↑𝑘) < 𝑟 → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑟)) | 
| 68 | 6, 67 | mpd 15 | . . 3
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑟) | 
| 69 | 68 | ralrimiva 3146 | . 2
⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑟) | 
| 70 |  | metxmet 24344 | . . . 4
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 71 | 44, 70 | syl 17 | . . 3
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) | 
| 72 |  | eqidd 2738 | . . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) = (𝐹‘𝑗)) | 
| 73 |  | eqidd 2738 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) | 
| 74 | 2, 71, 1, 72, 73, 46 | iscauf 25314 | . 2
⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑟)) | 
| 75 | 69, 74 | mpbird 257 | 1
⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) |