lgamgulmlem2 - Metamath Proof Explorer

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

Theorem lgamgulmlem2 24970

Description: Lemma for lgamgulm 24975. (Contributed by Mario Carneiro, 3-Jul-2017.)

**Hypotheses**
Ref	Expression
lgamgulm.r	⊢ (𝜑 → 𝑅 ∈ ℕ)
lgamgulm.u	⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}
lgamgulm.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
lgamgulm.a	⊢ (𝜑 → 𝐴 ∈ 𝑈)
lgamgulm.l	⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁)

**Assertion**
Ref	Expression
lgamgulmlem2	⊢ (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))

Distinct variable groups: 𝑥,𝑁 𝑥,𝑘,𝑅 𝐴,𝑘,𝑥 𝜑,𝑥 Allowed substitution hints: 𝜑(𝑘) 𝑈(𝑥,𝑘) 𝑁(𝑘)

Proof of Theorem lgamgulmlem2 Dummy variables 𝑦 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1elunit 12512	. . 3 ⊢ 1 ∈ (0[,]1)
2		0elunit 12511	. . 3 ⊢ 0 ∈ (0[,]1)
3		0red 10328	. . . 4 ⊢ (𝜑 → 0 ∈ ℝ)
4		1red 10326	. . . 4 ⊢ (𝜑 → 1 ∈ ℝ)
5		eqid 2806	. . . . 5 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
6	5	subcn 22882	. . . . . 6 ⊢ − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
8		lgamgulm.r	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℕ)
9		lgamgulm.u	. . . . . . . . . . 11 ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}
10	8, 9	lgamgulmlem1 24969	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
11		lgamgulm.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
12	10, 11	sseldd 3799	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
13	12	eldifad 3781	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
14		lgamgulm.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ)
15	14	nnred 11320	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℝ)
16	15	recnd 10353	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℂ)
17	14	nnne0d 11351	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ≠ 0)
18	13, 16, 17	divcld 11086	. . . . . . 7 ⊢ (𝜑 → (𝐴 / 𝑁) ∈ ℂ)
19		unitssre 12542	. . . . . . . . 9 ⊢ (0[,]1) ⊆ ℝ
20		ax-resscn 10278	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
21	19, 20	sstri 3807	. . . . . . . 8 ⊢ (0[,]1) ⊆ ℂ
22	21	a1i 11	. . . . . . 7 ⊢ (𝜑 → (0[,]1) ⊆ ℂ)
23		ssidd 3821	. . . . . . 7 ⊢ (𝜑 → ℂ ⊆ ℂ)
24		cncfmptc 22927	. . . . . . 7 ⊢ (((𝐴 / 𝑁) ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ (𝐴 / 𝑁)) ∈ ((0[,]1)–cn→ℂ))
25	18, 22, 23, 24	syl3anc 1483	. . . . . 6 ⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (𝐴 / 𝑁)) ∈ ((0[,]1)–cn→ℂ))
26		cncfmptid 22928	. . . . . . 7 ⊢ (((0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
27	21, 23, 26	sylancr 577	. . . . . 6 ⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
28	25, 27	mulcncf 23427	. . . . 5 ⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ ((𝐴 / 𝑁) · 𝑡)) ∈ ((0[,]1)–cn→ℂ))
29	18	adantr 468	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (𝐴 / 𝑁) ∈ ℂ)
30		simpr 473	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1))
31	19, 30	sseldi 3796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℝ)
32	31	recnd 10353	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℂ)
33	29, 32	mulcld 10345	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((𝐴 / 𝑁) · 𝑡) ∈ ℂ)
34		1cnd 10320	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 1 ∈ ℂ)
35	33, 34	addcld 10344	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ)
36		rere 14085	. . . . . . . . . . . 12 ⊢ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (((𝐴 / 𝑁) · 𝑡) + 1))
37	36	adantl 469	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑡 ∈ (0[,]1)) ∧ (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (((𝐴 / 𝑁) · 𝑡) + 1))
38	35	recld 14157	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℝ)
39	33	recld 14157	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∈ ℝ)
40	39	recnd 10353	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∈ ℂ)
41	40	abscld 14398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) ∈ ℝ)
42	33	abscld 14398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ∈ ℝ)
43		1red 10326	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 1 ∈ ℝ)
44		absrele 14271	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 / 𝑁) · 𝑡) ∈ ℂ → (abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) ≤ (abs‘((𝐴 / 𝑁) · 𝑡)))
45	33, 44	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) ≤ (abs‘((𝐴 / 𝑁) · 𝑡)))
46	43	rehalfcld 11546	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (1 / 2) ∈ ℝ)
47	8	nnred 11320	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑅 ∈ ℝ)
48	47	adantr 468	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 𝑅 ∈ ℝ)
49	14	adantr 468	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 𝑁 ∈ ℕ)
50	48, 49	nndivred 11355	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (𝑅 / 𝑁) ∈ ℝ)
51	18	abscld 14398	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (abs‘(𝐴 / 𝑁)) ∈ ℝ)
52	51	adantr 468	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘(𝐴 / 𝑁)) ∈ ℝ)
53	29	absge0d 14406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 0 ≤ (abs‘(𝐴 / 𝑁)))
54		elicc01 12510	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
55	54	simp2bi 1169	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ (0[,]1) → 0 ≤ 𝑡)
56	55	adantl 469	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 0 ≤ 𝑡)
57	13, 16, 17	absdivd 14417	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (abs‘(𝐴 / 𝑁)) = ((abs‘𝐴) / (abs‘𝑁)))
58	14	nnrpd 12084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
59	58	rpge0d 12090	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 0 ≤ 𝑁)
60	15, 59	absidd 14384	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (abs‘𝑁) = 𝑁)
61	60	oveq2d 6890	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((abs‘𝐴) / (abs‘𝑁)) = ((abs‘𝐴) / 𝑁))
62	57, 61	eqtr2d 2841	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((abs‘𝐴) / 𝑁) = (abs‘(𝐴 / 𝑁)))
63	13	abscld 14398	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ)
64		fveq2 6408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = 𝐴 → (abs‘𝑥) = (abs‘𝐴))
65	64	breq1d 4854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 = 𝐴 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝐴) ≤ 𝑅))
66		fvoveq1 6897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 = 𝐴 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝐴 + 𝑘)))
67	66	breq2d 4856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 = 𝐴 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
68	67	ralbidv 3174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 = 𝐴 → (∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
69	65, 68	anbi12d 618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝐴 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘)))))
70	69, 9	elrab2 3562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐴 ∈ 𝑈 ↔ (𝐴 ∈ ℂ ∧ ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘)))))
71	70	simprbi 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 ∈ 𝑈 → ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
72	11, 71	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
73	72	simpld 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (abs‘𝐴) ≤ 𝑅)
74	63, 47, 58, 73	lediv1dd 12144	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((abs‘𝐴) / 𝑁) ≤ (𝑅 / 𝑁))
75	62, 74	eqbrtrrd 4868	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (abs‘(𝐴 / 𝑁)) ≤ (𝑅 / 𝑁))
76	75	adantr 468	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘(𝐴 / 𝑁)) ≤ (𝑅 / 𝑁))
77	54	simp3bi 1170	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ (0[,]1) → 𝑡 ≤ 1)
78	77	adantl 469	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ≤ 1)
79	52, 50, 31, 43, 53, 56, 76, 78	lemul12ad 11251	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((abs‘(𝐴 / 𝑁)) · 𝑡) ≤ ((𝑅 / 𝑁) · 1))
80	29, 32	absmuld 14416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) = ((abs‘(𝐴 / 𝑁)) · (abs‘𝑡)))
81	31, 56	absidd 14384	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘𝑡) = 𝑡)
82	81	oveq2d 6890	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((abs‘(𝐴 / 𝑁)) · (abs‘𝑡)) = ((abs‘(𝐴 / 𝑁)) · 𝑡))
83	80, 82	eqtr2d 2841	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((abs‘(𝐴 / 𝑁)) · 𝑡) = (abs‘((𝐴 / 𝑁) · 𝑡)))
84	50	recnd 10353	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (𝑅 / 𝑁) ∈ ℂ)
85	84	mulid1d 10342	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((𝑅 / 𝑁) · 1) = (𝑅 / 𝑁))
86	79, 83, 85	3brtr3d 4875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (𝑅 / 𝑁))
87		lgamgulm.l	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁)
88		2rp 12051	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 ∈ ℝ⁺
89	88	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 2 ∈ ℝ⁺)
90	47, 15, 89	lemuldiv2d 12136	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((2 · 𝑅) ≤ 𝑁 ↔ 𝑅 ≤ (𝑁 / 2)))
91	87, 90	mpbid 223	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 ≤ (𝑁 / 2))
92		2cnd 11377	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 2 ∈ ℂ)
93		2ne0 11396	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2 ≠ 0
94	93	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 2 ≠ 0)
95	16, 92, 94	divrecd 11089	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2)))
96	91, 95	breqtrd 4870	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑅 ≤ (𝑁 · (1 / 2)))
97	4	rehalfcld 11546	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
98	47, 97, 58	ledivmuld 12139	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑅 / 𝑁) ≤ (1 / 2) ↔ 𝑅 ≤ (𝑁 · (1 / 2))))
99	96, 98	mpbird 248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 / 𝑁) ≤ (1 / 2))
100	99	adantr 468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (𝑅 / 𝑁) ≤ (1 / 2))
101	42, 50, 46, 86, 100	letrd 10479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (1 / 2))
102		halflt1 11517	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 / 2) < 1
103	102	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (1 / 2) < 1)
104	42, 46, 43, 101, 103	lelttrd 10480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) < 1)
105	41, 42, 43, 45, 104	lelttrd 10480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) < 1)
106	39, 43	absltd 14391	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((abs‘(ℜ‘((𝐴 / 𝑁) · 𝑡))) < 1 ↔ (-1 < (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∧ (ℜ‘((𝐴 / 𝑁) · 𝑡)) < 1)))
107	105, 106	mpbid 223	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (-1 < (ℜ‘((𝐴 / 𝑁) · 𝑡)) ∧ (ℜ‘((𝐴 / 𝑁) · 𝑡)) < 1))
108	107	simpld 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → -1 < (ℜ‘((𝐴 / 𝑁) · 𝑡)))
109	43	renegcld 10742	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → -1 ∈ ℝ)
110	109, 39	posdifd 10899	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (-1 < (ℜ‘((𝐴 / 𝑁) · 𝑡)) ↔ 0 < ((ℜ‘((𝐴 / 𝑁) · 𝑡)) − -1)))
111	108, 110	mpbid 223	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 0 < ((ℜ‘((𝐴 / 𝑁) · 𝑡)) − -1))
112	40, 34	subnegd 10684	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((ℜ‘((𝐴 / 𝑁) · 𝑡)) − -1) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1))
113	111, 112	breqtrd 4870	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 0 < ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1))
114	33, 34	readdd 14177	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + (ℜ‘1)))
115		re1 14117	. . . . . . . . . . . . . . . 16 ⊢ (ℜ‘1) = 1
116	115	oveq2i 6885	. . . . . . . . . . . . . . 15 ⊢ ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + (ℜ‘1)) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1)
117	114, 116	syl6eq 2856	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) = ((ℜ‘((𝐴 / 𝑁) · 𝑡)) + 1))
118	113, 117	breqtrrd 4872	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → 0 < (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)))
119	38, 118	elrpd 12083	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℝ⁺)
120	119	adantr 468	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑡 ∈ (0[,]1)) ∧ (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ) → (ℜ‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℝ⁺)
121	37, 120	eqeltrrd 2886	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑡 ∈ (0[,]1)) ∧ (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ⁺)
122	121	ex 399	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ⁺))
123		eqid 2806	. . . . . . . . . 10 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
124	123	ellogdm 24599	. . . . . . . . 9 ⊢ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)) ↔ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ ∧ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℝ⁺)))
125	35, 122, 124	sylanbrc 574	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)))
126		eqidd 2807	. . . . . . . 8 ⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) = (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)))
127	123	logcn 24607	. . . . . . . . . . 11 ⊢ (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
128	127	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ))
129		cncff 22909	. . . . . . . . . 10 ⊢ ((log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ) → (log ↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖ (-∞(,]0))⟶ℂ)
130	128, 129	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (log ↾ (ℂ ∖ (-∞(,]0))):(ℂ ∖ (-∞(,]0))⟶ℂ)
131	130	feqmptd 6470	. . . . . . . 8 ⊢ (𝜑 → (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦)))
132		fveq2 6408	. . . . . . . 8 ⊢ (𝑦 = (((𝐴 / 𝑁) · 𝑡) + 1) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦) = ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1)))
133	125, 126, 131, 132	fmptco 6619	. . . . . . 7 ⊢ (𝜑 → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0[,]1) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1))))
134		fvres 6427	. . . . . . . . 9 ⊢ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))
135	125, 134	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))
136	135	mpteq2dva 4938	. . . . . . 7 ⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘(((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0[,]1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))
137	133, 136	eqtrd 2840	. . . . . 6 ⊢ (𝜑 → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0[,]1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))
138	125	fmpttd 6607	. . . . . . . 8 ⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)):(0[,]1)⟶(ℂ ∖ (-∞(,]0)))
139		difss 3936	. . . . . . . . 9 ⊢ (ℂ ∖ (-∞(,]0)) ⊆ ℂ
140	5	addcn 22881	. . . . . . . . . . 11 ⊢ + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
141	140	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
142		1cnd 10320	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
143		cncfmptc 22927	. . . . . . . . . . 11 ⊢ ((1 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
144	142, 22, 23, 143	syl3anc 1483	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
145	5, 141, 28, 144	cncfmpt2f 22930	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→ℂ))
146		cncffvrn 22914	. . . . . . . . 9 ⊢ (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→ℂ)) → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)):(0[,]1)⟶(ℂ ∖ (-∞(,]0))))
147	139, 145, 146	sylancr 577	. . . . . . . 8 ⊢ (𝜑 → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)):(0[,]1)⟶(ℂ ∖ (-∞(,]0))))
148	138, 147	mpbird 248	. . . . . . 7 ⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ((0[,]1)–cn→(ℂ ∖ (-∞(,]0))))
149	148, 128	cncfco 22923	. . . . . 6 ⊢ (𝜑 → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ((0[,]1)–cn→ℂ))
150	137, 149	eqeltrrd 2886	. . . . 5 ⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ((0[,]1)–cn→ℂ))
151	5, 7, 28, 150	cncfmpt2f 22930	. . . 4 ⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) ∈ ((0[,]1)–cn→ℂ))
152	20	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ ⊆ ℂ)
153	19	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (0[,]1) ⊆ ℝ)
154	123	logdmn0 24600	. . . . . . . . . . 11 ⊢ ((((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)) → (((𝐴 / 𝑁) · 𝑡) + 1) ≠ 0)
155	125, 154	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ≠ 0)
156	35, 155	logcld 24531	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℂ)
157	33, 156	subcld 10677	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]1)) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ℂ)
158	5	tgioo2 22819	. . . . . . . 8 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
159		0re 10327	. . . . . . . . 9 ⊢ 0 ∈ ℝ
160		iccntr 22837	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
161	159, 4, 160	sylancr 577	. . . . . . . 8 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
162	152, 153, 157, 158, 5, 161	dvmptntr 23948	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (ℝ D (𝑡 ∈ (0(,)1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))))
163		reelprrecn 10313	. . . . . . . . 9 ⊢ ℝ ∈ {ℝ, ℂ}
164	163	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
165	13	adantr 468	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝐴 ∈ ℂ)
166	16	adantr 468	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑁 ∈ ℂ)
167	17	adantr 468	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑁 ≠ 0)
168	165, 166, 167	divcld 11086	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝐴 / 𝑁) ∈ ℂ)
169		ioossicc 12477	. . . . . . . . . . 11 ⊢ (0(,)1) ⊆ (0[,]1)
170	169	sseli 3794	. . . . . . . . . 10 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ (0[,]1))
171	170, 32	sylan2 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
172	168, 171	mulcld 10345	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · 𝑡) ∈ ℂ)
173	13	adantr 468	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝐴 ∈ ℂ)
174	16	adantr 468	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑁 ∈ ℂ)
175	17	adantr 468	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑁 ≠ 0)
176	173, 174, 175	divcld 11086	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝐴 / 𝑁) ∈ ℂ)
177	152	sselda 3798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
178	176, 177	mulcld 10345	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ((𝐴 / 𝑁) · 𝑡) ∈ ℂ)
179		1cnd 10320	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 1 ∈ ℂ)
180	164	dvmptid 23934	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1))
181	164, 177, 179, 180, 18	dvmptcmul 23941	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 𝑡))) = (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 1)))
182	18	mulid1d 10342	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 / 𝑁) · 1) = (𝐴 / 𝑁))
183	182	mpteq2dv 4939	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 1)) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁)))
184	181, 183	eqtrd 2840	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) · 𝑡))) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁)))
185	169, 153	syl5ss 3809	. . . . . . . . 9 ⊢ (𝜑 → (0(,)1) ⊆ ℝ)
186		retop 22778	. . . . . . . . . . 11 ⊢ (topGen‘ran (,)) ∈ Top
187		iooretop 22782	. . . . . . . . . . 11 ⊢ (0(,)1) ∈ (topGen‘ran (,))
188		isopn3i 21100	. . . . . . . . . . 11 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (0(,)1) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(0(,)1)) = (0(,)1))
189	186, 187, 188	mp2an 675	. . . . . . . . . 10 ⊢ ((int‘(topGen‘ran (,)))‘(0(,)1)) = (0(,)1)
190	189	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(0(,)1)) = (0(,)1))
191	164, 178, 176, 184, 185, 158, 5, 190	dvmptres2 23939	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (𝐴 / 𝑁)))
192	170, 156	sylan2 582	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℂ)
193		1cnd 10320	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 1 ∈ ℂ)
194	172, 193	addcld 10344	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ)
195	170, 155	sylan2 582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ≠ 0)
196	194, 195	reccld 11079	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (((𝐴 / 𝑁) · 𝑡) + 1)) ∈ ℂ)
197	196, 168	mulcld 10345	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)) ∈ ℂ)
198		cnelprrecn 10314	. . . . . . . . . 10 ⊢ ℂ ∈ {ℝ, ℂ}
199	198	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℂ ∈ {ℝ, ℂ})
200	170, 125	sylan2 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ (ℂ ∖ (-∞(,]0)))
201		eldifi 3931	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ∈ ℂ)
202	201	adantl 469	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → 𝑦 ∈ ℂ)
203	123	logdmn0 24600	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ≠ 0)
204	203	adantl 469	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → 𝑦 ≠ 0)
205	202, 204	logcld 24531	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ)
206	202, 204	reccld 11079	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ ℂ)
207	178, 179	addcld 10344	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (((𝐴 / 𝑁) · 𝑡) + 1) ∈ ℂ)
208		0cnd 10318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 0 ∈ ℂ)
209	164, 142	dvmptc 23935	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 1)) = (𝑡 ∈ ℝ ↦ 0))
210	164, 178, 176, 184, 179, 208, 209	dvmptadd 23937	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) + 0)))
211	18	addid1d 10521	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 / 𝑁) + 0) = (𝐴 / 𝑁))
212	211	mpteq2dv 4939	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ ((𝐴 / 𝑁) + 0)) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁)))
213	210, 212	eqtrd 2840	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ ℝ ↦ (𝐴 / 𝑁)))
214	164, 207, 176, 213, 185, 158, 5, 190	dvmptres2 23939	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ (((𝐴 / 𝑁) · 𝑡) + 1))) = (𝑡 ∈ (0(,)1) ↦ (𝐴 / 𝑁)))
215		fvres 6427	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦) = (log‘𝑦))
216	215	mpteq2ia 4934	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘𝑦)) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))
217	131, 216	syl6req 2857	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦)) = (log ↾ (ℂ ∖ (-∞(,]0))))
218	217	oveq2d 6890	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))))
219	123	dvlog 24611	. . . . . . . . . 10 ⊢ (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦))
220	218, 219	syl6eq 2856	. . . . . . . . 9 ⊢ (𝜑 → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦)))
221		fveq2 6408	. . . . . . . . 9 ⊢ (𝑦 = (((𝐴 / 𝑁) · 𝑡) + 1) → (log‘𝑦) = (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))
222		oveq2 6882	. . . . . . . . 9 ⊢ (𝑦 = (((𝐴 / 𝑁) · 𝑡) + 1) → (1 / 𝑦) = (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))
223	164, 199, 200, 168, 205, 206, 214, 220, 221, 222	dvmptco 23949	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) = (𝑡 ∈ (0(,)1) ↦ ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
224	164, 172, 168, 191, 192, 197, 223	dvmptsub 23944	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑡 ∈ (0(,)1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))))
225	162, 224	eqtrd 2840	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))))
226	225	dmeqd 5527	. . . . 5 ⊢ (𝜑 → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = dom (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))))
227		ovex 6906	. . . . . 6 ⊢ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) ∈ V
228		eqid 2806	. . . . . 6 ⊢ (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) = (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
229	227, 228	dmmpti 6234	. . . . 5 ⊢ dom (𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) = (0(,)1)
230	226, 229	syl6eq 2856	. . . 4 ⊢ (𝜑 → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))) = (0(,)1))
231		2re 11374	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
232	231	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℝ)
233	232, 47	remulcld 10355	. . . . . . . . 9 ⊢ (𝜑 → (2 · 𝑅) ∈ ℝ)
234	8	nnrpd 12084	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℝ⁺)
235	47, 234	ltaddrpd 12119	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 < (𝑅 + 𝑅))
236	47	recnd 10353	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℂ)
237	236	2timesd 11542	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑅) = (𝑅 + 𝑅))
238	235, 237	breqtrrd 4872	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 < (2 · 𝑅))
239	47, 233, 15, 238, 87	ltletrd 10482	. . . . . . . 8 ⊢ (𝜑 → 𝑅 < 𝑁)
240		difrp 12082	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑅 < 𝑁 ↔ (𝑁 − 𝑅) ∈ ℝ⁺))
241	47, 15, 240	syl2anc 575	. . . . . . . 8 ⊢ (𝜑 → (𝑅 < 𝑁 ↔ (𝑁 − 𝑅) ∈ ℝ⁺))
242	239, 241	mpbid 223	. . . . . . 7 ⊢ (𝜑 → (𝑁 − 𝑅) ∈ ℝ⁺)
243	242	rprecred 12097	. . . . . 6 ⊢ (𝜑 → (1 / (𝑁 − 𝑅)) ∈ ℝ)
244	14	nnrecred 11352	. . . . . 6 ⊢ (𝜑 → (1 / 𝑁) ∈ ℝ)
245	243, 244	resubcld 10743	. . . . 5 ⊢ (𝜑 → ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)) ∈ ℝ)
246	47, 245	remulcld 10355	. . . 4 ⊢ (𝜑 → (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ∈ ℝ)
247	225	fveq1d 6410	. . . . . . 7 ⊢ (𝜑 → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦) = ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦))
248	247	fveq2d 6412	. . . . . 6 ⊢ (𝜑 → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦)) = (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)))
249	248	adantr 468	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦)) = (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)))
250		nfv 2005	. . . . . . 7 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑦 ∈ (0(,)1))
251		nfcv 2948	. . . . . . . . 9 ⊢ Ⅎ𝑡abs
252		nffvmpt1 6419	. . . . . . . . 9 ⊢ Ⅎ𝑡((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)
253	251, 252	nffv 6418	. . . . . . . 8 ⊢ Ⅎ𝑡(abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦))
254		nfcv 2948	. . . . . . . 8 ⊢ Ⅎ𝑡 ≤
255		nfcv 2948	. . . . . . . 8 ⊢ Ⅎ𝑡(𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))
256	253, 254, 255	nfbr 4891	. . . . . . 7 ⊢ Ⅎ𝑡(abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))
257	250, 256	nfim 1987	. . . . . 6 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑦 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))
258		eleq1w 2868	. . . . . . . 8 ⊢ (𝑡 = 𝑦 → (𝑡 ∈ (0(,)1) ↔ 𝑦 ∈ (0(,)1)))
259	258	anbi2d 616	. . . . . . 7 ⊢ (𝑡 = 𝑦 → ((𝜑 ∧ 𝑡 ∈ (0(,)1)) ↔ (𝜑 ∧ 𝑦 ∈ (0(,)1))))
260		2fveq3 6413	. . . . . . . 8 ⊢ (𝑡 = 𝑦 → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) = (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)))
261	260	breq1d 4854	. . . . . . 7 ⊢ (𝑡 = 𝑦 → ((abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ↔ (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))))
262	259, 261	imbi12d 335	. . . . . 6 ⊢ (𝑡 = 𝑦 → (((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) ↔ ((𝜑 ∧ 𝑦 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))))
263		simpr 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0(,)1))
264	228	fvmpt2 6512	. . . . . . . . . 10 ⊢ ((𝑡 ∈ (0(,)1) ∧ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) ∈ V) → ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡) = ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
265	263, 227, 264	sylancl 576	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡) = ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
266	265	fveq2d 6412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) = (abs‘((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))))
267	168, 193, 196	subdid 10771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = (((𝐴 / 𝑁) · 1) − ((𝐴 / 𝑁) · (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))))
268	168	mulid1d 10342	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · 1) = (𝐴 / 𝑁))
269	168, 196	mulcomd 10346	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))
270	268, 269	oveq12d 6892	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 1) − ((𝐴 / 𝑁) · (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))
271	267, 270	eqtr2d 2841	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))) = ((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))))
272	271	fveq2d 6412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁)))) = (abs‘((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))))
273	165, 166, 167	absdivd 14417	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(𝐴 / 𝑁)) = ((abs‘𝐴) / (abs‘𝑁)))
274	15	adantr 468	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑁 ∈ ℝ)
275	59	adantr 468	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 0 ≤ 𝑁)
276	274, 275	absidd 14384	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘𝑁) = 𝑁)
277	276	oveq2d 6890	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘𝐴) / (abs‘𝑁)) = ((abs‘𝐴) / 𝑁))
278	273, 277	eqtrd 2840	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(𝐴 / 𝑁)) = ((abs‘𝐴) / 𝑁))
279	278	oveq1d 6889	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘(𝐴 / 𝑁)) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) = (((abs‘𝐴) / 𝑁) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))))
280	193, 196	subcld 10677	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) ∈ ℂ)
281	168, 280	absmuld 14416	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) = ((abs‘(𝐴 / 𝑁)) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))))
282	63	adantr 468	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘𝐴) ∈ ℝ)
283	282	recnd 10353	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘𝐴) ∈ ℂ)
284	280	abscld 14398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) ∈ ℝ)
285	284	recnd 10353	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) ∈ ℂ)
286	283, 285, 166, 167	div23d 11123	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁) = (((abs‘𝐴) / 𝑁) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))))
287	279, 281, 286	3eqtr4d 2850	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) = (((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁))
288	266, 272, 287	3eqtrd 2844	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) = (((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁))
289	47	adantr 468	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑅 ∈ ℝ)
290	243	adantr 468	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (𝑁 − 𝑅)) ∈ ℝ)
291	244	adantr 468	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / 𝑁) ∈ ℝ)
292	290, 291	resubcld 10743	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)) ∈ ℝ)
293	274, 292	remulcld 10355	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ∈ ℝ)
294	13	absge0d 14406	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ (abs‘𝐴))
295	294	adantr 468	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 0 ≤ (abs‘𝐴))
296	280	absge0d 14406	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 0 ≤ (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))))
297	73	adantr 468	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘𝐴) ≤ 𝑅)
298	242	adantr 468	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 − 𝑅) ∈ ℝ⁺)
299	234	adantr 468	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑅 ∈ ℝ⁺)
300	298, 299	rpdivcld 12103	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / 𝑅) ∈ ℝ⁺)
301	12	dmgmn0 24966	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ≠ 0)
302	301	adantr 468	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝐴 ≠ 0)
303	165, 166, 302, 167	divne0d 11102	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝐴 / 𝑁) ≠ 0)
304		eliooord 12451	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (0(,)1) → (0 < 𝑡 ∧ 𝑡 < 1))
305	304	adantl 469	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (0 < 𝑡 ∧ 𝑡 < 1))
306	305	simpld 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 0 < 𝑡)
307	306	gt0ne0d 10877	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ≠ 0)
308	168, 171, 303, 307	mulne0d 10964	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝐴 / 𝑁) · 𝑡) ≠ 0)
309	172, 308	reccld 11079	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / ((𝐴 / 𝑁) · 𝑡)) ∈ ℂ)
310	193, 309	addcld 10344	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 + (1 / ((𝐴 / 𝑁) · 𝑡))) ∈ ℂ)
311	172, 193, 172, 308	divdird 11124	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡)) = ((((𝐴 / 𝑁) · 𝑡) / ((𝐴 / 𝑁) · 𝑡)) + (1 / ((𝐴 / 𝑁) · 𝑡))))
312	172, 308	dividd 11084	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((𝐴 / 𝑁) · 𝑡) / ((𝐴 / 𝑁) · 𝑡)) = 1)
313	312	oveq1d 6889	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) / ((𝐴 / 𝑁) · 𝑡)) + (1 / ((𝐴 / 𝑁) · 𝑡))) = (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))
314	311, 313	eqtrd 2840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡)) = (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))
315	194, 172, 195, 308	divne0d 11102	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡)) ≠ 0)
316	314, 315	eqnetrrd 3046	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 + (1 / ((𝐴 / 𝑁) · 𝑡))) ≠ 0)
317	310, 316	absrpcld 14410	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) ∈ ℝ⁺)
318		1red 10326	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 1 ∈ ℝ)
319		0le1 10836	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 1
320	319	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 0 ≤ 1)
321	300	rpred 12086	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / 𝑅) ∈ ℝ)
322	309	negcld 10664	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → -(1 / ((𝐴 / 𝑁) · 𝑡)) ∈ ℂ)
323	322	abscld 14398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) ∈ ℝ)
324	323, 318	resubcld 10743	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1) ∈ ℝ)
325	310	abscld 14398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) ∈ ℝ)
326	236	adantr 468	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑅 ∈ ℂ)
327	299	rpne0d 12091	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑅 ≠ 0)
328	166, 326, 326, 327	divsubdird 11125	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / 𝑅) = ((𝑁 / 𝑅) − (𝑅 / 𝑅)))
329	326, 327	dividd 11084	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑅 / 𝑅) = 1)
330	329	oveq2d 6890	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 / 𝑅) − (𝑅 / 𝑅)) = ((𝑁 / 𝑅) − 1))
331	328, 330	eqtrd 2840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / 𝑅) = ((𝑁 / 𝑅) − 1))
332	274, 299	rerpdivcld 12117	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 / 𝑅) ∈ ℝ)
333	326, 166, 327, 167	recdivd 11103	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (𝑅 / 𝑁)) = (𝑁 / 𝑅))
334	170, 86	sylan2 582	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (𝑅 / 𝑁))
335	172, 308	absrpcld 14410	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝐴 / 𝑁) · 𝑡)) ∈ ℝ⁺)
336	58	adantr 468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → 𝑁 ∈ ℝ⁺)
337	299, 336	rpdivcld 12103	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑅 / 𝑁) ∈ ℝ⁺)
338	335, 337	lerecd 12105	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘((𝐴 / 𝑁) · 𝑡)) ≤ (𝑅 / 𝑁) ↔ (1 / (𝑅 / 𝑁)) ≤ (1 / (abs‘((𝐴 / 𝑁) · 𝑡)))))
339	334, 338	mpbid 223	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (𝑅 / 𝑁)) ≤ (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))
340	333, 339	eqbrtrrd 4868	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 / 𝑅) ≤ (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))
341	309	absnegd 14411	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) = (abs‘(1 / ((𝐴 / 𝑁) · 𝑡))))
342	193, 172, 308	absdivd 14417	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 / ((𝐴 / 𝑁) · 𝑡))) = ((abs‘1) / (abs‘((𝐴 / 𝑁) · 𝑡))))
343		abs1 14260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (abs‘1) = 1
344	343	oveq1i 6884	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs‘1) / (abs‘((𝐴 / 𝑁) · 𝑡))) = (1 / (abs‘((𝐴 / 𝑁) · 𝑡)))
345	342, 344	syl6eq 2856	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 / ((𝐴 / 𝑁) · 𝑡))) = (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))
346	341, 345	eqtrd 2840	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) = (1 / (abs‘((𝐴 / 𝑁) · 𝑡))))
347	340, 346	breqtrrd 4872	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 / 𝑅) ≤ (abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))))
348	332, 323, 318, 347	lesub1dd 10928	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 / 𝑅) − 1) ≤ ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1))
349	331, 348	eqbrtrd 4866	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / 𝑅) ≤ ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1))
350	343	oveq2i 6885	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − (abs‘1)) = ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1)
351	322, 193	abs2difd 14419	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − (abs‘1)) ≤ (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)))
352	350, 351	syl5eqbrr 4880	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1) ≤ (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)))
353	193, 309	addcomd 10523	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 + (1 / ((𝐴 / 𝑁) · 𝑡))) = ((1 / ((𝐴 / 𝑁) · 𝑡)) + 1))
354	353	negeqd 10560	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → -(1 + (1 / ((𝐴 / 𝑁) · 𝑡))) = -((1 / ((𝐴 / 𝑁) · 𝑡)) + 1))
355	309, 193	negdi2d 10691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → -((1 / ((𝐴 / 𝑁) · 𝑡)) + 1) = (-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1))
356	354, 355	eqtrd 2840	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → -(1 + (1 / ((𝐴 / 𝑁) · 𝑡))) = (-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1))
357	356	fveq2d 6412	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘-(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) = (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)))
358	310	absnegd 14411	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘-(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))) = (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
359	357, 358	eqtr3d 2842	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(-(1 / ((𝐴 / 𝑁) · 𝑡)) − 1)) = (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
360	352, 359	breqtrd 4870	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘-(1 / ((𝐴 / 𝑁) · 𝑡))) − 1) ≤ (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
361	321, 324, 325, 349, 360	letrd 10479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / 𝑅) ≤ (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
362	300, 317, 318, 320, 361	lediv2ad 12108	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) ≤ (1 / ((𝑁 − 𝑅) / 𝑅)))
363	16, 236	subcld 10677	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 𝑅) ∈ ℂ)
364	363	adantr 468	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 − 𝑅) ∈ ℂ)
365	47, 239	gtned 10457	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ≠ 𝑅)
366	16, 236, 365	subne0d 10686	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 𝑅) ≠ 0)
367	366	adantr 468	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 − 𝑅) ≠ 0)
368	364, 326, 367, 327	recdivd 11103	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / ((𝑁 − 𝑅) / 𝑅)) = (𝑅 / (𝑁 − 𝑅)))
369	166, 326	nncand 10682	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 − (𝑁 − 𝑅)) = 𝑅)
370	369	oveq1d 6889	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − (𝑁 − 𝑅)) / (𝑁 − 𝑅)) = (𝑅 / (𝑁 − 𝑅)))
371	166, 364, 364, 367	divsubdird 11125	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − (𝑁 − 𝑅)) / (𝑁 − 𝑅)) = ((𝑁 / (𝑁 − 𝑅)) − ((𝑁 − 𝑅) / (𝑁 − 𝑅))))
372	370, 371	eqtr3d 2842	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑅 / (𝑁 − 𝑅)) = ((𝑁 / (𝑁 − 𝑅)) − ((𝑁 − 𝑅) / (𝑁 − 𝑅))))
373	364, 367	dividd 11084	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 − 𝑅) / (𝑁 − 𝑅)) = 1)
374	373	oveq2d 6890	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 / (𝑁 − 𝑅)) − ((𝑁 − 𝑅) / (𝑁 − 𝑅))) = ((𝑁 / (𝑁 − 𝑅)) − 1))
375	368, 372, 374	3eqtrd 2844	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / ((𝑁 − 𝑅) / 𝑅)) = ((𝑁 / (𝑁 − 𝑅)) − 1))
376	362, 375	breqtrd 4870	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) ≤ ((𝑁 / (𝑁 − 𝑅)) − 1))
377	194, 193, 194, 195	divsubdird 11125	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((((𝐴 / 𝑁) · 𝑡) + 1) − 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) = (((((𝐴 / 𝑁) · 𝑡) + 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))
378	172, 193	pncand 10678	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) − 1) = ((𝐴 / 𝑁) · 𝑡))
379	378	oveq1d 6889	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((((𝐴 / 𝑁) · 𝑡) + 1) − 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) = (((𝐴 / 𝑁) · 𝑡) / (((𝐴 / 𝑁) · 𝑡) + 1)))
380	194, 195	dividd 11084	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((𝐴 / 𝑁) · 𝑡) + 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) = 1)
381	380	oveq1d 6889	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((((𝐴 / 𝑁) · 𝑡) + 1) / (((𝐴 / 𝑁) · 𝑡) + 1)) − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))
382	377, 379, 381	3eqtr3rd 2849	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = (((𝐴 / 𝑁) · 𝑡) / (((𝐴 / 𝑁) · 𝑡) + 1)))
383	194, 172, 195, 308	recdivd 11103	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡))) = (((𝐴 / 𝑁) · 𝑡) / (((𝐴 / 𝑁) · 𝑡) + 1)))
384	314	oveq2d 6890	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / ((((𝐴 / 𝑁) · 𝑡) + 1) / ((𝐴 / 𝑁) · 𝑡))) = (1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
385	382, 383, 384	3eqtr2d 2846	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))) = (1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
386	385	fveq2d 6412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = (abs‘(1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))))
387	193, 310, 316	absdivd 14417	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) = ((abs‘1) / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))))
388	343	oveq1i 6884	. . . . . . . . . . . . 13 ⊢ ((abs‘1) / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) = (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡)))))
389	387, 388	syl6eq 2856	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 / (1 + (1 / ((𝐴 / 𝑁) · 𝑡))))) = (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))))
390	386, 389	eqtrd 2840	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) = (1 / (abs‘(1 + (1 / ((𝐴 / 𝑁) · 𝑡))))))
391	363, 366	reccld 11079	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / (𝑁 − 𝑅)) ∈ ℂ)
392	391	adantr 468	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / (𝑁 − 𝑅)) ∈ ℂ)
393	244	recnd 10353	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 𝑁) ∈ ℂ)
394	393	adantr 468	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (1 / 𝑁) ∈ ℂ)
395	166, 392, 394	subdid 10771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) = ((𝑁 · (1 / (𝑁 − 𝑅))) − (𝑁 · (1 / 𝑁))))
396	166, 364, 367	divrecd 11089	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 / (𝑁 − 𝑅)) = (𝑁 · (1 / (𝑁 − 𝑅))))
397	396	eqcomd 2812	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 · (1 / (𝑁 − 𝑅))) = (𝑁 / (𝑁 − 𝑅)))
398	166, 167	recidd 11081	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 · (1 / 𝑁)) = 1)
399	397, 398	oveq12d 6892	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((𝑁 · (1 / (𝑁 − 𝑅))) − (𝑁 · (1 / 𝑁))) = ((𝑁 / (𝑁 − 𝑅)) − 1))
400	395, 399	eqtrd 2840	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑁 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) = ((𝑁 / (𝑁 − 𝑅)) − 1))
401	376, 390, 400	3brtr4d 4876	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1)))) ≤ (𝑁 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))
402	282, 289, 284, 293, 295, 296, 297, 401	lemul12ad 11251	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ≤ (𝑅 · (𝑁 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))))
403	245	recnd 10353	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)) ∈ ℂ)
404	403	adantr 468	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)) ∈ ℂ)
405	326, 166, 404	mul12d 10530	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑅 · (𝑁 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) = (𝑁 · (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))))
406	402, 405	breqtrd 4870	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ≤ (𝑁 · (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))))
407	282, 284	remulcld 10355	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ∈ ℝ)
408	246	adantr 468	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ∈ ℝ)
409	407, 408, 336	ledivmuld 12139	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → ((((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ↔ ((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) ≤ (𝑁 · (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))))
410	406, 409	mpbird 248	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (((abs‘𝐴) · (abs‘(1 − (1 / (((𝐴 / 𝑁) · 𝑡) + 1))))) / 𝑁) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))
411	288, 410	eqbrtrd 4866	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑡)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))
412	257, 262, 411	chvar 2436	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (0(,)1)) → (abs‘((𝑡 ∈ (0(,)1) ↦ ((𝐴 / 𝑁) − ((1 / (((𝐴 / 𝑁) · 𝑡) + 1)) · (𝐴 / 𝑁))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))
413	249, 412	eqbrtrd 4866	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))‘𝑦)) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))
414	3, 4, 151, 230, 246, 413	dvlip 23970	. . 3 ⊢ ((𝜑 ∧ (1 ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0))) ≤ ((𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))))
415	1, 2, 414	mpanr12 688	. 2 ⊢ (𝜑 → (abs‘(((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0))) ≤ ((𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))))
416		eqidd 2807	. . . . . 6 ⊢ (𝜑 → (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))) = (𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1)))))
417		oveq2 6882	. . . . . . . 8 ⊢ (𝑡 = 1 → ((𝐴 / 𝑁) · 𝑡) = ((𝐴 / 𝑁) · 1))
418	417, 182	sylan9eqr 2862	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 = 1) → ((𝐴 / 𝑁) · 𝑡) = (𝐴 / 𝑁))
419	418	fvoveq1d 6896	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 = 1) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘((𝐴 / 𝑁) + 1)))
420	418, 419	oveq12d 6892	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 = 1) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) = ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))
421	1	a1i 11	. . . . . 6 ⊢ (𝜑 → 1 ∈ (0[,]1))
422		ovexd 6908	. . . . . 6 ⊢ (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) ∈ V)
423	416, 420, 421, 422	fvmptd 6509	. . . . 5 ⊢ (𝜑 → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) = ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))
424		oveq2 6882	. . . . . . . . 9 ⊢ (𝑡 = 0 → ((𝐴 / 𝑁) · 𝑡) = ((𝐴 / 𝑁) · 0))
425	18	mul01d 10520	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 / 𝑁) · 0) = 0)
426	424, 425	sylan9eqr 2862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 = 0) → ((𝐴 / 𝑁) · 𝑡) = 0)
427	426	oveq1d 6889	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) + 1) = (0 + 1))
428		0p1e1 11414	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
429	427, 428	syl6eq 2856	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) + 1) = 1)
430	429	fveq2d 6412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 = 0) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) = (log‘1))
431		log1 24546	. . . . . . . . 9 ⊢ (log‘1) = 0
432	430, 431	syl6eq 2856	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 = 0) → (log‘(((𝐴 / 𝑁) · 𝑡) + 1)) = 0)
433	426, 432	oveq12d 6892	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) = (0 − 0))
434		0m0e0 11412	. . . . . . 7 ⊢ (0 − 0) = 0
435	433, 434	syl6eq 2856	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 = 0) → (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))) = 0)
436	2	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ (0[,]1))
437	416, 435, 436, 436	fvmptd 6509	. . . . 5 ⊢ (𝜑 → ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0) = 0)
438	423, 437	oveq12d 6892	. . . 4 ⊢ (𝜑 → (((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0)) = (((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) − 0))
439	18, 142	addcld 10344	. . . . . . 7 ⊢ (𝜑 → ((𝐴 / 𝑁) + 1) ∈ ℂ)
440	12, 14	dmgmdivn0 24968	. . . . . . 7 ⊢ (𝜑 → ((𝐴 / 𝑁) + 1) ≠ 0)
441	439, 440	logcld 24531	. . . . . 6 ⊢ (𝜑 → (log‘((𝐴 / 𝑁) + 1)) ∈ ℂ)
442	18, 441	subcld 10677	. . . . 5 ⊢ (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) ∈ ℂ)
443	442	subid1d 10666	. . . 4 ⊢ (𝜑 → (((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) − 0) = ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))
444	438, 443	eqtr2d 2841	. . 3 ⊢ (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) = (((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0)))
445	444	fveq2d 6412	. 2 ⊢ (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) = (abs‘(((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (((𝐴 / 𝑁) · 𝑡) − (log‘(((𝐴 / 𝑁) · 𝑡) + 1))))‘0))))
446		1m0e1 11413	. . . . . 6 ⊢ (1 − 0) = 1
447	446	fveq2i 6411	. . . . 5 ⊢ (abs‘(1 − 0)) = (abs‘1)
448	447, 343	eqtri 2828	. . . 4 ⊢ (abs‘(1 − 0)) = 1
449	448	oveq2i 6885	. . 3 ⊢ ((𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))) = ((𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) · 1)
450	236, 403	mulcld 10345	. . . 4 ⊢ (𝜑 → (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ∈ ℂ)
451	450	mulid1d 10342	. . 3 ⊢ (𝜑 → ((𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) · 1) = (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))
452	449, 451	syl5req 2853	. 2 ⊢ (𝜑 → (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) = ((𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) · (abs‘(1 − 0))))
453	415, 445, 452	3brtr4d 4876	1 ⊢ (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 197 ∧ wa 384 = wceq 1637 ∈ wcel 2156 ≠ wne 2978 ∀wral 3096 {crab 3100 Vcvv 3391 ∖ cdif 3766 ⊆ wss 3769 {cpr 4372 class class class wbr 4844 ↦ cmpt 4923 dom cdm 5311 ran crn 5312 ↾ cres 5313 ∘ ccom 5315 ⟶wf 6097 ‘cfv 6101 (class class class)co 6874 ℂcc 10219 ℝcr 10220 0cc0 10221 1c1 10222 + caddc 10224 · cmul 10226 -∞cmnf 10357 < clt 10359 ≤ cle 10360 − cmin 10551 -cneg 10552 / cdiv 10969 ℕcn 11305 2c2 11356 ℕ₀cn0 11559 ℤcz 11643 ℝ⁺crp 12046 (,)cioo 12393 (,]cioc 12394 [,]cicc 12396 ℜcre 14060 abscabs 14197 TopOpenctopn 16287 topGenctg 16303 ℂ_fldccnfld 19954 Topctop 20911 intcnt 21035 Cn ccn 21242 ×_t ctx 21577 –cn→ccncf 22892 D cdv 23841 logclog 24515

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2068 ax-7 2104 ax-8 2158 ax-9 2165 ax-10 2185 ax-11 2201 ax-12 2214 ax-13 2420 ax-ext 2784 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5096 ax-un 7179 ax-inf2 8785 ax-cnex 10277 ax-resscn 10278 ax-1cn 10279 ax-icn 10280 ax-addcl 10281 ax-addrcl 10282 ax-mulcl 10283 ax-mulrcl 10284 ax-mulcom 10285 ax-addass 10286 ax-mulass 10287 ax-distr 10288 ax-i2m1 10289 ax-1ne0 10290 ax-1rid 10291 ax-rnegex 10292 ax-rrecex 10293 ax-cnre 10294 ax-pre-lttri 10295 ax-pre-lttrn 10296 ax-pre-ltadd 10297 ax-pre-mulgt0 10298 ax-pre-sup 10299 ax-addf 10300 ax-mulf 10301

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3or 1101 df-3an 1102 df-tru 1641 df-fal 1651 df-ex 1860 df-nf 1864 df-sb 2061 df-eu 2634 df-mo 2635 df-clab 2793 df-cleq 2799 df-clel 2802 df-nfc 2937 df-ne 2979 df-nel 3082 df-ral 3101 df-rex 3102 df-reu 3103 df-rmo 3104 df-rab 3105 df-v 3393 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-nul 4117 df-if 4280 df-pw 4353 df-sn 4371 df-pr 4373 df-tp 4375 df-op 4377 df-uni 4631 df-int 4670 df-iun 4714 df-iin 4715 df-br 4845 df-opab 4907 df-mpt 4924 df-tr 4947 df-id 5219 df-eprel 5224 df-po 5232 df-so 5233 df-fr 5270 df-se 5271 df-we 5272 df-xp 5317 df-rel 5318 df-cnv 5319 df-co 5320 df-dm 5321 df-rn 5322 df-res 5323 df-ima 5324 df-pred 5893 df-ord 5939 df-on 5940 df-lim 5941 df-suc 5942 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-isom 6110 df-riota 6835 df-ov 6877 df-oprab 6878 df-mpt2 6879 df-of 7127 df-om 7296 df-1st 7398 df-2nd 7399 df-supp 7530 df-wrecs 7642 df-recs 7704 df-rdg 7742 df-1o 7796 df-2o 7797 df-oadd 7800 df-er 7979 df-map 8094 df-pm 8095 df-ixp 8146 df-en 8193 df-dom 8194 df-sdom 8195 df-fin 8196 df-fsupp 8515 df-fi 8556 df-sup 8587 df-inf 8588 df-oi 8654 df-card 9048 df-cda 9275 df-pnf 10361 df-mnf 10362 df-xr 10363 df-ltxr 10364 df-le 10365 df-sub 10553 df-neg 10554 df-div 10970 df-nn 11306 df-2 11364 df-3 11365 df-4 11366 df-5 11367 df-6 11368 df-7 11369 df-8 11370 df-9 11371 df-n0 11560 df-z 11644 df-dec 11760 df-uz 11905 df-q 12008 df-rp 12047 df-xneg 12162 df-xadd 12163 df-xmul 12164 df-ioo 12397 df-ioc 12398 df-ico 12399 df-icc 12400 df-fz 12550 df-fzo 12690 df-fl 12817 df-mod 12893 df-seq 13025 df-exp 13084 df-fac 13281 df-bc 13310 df-hash 13338 df-shft 14030 df-cj 14062 df-re 14063 df-im 14064 df-sqrt 14198 df-abs 14199 df-limsup 14425 df-clim 14442 df-rlim 14443 df-sum 14640 df-ef 15018 df-sin 15020 df-cos 15021 df-tan 15022 df-pi 15023 df-struct 16070 df-ndx 16071 df-slot 16072 df-base 16074 df-sets 16075 df-ress 16076 df-plusg 16166 df-mulr 16167 df-starv 16168 df-sca 16169 df-vsca 16170 df-ip 16171 df-tset 16172 df-ple 16173 df-ds 16175 df-unif 16176 df-hom 16177 df-cco 16178 df-rest 16288 df-topn 16289 df-0g 16307 df-gsum 16308 df-topgen 16309 df-pt 16310 df-prds 16313 df-xrs 16367 df-qtop 16372 df-imas 16373 df-xps 16375 df-mre 16451 df-mrc 16452 df-acs 16454 df-mgm 17447 df-sgrp 17489 df-mnd 17500 df-submnd 17541 df-mulg 17746 df-cntz 17951 df-cmn 18396 df-psmet 19946 df-xmet 19947 df-met 19948 df-bl 19949 df-mopn 19950 df-fbas 19951 df-fg 19952 df-cnfld 19955 df-top 20912 df-topon 20929 df-topsp 20951 df-bases 20964 df-cld 21037 df-ntr 21038 df-cls 21039 df-nei 21116 df-lp 21154 df-perf 21155 df-cn 21245 df-cnp 21246 df-haus 21333 df-cmp 21404 df-tx 21579 df-hmeo 21772 df-fil 21863 df-fm 21955 df-flim 21956 df-flf 21957 df-xms 22338 df-ms 22339 df-tms 22340 df-cncf 22894 df-limc 23844 df-dv 23845 df-log 24517

This theorem is referenced by: lgamgulmlem3 24971

W3C validator