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

Theorem logtayllem 24322
 Description: Lemma for logtayl 24323. (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 11674 . 2 0 = (ℤ‘0)
2 1nn0 11260 . . 3 1 ∈ ℕ0
32a1i 11 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ ℕ0)
4 oveq2 6618 . . . . 5 (𝑛 = 𝑘 → ((abs‘𝐴)↑𝑛) = ((abs‘𝐴)↑𝑘))
5 eqid 2621 . . . . 5 (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))
6 ovex 6638 . . . . 5 ((abs‘𝐴)↑𝑘) ∈ V
74, 5, 6fvmpt 6244 . . . 4 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘))
87adantl 482 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘))
9 abscl 13960 . . . . 5 (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
109adantr 481 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘𝐴) ∈ ℝ)
11 reexpcl 12825 . . . 4 (((abs‘𝐴) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((abs‘𝐴)↑𝑘) ∈ ℝ)
1210, 11sylan 488 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → ((abs‘𝐴)↑𝑘) ∈ ℝ)
138, 12eqeltrd 2698 . 2 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘) ∈ ℝ)
14 eqeq1 2625 . . . . . . 7 (𝑛 = 𝑘 → (𝑛 = 0 ↔ 𝑘 = 0))
15 oveq2 6618 . . . . . . 7 (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
1614, 15ifbieq2d 4088 . . . . . 6 (𝑛 = 𝑘 → if(𝑛 = 0, 0, (1 / 𝑛)) = if(𝑘 = 0, 0, (1 / 𝑘)))
17 oveq2 6618 . . . . . 6 (𝑛 = 𝑘 → (𝐴𝑛) = (𝐴𝑘))
1816, 17oveq12d 6628 . . . . 5 (𝑛 = 𝑘 → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
19 eqid 2621 . . . . 5 (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛))) = (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))
20 ovex 6638 . . . . 5 (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) ∈ V
2118, 19, 20fvmpt 6244 . . . 4 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
2221adantl 482 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
23 0cnd 9985 . . . . 5 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 = 0) → 0 ∈ ℂ)
24 nn0cn 11254 . . . . . . 7 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
2524adantl 482 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
26 df-ne 2791 . . . . . . 7 (𝑘 ≠ 0 ↔ ¬ 𝑘 = 0)
2726biimpri 218 . . . . . 6 𝑘 = 0 → 𝑘 ≠ 0)
28 reccl 10644 . . . . . 6 ((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) → (1 / 𝑘) ∈ ℂ)
2925, 27, 28syl2an 494 . . . . 5 ((((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) ∧ ¬ 𝑘 = 0) → (1 / 𝑘) ∈ ℂ)
3023, 29ifclda 4097 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → if(𝑘 = 0, 0, (1 / 𝑘)) ∈ ℂ)
31 expcl 12826 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
3231adantlr 750 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
3330, 32mulcld 10012 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) ∈ ℂ)
3422, 33eqeltrd 2698 . 2 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘) ∈ ℂ)
3510recnd 10020 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘𝐴) ∈ ℂ)
36 absidm 14005 . . . . . 6 (𝐴 ∈ ℂ → (abs‘(abs‘𝐴)) = (abs‘𝐴))
3736adantr 481 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘(abs‘𝐴)) = (abs‘𝐴))
38 simpr 477 . . . . 5 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘𝐴) < 1)
3937, 38eqbrtrd 4640 . . . 4 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → (abs‘(abs‘𝐴)) < 1)
4035, 39, 8geolim 14537 . . 3 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ⇝ (1 / (1 − (abs‘𝐴))))
41 seqex 12751 . . . 4 seq0( + , (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ∈ V
42 ovex 6638 . . . 4 (1 / (1 − (abs‘𝐴))) ∈ V
4341, 42breldm 5294 . . 3 (seq0( + , (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ⇝ (1 / (1 − (abs‘𝐴))) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ∈ dom ⇝ )
4440, 43syl 17 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ∈ dom ⇝ )
45 1red 10007 . 2 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 1 ∈ ℝ)
46 elnnuz 11676 . . 3 (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ‘1))
47 nnrecre 11009 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
4847adantl 482 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℝ)
4948recnd 10020 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℂ)
50 nnnn0 11251 . . . . . . . 8 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
5150, 32sylan2 491 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (𝐴𝑘) ∈ ℂ)
5249, 51absmuld 14135 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘((1 / 𝑘) · (𝐴𝑘))) = ((abs‘(1 / 𝑘)) · (abs‘(𝐴𝑘))))
53 nnrp 11794 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
5453adantl 482 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
5554rpreccld 11834 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℝ+)
5655rpge0d 11828 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 0 ≤ (1 / 𝑘))
5748, 56absidd 14103 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘(1 / 𝑘)) = (1 / 𝑘))
58 simpl 473 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ ℂ)
59 absexp 13986 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (abs‘(𝐴𝑘)) = ((abs‘𝐴)↑𝑘))
6058, 50, 59syl2an 494 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘(𝐴𝑘)) = ((abs‘𝐴)↑𝑘))
6157, 60oveq12d 6628 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ((abs‘(1 / 𝑘)) · (abs‘(𝐴𝑘))) = ((1 / 𝑘) · ((abs‘𝐴)↑𝑘)))
6252, 61eqtrd 2655 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘((1 / 𝑘) · (𝐴𝑘))) = ((1 / 𝑘) · ((abs‘𝐴)↑𝑘)))
63 1red 10007 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
6450, 12sylan2 491 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ((abs‘𝐴)↑𝑘) ∈ ℝ)
6551absge0d 14125 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 0 ≤ (abs‘(𝐴𝑘)))
6665, 60breqtrd 4644 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 0 ≤ ((abs‘𝐴)↑𝑘))
67 nnge1 10998 . . . . . . . . 9 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
6867adantl 482 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘)
69 0lt1 10502 . . . . . . . . . 10 0 < 1
7069a1i 11 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 0 < 1)
71 nnre 10979 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
7271adantl 482 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
73 nngt0 11001 . . . . . . . . . 10 (𝑘 ∈ ℕ → 0 < 𝑘)
7473adantl 482 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 0 < 𝑘)
75 lerec 10858 . . . . . . . . 9 (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → (1 ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / 1)))
7663, 70, 72, 74, 75syl22anc 1324 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / 1)))
7768, 76mpbid 222 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ≤ (1 / 1))
78 1div1e1 10669 . . . . . . 7 (1 / 1) = 1
7977, 78syl6breq 4659 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ≤ 1)
8048, 63, 64, 66, 79lemul1ad 10915 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑘) · ((abs‘𝐴)↑𝑘)) ≤ (1 · ((abs‘𝐴)↑𝑘)))
8162, 80eqbrtrd 4640 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘((1 / 𝑘) · (𝐴𝑘))) ≤ (1 · ((abs‘𝐴)↑𝑘)))
8250, 22sylan2 491 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)))
83 nnne0 11005 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
8483adantl 482 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ≠ 0)
8584neneqd 2795 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ¬ 𝑘 = 0)
8685iffalsed 4074 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → if(𝑘 = 0, 0, (1 / 𝑘)) = (1 / 𝑘))
8786oveq1d 6625 . . . . . 6 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴𝑘)) = ((1 / 𝑘) · (𝐴𝑘)))
8882, 87eqtrd 2655 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘) = ((1 / 𝑘) · (𝐴𝑘)))
8988fveq2d 6157 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘)) = (abs‘((1 / 𝑘) · (𝐴𝑘))))
9050, 8sylan2 491 . . . . 5 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘))
9190oveq2d 6626 . . . 4 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (1 · ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘)) = (1 · ((abs‘𝐴)↑𝑘)))
9281, 89, 913brtr4d 4650 . . 3 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘)) ≤ (1 · ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘)))
9346, 92sylan2br 493 . 2 (((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) ∧ 𝑘 ∈ (ℤ‘1)) → (abs‘((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))‘𝑘)) ≤ (1 · ((𝑛 ∈ ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘)))
941, 3, 13, 34, 44, 45, 93cvgcmpce 14488 1 ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴𝑛)))) ∈ dom ⇝ )
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ifcif 4063   class class class wbr 4618   ↦ cmpt 4678  dom cdm 5079  ‘cfv 5852  (class class class)co 6610  ℂcc 9886  ℝcr 9887  0cc0 9888  1c1 9889   + caddc 9891   · cmul 9893   < clt 10026   ≤ cle 10027   − cmin 10218   / cdiv 10636  ℕcn 10972  ℕ0cn0 11244  ℤ≥cuz 11639  ℝ+crp 11784  seqcseq 12749  ↑cexp 12808  abscabs 13916   ⇝ cli 14157 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8490  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966  ax-addf 9967  ax-mulf 9968 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-pm 7812  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-sup 8300  df-inf 8301  df-oi 8367  df-card 8717  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-n0 11245  df-z 11330  df-uz 11640  df-rp 11785  df-ico 12131  df-fz 12277  df-fzo 12415  df-fl 12541  df-seq 12750  df-exp 12809  df-hash 13066  df-cj 13781  df-re 13782  df-im 13783  df-sqrt 13917  df-abs 13918  df-limsup 14144  df-clim 14161  df-rlim 14162  df-sum 14359 This theorem is referenced by:  logtayl  24323
 Copyright terms: Public domain W3C validator