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

Theorem ivthinclemuopn 12799
 Description: Lemma for ivthinc 12804. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.)
Hypotheses
Ref Expression
ivth.1 (𝜑𝐴 ∈ ℝ)
ivth.2 (𝜑𝐵 ∈ ℝ)
ivth.3 (𝜑𝑈 ∈ ℝ)
ivth.4 (𝜑𝐴 < 𝐵)
ivth.5 (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
ivth.7 (𝜑𝐹 ∈ (𝐷cn→ℂ))
ivth.8 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)
ivth.9 (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))
ivthinc.i (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))
ivthinclem.l 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}
ivthinclem.r 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}
ivthinclemuopn.r (𝜑𝑆𝑅)
Assertion
Ref Expression
ivthinclemuopn (𝜑 → ∃𝑞𝑅 𝑞 < 𝑆)
Distinct variable groups:   𝑤,𝐴   𝑥,𝐴,𝑦   𝑤,𝐵   𝑥,𝐵,𝑦   𝑤,𝐹   𝑥,𝐹,𝑦   𝑅,𝑞   𝑆,𝑞   𝑤,𝑆   𝑥,𝑆,𝑦   𝑤,𝑈   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑤,𝑞)   𝐴(𝑞)   𝐵(𝑞)   𝐷(𝑥,𝑦,𝑤,𝑞)   𝑅(𝑥,𝑦,𝑤)   𝑈(𝑥,𝑦,𝑞)   𝐹(𝑞)   𝐿(𝑥,𝑦,𝑤,𝑞)

