Metamath Proof Explorer

Theorem cau3lem

Description: Lemma for cau3 . (Contributed by Mario Carneiro, 15-Feb-2014) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses cau3lem.1 ⊢ 𝑍 ⊆ ℤ
cau3lem.2 ⊢ ( 𝜏 → 𝜓 )
cau3lem.3 ⊢ ( ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) → ( 𝜓 ↔ 𝜒 ) )
cau3lem.4 ⊢ ( ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) → ( 𝜓 ↔ 𝜃 ) )
cau3lem.5 ⊢ ( ( 𝜑 ∧ 𝜒 ∧ 𝜓 ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) )
cau3lem.6 ⊢ ( ( 𝜑 ∧ 𝜃 ∧ 𝜒 ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) = ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) )
cau3lem.7 ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝑥 ∈ ℝ ) ) → ( ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < ( 𝑥 / 2 ) ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
Assertion cau3lem ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 cau3lem.1 ⊢ 𝑍 ⊆ ℤ
2 cau3lem.2 ⊢ ( 𝜏 → 𝜓 )
3 cau3lem.3 ⊢ ( ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) → ( 𝜓 ↔ 𝜒 ) )
4 cau3lem.4 ⊢ ( ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) → ( 𝜓 ↔ 𝜃 ) )
5 cau3lem.5 ⊢ ( ( 𝜑 ∧ 𝜒 ∧ 𝜓 ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) )
6 cau3lem.6 ⊢ ( ( 𝜑 ∧ 𝜃 ∧ 𝜒 ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) = ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) )
7 cau3lem.7 ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝑥 ∈ ℝ ) ) → ( ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < ( 𝑥 / 2 ) ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
8 breq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ↔ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑧 ) )
9 8 anbi2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑧 ) ) )
10 9 rexralbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑧 ) ) )
11 10 cbvralvw ⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑧 ) )
12 rphalfcl ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ∈ ℝ+ )
13 breq2 ⊢ ( 𝑧 = ( 𝑥 / 2 ) → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑧 ↔ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) )
14 13 anbi2d ⊢ ( 𝑧 = ( 𝑥 / 2 ) → ( ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑧 ) ↔ ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) )
15 14 rexralbidv ⊢ ( 𝑧 = ( 𝑥 / 2 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑧 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) )
16 15 rspcv ⊢ ( ( 𝑥 / 2 ) ∈ ℝ+ → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑧 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) )
17 12 16 syl ⊢ ( 𝑥 ∈ ℝ+ → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑧 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑧 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) )
19 2 ralimi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜏 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 )
20 r19.26 ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ↔ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) )
21 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
22 21 4 syl ⊢ ( 𝑘 = 𝑚 → ( 𝜓 ↔ 𝜃 ) )
23 21 fvoveq1d ⊢ ( 𝑘 = 𝑚 → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) = ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) )
24 23 breq1d ⊢ ( 𝑘 = 𝑚 → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ↔ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) )
25 22 24 anbi12d ⊢ ( 𝑘 = 𝑚 → ( ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ↔ ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) )
26 25 cbvralvw ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) )
27 26 biimpi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) )
28 27 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) )
29 20 28 syl5bir ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) )
30 29 expdimp ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) )
31 1 sseli ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
32 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
33 31 32 syl ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
34 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
35 34 3 syl ⊢ ( 𝑘 = 𝑗 → ( 𝜓 ↔ 𝜒 ) )
36 35 rspcva ⊢ ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → 𝜒 )
37 33 36 sylan ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → 𝜒 )
38 37 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → 𝜒 )
39 30 38 jctild ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ) )
40 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ 𝜓 ) → 𝜑 )
41 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ 𝜓 ) → 𝜃 )
42 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ 𝜓 ) → 𝜒 )
43 40 41 42 6 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ 𝜓 ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) = ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) )
44 43 breq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ 𝜓 ) → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ↔ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < ( 𝑥 / 2 ) ) )
45 44 anbi2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ 𝜓 ) → ( ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ↔ ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < ( 𝑥 / 2 ) ) ) )
46 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ 𝜓 ) → 𝜓 )
47 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ 𝜓 ) → 𝑥 ∈ ℝ+ )
48 47 rpred ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ 𝜓 ) → 𝑥 ∈ ℝ )
49 40 46 41 42 48 7 syl122anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ 𝜓 ) → ( ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < ( 𝑥 / 2 ) ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
50 45 49 sylbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ 𝜓 ) → ( ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
51 50 expd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ 𝜓 ) → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
52 51 impr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ 𝜃 ) ) ∧ ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
53 52 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ∧ ( 𝜒 ∧ 𝜃 ) ) → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
54 53 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ∧ 𝜒 ) ∧ 𝜃 ) → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
55 54 expimpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ∧ 𝜒 ) → ( ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
56 55 ralimdv ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ∧ 𝜒 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
57 56 impr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ∧ ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 )
58 57 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ) ∧ ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 )
59 58 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ) ∧ 𝜓 ) → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
60 uzss ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ℤ≥ ‘ 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑗 ) )
61 ssralv ⊢ ( ( ℤ≥ ‘ 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
62 60 61 syl ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
63 59 62 sylan9 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ) ∧ 𝜓 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
64 63 an32s ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝜓 ) → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
65 64 expimpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
66 65 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
67 66 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
68 67 com23 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ( ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
69 68 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜓 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ( ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
70 20 69 syl5bir ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ( ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
71 70 expdimp ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ( ( 𝜒 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜃 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
72 39 71 mpdd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
73 19 72 sylan2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜏 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
74 73 imdistanda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜏 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜏 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
75 r19.26 ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) ↔ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜏 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) )
76 r19.26 ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜏 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
77 74 75 76 3imtr4g ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
78 77 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < ( 𝑥 / 2 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
79 18 78 syld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑧 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
80 79 ralrimdva ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑧 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
81 11 80 syl5bi ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )
82 fveq2 ⊢ ( 𝑘 = 𝑗 → ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ 𝑗 ) )
83 34 fvoveq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) = ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) )
84 83 breq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ↔ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
85 82 84 raleqbidv ⊢ ( 𝑘 = 𝑗 → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
86 85 rspcv ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
87 86 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) )
88 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑘 ) )
89 88 oveq2d ⊢ ( 𝑚 = 𝑘 → ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) )
90 89 fveq2d ⊢ ( 𝑚 = 𝑘 → ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) = ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) )
91 90 breq1d ⊢ ( 𝑚 = 𝑘 → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ↔ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ) )
92 91 cbvralvw ⊢ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 )
93 36 anim2i ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) ) → ( 𝜑 ∧ 𝜒 ) )
94 93 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ( 𝜑 ∧ 𝜒 ) )
95 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 )
96 5 breq1d ⊢ ( ( 𝜑 ∧ 𝜒 ∧ 𝜓 ) → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ↔ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
97 96 3expia ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 → ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ↔ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
98 97 ralimdv ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ↔ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
99 94 95 98 sylc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ↔ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
100 ralbi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ↔ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
101 99 100 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
102 92 101 syl5bb ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
103 87 102 sylibd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
104 19 103 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜏 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
105 104 imdistanda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜏 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜏 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
106 33 105 sylan2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜏 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜏 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
107 r19.26 ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜏 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
108 106 76 107 3imtr4g ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
109 108 reximdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
110 109 ralimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
111 81 110 impbid ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜏 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐺 ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) ) )