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

Theorem logtayllem 24695
Description: Lemma for logtayl 24696. (Contributed by Mario Carneiro, 1-Apr-2015.)
Assertion
Ref Expression
logtayllem ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))) ∈ dom ⇝ )
Distinct variable group:   𝐴,𝑛

Proof of Theorem logtayllem
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 nn0uz 11921 . 2 0 = (ℤ‘0)
2 1nn0 11555 . . 3 1 ∈ ℕ0
32a1i 11 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ ℕ0)
4 oveq2 6849 . . . . 5 (𝑛 = 𝑘 → ((abs‘𝐴)↑𝑛) = ((abs‘𝐴)↑𝑘))
5 eqid 2764 . . . . 5 (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))
6 ovex 6873 . . . . 5 ((abs‘𝐴)↑𝑘) ∈ V
74, 5, 6fvmpt 6470 . . . 4 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘))
87adantl 473 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘))
9 abscl 14304 . . . . 5 (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
109adantr 472 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘𝐴) ∈ ℝ)
11 reexpcl 13083 . . . 4 (((abs‘𝐴) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((abs‘𝐴)↑𝑘) ∈ ℝ)
1210, 11sylan 575 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → ((abs‘𝐴)↑𝑘) ∈ ℝ)
138, 12eqeltrd 2843 . 2 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘) ∈ ℝ)
14 eqeq1 2768 . . . . . . 7 (𝑛 = 𝑘 → (𝑛 = 0 ↔ 𝑘 = 0))
15 oveq2 6849 . . . . . . 7 (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
1614, 15ifbieq2d 4267 . . . . . 6 (𝑛 = 𝑘 → if(𝑛 = 0, 0, (1 / 𝑛)) = if(𝑘 = 0, 0, (1 / 𝑘)))
17 oveq2 6849 . . . . . 6 (𝑛 = 𝑘 → (𝐴𝑛) = (𝐴𝑘))
1816, 17oveq12d 6859 . . . . 5 (𝑛 = 𝑘 → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
19 eqid 2764 . . . . 5 (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛))) = (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
20 ovex 6873 . . . . 5 (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) ∈ V
2118, 19, 20fvmpt 6470 . . . 4 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
2221adantl 473 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
23 0cnd 10285 . . . . 5 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 = 0) → 0 ∈ ℂ)
24 nn0cn 11548 . . . . . . 7 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
2524adantl 473 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
26 df-ne 2937 . . . . . . 7 (𝑘 ≠ 0 ↔ ¬ 𝑘 = 0)
2726biimpri 219 . . . . . 6 𝑘 = 0 → 𝑘 ≠ 0)
28 reccl 10945 . . . . . 6 ((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) → (1 / 𝑘) ∈ ℂ)
2925, 27, 28syl2an 589 . . . . 5 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 = 0) → (1 / 𝑘) ∈ ℂ)
3023, 29ifclda 4276 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → if(𝑘 = 0, 0, (1 / 𝑘)) ∈ ℂ)
31 expcl 13084 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
3231adantlr 706 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
3330, 32mulcld 10313 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) ∈ ℂ)
3422, 33eqeltrd 2843 . 2 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘) ∈ ℂ)
3510recnd 10321 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘𝐴) ∈ ℂ)
36 absidm 14349 . . . . . 6 (𝐴 ∈ ℂ → (abs‘(abs‘𝐴)) = (abs‘𝐴))
3736adantr 472 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘(abs‘𝐴)) = (abs‘𝐴))
38 simpr 477 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘𝐴) < 1)
3937, 38eqbrtrd 4830 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘(abs‘𝐴)) < 1)
4035, 39, 8geolim 14886 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ⇝ (1 / (1 − (abs‘𝐴))))
41 seqex 13009 . . . 4 seq0( + , (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ∈ V
42 ovex 6873 . . . 4 (1 / (1 − (abs‘𝐴))) ∈ V
4341, 42breldm 5496 . . 3 (seq0( + , (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ⇝ (1 / (1 − (abs‘𝐴))) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ∈ dom ⇝ )
4440, 43syl 17 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ∈ dom ⇝ )
45 1red 10293 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ ℝ)
46 elnnuz 11923 . . 3 (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ‘1))
47 nnrecre 11313 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
4847adantl 473 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℝ)
4948recnd 10321 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℂ)
50 nnnn0 11545 . . . . . . . 8 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
5150, 32sylan2 586 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (𝐴𝑘) ∈ ℂ)
5249, 51absmuld 14479 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘((1 / 𝑘) · (𝐴𝑘))) = ((abs‘(1 / 𝑘)) · (abs‘(𝐴𝑘))))
53 nnrp 12040 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
5453adantl 473 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
5554rpreccld 12079 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℝ+)
5655rpge0d 12073 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 0 ≤ (1 / 𝑘))
5748, 56absidd 14447 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘(1 / 𝑘)) = (1 / 𝑘))
58 simpl 474 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ ℂ)
59 absexp 14330 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (abs‘(𝐴𝑘)) = ((abs‘𝐴)↑𝑘))
6058, 50, 59syl2an 589 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘(𝐴𝑘)) = ((abs‘𝐴)↑𝑘))
6157, 60oveq12d 6859 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ((abs‘(1 / 𝑘)) · (abs‘(𝐴𝑘))) = ((1 / 𝑘) · ((abs‘𝐴)↑𝑘)))
6252, 61eqtrd 2798 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘((1 / 𝑘) · (𝐴𝑘))) = ((1 / 𝑘) · ((abs‘𝐴)↑𝑘)))
63 1red 10293 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
6450, 12sylan2 586 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ((abs‘𝐴)↑𝑘) ∈ ℝ)
6551absge0d 14469 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 0 ≤ (abs‘(𝐴𝑘)))
6665, 60breqtrd 4834 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 0 ≤ ((abs‘𝐴)↑𝑘))
67 nnge1 11302 . . . . . . . . 9 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
6867adantl 473 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘)
69 0lt1 10803 . . . . . . . . . 10 0 < 1
7069a1i 11 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 0 < 1)
71 nnre 11281 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
7271adantl 473 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
73 nngt0 11305 . . . . . . . . . 10 (𝑘 ∈ ℕ → 0 < 𝑘)
7473adantl 473 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 0 < 𝑘)
75 lerec 11159 . . . . . . . . 9 (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → (1 ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / 1)))
7663, 70, 72, 74, 75syl22anc 867 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / 1)))
7768, 76mpbid 223 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ≤ (1 / 1))
78 1div1e1 10970 . . . . . . 7 (1 / 1) = 1
7977, 78syl6breq 4849 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ≤ 1)
8048, 63, 64, 66, 79lemul1ad 11216 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑘) · ((abs‘𝐴)↑𝑘)) ≤ (1 · ((abs‘𝐴)↑𝑘)))
8162, 80eqbrtrd 4830 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘((1 / 𝑘) · (𝐴𝑘))) ≤ (1 · ((abs‘𝐴)↑𝑘)))
8250, 22sylan2 586 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
83 nnne0 11309 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
8483adantl 473 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ≠ 0)
8584neneqd 2941 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ¬ 𝑘 = 0)
8685iffalsed 4253 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → if(𝑘 = 0, 0, (1 / 𝑘)) = (1 / 𝑘))
8786oveq1d 6856 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) = ((1 / 𝑘) · (𝐴𝑘)))
8882, 87eqtrd 2798 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘) = ((1 / 𝑘) · (𝐴𝑘)))
8988fveq2d 6378 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘)) = (abs‘((1 / 𝑘) · (𝐴𝑘))))
9050, 8sylan2 586 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘))
9190oveq2d 6857 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 · ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘)) = (1 · ((abs‘𝐴)↑𝑘)))
9281, 89, 913brtr4d 4840 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘)) ≤ (1 · ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘)))
9346, 92sylan2br 588 . 2 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ (ℤ‘1)) → (abs‘((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘)) ≤ (1 · ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘)))
941, 3, 13, 34, 44, 45, 93cvgcmpce 14835 1 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))) ∈ dom ⇝ )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wne 2936  ifcif 4242   class class class wbr 4808  cmpt 4887  dom cdm 5276  cfv 6067  (class class class)co 6841  cc 10186  cr 10187  0cc0 10188  1c1 10189   + caddc 10191   · cmul 10193   < clt 10327  cle 10328  cmin 10519   / cdiv 10937  cn 11273  0cn0 11537  cuz 11885  +crp 12027  seqcseq 13007  cexp 13066  abscabs 14260  cli 14501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266  ax-addf 10267  ax-mulf 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-oadd 7767  df-er 7946  df-pm 8062  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-sup 8554  df-inf 8555  df-oi 8621  df-card 9015  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-n0 11538  df-z 11624  df-uz 11886  df-rp 12028  df-ico 12382  df-fz 12533  df-fzo 12673  df-fl 12800  df-seq 13008  df-exp 13067  df-hash 13321  df-cj 14125  df-re 14126  df-im 14127  df-sqrt 14261  df-abs 14262  df-limsup 14488  df-clim 14505  df-rlim 14506  df-sum 14703
This theorem is referenced by:  logtayl  24696
  Copyright terms: Public domain W3C validator