Proof of Theorem ivthinclemuopn
Dummy variables 𝑧 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ivth.7 . . 3 (𝜑𝐹 ∈ (𝐷cn→ℂ))
2 ivth.5 . . . 4 (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
3 ivthinclemuopn.r . . . . . 6 (𝜑𝑆𝑅)
4 fveq2 5421 . . . . . . . 8 (𝑤 = 𝑆 → (𝐹𝑤) = (𝐹𝑆))
54breq2d 3941 . . . . . . 7 (𝑤 = 𝑆 → (𝑈 < (𝐹𝑤) ↔ 𝑈 < (𝐹𝑆)))
6 ivthinclem.r . . . . . . 7 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}
75, 6elrab2 2843 . . . . . 6 (𝑆𝑅 ↔ (𝑆 ∈ (𝐴[,]𝐵) ∧ 𝑈 < (𝐹𝑆)))
83, 7sylib 121 . . . . 5 (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ∧ 𝑈 < (𝐹𝑆)))
98simpld 111 . . . 4 (𝜑𝑆 ∈ (𝐴[,]𝐵))
102, 9sseldd 3098 . . 3 (𝜑𝑆𝐷)
11 fveq2 5421 . . . . . . 7 (𝑥 = 𝑆 → (𝐹𝑥) = (𝐹𝑆))
1211eleq1d 2208 . . . . . 6 (𝑥 = 𝑆 → ((𝐹𝑥) ∈ ℝ ↔ (𝐹𝑆) ∈ ℝ))
13 ivth.8 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)
1413ralrimiva 2505 . . . . . 6 (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) ∈ ℝ)
1512, 14, 9rspcdva 2794 . . . . 5 (𝜑 → (𝐹𝑆) ∈ ℝ)
16 ivth.3 . . . . 5 (𝜑𝑈 ∈ ℝ)
1715, 16resubcld 8155 . . . 4 (𝜑 → ((𝐹𝑆) − 𝑈) ∈ ℝ)
188simprd 113 . . . . 5 (𝜑𝑈 < (𝐹𝑆))
1916, 15posdifd 8306 . . . . 5 (𝜑 → (𝑈 < (𝐹𝑆) ↔ 0 < ((𝐹𝑆) − 𝑈)))
2018, 19mpbid 146 . . . 4 (𝜑 → 0 < ((𝐹𝑆) − 𝑈))
2117, 20elrpd 9493 . . 3 (𝜑 → ((𝐹𝑆) − 𝑈) ∈ ℝ+)
22 cncfi 12748 . . 3 ((𝐹 ∈ (𝐷cn→ℂ) ∧ 𝑆𝐷 ∧ ((𝐹𝑆) − 𝑈) ∈ ℝ+) → ∃𝑑 ∈ ℝ+𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))
231, 10, 21, 22syl3anc 1216 . 2 (𝜑 → ∃𝑑 ∈ ℝ+𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))
24 ivth.1 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
25 ivth.2 . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
26 elicc2 9733 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑆 ∈ (𝐴[,]𝐵) ↔ (𝑆 ∈ ℝ ∧ 𝐴𝑆𝑆𝐵)))
2724, 25, 26syl2anc 408 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ↔ (𝑆 ∈ ℝ ∧ 𝐴𝑆𝑆𝐵)))
289, 27mpbid 146 . . . . . . . 8 (𝜑 → (𝑆 ∈ ℝ ∧ 𝐴𝑆𝑆𝐵))
2928simp1d 993 . . . . . . 7 (𝜑𝑆 ∈ ℝ)
3029adantr 274 . . . . . 6 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝑆 ∈ ℝ)
31 simprl 520 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝑑 ∈ ℝ+)
3231rphalfcld 9508 . . . . . . 7 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑑 / 2) ∈ ℝ+)
3332rpred 9495 . . . . . 6 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑑 / 2) ∈ ℝ)
3430, 33resubcld 8155 . . . . 5 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑆 − (𝑑 / 2)) ∈ ℝ)
3524adantr 274 . . . . . 6 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝐴 ∈ ℝ)
3631rpred 9495 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝑑 ∈ ℝ)
3730, 36resubcld 8155 . . . . . . 7 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑆𝑑) ∈ ℝ)
3815ad2antrr 479 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → (𝐹𝑆) ∈ ℝ)
3938recnd 7806 . . . . . . . . . . 11 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → (𝐹𝑆) ∈ ℂ)
4016recnd 7806 . . . . . . . . . . . 12 (𝜑𝑈 ∈ ℂ)
4140ad2antrr 479 . . . . . . . . . . 11 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → 𝑈 ∈ ℂ)
4239, 41nncand 8090 . . . . . . . . . 10 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → ((𝐹𝑆) − ((𝐹𝑆) − 𝑈)) = 𝑈)
43 simpr 109 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → (𝑆𝑑) < 𝐴)
4424ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → 𝐴 ∈ ℝ)
4529ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → 𝑆 ∈ ℝ)
4631adantr 274 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → 𝑑 ∈ ℝ+)
4746rpred 9495 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → 𝑑 ∈ ℝ)
4845, 47readdcld 7807 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → (𝑆 + 𝑑) ∈ ℝ)
4928simp2d 994 . . . . . . . . . . . . . . . 16 (𝜑𝐴𝑆)
5049ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → 𝐴𝑆)
5145, 46ltaddrpd 9529 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → 𝑆 < (𝑆 + 𝑑))
5244, 45, 48, 50, 51lelttrd 7899 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → 𝐴 < (𝑆 + 𝑑))
5344, 45, 47absdifltd 10962 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → ((abs‘(𝐴𝑆)) < 𝑑 ↔ ((𝑆𝑑) < 𝐴𝐴 < (𝑆 + 𝑑))))
5443, 52, 53mpbir2and 928 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → (abs‘(𝐴𝑆)) < 𝑑)
55 fvoveq1 5797 . . . . . . . . . . . . . . . 16 (𝑧 = 𝐴 → (abs‘(𝑧𝑆)) = (abs‘(𝐴𝑆)))
5655breq1d 3939 . . . . . . . . . . . . . . 15 (𝑧 = 𝐴 → ((abs‘(𝑧𝑆)) < 𝑑 ↔ (abs‘(𝐴𝑆)) < 𝑑))
5756imbrov2fvoveq 5799 . . . . . . . . . . . . . 14 (𝑧 = 𝐴 → (((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)) ↔ ((abs‘(𝐴𝑆)) < 𝑑 → (abs‘((𝐹𝐴) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈))))
58 simplrr 525 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))
5924rexrd 7827 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℝ*)
6025rexrd 7827 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℝ*)
61 ivth.4 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 < 𝐵)
6224, 25, 61ltled 7893 . . . . . . . . . . . . . . . . 17 (𝜑𝐴𝐵)
63 lbicc2 9779 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
6459, 60, 62, 63syl3anc 1216 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ (𝐴[,]𝐵))
652, 64sseldd 3098 . . . . . . . . . . . . . . 15 (𝜑𝐴𝐷)
6665ad2antrr 479 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → 𝐴𝐷)
6757, 58, 66rspcdva 2794 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → ((abs‘(𝐴𝑆)) < 𝑑 → (abs‘((𝐹𝐴) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))
6854, 67mpd 13 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → (abs‘((𝐹𝐴) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈))
69 fveq2 5421 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
7069eleq1d 2208 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 → ((𝐹𝑥) ∈ ℝ ↔ (𝐹𝐴) ∈ ℝ))
7114adantr 274 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) ∈ ℝ)
7264adantr 274 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝐴 ∈ (𝐴[,]𝐵))
7370, 71, 72rspcdva 2794 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝐹𝐴) ∈ ℝ)
7473adantr 274 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → (𝐹𝐴) ∈ ℝ)
7517ad2antrr 479 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → ((𝐹𝑆) − 𝑈) ∈ ℝ)
7674, 38, 75absdifltd 10962 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → ((abs‘((𝐹𝐴) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈) ↔ (((𝐹𝑆) − ((𝐹𝑆) − 𝑈)) < (𝐹𝐴) ∧ (𝐹𝐴) < ((𝐹𝑆) + ((𝐹𝑆) − 𝑈)))))
7768, 76mpbid 146 . . . . . . . . . . 11 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → (((𝐹𝑆) − ((𝐹𝑆) − 𝑈)) < (𝐹𝐴) ∧ (𝐹𝐴) < ((𝐹𝑆) + ((𝐹𝑆) − 𝑈))))
7877simpld 111 . . . . . . . . . 10 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → ((𝐹𝑆) − ((𝐹𝑆) − 𝑈)) < (𝐹𝐴))
7942, 78eqbrtrrd 3952 . . . . . . . . 9 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → 𝑈 < (𝐹𝐴))
8016ad2antrr 479 . . . . . . . . . 10 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → 𝑈 ∈ ℝ)
81 ivth.9 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))
8281simpld 111 . . . . . . . . . . 11 (𝜑 → (𝐹𝐴) < 𝑈)
8382ad2antrr 479 . . . . . . . . . 10 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → (𝐹𝐴) < 𝑈)
8474, 80, 83ltnsymd 7894 . . . . . . . . 9 (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) ∧ (𝑆𝑑) < 𝐴) → ¬ 𝑈 < (𝐹𝐴))
8579, 84pm2.65da 650 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → ¬ (𝑆𝑑) < 𝐴)
8635, 37, 85nltled 7895 . . . . . . 7 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝐴 ≤ (𝑆𝑑))
87 rphalflt 9483 . . . . . . . . 9 (𝑑 ∈ ℝ+ → (𝑑 / 2) < 𝑑)
8831, 87syl 14 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑑 / 2) < 𝑑)
8933, 36, 30, 88ltsub2dd 8332 . . . . . . 7 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑆𝑑) < (𝑆 − (𝑑 / 2)))
9035, 37, 34, 86, 89lelttrd 7899 . . . . . 6 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝐴 < (𝑆 − (𝑑 / 2)))
9135, 34, 90ltled 7893 . . . . 5 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝐴 ≤ (𝑆 − (𝑑 / 2)))
9225adantr 274 . . . . . 6 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝐵 ∈ ℝ)
9330, 32ltsubrpd 9528 . . . . . . 7 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑆 − (𝑑 / 2)) < 𝑆)
9434, 30, 93ltled 7893 . . . . . 6 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑆 − (𝑑 / 2)) ≤ 𝑆)
9528simp3d 995 . . . . . . 7 (𝜑𝑆𝐵)
9695adantr 274 . . . . . 6 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝑆𝐵)
9734, 30, 92, 94, 96letrd 7898 . . . . 5 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑆 − (𝑑 / 2)) ≤ 𝐵)
98 elicc2 9733 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝑆 − (𝑑 / 2)) ∈ (𝐴[,]𝐵) ↔ ((𝑆 − (𝑑 / 2)) ∈ ℝ ∧ 𝐴 ≤ (𝑆 − (𝑑 / 2)) ∧ (𝑆 − (𝑑 / 2)) ≤ 𝐵)))
9935, 92, 98syl2anc 408 . . . . 5 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → ((𝑆 − (𝑑 / 2)) ∈ (𝐴[,]𝐵) ↔ ((𝑆 − (𝑑 / 2)) ∈ ℝ ∧ 𝐴 ≤ (𝑆 − (𝑑 / 2)) ∧ (𝑆 − (𝑑 / 2)) ≤ 𝐵)))
10034, 91, 97, 99mpbir3and 1164 . . . 4 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑆 − (𝑑 / 2)) ∈ (𝐴[,]𝐵))
101 fveq2 5421 . . . . . . . . 9 (𝑥 = (𝑆 − (𝑑 / 2)) → (𝐹𝑥) = (𝐹‘(𝑆 − (𝑑 / 2))))
102101eleq1d 2208 . . . . . . . 8 (𝑥 = (𝑆 − (𝑑 / 2)) → ((𝐹𝑥) ∈ ℝ ↔ (𝐹‘(𝑆 − (𝑑 / 2))) ∈ ℝ))
103102, 71, 100rspcdva 2794 . . . . . . 7 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝐹‘(𝑆 − (𝑑 / 2))) ∈ ℝ)
10415adantr 274 . . . . . . 7 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝐹𝑆) ∈ ℝ)
105 breq2 3933 . . . . . . . . . . 11 (𝑦 = 𝑆 → ((𝑆 − (𝑑 / 2)) < 𝑦 ↔ (𝑆 − (𝑑 / 2)) < 𝑆))
106 fveq2 5421 . . . . . . . . . . . 12 (𝑦 = 𝑆 → (𝐹𝑦) = (𝐹𝑆))
107106breq2d 3941 . . . . . . . . . . 11 (𝑦 = 𝑆 → ((𝐹‘(𝑆 − (𝑑 / 2))) < (𝐹𝑦) ↔ (𝐹‘(𝑆 − (𝑑 / 2))) < (𝐹𝑆)))
108105, 107imbi12d 233 . . . . . . . . . 10 (𝑦 = 𝑆 → (((𝑆 − (𝑑 / 2)) < 𝑦 → (𝐹‘(𝑆 − (𝑑 / 2))) < (𝐹𝑦)) ↔ ((𝑆 − (𝑑 / 2)) < 𝑆 → (𝐹‘(𝑆 − (𝑑 / 2))) < (𝐹𝑆))))
109 breq1 3932 . . . . . . . . . . . . 13 (𝑥 = (𝑆 − (𝑑 / 2)) → (𝑥 < 𝑦 ↔ (𝑆 − (𝑑 / 2)) < 𝑦))
110101breq1d 3939 . . . . . . . . . . . . 13 (𝑥 = (𝑆 − (𝑑 / 2)) → ((𝐹𝑥) < (𝐹𝑦) ↔ (𝐹‘(𝑆 − (𝑑 / 2))) < (𝐹𝑦)))
111109, 110imbi12d 233 . . . . . . . . . . . 12 (𝑥 = (𝑆 − (𝑑 / 2)) → ((𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)) ↔ ((𝑆 − (𝑑 / 2)) < 𝑦 → (𝐹‘(𝑆 − (𝑑 / 2))) < (𝐹𝑦))))
112111ralbidv 2437 . . . . . . . . . . 11 (𝑥 = (𝑆 − (𝑑 / 2)) → (∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)((𝑆 − (𝑑 / 2)) < 𝑦 → (𝐹‘(𝑆 − (𝑑 / 2))) < (𝐹𝑦))))
113 ivthinc.i . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))
114113expr 372 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)))
115114ralrimiva 2505 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)))
116115ralrimiva 2505 . . . . . . . . . . . 12 (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)))
117116adantr 274 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)))
118112, 117, 100rspcdva 2794 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → ∀𝑦 ∈ (𝐴[,]𝐵)((𝑆 − (𝑑 / 2)) < 𝑦 → (𝐹‘(𝑆 − (𝑑 / 2))) < (𝐹𝑦)))
1199adantr 274 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝑆 ∈ (𝐴[,]𝐵))
120108, 118, 119rspcdva 2794 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → ((𝑆 − (𝑑 / 2)) < 𝑆 → (𝐹‘(𝑆 − (𝑑 / 2))) < (𝐹𝑆)))
12193, 120mpd 13 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝐹‘(𝑆 − (𝑑 / 2))) < (𝐹𝑆))
122103, 104, 121ltled 7893 . . . . . . 7 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝐹‘(𝑆 − (𝑑 / 2))) ≤ (𝐹𝑆))
123103, 104, 122abssuble0d 10961 . . . . . 6 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (abs‘((𝐹‘(𝑆 − (𝑑 / 2))) − (𝐹𝑆))) = ((𝐹𝑆) − (𝐹‘(𝑆 − (𝑑 / 2)))))
12434recnd 7806 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑆 − (𝑑 / 2)) ∈ ℂ)
12530recnd 7806 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝑆 ∈ ℂ)
126124, 125abssubd 10977 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (abs‘((𝑆 − (𝑑 / 2)) − 𝑆)) = (abs‘(𝑆 − (𝑆 − (𝑑 / 2)))))
12733recnd 7806 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑑 / 2) ∈ ℂ)
128125, 127nncand 8090 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑆 − (𝑆 − (𝑑 / 2))) = (𝑑 / 2))
129128fveq2d 5425 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (abs‘(𝑆 − (𝑆 − (𝑑 / 2)))) = (abs‘(𝑑 / 2)))
13032rpge0d 9499 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 0 ≤ (𝑑 / 2))
13133, 130absidd 10951 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (abs‘(𝑑 / 2)) = (𝑑 / 2))
132126, 129, 1313eqtrd 2176 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (abs‘((𝑆 − (𝑑 / 2)) − 𝑆)) = (𝑑 / 2))
133132, 88eqbrtrd 3950 . . . . . . 7 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (abs‘((𝑆 − (𝑑 / 2)) − 𝑆)) < 𝑑)
134 fvoveq1 5797 . . . . . . . . . 10 (𝑧 = (𝑆 − (𝑑 / 2)) → (abs‘(𝑧𝑆)) = (abs‘((𝑆 − (𝑑 / 2)) − 𝑆)))
135134breq1d 3939 . . . . . . . . 9 (𝑧 = (𝑆 − (𝑑 / 2)) → ((abs‘(𝑧𝑆)) < 𝑑 ↔ (abs‘((𝑆 − (𝑑 / 2)) − 𝑆)) < 𝑑))
136135imbrov2fvoveq 5799 . . . . . . . 8 (𝑧 = (𝑆 − (𝑑 / 2)) → (((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)) ↔ ((abs‘((𝑆 − (𝑑 / 2)) − 𝑆)) < 𝑑 → (abs‘((𝐹‘(𝑆 − (𝑑 / 2))) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈))))
137 simprr 521 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))
1382adantr 274 . . . . . . . . 9 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝐴[,]𝐵) ⊆ 𝐷)
139138, 100sseldd 3098 . . . . . . . 8 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑆 − (𝑑 / 2)) ∈ 𝐷)
140136, 137, 139rspcdva 2794 . . . . . . 7 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → ((abs‘((𝑆 − (𝑑 / 2)) − 𝑆)) < 𝑑 → (abs‘((𝐹‘(𝑆 − (𝑑 / 2))) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))
141133, 140mpd 13 . . . . . 6 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (abs‘((𝐹‘(𝑆 − (𝑑 / 2))) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈))
142123, 141eqbrtrrd 3952 . . . . 5 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → ((𝐹𝑆) − (𝐹‘(𝑆 − (𝑑 / 2)))) < ((𝐹𝑆) − 𝑈))
14316adantr 274 . . . . . 6 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝑈 ∈ ℝ)
144143, 103, 104ltsub2d 8329 . . . . 5 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑈 < (𝐹‘(𝑆 − (𝑑 / 2))) ↔ ((𝐹𝑆) − (𝐹‘(𝑆 − (𝑑 / 2)))) < ((𝐹𝑆) − 𝑈)))
145142, 144mpbird 166 . . . 4 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → 𝑈 < (𝐹‘(𝑆 − (𝑑 / 2))))
146 fveq2 5421 . . . . . 6 (𝑤 = (𝑆 − (𝑑 / 2)) → (𝐹𝑤) = (𝐹‘(𝑆 − (𝑑 / 2))))
147146breq2d 3941 . . . . 5 (𝑤 = (𝑆 − (𝑑 / 2)) → (𝑈 < (𝐹𝑤) ↔ 𝑈 < (𝐹‘(𝑆 − (𝑑 / 2)))))
148147, 6elrab2 2843 . . . 4 ((𝑆 − (𝑑 / 2)) ∈ 𝑅 ↔ ((𝑆 − (𝑑 / 2)) ∈ (𝐴[,]𝐵) ∧ 𝑈 < (𝐹‘(𝑆 − (𝑑 / 2)))))
149100, 145, 148sylanbrc 413 . . 3 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → (𝑆 − (𝑑 / 2)) ∈ 𝑅)
150 breq1 3932 . . . 4 (𝑞 = (𝑆 − (𝑑 / 2)) → (𝑞 < 𝑆 ↔ (𝑆 − (𝑑 / 2)) < 𝑆))
151150rspcev 2789 . . 3 (((𝑆 − (𝑑 / 2)) ∈ 𝑅 ∧ (𝑆 − (𝑑 / 2)) < 𝑆) → ∃𝑞𝑅 𝑞 < 𝑆)
152149, 93, 151syl2anc 408 . 2 ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧ ∀𝑧𝐷 ((abs‘(𝑧𝑆)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑆))) < ((𝐹𝑆) − 𝑈)))) → ∃𝑞𝑅 𝑞 < 𝑆)
15323, 152rexlimddv 2554 1 (𝜑 → ∃𝑞𝑅 𝑞 < 𝑆)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 962   = wceq 1331   ∈ wcel 1480  ∀wral 2416  ∃wrex 2417  {crab 2420   ⊆ wss 3071   class class class wbr 3929  ‘cfv 5123  (class class class)co 5774  ℂcc 7630  ℝcr 7631  0cc0 7632   + caddc 7635  ℝ*cxr 7811   < clt 7812   ≤ cle 7813   − cmin 7945   / cdiv 8444  2c2 8783  ℝ+crp 9453  [,]cicc 9686  abscabs 10781  –cn→ccncf 12740 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7723  ax-resscn 7724  ax-1cn 7725  ax-1re 7726  ax-icn 7727  ax-addcl 7728  ax-addrcl 7729  ax-mulcl 7730  ax-mulrcl 7731  ax-addcom 7732  ax-mulcom 7733  ax-addass 7734  ax-mulass 7735  ax-distr 7736  ax-i2m1 7737  ax-0lt1 7738  ax-1rid 7739  ax-0id 7740  ax-rnegex 7741  ax-precex 7742  ax-cnre 7743  ax-pre-ltirr 7744  ax-pre-ltwlin 7745  ax-pre-lttrn 7746  ax-pre-apti 7747  ax-pre-ltadd 7748  ax-pre-mulgt0 7749  ax-pre-mulext 7750  ax-arch 7751  ax-caucvg 7752 This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-map 6544  df-pnf 7814  df-mnf 7815  df-xr 7816  df-ltxr 7817  df-le 7818  df-sub 7947  df-neg 7948  df-reap 8349  df-ap 8356  df-div 8445  df-inn 8733  df-2 8791  df-3 8792  df-4 8793  df-n0 8990  df-z 9067  df-uz 9339  df-rp 9454  df-icc 9690  df-seqfrec 10231  df-exp 10305  df-cj 10626  df-re 10627  df-im 10628  df-rsqrt 10782  df-abs 10783  df-cncf 12741 This theorem is referenced by:  ivthinclemur  12800
 Copyright terms: Public domain W3C validator