Metamath Proof Explorer

Theorem iscau3

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)

Ref Expression
Hypotheses iscau3.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
iscau3.3 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
iscau3.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
Assertion iscau3 ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 iscau3.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 iscau3.3 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3 iscau3.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 iscau2 ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )
5 2 4 syl ⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )
6 2 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
7 ssid ⊢ ℤ ⊆ ℤ
8 simpr ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
9 eleq1 ⊢ ( ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ↔ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) )
10 eleq1 ⊢ ( ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ↔ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) )
11 xmetsym ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) )
12 11 fveq2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) → ( I ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) = ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) )
13 xmetsym ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) )
14 13 fveq2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) → ( I ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) = ( I ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) )
15 simp1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
16 simp2l ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
17 simp3l ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 )
18 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ* )
19 15 16 17 18 syl3anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ* )
20 simp2r ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 )
21 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ* )
22 15 17 20 21 syl3anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ* )
23 simp3r ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → 𝑥 ∈ ℝ )
24 23 rehalfcld ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( 𝑥 / 2 ) ∈ ℝ )
25 24 rexrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( 𝑥 / 2 ) ∈ ℝ* )
26 xlt2add ⊢ ( ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ* ∧ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ* ) ∧ ( ( 𝑥 / 2 ) ∈ ℝ* ∧ ( 𝑥 / 2 ) ∈ ℝ* ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < ( 𝑥 / 2 ) ∧ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < ( 𝑥 / 2 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < ( ( 𝑥 / 2 ) +𝑒 ( 𝑥 / 2 ) ) ) )
27 19 22 25 25 26 syl22anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < ( 𝑥 / 2 ) ∧ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < ( 𝑥 / 2 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < ( ( 𝑥 / 2 ) +𝑒 ( 𝑥 / 2 ) ) ) )
28 24 24 rexaddd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( 𝑥 / 2 ) +𝑒 ( 𝑥 / 2 ) ) = ( ( 𝑥 / 2 ) + ( 𝑥 / 2 ) ) )
29 23 recnd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → 𝑥 ∈ ℂ )
30 29 2halvesd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( 𝑥 / 2 ) + ( 𝑥 / 2 ) ) = 𝑥 )
31 28 30 eqtrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( 𝑥 / 2 ) +𝑒 ( 𝑥 / 2 ) ) = 𝑥 )
32 31 breq2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < ( ( 𝑥 / 2 ) +𝑒 ( 𝑥 / 2 ) ) ↔ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
33 xmettri ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ≤ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) )
34 15 16 20 17 33 syl13anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ≤ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) )
35 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ* )
36 15 16 20 35 syl3anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ* )
37 19 22 xaddcld ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ* )
38 23 rexrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → 𝑥 ∈ ℝ* )
39 xrlelttr ⊢ ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ* ∧ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ≤ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
40 36 37 38 39 syl3anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ≤ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
41 34 40 mpand ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
42 32 41 sylbid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) +𝑒 ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < ( ( 𝑥 / 2 ) +𝑒 ( 𝑥 / 2 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
43 27 42 syld ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < ( 𝑥 / 2 ) ∧ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < ( 𝑥 / 2 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
44 ovex ⊢ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ∈ V
45 fvi ⊢ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ∈ V → ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) )
46 44 45 ax-mp ⊢ ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) )
47 46 breq1i ⊢ ( ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < ( 𝑥 / 2 ) )
48 ovex ⊢ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ∈ V
49 fvi ⊢ ( ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ∈ V → ( I ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) = ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) )
50 48 49 ax-mp ⊢ ( I ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) = ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) )
51 50 breq1i ⊢ ( ( I ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < ( 𝑥 / 2 ) ↔ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < ( 𝑥 / 2 ) )
52 47 51 anbi12i ⊢ ( ( ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ∧ ( I ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < ( 𝑥 / 2 ) ) ↔ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < ( 𝑥 / 2 ) ∧ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < ( 𝑥 / 2 ) ) )
53 ovex ⊢ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ∈ V
54 fvi ⊢ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ∈ V → ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) )
55 53 54 ax-mp ⊢ ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) )
56 55 breq1i ⊢ ( ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 )
57 43 52 56 3imtr4g ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ ) ) → ( ( ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ∧ ( I ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < ( 𝑥 / 2 ) ) → ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
58 7 8 9 10 12 14 57 cau3lem ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
59 6 58 syl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
60 46 breq1i ⊢ ( ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 )
61 60 anbi2i ⊢ ( ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) )
62 df-3an ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) )
63 61 62 bitr4i ⊢ ( ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) )
64 63 ralbii ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) )
65 64 rexbii ⊢ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) )
66 65 ralbii ⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) )
67 56 ralbii ⊢ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 )
68 67 anbi2i ⊢ ( ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
69 df-3an ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
70 68 69 bitr4i ⊢ ( ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
71 70 ralbii ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
72 71 rexbii ⊢ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
73 72 ralbii ⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( I ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
74 59 66 73 3bitr3g ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
75 3 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → 𝑀 ∈ ℤ )
76 1 rexuz3 ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
77 75 76 syl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
78 77 ralbidv ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
79 74 78 bitr4d ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
80 79 pm5.32da ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) ) )
81 5 80 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) ) )