cvg1nlemres - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > cvg1nlemres		GIF version

Theorem cvg1nlemres 10479

Description: Lemma for cvg1n 10480. The original sequence 𝐹 has a limit (turns out it is the same as the limit of the modified sequence 𝐺). (Contributed by Jim Kingdon, 1-Aug-2021.)

**Hypotheses**
Ref	Expression
cvg1n.f	⊢ (𝜑 → 𝐹:ℕ⟶ℝ)
cvg1n.c	⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
cvg1n.cau	⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))))
cvg1nlem.g	⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍)))
cvg1nlem.z	⊢ (𝜑 → 𝑍 ∈ ℕ)
cvg1nlem.start	⊢ (𝜑 → 𝐶 < 𝑍)

**Assertion**
Ref	Expression
cvg1nlemres	⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))

Distinct variable groups: 𝐶,𝑖,𝑘 𝐶,𝑛,𝑘 𝑗,𝐹,𝑘,𝑛 𝑖,𝐺,𝑦,𝑘 𝑛,𝐺 𝑥,𝐺,𝑖,𝑦 𝑖,𝑍,𝑗,𝑘 𝑛,𝑍 𝜑,𝑖,𝑥,𝑦,𝑗 𝜑,𝑘,𝑛 𝑥,𝑗,𝑦 Allowed substitution hints: 𝐶(𝑥,𝑦,𝑗) 𝐹(𝑥,𝑦,𝑖) 𝐺(𝑗) 𝑍(𝑥,𝑦)

