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

Theorem pntlem3 25098
Description: Lemma for pnt 25103. 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 11719 . . . 4 + ⊆ ℝ
2 eqid 2610 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
32subcn 22477 . . . . . . . . . . . 12 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
43a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
5 ssid 3587 . . . . . . . . . . . . 13 ℂ ⊆ ℂ
6 cncfmptid 22523 . . . . . . . . . . . . 13 ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑝 ∈ ℂ ↦ 𝑝) ∈ (ℂ–cn→ℂ))
75, 5, 6mp2an 704 . . . . . . . . . . . 12 (𝑝 ∈ ℂ ↦ 𝑝) ∈ (ℂ–cn→ℂ)
87a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ 𝑝) ∈ (ℂ–cn→ℂ))
9 pntlem3.2 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℝ+)
109adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → 𝐶 ∈ ℝ+)
1110rpcnd 11750 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → 𝐶 ∈ ℂ)
125a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → ℂ ⊆ ℂ)
13 cncfmptc 22522 . . . . . . . . . . . . 13 ((𝐶 ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑝 ∈ ℂ ↦ 𝐶) ∈ (ℂ–cn→ℂ))
1411, 12, 12, 13syl3anc 1318 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ 𝐶) ∈ (ℂ–cn→ℂ))
15 3nn0 11187 . . . . . . . . . . . . . 14 3 ∈ ℕ0
162expcn 22483 . . . . . . . . . . . . . 14 (3 ∈ ℕ0 → (𝑝 ∈ ℂ ↦ (𝑝↑3)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
1715, 16mp1i 13 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝑝↑3)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
182cncfcn1 22521 . . . . . . . . . . . . 13 (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
1917, 18syl6eleqr 2699 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝑝↑3)) ∈ (ℂ–cn→ℂ))
2014, 19mulcncf 23023 . . . . . . . . . . 11 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝐶 · (𝑝↑3))) ∈ (ℂ–cn→ℂ))
212, 4, 8, 20cncfmpt2f 22525 . . . . . . . . . 10 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) ∈ (ℂ–cn→ℂ))
22 pntlem3.1 . . . . . . . . . . . . . . 15 𝑇 = {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡}
23 ssrab2 3650 . . . . . . . . . . . . . . 15 {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡} ⊆ (0[,]𝐴)
2422, 23eqsstri 3598 . . . . . . . . . . . . . 14 𝑇 ⊆ (0[,]𝐴)
25 0re 9919 . . . . . . . . . . . . . . 15 0 ∈ ℝ
26 pntlem3.a . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℝ+)
2726rpred 11748 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℝ)
28 iccssre 12126 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0[,]𝐴) ⊆ ℝ)
2925, 27, 28sylancr 694 . . . . . . . . . . . . . 14 (𝜑 → (0[,]𝐴) ⊆ ℝ)
3024, 29syl5ss 3579 . . . . . . . . . . . . 13 (𝜑𝑇 ⊆ ℝ)
31 0xr 9965 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ*
3231a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℝ*)
3326rpxrd 11749 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℝ*)
3426rpge0d 11752 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 𝐴)
35 ubicc2 12160 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ*𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ∈ (0[,]𝐴))
3632, 33, 34, 35syl3anc 1318 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ (0[,]𝐴))
37 1rp 11712 . . . . . . . . . . . . . . . 16 1 ∈ ℝ+
38 1re 9918 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ
39 elicopnf 12140 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℝ → (𝑧 ∈ (1[,)+∞) ↔ (𝑧 ∈ ℝ ∧ 1 ≤ 𝑧)))
4038, 39mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑧 ∈ (1[,)+∞) ↔ (𝑧 ∈ ℝ ∧ 1 ≤ 𝑧)))
4140simprbda 651 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (1[,)+∞)) → 𝑧 ∈ ℝ)
42 0red 9920 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (1[,)+∞)) → 0 ∈ ℝ)
4338a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (1[,)+∞)) → 1 ∈ ℝ)
44 0lt1 10429 . . . . . . . . . . . . . . . . . . . . 21 0 < 1
4544a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (1[,)+∞)) → 0 < 1)
4640simplbda 652 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (1[,)+∞)) → 1 ≤ 𝑧)
4742, 43, 41, 45, 46ltletrd 10076 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (1[,)+∞)) → 0 < 𝑧)
4841, 47elrpd 11745 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (1[,)+∞)) → 𝑧 ∈ ℝ+)
49 pntlem3.A . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
5049adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (1[,)+∞)) → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
51 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → (𝑅𝑥) = (𝑅𝑧))
52 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧𝑥 = 𝑧)
5351, 52oveq12d 6567 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → ((𝑅𝑥) / 𝑥) = ((𝑅𝑧) / 𝑧))
5453fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (abs‘((𝑅𝑥) / 𝑥)) = (abs‘((𝑅𝑧) / 𝑧)))
5554breq1d 4593 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → ((abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴 ↔ (abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴))
5655rspcv 3278 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ℝ+ → (∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴 → (abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴))
5748, 50, 56sylc 63 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (1[,)+∞)) → (abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴)
5857ralrimiva 2949 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴)
59 oveq1 6556 . . . . . . . . . . . . . . . . . 18 (𝑦 = 1 → (𝑦[,)+∞) = (1[,)+∞))
6059raleqdv 3121 . . . . . . . . . . . . . . . . 17 (𝑦 = 1 → (∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴 ↔ ∀𝑧 ∈ (1[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴))
6160rspcev 3282 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ+ ∧ ∀𝑧 ∈ (1[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴)
6237, 58, 61sylancr 694 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴)
63 breq2 4587 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝐴 → ((abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ↔ (abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴))
6463rexralbidv 3040 . . . . . . . . . . . . . . . 16 (𝑡 = 𝐴 → (∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ↔ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴))
6564, 22elrab2 3333 . . . . . . . . . . . . . . 15 (𝐴𝑇 ↔ (𝐴 ∈ (0[,]𝐴) ∧ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝐴))
6636, 62, 65sylanbrc 695 . . . . . . . . . . . . . 14 (𝜑𝐴𝑇)
67 ne0i 3880 . . . . . . . . . . . . . 14 (𝐴𝑇𝑇 ≠ ∅)
6866, 67syl 17 . . . . . . . . . . . . 13 (𝜑𝑇 ≠ ∅)
69 elicc2 12109 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑡 ∈ (0[,]𝐴) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡𝐴)))
7025, 27, 69sylancr 694 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑡 ∈ (0[,]𝐴) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡𝐴)))
7170biimpa 500 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (0[,]𝐴)) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡𝐴))
7271simp2d 1067 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ (0[,]𝐴)) → 0 ≤ 𝑡)
7372a1d 25 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0[,]𝐴)) → (∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡))
7473ralrimiva 2949 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡))
7522raleqi 3119 . . . . . . . . . . . . . . . 16 (∀𝑤𝑇 0 ≤ 𝑤 ↔ ∀𝑤 ∈ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡}0 ≤ 𝑤)
76 breq2 4587 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑡 → (0 ≤ 𝑤 ↔ 0 ≤ 𝑡))
7776ralrab2 3339 . . . . . . . . . . . . . . . 16 (∀𝑤 ∈ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡}0 ≤ 𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡))
7875, 77bitri 263 . . . . . . . . . . . . . . 15 (∀𝑤𝑇 0 ≤ 𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡))
7974, 78sylibr 223 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑤𝑇 0 ≤ 𝑤)
80 breq1 4586 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → (𝑥𝑤 ↔ 0 ≤ 𝑤))
8180ralbidv 2969 . . . . . . . . . . . . . . 15 (𝑥 = 0 → (∀𝑤𝑇 𝑥𝑤 ↔ ∀𝑤𝑇 0 ≤ 𝑤))
8281rspcev 3282 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ ∀𝑤𝑇 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤)
8325, 79, 82sylancr 694 . . . . . . . . . . . . 13 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤)
84 infrecl 10882 . . . . . . . . . . . . 13 ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤) → inf(𝑇, ℝ, < ) ∈ ℝ)
8530, 68, 83, 84syl3anc 1318 . . . . . . . . . . . 12 (𝜑 → inf(𝑇, ℝ, < ) ∈ ℝ)
8685recnd 9947 . . . . . . . . . . 11 (𝜑 → inf(𝑇, ℝ, < ) ∈ ℂ)
8786adantr 480 . . . . . . . . . 10 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → inf(𝑇, ℝ, < ) ∈ ℂ)
88 elrp 11710 . . . . . . . . . . . . . 14 (inf(𝑇, ℝ, < ) ∈ ℝ+ ↔ (inf(𝑇, ℝ, < ) ∈ ℝ ∧ 0 < inf(𝑇, ℝ, < )))
8988biimpri 217 . . . . . . . . . . . . 13 ((inf(𝑇, ℝ, < ) ∈ ℝ ∧ 0 < inf(𝑇, ℝ, < )) → inf(𝑇, ℝ, < ) ∈ ℝ+)
9085, 89sylan 487 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → inf(𝑇, ℝ, < ) ∈ ℝ+)
91 3z 11287 . . . . . . . . . . . 12 3 ∈ ℤ
92 rpexpcl 12741 . . . . . . . . . . . 12 ((inf(𝑇, ℝ, < ) ∈ ℝ+ ∧ 3 ∈ ℤ) → (inf(𝑇, ℝ, < )↑3) ∈ ℝ+)
9390, 91, 92sylancl 693 . . . . . . . . . . 11 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (inf(𝑇, ℝ, < )↑3) ∈ ℝ+)
9410, 93rpmulcld 11764 . . . . . . . . . 10 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈ ℝ+)
95 cncfi 22505 . . . . . . . . . 10 (((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) ∈ (ℂ–cn→ℂ) ∧ inf(𝑇, ℝ, < ) ∈ ℂ ∧ (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈ ℝ+) → ∃𝑠 ∈ ℝ+𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))))
9621, 87, 94, 95syl3anc 1318 . . . . . . . . 9 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → ∃𝑠 ∈ ℝ+𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))))
9785ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → inf(𝑇, ℝ, < ) ∈ ℝ)
98 rphalfcl 11734 . . . . . . . . . . . . . 14 (𝑠 ∈ ℝ+ → (𝑠 / 2) ∈ ℝ+)
9998adantl 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (𝑠 / 2) ∈ ℝ+)
10097, 99ltaddrpd 11781 . . . . . . . . . . . 12 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → inf(𝑇, ℝ, < ) < (inf(𝑇, ℝ, < ) + (𝑠 / 2)))
10199rpred 11748 . . . . . . . . . . . . . 14 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (𝑠 / 2) ∈ ℝ)
10297, 101readdcld 9948 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ∈ ℝ)
10397, 102ltnled 10063 . . . . . . . . . . . 12 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (inf(𝑇, ℝ, < ) < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ↔ ¬ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < )))
104100, 103mpbid 221 . . . . . . . . . . 11 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → ¬ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < ))
105 ax-resscn 9872 . . . . . . . . . . . . . . 15 ℝ ⊆ ℂ
10630, 105syl6ss 3580 . . . . . . . . . . . . . 14 (𝜑𝑇 ⊆ ℂ)
107106ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → 𝑇 ⊆ ℂ)
108 ssralv 3629 . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → 𝑇 ⊆ ℝ)
111110sselda 3568 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 𝑢 ∈ ℝ)
112102adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ∈ ℝ)
113111, 112ltnled 10063 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ↔ ¬ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
11485ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → inf(𝑇, ℝ, < ) ∈ ℝ)
115101adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑠 / 2) ∈ ℝ)
116114, 115resubcld 10337 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) ∈ ℝ)
11797, 99ltsubrpd 11780 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) < inf(𝑇, ℝ, < ))
118117adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) < inf(𝑇, ℝ, < ))
11930ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 𝑇 ⊆ ℝ)
12083ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤)
121 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 𝑢𝑇)
122 infrelb 10885 . . . . . . . . . . . . . . . . . . . . 21 ((𝑇 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤𝑢𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑢)
123119, 120, 121, 122syl3anc 1318 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑢)
124116, 114, 111, 118, 123ltletrd 10076 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) < 𝑢)
125111, 114, 115absdifltd 14020 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) ↔ ((inf(𝑇, ℝ, < ) − (𝑠 / 2)) < 𝑢𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)))))
126125biimprd 237 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (((inf(𝑇, ℝ, < ) − (𝑠 / 2)) < 𝑢𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2))) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2)))
127124, 126mpand 707 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2)))
128 rphalflt 11736 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ℝ+ → (𝑠 / 2) < 𝑠)
129128ad2antlr 759 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑠 / 2) < 𝑠)
130111, 114resubcld 10337 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 − inf(𝑇, ℝ, < )) ∈ ℝ)
131130recnd 9947 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 − inf(𝑇, ℝ, < )) ∈ ℂ)
132131abscld 14023 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) ∈ ℝ)
133 rpre 11715 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ℝ+𝑠 ∈ ℝ)
134133ad2antlr 759 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 𝑠 ∈ ℝ)
135 lttr 9993 . . . . . . . . . . . . . . . . . . . 20 (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) ∈ ℝ ∧ (𝑠 / 2) ∈ ℝ ∧ 𝑠 ∈ ℝ) → (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) ∧ (𝑠 / 2) < 𝑠) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠))
136132, 115, 134, 135syl3anc 1318 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) ∧ (𝑠 / 2) < 𝑠) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠))
137129, 136mpan2d 706 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠))
138127, 137syld 46 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠))
139113, 138sylbird 249 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (¬ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢 → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠))
140139con1d 138 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (¬ (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
141111recnd 9947 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 𝑢 ∈ ℂ)
142 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑢𝑝 = 𝑢)
143 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑢 → (𝑝↑3) = (𝑢↑3))
144143oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑢 → (𝐶 · (𝑝↑3)) = (𝐶 · (𝑢↑3)))
145142, 144oveq12d 6567 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = 𝑢 → (𝑝 − (𝐶 · (𝑝↑3))) = (𝑢 − (𝐶 · (𝑢↑3))))
146 eqid 2610 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) = (𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))
147 ovex 6577 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 − (𝐶 · (𝑢↑3))) ∈ V
148145, 146, 147fvmpt 6191 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ ℂ → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) = (𝑢 − (𝐶 · (𝑢↑3))))
149141, 148syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) = (𝑢 − (𝐶 · (𝑢↑3))))
15087ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → inf(𝑇, ℝ, < ) ∈ ℂ)
151 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = inf(𝑇, ℝ, < ) → 𝑝 = inf(𝑇, ℝ, < ))
152 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = inf(𝑇, ℝ, < ) → (𝑝↑3) = (inf(𝑇, ℝ, < )↑3))
153152oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = inf(𝑇, ℝ, < ) → (𝐶 · (𝑝↑3)) = (𝐶 · (inf(𝑇, ℝ, < )↑3)))
154151, 153oveq12d 6567 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = inf(𝑇, ℝ, < ) → (𝑝 − (𝐶 · (𝑝↑3))) = (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))
155 ovex 6577 . . . . . . . . . . . . . . . . . . . . 21 (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) ∈ V
156154, 146, 155fvmpt 6191 . . . . . . . . . . . . . . . . . . . 20 (inf(𝑇, ℝ, < ) ∈ ℂ → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )) = (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))
157150, 156syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )) = (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))
158149, 157oveq12d 6567 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < ))) = ((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3)))))
159158fveq2d 6107 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) = (abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))))
160159breq1d 4593 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) ↔ (abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))))
1619rpred 11748 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐶 ∈ ℝ)
162161ad3antrrr 762 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 𝐶 ∈ ℝ)
163 reexpcl 12739 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ∈ ℝ ∧ 3 ∈ ℕ0) → (𝑢↑3) ∈ ℝ)
164111, 15, 163sylancl 693 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢↑3) ∈ ℝ)
165162, 164remulcld 9949 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝐶 · (𝑢↑3)) ∈ ℝ)
166111, 165resubcld 10337 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ ℝ)
16715a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → 3 ∈ ℕ0)
168114, 167reexpcld 12887 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (inf(𝑇, ℝ, < )↑3) ∈ ℝ)
169162, 168remulcld 9949 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈ ℝ)
170114, 169resubcld 10337 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) ∈ ℝ)
171166, 170, 169absdifltd 14020 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) ↔ (((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) < (𝑢 − (𝐶 · (𝑢↑3))) ∧ (𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))))))
172169recnd 9947 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈ ℂ)
173150, 172npcand 10275 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))) = inf(𝑇, ℝ, < ))
174173breq2d 4595 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))) ↔ (𝑢 − (𝐶 · (𝑢↑3))) < inf(𝑇, ℝ, < )))
175 pntlem3.3 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇)
176175ad4ant14 1285 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇)
177 infrelb 10885 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑇 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤 ∧ (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ (𝑢 − (𝐶 · (𝑢↑3))))
178119, 120, 176, 177syl3anc 1318 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → inf(𝑇, ℝ, < ) ≤ (𝑢 − (𝐶 · (𝑢↑3))))
179114, 166, 178lensymd 10067 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ¬ (𝑢 − (𝐶 · (𝑢↑3))) < inf(𝑇, ℝ, < ))
180179pm2.21d 117 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((𝑢 − (𝐶 · (𝑢↑3))) < inf(𝑇, ℝ, < ) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
181174, 180sylbid 229 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
182181adantld 482 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) < (𝑢 − (𝐶 · (𝑢↑3))) ∧ (𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3)))) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
183171, 182sylbid 229 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
184160, 183sylbid 229 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → ((abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
185140, 184jad 173 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) ∧ 𝑢𝑇) → (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
186185ralimdva 2945 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (∀𝑢𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) → ∀𝑢𝑇 (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
18768ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → 𝑇 ≠ ∅)
18883ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤)
189 infregelb 10884 . . . . . . . . . . . . . 14 (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤) ∧ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ∈ ℝ) → ((inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑢𝑇 (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
190110, 187, 188, 102, 189syl31anc 1321 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → ((inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑢𝑇 (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢))
191186, 190sylibrd 248 . . . . . . . . . . . 12 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (∀𝑢𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < )))
192109, 191syld 46 . . . . . . . . . . 11 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → (∀𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < )))
193104, 192mtod 188 . . . . . . . . . 10 (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+) → ¬ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))))
194193nrexdv 2984 . . . . . . . . 9 ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → ¬ ∃𝑠 ∈ ℝ+𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))))
19596, 194pm2.65da 598 . . . . . . . 8 (𝜑 → ¬ 0 < inf(𝑇, ℝ, < ))
196195adantr 480 . . . . . . 7 ((𝜑𝑠 ∈ ℝ+) → ¬ 0 < inf(𝑇, ℝ, < ))
19730adantr 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ+) → 𝑇 ⊆ ℝ)
19868adantr 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ+) → 𝑇 ≠ ∅)
19983adantr 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ+) → ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤)
200133adantl 481 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ+) → 𝑠 ∈ ℝ)
201 infregelb 10884 . . . . . . . . . 10 (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑇 𝑥𝑤) ∧ 𝑠 ∈ ℝ) → (𝑠 ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑤𝑇 𝑠𝑤))
202197, 198, 199, 200, 201syl31anc 1321 . . . . . . . . 9 ((𝜑𝑠 ∈ ℝ+) → (𝑠 ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑤𝑇 𝑠𝑤))
20322raleqi 3119 . . . . . . . . . 10 (∀𝑤𝑇 𝑠𝑤 ↔ ∀𝑤 ∈ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡}𝑠𝑤)
204 breq2 4587 . . . . . . . . . . 11 (𝑤 = 𝑡 → (𝑠𝑤𝑠𝑡))
205204ralrab2 3339 . . . . . . . . . 10 (∀𝑤 ∈ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡}𝑠𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡𝑠𝑡))
206203, 205bitri 263 . . . . . . . . 9 (∀𝑤𝑇 𝑠𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡𝑠𝑡))
207202, 206syl6bb 275 . . . . . . . 8 ((𝜑𝑠 ∈ ℝ+) → (𝑠 ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡𝑠𝑡)))
208 rpgt0 11720 . . . . . . . . . 10 (𝑠 ∈ ℝ+ → 0 < 𝑠)
209208adantl 481 . . . . . . . . 9 ((𝜑𝑠 ∈ ℝ+) → 0 < 𝑠)
210 0red 9920 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ+) → 0 ∈ ℝ)
21185adantr 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℝ+) → inf(𝑇, ℝ, < ) ∈ ℝ)
212 ltletr 10008 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ inf(𝑇, ℝ, < ) ∈ ℝ) → ((0 < 𝑠𝑠 ≤ inf(𝑇, ℝ, < )) → 0 < inf(𝑇, ℝ, < )))
213210, 200, 211, 212syl3anc 1318 . . . . . . . . 9 ((𝜑𝑠 ∈ ℝ+) → ((0 < 𝑠𝑠 ≤ inf(𝑇, ℝ, < )) → 0 < inf(𝑇, ℝ, < )))
214209, 213mpand 707 . . . . . . . 8 ((𝜑𝑠 ∈ ℝ+) → (𝑠 ≤ inf(𝑇, ℝ, < ) → 0 < inf(𝑇, ℝ, < )))
215207, 214sylbird 249 . . . . . . 7 ((𝜑𝑠 ∈ ℝ+) → (∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡𝑠𝑡) → 0 < inf(𝑇, ℝ, < )))
216196, 215mtod 188 . . . . . 6 ((𝜑𝑠 ∈ ℝ+) → ¬ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡𝑠𝑡))
217 rexanali 2981 . . . . . 6 (∃𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠𝑡) ↔ ¬ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡𝑠𝑡))
218216, 217sylibr 223 . . . . 5 ((𝜑𝑠 ∈ ℝ+) → ∃𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠𝑡))
219 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → (𝑅𝑧) = (𝑅𝑥))
220 id 22 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥𝑧 = 𝑥)
221219, 220oveq12d 6567 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → ((𝑅𝑧) / 𝑧) = ((𝑅𝑥) / 𝑥))
222221fveq2d 6107 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (abs‘((𝑅𝑧) / 𝑧)) = (abs‘((𝑅𝑥) / 𝑥)))
223222breq1d 4593 . . . . . . . . . . . 12 (𝑧 = 𝑥 → ((abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ↔ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡))
224223cbvralv 3147 . . . . . . . . . . 11 (∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ↔ ∀𝑥 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡)
225 rpre 11715 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
226225ad2antll 761 . . . . . . . . . . . . . . . 16 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑥 ∈ ℝ)
227 simprl 790 . . . . . . . . . . . . . . . 16 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑦𝑥)
228 simplr 788 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
229228rpred 11748 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑦 ∈ ℝ)
230 elicopnf 12140 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ → (𝑥 ∈ (𝑦[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑦𝑥)))
231229, 230syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (𝑥 ∈ (𝑦[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑦𝑥)))
232226, 227, 231mpbir2and 959 . . . . . . . . . . . . . . 15 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑥 ∈ (𝑦[,)+∞))
233 pntlem3.r . . . . . . . . . . . . . . . . . . . . . 22 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
234233pntrval 25051 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ+ → (𝑅𝑥) = ((ψ‘𝑥) − 𝑥))
235234ad2antll 761 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (𝑅𝑥) = ((ψ‘𝑥) − 𝑥))
236235oveq1d 6564 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ((𝑅𝑥) / 𝑥) = (((ψ‘𝑥) − 𝑥) / 𝑥))
237 chpcl 24650 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
238226, 237syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (ψ‘𝑥) ∈ ℝ)
239238recnd 9947 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (ψ‘𝑥) ∈ ℂ)
240 rpcn 11717 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
241240ad2antll 761 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑥 ∈ ℂ)
242 rpne0 11724 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ+𝑥 ≠ 0)
243242ad2antll 761 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑥 ≠ 0)
244239, 241, 241, 243divsubdird 10719 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (((ψ‘𝑥) − 𝑥) / 𝑥) = (((ψ‘𝑥) / 𝑥) − (𝑥 / 𝑥)))
245241, 243dividd 10678 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (𝑥 / 𝑥) = 1)
246245oveq2d 6565 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (((ψ‘𝑥) / 𝑥) − (𝑥 / 𝑥)) = (((ψ‘𝑥) / 𝑥) − 1))
247236, 244, 2463eqtrrd 2649 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (((ψ‘𝑥) / 𝑥) − 1) = ((𝑅𝑥) / 𝑥))
248247fveq2d 6107 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) = (abs‘((𝑅𝑥) / 𝑥)))
249248breq1d 4593 . . . . . . . . . . . . . . . 16 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡 ↔ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡))
250 simprr 792 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) → ¬ 𝑠𝑡)
251250ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ¬ 𝑠𝑡)
25229ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) → (0[,]𝐴) ⊆ ℝ)
253252ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (0[,]𝐴) ⊆ ℝ)
254 simplrl 796 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) → 𝑡 ∈ (0[,]𝐴))
255254adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑡 ∈ (0[,]𝐴))
256253, 255sseldd 3569 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑡 ∈ ℝ)
257 simp-4r 803 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑠 ∈ ℝ+)
258257rpred 11748 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑠 ∈ ℝ)
259256, 258ltnled 10063 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (𝑡 < 𝑠 ↔ ¬ 𝑠𝑡))
260251, 259mpbird 246 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → 𝑡 < 𝑠)
261225, 237syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ+ → (ψ‘𝑥) ∈ ℝ)
262 rerpdivcl 11737 . . . . . . . . . . . . . . . . . . . . . . 23 (((ψ‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
263261, 262mpancom 700 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ+ → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
264263ad2antll 761 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
265 resubcl 10224 . . . . . . . . . . . . . . . . . . . . 21 ((((ψ‘𝑥) / 𝑥) ∈ ℝ ∧ 1 ∈ ℝ) → (((ψ‘𝑥) / 𝑥) − 1) ∈ ℝ)
266264, 38, 265sylancl 693 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (((ψ‘𝑥) / 𝑥) − 1) ∈ ℝ)
267266recnd 9947 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (((ψ‘𝑥) / 𝑥) − 1) ∈ ℂ)
268267abscld 14023 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) ∈ ℝ)
269 lelttr 10007 . . . . . . . . . . . . . . . . . 18 (((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ∈ ℝ ∧ 𝑡 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡𝑡 < 𝑠) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
270268, 256, 258, 269syl3anc 1318 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → (((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡𝑡 < 𝑠) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
271260, 270mpan2d 706 . . . . . . . . . . . . . . . 16 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
272249, 271sylbird 249 . . . . . . . . . . . . . . 15 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ((abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
273232, 272embantd 57 . . . . . . . . . . . . . 14 (((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦𝑥𝑥 ∈ ℝ+)) → ((𝑥 ∈ (𝑦[,)+∞) → (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
274273exp32 629 . . . . . . . . . . . . 13 ((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) → (𝑦𝑥 → (𝑥 ∈ ℝ+ → ((𝑥 ∈ (𝑦[,)+∞) → (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))))
275274com24 93 . . . . . . . . . . . 12 ((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) → ((𝑥 ∈ (𝑦[,)+∞) → (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡) → (𝑥 ∈ ℝ+ → (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))))
276275ralimdv2 2944 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) → (∀𝑥 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑡 → ∀𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
277224, 276syl5bi 231 . . . . . . . . . 10 ((((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) ∧ 𝑦 ∈ ℝ+) → (∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → ∀𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
278277reximdva 3000 . . . . . . . . 9 (((𝜑𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠𝑡)) → (∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → ∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
279278anassrs 678 . . . . . . . 8 ((((𝜑𝑠 ∈ ℝ+) ∧ 𝑡 ∈ (0[,]𝐴)) ∧ ¬ 𝑠𝑡) → (∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 → ∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
280279impancom 455 . . . . . . 7 ((((𝜑𝑠 ∈ ℝ+) ∧ 𝑡 ∈ (0[,]𝐴)) ∧ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡) → (¬ 𝑠𝑡 → ∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
281280expimpd 627 . . . . . 6 (((𝜑𝑠 ∈ ℝ+) ∧ 𝑡 ∈ (0[,]𝐴)) → ((∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠𝑡) → ∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
282281rexlimdva 3013 . . . . 5 ((𝜑𝑠 ∈ ℝ+) → (∃𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠𝑡) → ∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
283218, 282mpd 15 . . . 4 ((𝜑𝑠 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
284 ssrexv 3630 . . . 4 (ℝ+ ⊆ ℝ → (∃𝑦 ∈ ℝ+𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
2851, 283, 284mpsyl 66 . . 3 ((𝜑𝑠 ∈ ℝ+) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
286285ralrimiva 2949 . 2 (𝜑 → ∀𝑠 ∈ ℝ+𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))
287263recnd 9947 . . . . 5 (𝑥 ∈ ℝ+ → ((ψ‘𝑥) / 𝑥) ∈ ℂ)
288287rgen 2906 . . . 4 𝑥 ∈ ℝ+ ((ψ‘𝑥) / 𝑥) ∈ ℂ
289288a1i 11 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+ ((ψ‘𝑥) / 𝑥) ∈ ℂ)
2901a1i 11 . . 3 (𝜑 → ℝ+ ⊆ ℝ)
291 1cnd 9935 . . 3 (𝜑 → 1 ∈ ℂ)
292289, 290, 291rlim2 14075 . 2 (𝜑 → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1 ↔ ∀𝑠 ∈ ℝ+𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑦𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))
293286, 292mpbird 246 1 (𝜑 → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wne 2780  wral 2896  wrex 2897  {crab 2900  wss 3540  c0 3874   class class class wbr 4583  cmpt 4643  cfv 5804  (class class class)co 6549  infcinf 8230  cc 9813  cr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  +∞cpnf 9950  *cxr 9952   < clt 9953  cle 9954  cmin 10145   / cdiv 10563  2c2 10947  3c3 10948  0cn0 11169  cz 11254  +crp 11708  [,)cico 12048  [,]cicc 12049  cexp 12722  abscabs 13822  𝑟 crli 14064  TopOpenctopn 15905  fldccnfld 19567   Cn ccn 20838   ×t ctx 21173  cnccncf 22487  ψcchp 24619
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-sin 14639  df-cos 14640  df-pi 14642  df-dvds 14822  df-gcd 15055  df-prm 15224  df-pc 15380  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-limc 23436  df-dv 23437  df-log 24107  df-vma 24624  df-chp 24625
This theorem is referenced by:  pntleml  25100
  Copyright terms: Public domain W3C validator