pntlem3

Description: Lemma for pnt . Equation 10.6.35 in Shapiro, p. 436. (Contributed by Mario Carneiro, 8-Apr-2016) (Proof shortened by AV, 27-Sep-2020)

	Ref	Expression
Hypotheses	pntlem3.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ⁺ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
	pntlem3.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ⁺ )
	pntlem3.A	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
	pntlem3.1	⊢ 𝑇 = { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 }
	pntlem3.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ⁺ )
	pntlem3.3	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑇 ) → ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) ∈ 𝑇 )
Assertion	pntlem3	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝_𝑟 1 )

Proof

Step	Hyp	Ref	Expression
1		pntlem3.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ⁺ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		pntlem3.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ⁺ )
3		pntlem3.A	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
4		pntlem3.1	⊢ 𝑇 = { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 }
5		pntlem3.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ⁺ )
6		pntlem3.3	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑇 ) → ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) ∈ 𝑇 )
7		rpssre	⊢ ℝ⁺ ⊆ ℝ
8		eqid	⊢ ( TopOpen ‘ ℂ_fld ) = ( TopOpen ‘ ℂ_fld )
9	8	subcn	⊢ − ∈ ( ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) Cn ( TopOpen ‘ ℂ_fld ) )
10	9	a1i	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → − ∈ ( ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) Cn ( TopOpen ‘ ℂ_fld ) ) )
11		ssid	⊢ ℂ ⊆ ℂ
12		cncfmptid	⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑝 ∈ ℂ ↦ 𝑝 ) ∈ ( ℂ –cn→ ℂ ) )
13	11 11 12	mp2an	⊢ ( 𝑝 ∈ ℂ ↦ 𝑝 ) ∈ ( ℂ –cn→ ℂ )
14	13	a1i	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → ( 𝑝 ∈ ℂ ↦ 𝑝 ) ∈ ( ℂ –cn→ ℂ ) )
15	5	adantr	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → 𝐶 ∈ ℝ⁺ )
16	15	rpcnd	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → 𝐶 ∈ ℂ )
17	11	a1i	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → ℂ ⊆ ℂ )
18		cncfmptc	⊢ ( ( 𝐶 ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑝 ∈ ℂ ↦ 𝐶 ) ∈ ( ℂ –cn→ ℂ ) )
19	16 17 17 18	syl3anc	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → ( 𝑝 ∈ ℂ ↦ 𝐶 ) ∈ ( ℂ –cn→ ℂ ) )
20		3nn0	⊢ 3 ∈ ℕ₀
21	8	expcn	⊢ ( 3 ∈ ℕ₀ → ( 𝑝 ∈ ℂ ↦ ( 𝑝 ↑ 3 ) ) ∈ ( ( TopOpen ‘ ℂ_fld ) Cn ( TopOpen ‘ ℂ_fld ) ) )
22	20 21	mp1i	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → ( 𝑝 ∈ ℂ ↦ ( 𝑝 ↑ 3 ) ) ∈ ( ( TopOpen ‘ ℂ_fld ) Cn ( TopOpen ‘ ℂ_fld ) ) )
23	8	cncfcn1	⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂ_fld ) Cn ( TopOpen ‘ ℂ_fld ) )
24	22 23	eleqtrrdi	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → ( 𝑝 ∈ ℂ ↦ ( 𝑝 ↑ 3 ) ) ∈ ( ℂ –cn→ ℂ ) )
25	19 24	mulcncf	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → ( 𝑝 ∈ ℂ ↦ ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
26	8 10 14 25	cncfmpt2f	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
27	4	ssrab3	⊢ 𝑇 ⊆ ( 0 [,] 𝐴 )
28		0re	⊢ 0 ∈ ℝ
29	2	rpred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
30		iccssre	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 [,] 𝐴 ) ⊆ ℝ )
31	28 29 30	sylancr	⊢ ( 𝜑 → ( 0 [,] 𝐴 ) ⊆ ℝ )
32	27 31	sstrid	⊢ ( 𝜑 → 𝑇 ⊆ ℝ )
33		0xr	⊢ 0 ∈ ℝ^*
34	2	rpxrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
35	2	rpge0d	⊢ ( 𝜑 → 0 ≤ 𝐴 )
36		ubicc2	⊢ ( ( 0 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ( 0 [,] 𝐴 ) )
37	33 34 35 36	mp3an2i	⊢ ( 𝜑 → 𝐴 ∈ ( 0 [,] 𝐴 ) )
38		1rp	⊢ 1 ∈ ℝ⁺
39		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑧 ) )
40		id	⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
41	39 40	oveq12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) = ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) )
42	41	fveq2d	⊢ ( 𝑥 = 𝑧 → ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) )
43	42	breq1d	⊢ ( 𝑥 = 𝑧 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝐴 ) )
44	3	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 [,) +∞ ) ) → ∀ 𝑥 ∈ ℝ⁺ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
45		1re	⊢ 1 ∈ ℝ
46		elicopnf	⊢ ( 1 ∈ ℝ → ( 𝑧 ∈ ( 1 [,) +∞ ) ↔ ( 𝑧 ∈ ℝ ∧ 1 ≤ 𝑧 ) ) )
47	45 46	mp1i	⊢ ( 𝜑 → ( 𝑧 ∈ ( 1 [,) +∞ ) ↔ ( 𝑧 ∈ ℝ ∧ 1 ≤ 𝑧 ) ) )
48	47	simprbda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 [,) +∞ ) ) → 𝑧 ∈ ℝ )
49		0red	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 [,) +∞ ) ) → 0 ∈ ℝ )
50	45	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 [,) +∞ ) ) → 1 ∈ ℝ )
51		0lt1	⊢ 0 < 1
52	51	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 [,) +∞ ) ) → 0 < 1 )
53	47	simplbda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑧 )
54	49 50 48 52 53	ltletrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 [,) +∞ ) ) → 0 < 𝑧 )
55	48 54	elrpd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 [,) +∞ ) ) → 𝑧 ∈ ℝ⁺ )
56	43 44 55	rspcdva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 [,) +∞ ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝐴 )
57	56	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝐴 )
58		oveq1	⊢ ( 𝑦 = 1 → ( 𝑦 [,) +∞ ) = ( 1 [,) +∞ ) )
59	58	raleqdv	⊢ ( 𝑦 = 1 → ( ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝐴 ) )
60	59	rspcev	⊢ ( ( 1 ∈ ℝ⁺ ∧ ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝐴 ) → ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝐴 )
61	38 57 60	sylancr	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝐴 )
62		breq2	⊢ ( 𝑡 = 𝐴 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝐴 ) )
63	62	rexralbidv	⊢ ( 𝑡 = 𝐴 → ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ↔ ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝐴 ) )
64	63 4	elrab2	⊢ ( 𝐴 ∈ 𝑇 ↔ ( 𝐴 ∈ ( 0 [,] 𝐴 ) ∧ ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝐴 ) )
65	37 61 64	sylanbrc	⊢ ( 𝜑 → 𝐴 ∈ 𝑇 )
66	65	ne0d	⊢ ( 𝜑 → 𝑇 ≠ ∅ )
67		elicc2	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑡 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 𝐴 ) ) )
68	28 29 67	sylancr	⊢ ( 𝜑 → ( 𝑡 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 𝐴 ) ) )
69	68	biimpa	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 𝐴 ) ) → ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 𝐴 ) )
70	69	simp2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 𝐴 ) ) → 0 ≤ 𝑡 )
71	70	a1d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 𝐴 ) ) → ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → 0 ≤ 𝑡 ) )
72	71	ralrimiva	⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 0 [,] 𝐴 ) ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → 0 ≤ 𝑡 ) )
73	4	raleqi	⊢ ( ∀ 𝑤 ∈ 𝑇 0 ≤ 𝑤 ↔ ∀ 𝑤 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } 0 ≤ 𝑤 )
74		breq2	⊢ ( 𝑤 = 𝑡 → ( 0 ≤ 𝑤 ↔ 0 ≤ 𝑡 ) )
75	74	ralrab2	⊢ ( ∀ 𝑤 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } 0 ≤ 𝑤 ↔ ∀ 𝑡 ∈ ( 0 [,] 𝐴 ) ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → 0 ≤ 𝑡 ) )
76	73 75	bitri	⊢ ( ∀ 𝑤 ∈ 𝑇 0 ≤ 𝑤 ↔ ∀ 𝑡 ∈ ( 0 [,] 𝐴 ) ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → 0 ≤ 𝑡 ) )
77	72 76	sylibr	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑇 0 ≤ 𝑤 )
78		breq1	⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) )
79	78	ralbidv	⊢ ( 𝑥 = 0 → ( ∀ 𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑇 0 ≤ 𝑤 ) )
80	79	rspcev	⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑇 0 ≤ 𝑤 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 )
81	28 77 80	sylancr	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 )
82		infrecl	⊢ ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 ) → inf ( 𝑇 , ℝ , < ) ∈ ℝ )
83	32 66 81 82	syl3anc	⊢ ( 𝜑 → inf ( 𝑇 , ℝ , < ) ∈ ℝ )
84	83	recnd	⊢ ( 𝜑 → inf ( 𝑇 , ℝ , < ) ∈ ℂ )
85	84	adantr	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → inf ( 𝑇 , ℝ , < ) ∈ ℂ )
86		elrp	⊢ ( inf ( 𝑇 , ℝ , < ) ∈ ℝ⁺ ↔ ( inf ( 𝑇 , ℝ , < ) ∈ ℝ ∧ 0 < inf ( 𝑇 , ℝ , < ) ) )
87	86	biimpri	⊢ ( ( inf ( 𝑇 , ℝ , < ) ∈ ℝ ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → inf ( 𝑇 , ℝ , < ) ∈ ℝ⁺ )
88	83 87	sylan	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → inf ( 𝑇 , ℝ , < ) ∈ ℝ⁺ )
89		3z	⊢ 3 ∈ ℤ
90		rpexpcl	⊢ ( ( inf ( 𝑇 , ℝ , < ) ∈ ℝ⁺ ∧ 3 ∈ ℤ ) → ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ∈ ℝ⁺ )
91	88 89 90	sylancl	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ∈ ℝ⁺ )
92	15 91	rpmulcld	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ∈ ℝ⁺ )
93		cncfi	⊢ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) ∧ inf ( 𝑇 , ℝ , < ) ∈ ℂ ∧ ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ∈ ℝ⁺ ) → ∃ 𝑠 ∈ ℝ⁺ ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) )
94	26 85 92 93	syl3anc	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → ∃ 𝑠 ∈ ℝ⁺ ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) )
95	83	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → inf ( 𝑇 , ℝ , < ) ∈ ℝ )
96		rphalfcl	⊢ ( 𝑠 ∈ ℝ⁺ → ( 𝑠 / 2 ) ∈ ℝ⁺ )
97	96	adantl	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ( 𝑠 / 2 ) ∈ ℝ⁺ )
98	95 97	ltaddrpd	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → inf ( 𝑇 , ℝ , < ) < ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) )
99	97	rpred	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ( 𝑠 / 2 ) ∈ ℝ )
100	95 99	readdcld	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ∈ ℝ )
101	95 100	ltnled	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ( inf ( 𝑇 , ℝ , < ) < ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ↔ ¬ ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ inf ( 𝑇 , ℝ , < ) ) )
102	98 101	mpbid	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ¬ ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ inf ( 𝑇 , ℝ , < ) )
103		ax-resscn	⊢ ℝ ⊆ ℂ
104	32 103	sstrdi	⊢ ( 𝜑 → 𝑇 ⊆ ℂ )
105	104	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → 𝑇 ⊆ ℂ )
106		ssralv	⊢ ( 𝑇 ⊆ ℂ → ( ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) → ∀ 𝑢 ∈ 𝑇 ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) ) )
107	105 106	syl	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ( ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) → ∀ 𝑢 ∈ 𝑇 ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) ) )
108	32	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → 𝑇 ⊆ ℝ )
109	108	sselda	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → 𝑢 ∈ ℝ )
110	100	adantr	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ∈ ℝ )
111	109 110	ltnled	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝑢 < ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ↔ ¬ ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ 𝑢 ) )
112	83	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ∈ ℝ )
113	99	adantr	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝑠 / 2 ) ∈ ℝ )
114	112 113	resubcld	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( inf ( 𝑇 , ℝ , < ) − ( 𝑠 / 2 ) ) ∈ ℝ )
115	95 97	ltsubrpd	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ( inf ( 𝑇 , ℝ , < ) − ( 𝑠 / 2 ) ) < inf ( 𝑇 , ℝ , < ) )
116	115	adantr	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( inf ( 𝑇 , ℝ , < ) − ( 𝑠 / 2 ) ) < inf ( 𝑇 , ℝ , < ) )
117	32	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → 𝑇 ⊆ ℝ )
118	81	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 )
119		simpr	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → 𝑢 ∈ 𝑇 )
120		infrelb	⊢ ( ( 𝑇 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 ∧ 𝑢 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ 𝑢 )
121	117 118 119 120	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ 𝑢 )
122	114 112 109 116 121	ltletrd	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( inf ( 𝑇 , ℝ , < ) − ( 𝑠 / 2 ) ) < 𝑢 )
123	109 112 113	absdifltd	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < ( 𝑠 / 2 ) ↔ ( ( inf ( 𝑇 , ℝ , < ) − ( 𝑠 / 2 ) ) < 𝑢 ∧ 𝑢 < ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ) ) )
124	123	biimprd	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( ( inf ( 𝑇 , ℝ , < ) − ( 𝑠 / 2 ) ) < 𝑢 ∧ 𝑢 < ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ) → ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < ( 𝑠 / 2 ) ) )
125	122 124	mpand	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝑢 < ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) → ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < ( 𝑠 / 2 ) ) )
126		rphalflt	⊢ ( 𝑠 ∈ ℝ⁺ → ( 𝑠 / 2 ) < 𝑠 )
127	126	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝑠 / 2 ) < 𝑠 )
128	109 112	resubcld	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ∈ ℝ )
129	128	recnd	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ∈ ℂ )
130	129	abscld	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) ∈ ℝ )
131		rpre	⊢ ( 𝑠 ∈ ℝ⁺ → 𝑠 ∈ ℝ )
132	131	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → 𝑠 ∈ ℝ )
133		lttr	⊢ ( ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) ∈ ℝ ∧ ( 𝑠 / 2 ) ∈ ℝ ∧ 𝑠 ∈ ℝ ) → ( ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < ( 𝑠 / 2 ) ∧ ( 𝑠 / 2 ) < 𝑠 ) → ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 ) )
134	130 113 132 133	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < ( 𝑠 / 2 ) ∧ ( 𝑠 / 2 ) < 𝑠 ) → ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 ) )
135	127 134	mpan2d	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < ( 𝑠 / 2 ) → ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 ) )
136	125 135	syld	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝑢 < ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) → ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 ) )
137	111 136	sylbird	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ¬ ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ 𝑢 → ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 ) )
138	137	con1d	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ¬ ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ 𝑢 ) )
139	109	recnd	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → 𝑢 ∈ ℂ )
140		id	⊢ ( 𝑝 = 𝑢 → 𝑝 = 𝑢 )
141		oveq1	⊢ ( 𝑝 = 𝑢 → ( 𝑝 ↑ 3 ) = ( 𝑢 ↑ 3 ) )
142	141	oveq2d	⊢ ( 𝑝 = 𝑢 → ( 𝐶 · ( 𝑝 ↑ 3 ) ) = ( 𝐶 · ( 𝑢 ↑ 3 ) ) )
143	140 142	oveq12d	⊢ ( 𝑝 = 𝑢 → ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) = ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) )
144		eqid	⊢ ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) = ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) )
145		ovex	⊢ ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) ∈ V
146	143 144 145	fvmpt	⊢ ( 𝑢 ∈ ℂ → ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) = ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) )
147	139 146	syl	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) = ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) )
148	85	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ∈ ℂ )
149		id	⊢ ( 𝑝 = inf ( 𝑇 , ℝ , < ) → 𝑝 = inf ( 𝑇 , ℝ , < ) )
150		oveq1	⊢ ( 𝑝 = inf ( 𝑇 , ℝ , < ) → ( 𝑝 ↑ 3 ) = ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) )
151	150	oveq2d	⊢ ( 𝑝 = inf ( 𝑇 , ℝ , < ) → ( 𝐶 · ( 𝑝 ↑ 3 ) ) = ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) )
152	149 151	oveq12d	⊢ ( 𝑝 = inf ( 𝑇 , ℝ , < ) → ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) = ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) )
153		ovex	⊢ ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) ∈ V
154	152 144 153	fvmpt	⊢ ( inf ( 𝑇 , ℝ , < ) ∈ ℂ → ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) = ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) )
155	148 154	syl	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) = ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) )
156	147 155	oveq12d	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) = ( ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) − ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) ) )
157	156	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) = ( abs ‘ ( ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) − ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) ) ) )
158	157	breq1d	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ↔ ( abs ‘ ( ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) − ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) )
159	5	rpred	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
160	159	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → 𝐶 ∈ ℝ )
161		reexpcl	⊢ ( ( 𝑢 ∈ ℝ ∧ 3 ∈ ℕ₀ ) → ( 𝑢 ↑ 3 ) ∈ ℝ )
162	109 20 161	sylancl	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝑢 ↑ 3 ) ∈ ℝ )
163	160 162	remulcld	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝐶 · ( 𝑢 ↑ 3 ) ) ∈ ℝ )
164	109 163	resubcld	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) ∈ ℝ )
165	20	a1i	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → 3 ∈ ℕ₀ )
166	112 165	reexpcld	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ∈ ℝ )
167	160 166	remulcld	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ∈ ℝ )
168	112 167	resubcld	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) ∈ ℝ )
169	164 168 167	absdifltd	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( abs ‘ ( ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) − ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ↔ ( ( ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) < ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) ∧ ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) < ( ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) + ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) ) ) )
170	167	recnd	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ∈ ℂ )
171	148 170	npcand	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) + ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) = inf ( 𝑇 , ℝ , < ) )
172	171	breq2d	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) < ( ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) + ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) ↔ ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) < inf ( 𝑇 , ℝ , < ) ) )
173	6	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) ∈ 𝑇 )
174		infrelb	⊢ ( ( 𝑇 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 ∧ ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) )
175	117 118 173 174	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) )
176	112 164 175	lensymd	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ¬ ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) < inf ( 𝑇 , ℝ , < ) )
177	176	pm2.21d	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) < inf ( 𝑇 , ℝ , < ) → ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ 𝑢 ) )
178	172 177	sylbid	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) < ( ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) + ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) → ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ 𝑢 ) )
179	178	adantld	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( ( ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) < ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) ∧ ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) < ( ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) + ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) ) → ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ 𝑢 ) )
180	169 179	sylbid	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( abs ‘ ( ( 𝑢 − ( 𝐶 · ( 𝑢 ↑ 3 ) ) ) − ( inf ( 𝑇 , ℝ , < ) − ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) → ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ 𝑢 ) )
181	158 180	sylbid	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) → ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ 𝑢 ) )
182	138 181	jad	⊢ ( ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑢 ∈ 𝑇 ) → ( ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) → ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ 𝑢 ) )
183	182	ralimdva	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ( ∀ 𝑢 ∈ 𝑇 ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) → ∀ 𝑢 ∈ 𝑇 ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ 𝑢 ) )
184	66	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → 𝑇 ≠ ∅ )
185	81	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 )
186		infregelb	⊢ ( ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 ) ∧ ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ∈ ℝ ) → ( ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ inf ( 𝑇 , ℝ , < ) ↔ ∀ 𝑢 ∈ 𝑇 ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ 𝑢 ) )
187	108 184 185 100 186	syl31anc	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ( ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ inf ( 𝑇 , ℝ , < ) ↔ ∀ 𝑢 ∈ 𝑇 ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ 𝑢 ) )
188	183 187	sylibrd	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ( ∀ 𝑢 ∈ 𝑇 ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) → ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ inf ( 𝑇 , ℝ , < ) ) )
189	107 188	syld	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ( ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) → ( inf ( 𝑇 , ℝ , < ) + ( 𝑠 / 2 ) ) ≤ inf ( 𝑇 , ℝ , < ) ) )
190	102 189	mtod	⊢ ( ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) ∧ 𝑠 ∈ ℝ⁺ ) → ¬ ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) )
191	190	nrexdv	⊢ ( ( 𝜑 ∧ 0 < inf ( 𝑇 , ℝ , < ) ) → ¬ ∃ 𝑠 ∈ ℝ⁺ ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − inf ( 𝑇 , ℝ , < ) ) ) < 𝑠 → ( abs ‘ ( ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ 𝑢 ) − ( ( 𝑝 ∈ ℂ ↦ ( 𝑝 − ( 𝐶 · ( 𝑝 ↑ 3 ) ) ) ) ‘ inf ( 𝑇 , ℝ , < ) ) ) ) < ( 𝐶 · ( inf ( 𝑇 , ℝ , < ) ↑ 3 ) ) ) )
192	94 191	pm2.65da	⊢ ( 𝜑 → ¬ 0 < inf ( 𝑇 , ℝ , < ) )
193	192	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → ¬ 0 < inf ( 𝑇 , ℝ , < ) )
194	32	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → 𝑇 ⊆ ℝ )
195	66	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → 𝑇 ≠ ∅ )
196	81	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 )
197	131	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → 𝑠 ∈ ℝ )
198		infregelb	⊢ ( ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 ) ∧ 𝑠 ∈ ℝ ) → ( 𝑠 ≤ inf ( 𝑇 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑇 𝑠 ≤ 𝑤 ) )
199	194 195 196 197 198	syl31anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → ( 𝑠 ≤ inf ( 𝑇 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑇 𝑠 ≤ 𝑤 ) )
200	4	raleqi	⊢ ( ∀ 𝑤 ∈ 𝑇 𝑠 ≤ 𝑤 ↔ ∀ 𝑤 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } 𝑠 ≤ 𝑤 )
201		breq2	⊢ ( 𝑤 = 𝑡 → ( 𝑠 ≤ 𝑤 ↔ 𝑠 ≤ 𝑡 ) )
202	201	ralrab2	⊢ ( ∀ 𝑤 ∈ { 𝑡 ∈ ( 0 [,] 𝐴 ) ∣ ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 } 𝑠 ≤ 𝑤 ↔ ∀ 𝑡 ∈ ( 0 [,] 𝐴 ) ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → 𝑠 ≤ 𝑡 ) )
203	200 202	bitri	⊢ ( ∀ 𝑤 ∈ 𝑇 𝑠 ≤ 𝑤 ↔ ∀ 𝑡 ∈ ( 0 [,] 𝐴 ) ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → 𝑠 ≤ 𝑡 ) )
204	199 203	bitrdi	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → ( 𝑠 ≤ inf ( 𝑇 , ℝ , < ) ↔ ∀ 𝑡 ∈ ( 0 [,] 𝐴 ) ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → 𝑠 ≤ 𝑡 ) ) )
205		rpgt0	⊢ ( 𝑠 ∈ ℝ⁺ → 0 < 𝑠 )
206	205	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → 0 < 𝑠 )
207	83	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → inf ( 𝑇 , ℝ , < ) ∈ ℝ )
208		ltletr	⊢ ( ( 0 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ inf ( 𝑇 , ℝ , < ) ∈ ℝ ) → ( ( 0 < 𝑠 ∧ 𝑠 ≤ inf ( 𝑇 , ℝ , < ) ) → 0 < inf ( 𝑇 , ℝ , < ) ) )
209	28 197 207 208	mp3an2i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → ( ( 0 < 𝑠 ∧ 𝑠 ≤ inf ( 𝑇 , ℝ , < ) ) → 0 < inf ( 𝑇 , ℝ , < ) ) )
210	206 209	mpand	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → ( 𝑠 ≤ inf ( 𝑇 , ℝ , < ) → 0 < inf ( 𝑇 , ℝ , < ) ) )
211	204 210	sylbird	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → ( ∀ 𝑡 ∈ ( 0 [,] 𝐴 ) ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → 𝑠 ≤ 𝑡 ) → 0 < inf ( 𝑇 , ℝ , < ) ) )
212	193 211	mtod	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → ¬ ∀ 𝑡 ∈ ( 0 [,] 𝐴 ) ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → 𝑠 ≤ 𝑡 ) )
213		rexanali	⊢ ( ∃ 𝑡 ∈ ( 0 [,] 𝐴 ) ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ∧ ¬ 𝑠 ≤ 𝑡 ) ↔ ¬ ∀ 𝑡 ∈ ( 0 [,] 𝐴 ) ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → 𝑠 ≤ 𝑡 ) )
214	212 213	sylibr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → ∃ 𝑡 ∈ ( 0 [,] 𝐴 ) ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ∧ ¬ 𝑠 ≤ 𝑡 ) )
215		fveq2	⊢ ( 𝑧 = 𝑥 → ( 𝑅 ‘ 𝑧 ) = ( 𝑅 ‘ 𝑥 ) )
216		id	⊢ ( 𝑧 = 𝑥 → 𝑧 = 𝑥 )
217	215 216	oveq12d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) = ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) )
218	217	fveq2d	⊢ ( 𝑧 = 𝑥 → ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) )
219	218	breq1d	⊢ ( 𝑧 = 𝑥 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑡 ) )
220	219	cbvralvw	⊢ ( ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ↔ ∀ 𝑥 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑡 )
221		rpre	⊢ ( 𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ )
222	221	ad2antll	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → 𝑥 ∈ ℝ )
223		simprl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → 𝑦 ≤ 𝑥 )
224		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → 𝑦 ∈ ℝ⁺ )
225	224	rpred	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → 𝑦 ∈ ℝ )
226		elicopnf	⊢ ( 𝑦 ∈ ℝ → ( 𝑥 ∈ ( 𝑦 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑦 ≤ 𝑥 ) ) )
227	225 226	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( 𝑥 ∈ ( 𝑦 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑦 ≤ 𝑥 ) ) )
228	222 223 227	mpbir2and	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → 𝑥 ∈ ( 𝑦 [,) +∞ ) )
229	1	pntrval	⊢ ( 𝑥 ∈ ℝ⁺ → ( 𝑅 ‘ 𝑥 ) = ( ( ψ ‘ 𝑥 ) − 𝑥 ) )
230	229	ad2antll	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( 𝑅 ‘ 𝑥 ) = ( ( ψ ‘ 𝑥 ) − 𝑥 ) )
231	230	oveq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) = ( ( ( ψ ‘ 𝑥 ) − 𝑥 ) / 𝑥 ) )
232		chpcl	⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
233	222 232	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ψ ‘ 𝑥 ) ∈ ℝ )
234	233	recnd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ψ ‘ 𝑥 ) ∈ ℂ )
235		rpcn	⊢ ( 𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ )
236	235	ad2antll	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → 𝑥 ∈ ℂ )
237		rpne0	⊢ ( 𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0 )
238	237	ad2antll	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → 𝑥 ≠ 0 )
239	234 236 236 238	divsubdird	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ( ( ψ ‘ 𝑥 ) − 𝑥 ) / 𝑥 ) = ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − ( 𝑥 / 𝑥 ) ) )
240	236 238	dividd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( 𝑥 / 𝑥 ) = 1 )
241	240	oveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − ( 𝑥 / 𝑥 ) ) = ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) )
242	231 239 241	3eqtrrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) = ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) )
243	242	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) )
244	243	breq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) ≤ 𝑡 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑡 ) )
245		simprr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) → ¬ 𝑠 ≤ 𝑡 )
246	245	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ¬ 𝑠 ≤ 𝑡 )
247	31	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) → ( 0 [,] 𝐴 ) ⊆ ℝ )
248	247	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( 0 [,] 𝐴 ) ⊆ ℝ )
249		simplrl	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) → 𝑡 ∈ ( 0 [,] 𝐴 ) )
250	249	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → 𝑡 ∈ ( 0 [,] 𝐴 ) )
251	248 250	sseldd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → 𝑡 ∈ ℝ )
252		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → 𝑠 ∈ ℝ⁺ )
253	252	rpred	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → 𝑠 ∈ ℝ )
254	251 253	ltnled	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( 𝑡 < 𝑠 ↔ ¬ 𝑠 ≤ 𝑡 ) )
255	246 254	mpbird	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → 𝑡 < 𝑠 )
256	221 232	syl	⊢ ( 𝑥 ∈ ℝ⁺ → ( ψ ‘ 𝑥 ) ∈ ℝ )
257		rerpdivcl	⊢ ( ( ( ψ ‘ 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ ℝ⁺ ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
258	256 257	mpancom	⊢ ( 𝑥 ∈ ℝ⁺ → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
259	258	ad2antll	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
260		resubcl	⊢ ( ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ∈ ℝ )
261	259 45 260	sylancl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ∈ ℝ )
262	261	recnd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ∈ ℂ )
263	262	abscld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) ∈ ℝ )
264		lelttr	⊢ ( ( ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) ∈ ℝ ∧ 𝑡 ∈ ℝ ∧ 𝑠 ∈ ℝ ) → ( ( ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) ≤ 𝑡 ∧ 𝑡 < 𝑠 ) → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) )
265	263 251 253 264	syl3anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ( ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) ≤ 𝑡 ∧ 𝑡 < 𝑠 ) → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) )
266	255 265	mpan2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) ≤ 𝑡 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) )
267	244 266	sylbird	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑡 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) )
268	228 267	embantd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ⁺ ) ) → ( ( 𝑥 ∈ ( 𝑦 [,) +∞ ) → ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑡 ) → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) )
269	268	exp32	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) → ( 𝑦 ≤ 𝑥 → ( 𝑥 ∈ ℝ⁺ → ( ( 𝑥 ∈ ( 𝑦 [,) +∞ ) → ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑡 ) → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) ) ) )
270	269	com24	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) → ( ( 𝑥 ∈ ( 𝑦 [,) +∞ ) → ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑡 ) → ( 𝑥 ∈ ℝ⁺ → ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) ) ) )
271	270	ralimdv2	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) → ( ∀ 𝑥 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑡 → ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) ) )
272	220 271	biimtrid	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) ∧ 𝑦 ∈ ℝ⁺ ) → ( ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) ) )
273	272	reximdva	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ ( 𝑡 ∈ ( 0 [,] 𝐴 ) ∧ ¬ 𝑠 ≤ 𝑡 ) ) → ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) ) )
274	273	anassrs	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑡 ∈ ( 0 [,] 𝐴 ) ) ∧ ¬ 𝑠 ≤ 𝑡 ) → ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 → ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) ) )
275	274	impancom	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑡 ∈ ( 0 [,] 𝐴 ) ) ∧ ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ) → ( ¬ 𝑠 ≤ 𝑡 → ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) ) )
276	275	expimpd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) ∧ 𝑡 ∈ ( 0 [,] 𝐴 ) ) → ( ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ∧ ¬ 𝑠 ≤ 𝑡 ) → ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) ) )
277	276	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → ( ∃ 𝑡 ∈ ( 0 [,] 𝐴 ) ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ ( 𝑦 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑡 ∧ ¬ 𝑠 ≤ 𝑡 ) → ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) ) )
278	214 277	mpd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) )
279		ssrexv	⊢ ( ℝ⁺ ⊆ ℝ → ( ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) ) )
280	7 278 279	mpsyl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) )
281	280	ralrimiva	⊢ ( 𝜑 → ∀ 𝑠 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) )
282	258	recnd	⊢ ( 𝑥 ∈ ℝ⁺ → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℂ )
283	282	rgen	⊢ ∀ 𝑥 ∈ ℝ⁺ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℂ
284	283	a1i	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℂ )
285	7	a1i	⊢ ( 𝜑 → ℝ⁺ ⊆ ℝ )
286		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
287	284 285 286	rlim2	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ⁺ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝_𝑟 1 ↔ ∀ 𝑠 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ℝ⁺ ( 𝑦 ≤ 𝑥 → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) − 1 ) ) < 𝑠 ) ) )
288	281 287	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝_𝑟 1 )

Metamath Proof Explorer

Theorem pntlem3

Proof