Proof of Theorem cvg1nlemres Dummy variables 𝑒 𝑎 𝑏 𝑐 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cvg1n.f	. . . 4 ⊢ (𝜑 → 𝐹:ℕ⟶ℝ)
2		cvg1n.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
3		cvg1n.cau	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))))
4		cvg1nlem.g	. . . 4 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍)))
5		cvg1nlem.z	. . . 4 ⊢ (𝜑 → 𝑍 ∈ ℕ)
6		cvg1nlem.start	. . . 4 ⊢ (𝜑 → 𝐶 < 𝑍)
7	1, 2, 3, 4, 5, 6	cvg1nlemf 10477	. . 3 ⊢ (𝜑 → 𝐺:ℕ⟶ℝ)
8	1, 2, 3, 4, 5, 6	cvg1nlemcau 10478	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((𝐺‘𝑛) < ((𝐺‘𝑘) + (1 / 𝑛)) ∧ (𝐺‘𝑘) < ((𝐺‘𝑛) + (1 / 𝑛))))
9	7, 8	caucvgre 10475	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)))
10		fveq2 5318	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑤 → (ℤ_≥‘𝑎) = (ℤ_≥‘𝑤))
11	10	raleqdv 2569	. . . . . . . . . 10 ⊢ (𝑎 = 𝑤 → (∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))))
12	11	cbvrexv 2592	. . . . . . . . 9 ⊢ (∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)))
13	12	ralbii 2385	. . . . . . . 8 ⊢ (∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)))
14	13	anbi2i 446	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ↔ ((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))))
15	14	anbi1i 447	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ↔ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺))
16		oveq2 5674	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑥 / 2) → (𝑦 + 𝑐) = (𝑦 + (𝑥 / 2)))
17	16	breq2d 3863	. . . . . . . . . . 11 ⊢ (𝑐 = (𝑥 / 2) → ((𝐺‘𝑏) < (𝑦 + 𝑐) ↔ (𝐺‘𝑏) < (𝑦 + (𝑥 / 2))))
18		oveq2 5674	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑥 / 2) → ((𝐺‘𝑏) + 𝑐) = ((𝐺‘𝑏) + (𝑥 / 2)))
19	18	breq2d 3863	. . . . . . . . . . 11 ⊢ (𝑐 = (𝑥 / 2) → (𝑦 < ((𝐺‘𝑏) + 𝑐) ↔ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))
20	17, 19	anbi12d 458	. . . . . . . . . 10 ⊢ (𝑐 = (𝑥 / 2) → (((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)))))
21	20	rexralbidv 2405	. . . . . . . . 9 ⊢ (𝑐 = (𝑥 / 2) → (∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) ↔ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)))))
22		simplr 498	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) → ∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)))
23		simpr 109	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
24	23	rphalfcld 9247	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 / 2) ∈ ℝ⁺)
25	21, 22, 24	rspcdva 2728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))
26	15, 25	sylbir 134	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))
27	2	rpred 9234	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ℝ)
28	27	ad4antr 479	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝐶 ∈ ℝ)
29		2re 8553	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ
30	29	a1i 9	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 2 ∈ ℝ)
31	28, 30	remulcld 7579	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → (𝐶 · 2) ∈ ℝ)
32		simplr 498	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝑥 ∈ ℝ⁺)
33	31, 32	rerpdivcld 9266	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ((𝐶 · 2) / 𝑥) ∈ ℝ)
34	5	ad4antr 479	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝑍 ∈ ℕ)
35	33, 34	nndivred 8533	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → (((𝐶 · 2) / 𝑥) / 𝑍) ∈ ℝ)
36		simprl 499	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝑎 ∈ ℕ)
37	36	nnred 8496	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → 𝑎 ∈ ℝ)
38	35, 37	readdcld 7578	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) ∈ ℝ)
39		arch 8731	. . . . . . . . 9 ⊢ (((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) ∈ ℝ → ∃𝑒 ∈ ℕ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)
40	38, 39	syl 14	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ∃𝑒 ∈ ℕ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)
41		simprl 499	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → 𝑒 ∈ ℕ)
42	34	adantr 271	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → 𝑍 ∈ ℕ)
43	41, 42	nnmulcld 8532	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → (𝑒 · 𝑍) ∈ ℕ)
44	1	ad6antr 483	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝐹:ℕ⟶ℝ)
45		simplrl 503	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑒 ∈ ℕ)
46	5	ad6antr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑍 ∈ ℕ)
47	45, 46	nnmulcld 8532	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝑒 · 𝑍) ∈ ℕ)
48		eluznn 9148	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 · 𝑍) ∈ ℕ ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑖 ∈ ℕ)
49	47, 48	sylancom 412	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑖 ∈ ℕ)
50	44, 49	ffvelrnd 5449	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) ∈ ℝ)
51	44, 47	ffvelrnd 5449	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐹‘(𝑒 · 𝑍)) ∈ ℝ)
52	32	ad2antrr 473	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℝ⁺)
53	52	rpred 9234	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℝ)
54	53	rehalfcld 8723	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝑥 / 2) ∈ ℝ)
55	51, 54	readdcld 7578	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)) ∈ ℝ)
56		simpllr 502	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) → 𝑦 ∈ ℝ)
57	56	ad3antrrr 477	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑦 ∈ ℝ)
58	57, 54	readdcld 7578	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝑦 + (𝑥 / 2)) ∈ ℝ)
59	58, 54	readdcld 7578	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝑦 + (𝑥 / 2)) + (𝑥 / 2)) ∈ ℝ)
60	27	ad6antr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝐶 ∈ ℝ)
61	60, 47	nndivred 8533	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐶 / (𝑒 · 𝑍)) ∈ ℝ)
62	51, 61	readdcld 7578	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))) ∈ ℝ)
63		fveq2 5318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
64	63	oveq1d 5681	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) = ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))))
65	64	breq2d 3863	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ↔ (𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍)))))
66	63	breq1d 3861	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))) ↔ (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))))
67	65, 66	anbi12d 458	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑖 → (((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))) ↔ ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))))
68		fveq2 5318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = (𝑒 · 𝑍) → (ℤ_≥‘𝑛) = (ℤ_≥‘(𝑒 · 𝑍)))
69		fveq2 5318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = (𝑒 · 𝑍) → (𝐹‘𝑛) = (𝐹‘(𝑒 · 𝑍)))
70		oveq2 5674	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (𝑒 · 𝑍) → (𝐶 / 𝑛) = (𝐶 / (𝑒 · 𝑍)))
71	70	oveq2d 5682	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = (𝑒 · 𝑍) → ((𝐹‘𝑘) + (𝐶 / 𝑛)) = ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))))
72	69, 71	breq12d 3864	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = (𝑒 · 𝑍) → ((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ↔ (𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍)))))
73	69, 70	oveq12d 5684	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = (𝑒 · 𝑍) → ((𝐹‘𝑛) + (𝐶 / 𝑛)) = ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))
74	73	breq2d 3863	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = (𝑒 · 𝑍) → ((𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛)) ↔ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))))
75	72, 74	anbi12d 458	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = (𝑒 · 𝑍) → (((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))) ↔ ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))))
76	68, 75	raleqbidv 2575	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑒 · 𝑍) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))) ↔ ∀𝑘 ∈ (ℤ_≥‘(𝑒 · 𝑍))((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))))
77	3	ad6antr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))))
78	76, 77, 47	rspcdva 2728	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ∀𝑘 ∈ (ℤ_≥‘(𝑒 · 𝑍))((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑘) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑘) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))))
79		simpr 109	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍)))
80	67, 78, 79	rspcdva 2728	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ∧ (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍)))))
81	80	simprd 113	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))))
82		simpr 109	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
83	82	ad3antrrr 477	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℝ⁺)
84	83	rpred 9234	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℝ)
85	84	rehalfcld 8723	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝑥 / 2) ∈ ℝ)
86	2	ad6antr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝐶 ∈ ℝ⁺)
87	36	ad2antrr 473	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑎 ∈ ℕ)
88		simplrr 504	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)
89	86, 83, 46, 45, 87, 88	cvg1nlemcxze 10476	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐶 / (𝑒 · 𝑍)) < (𝑥 / 2))
90	61, 85, 89	ltled 7663	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐶 / (𝑒 · 𝑍)) ≤ (𝑥 / 2))
91	61, 54, 51, 90	leadd2dd 8098	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝐶 / (𝑒 · 𝑍))) ≤ ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)))
92	50, 62, 55, 81, 91	ltletrd 7962	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)))
93		fveq2 5318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑒 → (𝐺‘𝑏) = (𝐺‘𝑒))
94	93	breq1d 3861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑒 → ((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ↔ (𝐺‘𝑒) < (𝑦 + (𝑥 / 2))))
95	93	oveq1d 5681	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑒 → ((𝐺‘𝑏) + (𝑥 / 2)) = ((𝐺‘𝑒) + (𝑥 / 2)))
96	95	breq2d 3863	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑒 → (𝑦 < ((𝐺‘𝑏) + (𝑥 / 2)) ↔ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2))))
97	94, 96	anbi12d 458	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑒 → (((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))) ↔ ((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2)))))
98		simprr 500	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))
99	98	ad2antrr 473	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))
100	87	nnred 8496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑎 ∈ ℝ)
101	45	nnred 8496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑒 ∈ ℝ)
102		2rp 9200	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 ∈ ℝ⁺
103	102	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 2 ∈ ℝ⁺)
104	86, 103	rpmulcld 9251	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐶 · 2) ∈ ℝ⁺)
105	104, 83	rpdivcld 9252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐶 · 2) / 𝑥) ∈ ℝ⁺)
106	46	nnrpd 9233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑍 ∈ ℝ⁺)
107	105, 106	rpdivcld 9252	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (((𝐶 · 2) / 𝑥) / 𝑍) ∈ ℝ⁺)
108	107	rpred 9234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (((𝐶 · 2) / 𝑥) / 𝑍) ∈ ℝ)
109	108, 100	readdcld 7578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) ∈ ℝ)
110	100, 107	ltaddrp2d 9269	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑎 < ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎))
111	100, 109, 101, 110, 88	lttrd 7670	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑎 < 𝑒)
112	100, 101, 111	ltled 7663	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑎 ≤ 𝑒)
113	87	nnzd 8928	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑎 ∈ ℤ)
114	45	nnzd 8928	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑒 ∈ ℤ)
115		eluz 9093	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ℤ ∧ 𝑒 ∈ ℤ) → (𝑒 ∈ (ℤ_≥‘𝑎) ↔ 𝑎 ≤ 𝑒))
116	113, 114, 115	syl2anc 404	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝑒 ∈ (ℤ_≥‘𝑎) ↔ 𝑎 ≤ 𝑒))
117	112, 116	mpbird 166	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑒 ∈ (ℤ_≥‘𝑎))
118	97, 99, 117	rspcdva 2728	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2))))
119		oveq1 5673	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑒 → (𝑗 · 𝑍) = (𝑒 · 𝑍))
120	119	fveq2d 5322	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑒 → (𝐹‘(𝑗 · 𝑍)) = (𝐹‘(𝑒 · 𝑍)))
121	120, 4	fvmptg 5393	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 ∈ ℕ ∧ (𝐹‘(𝑒 · 𝑍)) ∈ ℝ) → (𝐺‘𝑒) = (𝐹‘(𝑒 · 𝑍)))
122	45, 51, 121	syl2anc 404	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐺‘𝑒) = (𝐹‘(𝑒 · 𝑍)))
123	122	breq1d 3861	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ↔ (𝐹‘(𝑒 · 𝑍)) < (𝑦 + (𝑥 / 2))))
124	122	oveq1d 5681	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐺‘𝑒) + (𝑥 / 2)) = ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)))
125	124	breq2d 3863	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝑦 < ((𝐺‘𝑒) + (𝑥 / 2)) ↔ 𝑦 < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2))))
126	123, 125	anbi12d 458	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (((𝐺‘𝑒) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑒) + (𝑥 / 2))) ↔ ((𝐹‘(𝑒 · 𝑍)) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)))))
127	118, 126	mpbid 146	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2))))
128	127	simpld 111	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐹‘(𝑒 · 𝑍)) < (𝑦 + (𝑥 / 2)))
129	51, 58, 54, 128	ltadd1dd 8094	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)) < ((𝑦 + (𝑥 / 2)) + (𝑥 / 2)))
130	50, 55, 59, 92, 129	lttrd 7670	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < ((𝑦 + (𝑥 / 2)) + (𝑥 / 2)))
131	57	recnd 7577	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑦 ∈ ℂ)
132	54	recnd 7577	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝑥 / 2) ∈ ℂ)
133	131, 132, 132	addassd 7571	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝑦 + (𝑥 / 2)) + (𝑥 / 2)) = (𝑦 + ((𝑥 / 2) + (𝑥 / 2))))
134	130, 133	breqtrd 3875	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < (𝑦 + ((𝑥 / 2) + (𝑥 / 2))))
135	52	rpcnd 9236	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑥 ∈ ℂ)
136	135	2halvesd 8722	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥)
137	136	oveq2d 5682	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝑦 + ((𝑥 / 2) + (𝑥 / 2))) = (𝑦 + 𝑥))
138	134, 137	breqtrd 3875	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) < (𝑦 + 𝑥))
139	50, 54	readdcld 7578	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) + (𝑥 / 2)) ∈ ℝ)
140	139, 54	readdcld 7578	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (((𝐹‘𝑖) + (𝑥 / 2)) + (𝑥 / 2)) ∈ ℝ)
141	127	simprd 113	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑦 < ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)))
142	50, 61	readdcld 7578	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ∈ ℝ)
143	80	simpld 111	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))))
144	61, 54, 50, 90	leadd2dd 8098	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) + (𝐶 / (𝑒 · 𝑍))) ≤ ((𝐹‘𝑖) + (𝑥 / 2)))
145	51, 142, 139, 143, 144	ltletrd 7962	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐹‘(𝑒 · 𝑍)) < ((𝐹‘𝑖) + (𝑥 / 2)))
146	51, 139, 54, 145	ltadd1dd 8094	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐹‘(𝑒 · 𝑍)) + (𝑥 / 2)) < (((𝐹‘𝑖) + (𝑥 / 2)) + (𝑥 / 2)))
147	57, 55, 140, 141, 146	lttrd 7670	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑦 < (((𝐹‘𝑖) + (𝑥 / 2)) + (𝑥 / 2)))
148	50	recnd 7577	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (𝐹‘𝑖) ∈ ℂ)
149	148, 132, 132	addassd 7571	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → (((𝐹‘𝑖) + (𝑥 / 2)) + (𝑥 / 2)) = ((𝐹‘𝑖) + ((𝑥 / 2) + (𝑥 / 2))))
150	147, 149	breqtrd 3875	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑦 < ((𝐹‘𝑖) + ((𝑥 / 2) + (𝑥 / 2))))
151	136	oveq2d 5682	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) + ((𝑥 / 2) + (𝑥 / 2))) = ((𝐹‘𝑖) + 𝑥))
152	150, 151	breqtrd 3875	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → 𝑦 < ((𝐹‘𝑖) + 𝑥))
153	138, 152	jca 301	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) ∧ 𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))) → ((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
154	153	ralrimiva 2447	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → ∀𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
155		fveq2 5318	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑒 · 𝑍) → (ℤ_≥‘𝑗) = (ℤ_≥‘(𝑒 · 𝑍)))
156	155	raleqdv 2569	. . . . . . . . . 10 ⊢ (𝑗 = (𝑒 · 𝑍) → (∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)) ↔ ∀𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))))
157	156	rspcev 2723	. . . . . . . . 9 ⊢ (((𝑒 · 𝑍) ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘(𝑒 · 𝑍))((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
158	43, 154, 157	syl2anc 404	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) ∧ (𝑒 ∈ ℕ ∧ ((((𝐶 · 2) / 𝑥) / 𝑍) + 𝑎) < 𝑒)) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
159	40, 158	rexlimddv 2494	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑎 ∈ ℕ ∧ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + (𝑥 / 2)) ∧ 𝑦 < ((𝐺‘𝑏) + (𝑥 / 2))))) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
160	26, 159	rexlimddv 2494	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑤)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
161	15, 160	sylbi 120	. . . . 5 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) ∧ 𝑥 ∈ ℝ⁺) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
162	161	ralrimiva 2447	. . . 4 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐))) → ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
163	162	ex 114	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) → ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))))
164	163	reximdva 2476	. 2 ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑐 ∈ ℝ⁺ ∃𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ_≥‘𝑎)((𝐺‘𝑏) < (𝑦 + 𝑐) ∧ 𝑦 < ((𝐺‘𝑏) + 𝑐)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))))
165	9, 164	mpd 13	1 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1290 ∈ wcel 1439 ∀wral 2360 ∃wrex 2361 class class class wbr 3851 ↦ cmpt 3905 ⟶wf 5024 ‘cfv 5028 (class class class)co 5666 ℝcr 7410 + caddc 7414 · cmul 7416 < clt 7583 ≤ cle 7584 / cdiv 8200 ℕcn 8483 2c2 8534 ℤcz 8811 ℤ_≥cuz 9080 ℝ⁺crp 9195

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 580 ax-in2 581 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-13 1450 ax-14 1451 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-sep 3963 ax-pow 4015 ax-pr 4045 ax-un 4269 ax-setind 4366 ax-cnex 7497 ax-resscn 7498 ax-1cn 7499 ax-1re 7500 ax-icn 7501 ax-addcl 7502 ax-addrcl 7503 ax-mulcl 7504 ax-mulrcl 7505 ax-addcom 7506 ax-mulcom 7507 ax-addass 7508 ax-mulass 7509 ax-distr 7510 ax-i2m1 7511 ax-0lt1 7512 ax-1rid 7513 ax-0id 7514 ax-rnegex 7515 ax-precex 7516 ax-cnre 7517 ax-pre-ltirr 7518 ax-pre-ltwlin 7519 ax-pre-lttrn 7520 ax-pre-apti 7521 ax-pre-ltadd 7522 ax-pre-mulgt0 7523 ax-pre-mulext 7524 ax-arch 7525 ax-caucvg 7526

