MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pntlem3 Structured version   Visualization version   GIF version

Theorem pntlem3 25015
Description: Lemma for pnt 25020. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 8-Apr-2016.) (Proof shortened by AV, 27-Sep-2020.)
Hypotheses
Ref Expression
pntlem3.r 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
pntlem3.a (𝜑𝐴 ∈ ℝ+)
pntlem3.A (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
pntlem3.1 𝑇 = {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡}
pntlem3.2 (𝜑𝐶 ∈ ℝ+)
pntlem3.3 ((𝜑𝑢𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇)
Assertion
Ref Expression
pntlem3 (𝜑 → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1)
Distinct variable groups:   𝑥,𝑡,𝑦,𝑧,𝐴   𝑢,𝑎,𝑥,𝑦,𝑧   𝑢,𝐶   𝑢,𝑡,𝑅,𝑥,𝑦,𝑧   𝑡,𝑎   𝑢,𝑇,𝑥   𝜑,𝑡,𝑥,𝑦,𝑢,𝑧
Allowed substitution hints:   𝜑(𝑎)   𝐴(𝑢,𝑎)   𝐶(𝑥,𝑦,𝑧,𝑡,𝑎)   𝑅(𝑎)   𝑇(𝑦,𝑧,𝑡,𝑎)

Proof of Theorem pntlem3
Dummy variables 𝑠 𝑤 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rpssre 11675 . . . 4 + ⊆ ℝ
2 eqid 2609 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
32subcn 22408 . . . . . . . . . . . 12 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
43a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
5 ssid 3586 . . . . . . . . . . . . 13 ℂ ⊆ ℂ
6 cncfmptid 22454 . . . . . . . . . . . . 13 ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑝 ∈ ℂ ↦ 𝑝) ∈ (ℂ–cn→ℂ))
75, 5, 6mp2an 703 . . . . . . . . . . . 12 (𝑝 ∈ ℂ ↦ 𝑝) ∈ (ℂ–cn→ℂ)
87a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ 𝑝) ∈ (ℂ–cn→ℂ))
9 pntlem3.2 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℝ+)
109adantr 479 . . . . . . . . . . . . . 14 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → 𝐶 ∈ ℝ+)
1110rpcnd 11706 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → 𝐶 ∈ ℂ)
125a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → ℂ ⊆ ℂ)
13 cncfmptc 22453 . . . . . . . . . . . . 13 ((𝐶 ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑝 ∈ ℂ ↦ 𝐶) ∈ (ℂ–cn→ℂ))
1411, 12, 12, 13syl3anc 1317 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ 𝐶) ∈ (ℂ–cn→ℂ))
15 3nn0 11157 . . . . . . . . . . . . . 14 3 ∈ ℕ0
162expcn 22414 . . . . . . . . . . . . . 14 (3 ∈ ℕ0 → (𝑝 ∈ ℂ ↦ (𝑝↑3)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
1715, 16mp1i 13 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝑝↑3)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
182cncfcn1 22452 . . . . . . . . . . . . 13 (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
1917, 18syl6eleqr 2698 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝑝↑3)) ∈ (ℂ–cn→ℂ))
2014, 19mulcncf 22940 . . . . . . . . . . 11 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝐶 · (𝑝↑3))) ∈ (ℂ–cn→ℂ))
212, 4, 8, 20cncfmpt2f 22456 . . . . . . . . . 10 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) ∈ (ℂ–cn→ℂ))
22 pntlem3.1 . . . . . . . . . . . . . . 15 𝑇 = {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡}
23 ssrab2 3649 . . . . . . . . . . . . . . 15 {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡} ⊆ (0[,]𝐴)
2422, 23eqsstri 3597 . . . . . . . . . . . . . 14 𝑇 ⊆ (0[,]𝐴)
25 0re 9896 . . . . . . . . . . . . . . 15 0 ∈ ℝ
26 pntlem3.a . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℝ+)
2726rpred 11704 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℝ)
28 iccssre 12082 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0[,]𝐴) ⊆ ℝ)
2925, 27, 28sylancr 693 . . . . . . . . . . . . . 14 (𝜑 → (0[,]𝐴) ⊆ ℝ)
3024, 29syl5ss 3578 . . . . . . . . . . . . 13 (𝜑𝑇 ⊆ ℝ)
31 0xr 9942 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ*
3231a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℝ*)
3326rpxrd 11705 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℝ*)
3426rpge0d 11708 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 𝐴)
35 ubicc2 12116 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ*𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ∈ (0[,]𝐴))
3632, 33, 34, 35syl3anc 1317 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ (0[,]𝐴))
37 1rp 11668 . . . . . . . . . . . . . . . 16 1 ∈ ℝ+
38 1re 9895 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ
39 elicopnf 12096 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℝ → (𝑧 ∈ (1[,)+∞) ↔ (𝑧 ∈ ℝ ∧ 1 ≤ 𝑧)))
4038, 39mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑧 ∈ (1[,)+∞) ↔ (𝑧 ∈ ℝ ∧ 1 ≤ 𝑧)))
4140simprbda 650 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (1[,)+∞)) → 𝑧 ∈ ℝ)
42 0red 9897 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (1[,)+∞)) → 0 ∈ ℝ)
4338a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (1[,)+∞)) → 1 ∈ ℝ)
44 0lt1 10399 . . . . . . . . . . . . . . . . . . . . 21 0 < 1
4544a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (1[,)+∞)) → 0 < 1)
4640simplbda 651 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (1[,)+∞)) → 1 ≤ 𝑧)
4742, 43, 41, 45, 46ltletrd 10048 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (1[,)+∞)) → 0 < 𝑧)
4841, 47elrpd 11701 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (1[,)+∞)) → 𝑧 ∈ ℝ+)
49 pntlem3.A . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
5049adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (1[,)+∞)) → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
51 fveq2 6088 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → (𝑅𝑥) = (𝑅𝑧))
52 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧𝑥 = 𝑧)
5351, 52oveq12d 6545 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → ((𝑅𝑥) / 𝑥) = ((𝑅𝑧) / 𝑧))
5453fveq2d 6092 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (abs‘((𝑅𝑥) / 𝑥)) = (abs‘((𝑅𝑧) / 𝑧)))
5554breq1d 4587 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → ((abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴 ↔ (abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴))
5655rspcv 3277 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ℝ+ → (∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴 → (abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴))
5748, 50, 56sylc 62 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (1[,)+∞)) → (abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴)
5857ralrimiva 2948 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴)
59 oveq1 6534 . . . . . . . . . . . . . . . . . 18 (𝑦 = 1 → (𝑦[,)+∞) = (1[,)+∞))
6059raleqdv 3120 . . . . . . . . . . . . . . . . 17 (𝑦 = 1 → (∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴 ↔ ∀𝑧 ∈ (1[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴))
6160rspcev 3281 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ+ ∧ ∀𝑧 ∈ (1[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴)
6237, 58, 61sylancr 693 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴)
63 breq2 4581 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝐴 → ((abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ↔ (abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴))
6463rexralbidv 3039 . . . . . . . . . . . . . . . 16 (𝑡 = 𝐴 → (∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ↔ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴))
6564, 22elrab2 3332 . . . . . . . . . . . . . . 15 (𝐴𝑇 ↔ (𝐴 ∈ (0[,]𝐴) ∧ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴))
6636, 62, 65sylanbrc 694 . . . . . . . . . . . . . 14 (𝜑𝐴𝑇)
67 ne0i 3879 . . . . . . . . . . . . . 14 (𝐴𝑇𝑇 ≠ ∅)
6866, 67syl 17 . . . . . . . . . . . . 13 (𝜑𝑇 ≠ ∅)
69 elicc2 12065 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑡 ∈ (0[,]𝐴) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡𝐴)))
7025, 27, 69sylancr 693 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑡 ∈ (0[,]𝐴) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡𝐴)))
7170biimpa 499 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0[,]𝐴)) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡𝐴))
7271simp2d 1066 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0[,]𝐴)) → 0 ≤ 𝑡)
7372a1d 25 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0[,]𝐴)) → (∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡))
7473ralrimiva 2948 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡))
7522raleqi 3118 . . . . . . . . . . . . . . . 16 (∀𝑤𝑇 0 ≤ 𝑤 ↔ ∀𝑤 ∈ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡}0 ≤ 𝑤)
76 breq2 4581 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑡 → (0 ≤ 𝑤 ↔ 0 ≤ 𝑡))
7776ralrab2 3338 . . . . . . . . . . . . . . . 16 (∀𝑤 ∈ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡}0 ≤ 𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡))
7875, 77bitri 262 . . . . . . . . . . . . . . 15 (∀𝑤𝑇 0 ≤ 𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡))
7974, 78sylibr 222 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑤𝑇 0 ≤ 𝑤)
80 breq1 4580 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → (𝑥𝑤 ↔ 0 ≤ 𝑤))
8180ralbidv 2968 . . . . . . . . . . . . . . 15 (𝑥 = 0 → (∀𝑤𝑇 𝑥𝑤 ↔ ∀𝑤𝑇 0 ≤ 𝑤))
8281rspcev 3281 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ ∀𝑤𝑇 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤)
8325, 79, 82sylancr 693 . . . . . . . . . . . . 13 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤)
84 infrecl 10852 . . . . . . . . . . . . 13 ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤) → inf(𝑇, ℝ, < ) ∈ ℝ)
8530, 68, 83, 84syl3anc 1317 . . . . . . . . . . . 12 (𝜑 → inf(𝑇, ℝ, < ) ∈ ℝ)
8685recnd 9924 . . . . . . . . . . 11 (𝜑 → inf(𝑇, ℝ, < ) ∈ ℂ)
8786adantr 479 . . . . . . . . . 10 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → inf(𝑇, ℝ, < ) ∈ ℂ)
88 elrp 11666 . . . . . . . . . . . . . 14 (inf(𝑇, ℝ, < ) ∈ ℝ+ ↔ (inf(𝑇, ℝ, < ) ∈ ℝ ∧ 0 < inf(𝑇, ℝ, < )))
8988biimpri 216 . . . . . . . . . . . . 13 ((inf(𝑇, ℝ, < ) ∈ ℝ ∧ 0 < inf(𝑇, ℝ, < )) → inf(𝑇, ℝ, < ) ∈ ℝ+)
9085, 89sylan 486 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → inf(𝑇, ℝ, < ) ∈ ℝ+)
91 3z 11243 . . . . . . . . . . . 12 3 ∈ ℤ
92 rpexpcl 12696 . . . . . . . . . . . 12 ((inf(𝑇, ℝ, < ) ∈ ℝ+ ∧ 3 ∈ ℤ) → (inf(𝑇, ℝ, < )↑3) ∈ ℝ+)
9390, 91, 92sylancl 692 . . . . . . . . . . 11 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (inf(𝑇, ℝ, < )↑3) ∈ ℝ+)
9410, 93rpmulcld 11720 . . . . . . . . . 10 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈ ℝ+)
95 cncfi 22436 . . . . . . . . . 10 (((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) ∈ (ℂ–cn→ℂ) ∧ inf(𝑇, ℝ, < ) ∈ ℂ ∧ (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈ ℝ+) → ∃𝑠 ∈ ℝ+𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))))
9621, 87, 94, 95syl3anc 1317 . . . . . . . . 9 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → ∃𝑠 ∈ ℝ+𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))))
9785ad2antrr 757 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → inf(𝑇, ℝ, < ) ∈ ℝ)
98 rphalfcl 11690 . . . . . . . . . . . . . 14 (𝑠 ∈ ℝ+ → (𝑠 / 2) ∈ ℝ+)
9998adantl 480 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (𝑠 / 2) ∈ ℝ+)
10097, 99ltaddrpd 11737 . . . . . . . . . . . 12 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → inf(𝑇, ℝ, < ) < (inf(𝑇, ℝ, < ) + (𝑠 / 2)))
10199rpred 11704 . . . . . . . . . . . . . 14 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (𝑠 / 2) ∈ ℝ)
10297, 101readdcld 9925 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ∈ ℝ)
10397, 102ltnled 10035 . . . . . . . . . . . 12 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (inf(𝑇, ℝ, < ) < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ↔ ¬ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < )))
104100, 103mpbid 220 . . . . . . . . . . 11 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → ¬ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < ))
105 ax-resscn 9849 . . . . . . . . . . . . . . 15 ℝ ⊆ ℂ
10630, 105syl6ss 3579 . . . . . . . . . . . . . 14 (𝜑𝑇 ⊆ ℂ)
107106ad2antrr 757 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → 𝑇 ⊆ ℂ)
108 ssralv 3628 . . . . . . . . . . . . 13 (𝑇 ⊆ ℂ → (∀𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) → ∀𝑢𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)))))
109107, 108syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (∀𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) → ∀𝑢𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)))))
11030ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → 𝑇 ⊆ ℝ)
111110sselda 3567 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 𝑢 ∈ ℝ)
112102adantr 479 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ∈ ℝ)
113111, 112ltnled 10035 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ↔ ¬ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
11485ad3antrrr 761 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → inf(𝑇, ℝ, < ) ∈ ℝ)
115101adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑠 / 2) ∈ ℝ)
116114, 115resubcld 10309 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) ∈ ℝ)
11797, 99ltsubrpd 11736 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) < inf(𝑇, ℝ, < ))
118117adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) < inf(𝑇, ℝ, < ))
11930ad3antrrr 761 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 𝑇 ⊆ ℝ)
12083ad3antrrr 761 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤)
121 simpr 475 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 𝑢𝑇)
122 infrelb 10855 . . . . . . . . . . . . . . . . . . . . 21 ((𝑇 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤𝑢𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑢)
123119, 120, 121, 122syl3anc 1317 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑢)
124116, 114, 111, 118, 123ltletrd 10048 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) < 𝑢)
125111, 114, 115absdifltd 13966 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) ↔ ((inf(𝑇, ℝ, < ) − (𝑠 / 2)) < 𝑢𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)))))
126125biimprd 236 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (((inf(𝑇, ℝ, < ) − (𝑠 / 2)) < 𝑢𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2))) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2)))
127124, 126mpand 706 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2)))
128 rphalflt 11692 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ℝ+ → (𝑠 / 2) < 𝑠)
129128ad2antlr 758 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑠 / 2) < 𝑠)
130111, 114resubcld 10309 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 − inf(𝑇, ℝ, < )) ∈ ℝ)
131130recnd 9924 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 − inf(𝑇, ℝ, < )) ∈ ℂ)
132131abscld 13969 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) ∈ ℝ)
133 rpre 11671 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ℝ+𝑠 ∈ ℝ)
134133ad2antlr 758 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 𝑠 ∈ ℝ)
135 lttr 9965 . . . . . . . . . . . . . . . . . . . 20 (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) ∈ ℝ ∧ (𝑠 / 2) ∈ ℝ ∧ 𝑠 ∈ ℝ) → (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) ∧ (𝑠 / 2) < 𝑠) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠))
136132, 115, 134, 135syl3anc 1317 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) ∧ (𝑠 / 2) < 𝑠) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠))
137129, 136mpan2d 705 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠))
138127, 137syld 45 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠))
139113, 138sylbird 248 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (¬ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢 → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠))
140139con1d 137 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (¬ (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
141111recnd 9924 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 𝑢 ∈ ℂ)
142 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑢𝑝 = 𝑢)
143 oveq1 6534 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑢 → (𝑝↑3) = (𝑢↑3))
144143oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑢 → (𝐶 · (𝑝↑3)) = (𝐶 · (𝑢↑3)))
145142, 144oveq12d 6545 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = 𝑢 → (𝑝 − (𝐶 · (𝑝↑3))) = (𝑢 − (𝐶 · (𝑢↑3))))
146 eqid 2609 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) = (𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))
147 ovex 6555 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 − (𝐶 · (𝑢↑3))) ∈ V
148145, 146, 147fvmpt 6176 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ ℂ → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) = (𝑢 − (𝐶 · (𝑢↑3))))
149141, 148syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) = (𝑢 − (𝐶 · (𝑢↑3))))
15087ad2antrr 757 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → inf(𝑇, ℝ, < ) ∈ ℂ)
151 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = inf(𝑇, ℝ, < ) → 𝑝 = inf(𝑇, ℝ, < ))
152 oveq1 6534 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = inf(𝑇, ℝ, < ) → (𝑝↑3) = (inf(𝑇, ℝ, < )↑3))
153152oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = inf(𝑇, ℝ, < ) → (𝐶 · (𝑝↑3)) = (𝐶 · (inf(𝑇, ℝ, < )↑3)))
154151, 153oveq12d 6545 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = inf(𝑇, ℝ, < ) → (𝑝 − (𝐶 · (𝑝↑3))) = (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))
155 ovex 6555 . . . . . . . . . . . . . . . . . . . . 21 (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) ∈ V
156154, 146, 155fvmpt 6176 . . . . . . . . . . . . . . . . . . . 20 (inf(𝑇, ℝ, < ) ∈ ℂ → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )) = (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))
157150, 156syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )) = (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))
158149, 157oveq12d 6545 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < ))) = ((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3)))))
159158fveq2d 6092 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) = (abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))))
160159breq1d 4587 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) ↔ (abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))))
1619rpred 11704 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐶 ∈ ℝ)
162161ad3antrrr 761 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 𝐶 ∈ ℝ)
163 reexpcl 12694 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ∈ ℝ ∧ 3 ∈ ℕ0) → (𝑢↑3) ∈ ℝ)
164111, 15, 163sylancl 692 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢↑3) ∈ ℝ)
165162, 164remulcld 9926 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝐶 · (𝑢↑3)) ∈ ℝ)
166111, 165resubcld 10309 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ ℝ)
16715a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 3 ∈ ℕ0)
168114, 167reexpcld 12842 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (inf(𝑇, ℝ, < )↑3) ∈ ℝ)
169162, 168remulcld 9926 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈ ℝ)
170114, 169resubcld 10309 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) ∈ ℝ)
171166, 170, 169absdifltd 13966 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) ↔ (((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) < (𝑢 − (𝐶 · (𝑢↑3))) ∧ (𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))))))
172169recnd 9924 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈ ℂ)
173150, 172npcand 10247 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))) = inf(𝑇, ℝ, < ))
174173breq2d 4589 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))) ↔ (𝑢 − (𝐶 · (𝑢↑3))) < inf(𝑇, ℝ, < )))
175 pntlem3.3 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇)
176175ad4ant14 1284 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇)
177 infrelb 10855 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑇 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤 ∧ (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ (𝑢 − (𝐶 · (𝑢↑3))))
178119, 120, 176, 177syl3anc 1317 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → inf(𝑇, ℝ, < ) ≤ (𝑢 − (𝐶 · (𝑢↑3))))
179114, 166, 178lensymd 10039 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ¬ (𝑢 − (𝐶 · (𝑢↑3))) < inf(𝑇, ℝ, < ))
180179pm2.21d 116 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((𝑢 − (𝐶 · (𝑢↑3))) < inf(𝑇, ℝ, < ) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
181174, 180sylbid 228 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
182181adantld 481 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) < (𝑢 − (𝐶 · (𝑢↑3))) ∧ (𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3)))) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
183171, 182sylbid 228 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
184160, 183sylbid 228 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
185140, 184jad 172 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
186185ralimdva 2944 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (∀𝑢𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) → ∀𝑢𝑇 (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
18768ad2antrr 757 . . . . . . . . . . . . . 14 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → 𝑇 ≠ ∅)
18883ad2antrr 757 . . . . . . . . . . . . . 14 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤)
189 infregelb 10854 . . . . . . . . . . . . . 14 (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤) ∧ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ∈ ℝ) → ((inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑢𝑇 (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
190110, 187, 188, 102, 189syl31anc 1320 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → ((inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑢𝑇 (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
191186, 190sylibrd 247 . . . . . . . . . . . 12 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (∀𝑢𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < )))
192109, 191syld 45 . . . . . . . . . . 11 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (∀𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < )))
193104, 192mtod 187 . . . . . . . . . 10 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → ¬ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))))
194193nrexdv 2983 . . . . . . . . 9 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → ¬ ∃𝑠 ∈ ℝ+𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))))
19596, 194pm2.65da 597 . . . . . . . 8 (𝜑 → ¬ 0 < inf(𝑇, ℝ, < ))
196195adantr 479 . . . . . . 7 ((𝜑𝑠 ∈ ℝ+) → ¬ 0 < inf(𝑇, ℝ, < ))
19730adantr 479 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ+) → 𝑇 ⊆ ℝ)
19868adantr 479 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ+) → 𝑇 ≠ ∅)
19983adantr 479 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ+) → ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤)
200133adantl 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ+) → 𝑠 ∈ ℝ)
201 infregelb 10854 . . . . . . . . . 10 (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤) ∧ 𝑠 ∈ ℝ) → (𝑠 ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑤𝑇 𝑠𝑤))
202197, 198, 199, 200, 201syl31anc 1320 . . . . . . . . 9 ((𝜑𝑠 ∈ ℝ+) → (𝑠 ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑤𝑇 𝑠𝑤))
20322raleqi 3118 . . . . . . . . . 10 (∀𝑤𝑇 𝑠𝑤 ↔ ∀𝑤 ∈ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡}𝑠𝑤)
204 breq2 4581 . . . . . . . . . . 11 (𝑤 = 𝑡 → (𝑠𝑤𝑠𝑡))
205204ralrab2 3338 . . . . . . . . . 10 (∀𝑤 ∈ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡}𝑠𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡𝑠𝑡))
206203, 205bitri 262 . . . . . . . . 9 (∀𝑤𝑇 𝑠𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡𝑠𝑡))
207202, 206syl6bb 274 . . . . . . . 8 ((𝜑𝑠 ∈ ℝ+) → (𝑠 ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡𝑠𝑡)))
208 rpgt0 11676 . . . . . . . . . 10 (𝑠 ∈ ℝ+ → 0 < 𝑠)
209208adantl 480 . . . . . . . . 9 ((𝜑𝑠 ∈ ℝ+) → 0 < 𝑠)
210 0red 9897 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ+) → 0 ∈ ℝ)
21185adantr 479 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ+) → inf(𝑇, ℝ, < ) ∈ ℝ)
212 ltletr 9980 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ inf(𝑇, ℝ, < ) ∈ ℝ) → ((0 < 𝑠𝑠 ≤ inf(𝑇, ℝ, < )) → 0 < inf(𝑇, ℝ, < )))
213210, 200, 211, 212syl3anc 1317 . . . . . . . . 9 ((𝜑𝑠 ∈ ℝ+) → ((0 < 𝑠𝑠 ≤ inf(𝑇, ℝ, < )) → 0 < inf(𝑇, ℝ, < )))
214209, 213mpand 706 . . . . . . . 8 ((𝜑𝑠 ∈ ℝ+) → (𝑠 ≤ inf(𝑇, ℝ, < ) → 0 < inf(𝑇, ℝ, < )))
215207, 214sylbird 248 . . . . . . 7 ((𝜑𝑠 ∈ ℝ+) → (∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡𝑠𝑡) → 0 < inf(𝑇, ℝ, < )))
216196, 215mtod 187 . . . . . 6 ((𝜑𝑠 ∈ ℝ+) → ¬ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡𝑠𝑡))
217 rexanali 2980 . . . . . 6 (∃𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠𝑡) ↔ ¬ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡𝑠𝑡))
218216, 217sylibr 222 . . . . 5 ((𝜑𝑠 ∈ ℝ+) → ∃𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠𝑡))
219 fveq2 6088 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → (𝑅𝑧) = (𝑅𝑥))
220 id 22 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥𝑧 = 𝑥)
221219, 220oveq12d 6545 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → ((𝑅𝑧) / 𝑧) = ((𝑅𝑥) / 𝑥))
222221fveq2d 6092 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (abs‘((𝑅𝑧) / 𝑧)) = (abs‘((𝑅𝑥) / 𝑥)))
223222breq1d 4587 . . . . . . . . . . . 12 (𝑧 = 𝑥 → ((abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ↔ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡))
224223cbvralv 3146 . . . . . . . . . . 11 (∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ↔ ∀𝑥 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡)
225 rpre 11671 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
226225ad2antll 760 . . . . . . . . . . . . . . . 16 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑥 ∈ ℝ)
227 simprl 789 . . . . . . . . . . . . . . . 16 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑦𝑥)
228 simplr 787 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
229228rpred 11704 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑦 ∈ ℝ)
230 elicopnf 12096 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ → (𝑥 ∈ (𝑦[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑦𝑥)))
231229, 230syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (𝑥 ∈ (𝑦[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑦𝑥)))
232226, 227, 231mpbir2and 958 . . . . . . . . . . . . . . 15 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑥 ∈ (𝑦[,)+∞))
233 pntlem3.r . . . . . . . . . . . . . . . . . . . . . 22 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
234233pntrval 24968 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ+ → (𝑅𝑥) = ((ψ‘𝑥) − 𝑥))
235234ad2antll 760 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (𝑅𝑥) = ((ψ‘𝑥) − 𝑥))
236235oveq1d 6542 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ((𝑅𝑥) / 𝑥) = (((ψ‘𝑥) − 𝑥) / 𝑥))
237 chpcl 24567 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
238226, 237syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (ψ‘𝑥) ∈ ℝ)
239238recnd 9924 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (ψ‘𝑥) ∈ ℂ)
240 rpcn 11673 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
241240ad2antll 760 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑥 ∈ ℂ)
242 rpne0 11680 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ+𝑥 ≠ 0)
243242ad2antll 760 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑥 ≠ 0)
244239, 241, 241, 243divsubdird 10689 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (((ψ‘𝑥) − 𝑥) / 𝑥) = (((ψ‘𝑥) / 𝑥) − (𝑥 / 𝑥)))
245241, 243dividd 10648 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (𝑥 / 𝑥) = 1)
246245oveq2d 6543 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (((ψ‘𝑥) / 𝑥) − (𝑥 / 𝑥)) = (((ψ‘𝑥) / 𝑥) − 1))
247236, 244, 2463eqtrrd 2648 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (((ψ‘𝑥) / 𝑥) − 1) = ((𝑅𝑥) / 𝑥))
248247fveq2d 6092 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) = (abs‘((𝑅𝑥) / 𝑥)))
249248breq1d 4587 . . . . . . . . . . . . . . . 16 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡 ↔ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡))
250 simprr 791 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) → ¬ 𝑠𝑡)
251250ad2antrr 757 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ¬ 𝑠𝑡)
25229ad2antrr 757 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) → (0[,]𝐴) ⊆ ℝ)
253252ad2antrr 757 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (0[,]𝐴) ⊆ ℝ)
254 simplrl 795 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) → 𝑡 ∈ (0[,]𝐴))
255254adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑡 ∈ (0[,]𝐴))
256253, 255sseldd 3568 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑡 ∈ ℝ)
257 simp-4r 802 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑠 ∈ ℝ+)
258257rpred 11704 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑠 ∈ ℝ)
259256, 258ltnled 10035 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (𝑡 < 𝑠 ↔ ¬ 𝑠𝑡))
260251, 259mpbird 245 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑡 < 𝑠)
261225, 237syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ+ → (ψ‘𝑥) ∈ ℝ)
262 rerpdivcl 11693 . . . . . . . . . . . . . . . . . . . . . . 23 (((ψ‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
263261, 262mpancom 699 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ+ → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
264263ad2antll 760 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
265 resubcl 10196 . . . . . . . . . . . . . . . . . . . . 21 ((((ψ‘𝑥) / 𝑥) ∈ ℝ ∧ 1 ∈ ℝ) → (((ψ‘𝑥) / 𝑥) − 1) ∈ ℝ)
266264, 38, 265sylancl 692 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (((ψ‘𝑥) / 𝑥) − 1) ∈ ℝ)
267266recnd 9924 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (((ψ‘𝑥) / 𝑥) − 1) ∈ ℂ)
268267abscld 13969 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) ∈ ℝ)
269 lelttr 9979 . . . . . . . . . . . . . . . . . 18 (((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ∈ ℝ ∧ 𝑡 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡𝑡 < 𝑠) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
270268, 256, 258, 269syl3anc 1317 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡𝑡 < 𝑠) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
271260, 270mpan2d 705 . . . . . . . . . . . . . . . 16 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
272249, 271sylbird 248 . . . . . . . . . . . . . . 15 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ((abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
273232, 272embantd 56 . . . . . . . . . . . . . 14 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ((𝑥 ∈ (𝑦[,)+∞) → (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
274273exp32 628 . . . . . . . . . . . . 13 ((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) → (𝑦𝑥 → (𝑥 ∈ ℝ+ → ((𝑥 ∈ (𝑦[,)+∞) → (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))))
275274com24 92 . . . . . . . . . . . 12 ((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) → ((𝑥 ∈ (𝑦[,)+∞) → (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡) → (𝑥 ∈ ℝ+ → (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))))
276275ralimdv2 2943 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡 → ∀𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
277224, 276syl5bi 230 . . . . . . . . . 10 ((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) → (∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → ∀𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
278277reximdva 2999 . . . . . . . . 9 (((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) → (∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → ∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
279278anassrs 677 . . . . . . . 8 ((((𝜑𝑠 ∈ ℝ+) ∧ 𝑡 ∈ (0[,]𝐴)) ∧ ¬ 𝑠𝑡) → (∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → ∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
280279impancom 454 . . . . . . 7 ((((𝜑𝑠 ∈ ℝ+) ∧ 𝑡 ∈ (0[,]𝐴)) ∧ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡) → (¬ 𝑠𝑡 → ∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
281280expimpd 626 . . . . . 6 (((𝜑𝑠 ∈ ℝ+) ∧ 𝑡 ∈ (0[,]𝐴)) → ((∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠𝑡) → ∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
282281rexlimdva 3012 . . . . 5 ((𝜑𝑠 ∈ ℝ+) → (∃𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠𝑡) → ∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
283218, 282mpd 15 . . . 4 ((𝜑𝑠 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
284 ssrexv 3629 . . . 4 (ℝ+ ⊆ ℝ → (∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
2851, 283, 284mpsyl 65 . . 3 ((𝜑𝑠 ∈ ℝ+) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
286285ralrimiva 2948 . 2 (𝜑 → ∀𝑠 ∈ ℝ+𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
287263recnd 9924 . . . . 5 (𝑥 ∈ ℝ+ → ((ψ‘𝑥) / 𝑥) ∈ ℂ)
288287rgen 2905 . . . 4 𝑥 ∈ ℝ+ ((ψ‘𝑥) / 𝑥) ∈ ℂ
289288a1i 11 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+ ((ψ‘𝑥) / 𝑥) ∈ ℂ)
2901a1i 11 . . 3 (𝜑 → ℝ+ ⊆ ℝ)
291 1cnd 9912 . . 3 (𝜑 → 1 ∈ ℂ)
292289, 290, 291rlim2 14021 . 2 (𝜑 → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1 ↔ ∀𝑠 ∈ ℝ+𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
293286, 292mpbird 245 1 (𝜑 → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896  {crab 2899  wss 3539  c0 3873   class class class wbr 4577  cmpt 4637  cfv 5790  (class class class)co 6527  infcinf 8207  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797  +∞cpnf 9927  *cxr 9929   < clt 9930  cle 9931  cmin 10117   / cdiv 10533  2c2 10917  3c3 10918  0cn0 11139  cz 11210  +crp 11664  [,)cico 12004  [,]cicc 12005  cexp 12677  abscabs 13768  𝑟 crli 14010  TopOpenctopn 15851  fldccnfld 19513   Cn ccn 20780   ×t ctx 21115  cnccncf 22418  ψcchp 24536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871  ax-mulf 9872
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6772  df-om 6935  df-1st 7036  df-2nd 7037  df-supp 7160  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fsupp 8136  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-5 10929  df-6 10930  df-7 10931  df-8 10932  df-9 10933  df-n0 11140  df-z 11211  df-dec 11326  df-uz 11520  df-q 11621  df-rp 11665  df-xneg 11778  df-xadd 11779  df-xmul 11780  df-ioo 12006  df-ioc 12007  df-ico 12008  df-icc 12009  df-fz 12153  df-fzo 12290  df-fl 12410  df-mod 12486  df-seq 12619  df-exp 12678  df-fac 12878  df-bc 12907  df-hash 12935  df-shft 13601  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-limsup 13996  df-clim 14013  df-rlim 14014  df-sum 14211  df-ef 14583  df-sin 14585  df-cos 14586  df-pi 14588  df-dvds 14768  df-gcd 15001  df-prm 15170  df-pc 15326  df-struct 15643  df-ndx 15644  df-slot 15645  df-base 15646  df-sets 15647  df-ress 15648  df-plusg 15727  df-mulr 15728  df-starv 15729  df-sca 15730  df-vsca 15731  df-ip 15732  df-tset 15733  df-ple 15734  df-ds 15737  df-unif 15738  df-hom 15739  df-cco 15740  df-rest 15852  df-topn 15853  df-0g 15871  df-gsum 15872  df-topgen 15873  df-pt 15874  df-prds 15877  df-xrs 15931  df-qtop 15936  df-imas 15937  df-xps 15939  df-mre 16015  df-mrc 16016  df-acs 16018  df-mgm 17011  df-sgrp 17053  df-mnd 17064  df-submnd 17105  df-mulg 17310  df-cntz 17519  df-cmn 17964  df-psmet 19505  df-xmet 19506  df-met 19507  df-bl 19508  df-mopn 19509  df-fbas 19510  df-fg 19511  df-cnfld 19514  df-top 20463  df-bases 20464  df-topon 20465  df-topsp 20466  df-cld 20575  df-ntr 20576  df-cls 20577  df-nei 20654  df-lp 20692  df-perf 20693  df-cn 20783  df-cnp 20784  df-haus 20871  df-tx 21117  df-hmeo 21310  df-fil 21402  df-fm 21494  df-flim 21495  df-flf 21496  df-xms 21876  df-ms 21877  df-tms 21878  df-cncf 22420  df-limc 23353  df-dv 23354  df-log 24024  df-vma 24541  df-chp 24542
This theorem is referenced by:  pntleml  25017
  Copyright terms: Public domain W3C validator