This theorem depends on definitions: df-bi 116 df-3or 926 df-3an 927 df-tru 1293 df-fal 1296 df-nf 1396 df-sb 1694 df-eu 1952 df-mo 1953 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ne 2257 df-nel 2352 df-ral 2365 df-rex 2366 df-reu 2367 df-rmo 2368 df-rab 2369 df-v 2622 df-sbc 2842 df-dif 3002 df-un 3004 df-in 3006 df-ss 3013 df-pw 3435 df-sn 3456 df-pr 3457 df-op 3459 df-uni 3660 df-int 3695 df-br 3852 df-opab 3906 df-mpt 3907 df-id 4129 df-po 4132 df-iso 4133 df-xp 4458 df-rel 4459 df-cnv 4460 df-co 4461 df-dm 4462 df-rn 4463 df-res 4464 df-ima 4465 df-iota 4993 df-fun 5030 df-fn 5031 df-f 5032 df-fv 5036 df-riota 5622 df-ov 5669 df-oprab 5670 df-mpt2 5671 df-pnf 7585 df-mnf 7586 df-xr 7587 df-ltxr 7588 df-le 7589 df-sub 7716 df-neg 7717 df-reap 8113 df-ap 8120 df-div 8201 df-inn 8484 df-2 8542 df-n0 8735 df-z 8812 df-uz 9081 df-rp 9196

This theorem is referenced by: cvg1n 10480

W3C validator