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

Theorem eftlub 15457
Description: An upper bound on the absolute value of the infinite tail of the series expansion of the exponential function on the closed unit disk. (Contributed by Paul Chapman, 19-Jan-2008.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
Hypotheses
Ref Expression
eftl.1 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) / (!‘𝑛)))
eftl.2 𝐺 = (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))
eftl.3 𝐻 = (𝑛 ∈ ℕ0 ↦ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)))
eftl.4 (𝜑𝑀 ∈ ℕ)
eftl.5 (𝜑𝐴 ∈ ℂ)
eftl.6 (𝜑 → (abs‘𝐴) ≤ 1)
Assertion
Ref Expression
eftlub (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
Distinct variable groups:   𝑘,𝑛,𝐴   𝑘,𝐹   𝑘,𝐺   𝑘,𝑀,𝑛   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑛)   𝐹(𝑛)   𝐺(𝑛)   𝐻(𝑘,𝑛)

Proof of Theorem eftlub
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 eftl.5 . . . 4 (𝜑𝐴 ∈ ℂ)
2 eftl.4 . . . . 5 (𝜑𝑀 ∈ ℕ)
32nnnn0d 11949 . . . 4 (𝜑𝑀 ∈ ℕ0)
4 eftl.1 . . . . 5 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) / (!‘𝑛)))
54eftlcl 15455 . . . 4 ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘) ∈ ℂ)
61, 3, 5syl2anc 584 . . 3 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘) ∈ ℂ)
76abscld 14791 . 2 (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ∈ ℝ)
81abscld 14791 . . 3 (𝜑 → (abs‘𝐴) ∈ ℝ)
9 eftl.2 . . . 4 𝐺 = (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))
109reeftlcl 15456 . . 3 (((abs‘𝐴) ∈ ℝ ∧ 𝑀 ∈ ℕ0) → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ)
118, 3, 10syl2anc 584 . 2 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ)
128, 3reexpcld 13522 . . 3 (𝜑 → ((abs‘𝐴)↑𝑀) ∈ ℝ)
13 peano2nn0 11931 . . . . . 6 (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ0)
143, 13syl 17 . . . . 5 (𝜑 → (𝑀 + 1) ∈ ℕ0)
1514nn0red 11950 . . . 4 (𝜑 → (𝑀 + 1) ∈ ℝ)
163faccld 13639 . . . . 5 (𝜑 → (!‘𝑀) ∈ ℕ)
1716, 2nnmulcld 11684 . . . 4 (𝜑 → ((!‘𝑀) · 𝑀) ∈ ℕ)
1815, 17nndivred 11685 . . 3 (𝜑 → ((𝑀 + 1) / ((!‘𝑀) · 𝑀)) ∈ ℝ)
1912, 18remulcld 10665 . 2 (𝜑 → (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) ∈ ℝ)
20 eqid 2826 . . 3 (ℤ𝑀) = (ℤ𝑀)
212nnzd 12080 . . . 4 (𝜑𝑀 ∈ ℤ)
22 eqidd 2827 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) = (𝐹𝑘))
23 eluznn0 12311 . . . . . 6 ((𝑀 ∈ ℕ0𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ0)
243, 23sylan 580 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ0)
254eftval 15425 . . . . . . 7 (𝑘 ∈ ℕ0 → (𝐹𝑘) = ((𝐴𝑘) / (!‘𝑘)))
2625adantl 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) = ((𝐴𝑘) / (!‘𝑘)))
27 eftcl 15422 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐴𝑘) / (!‘𝑘)) ∈ ℂ)
281, 27sylan 580 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝐴𝑘) / (!‘𝑘)) ∈ ℂ)
2926, 28eqeltrd 2918 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ∈ ℂ)
3024, 29syldan 591 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℂ)
314eftlcvg 15454 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
321, 3, 31syl2anc 584 . . . 4 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
3320, 21, 22, 30, 32isumclim2 15108 . . 3 (𝜑 → seq𝑀( + , 𝐹) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘))
34 eqidd 2827 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) = (𝐺𝑘))
359eftval 15425 . . . . . . . 8 (𝑘 ∈ ℕ0 → (𝐺𝑘) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
3635adantl 482 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
37 reeftcl 15423 . . . . . . . 8 (((abs‘𝐴) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ)
388, 37sylan 580 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ)
3936, 38eqeltrd 2918 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℝ)
4024, 39syldan 591 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) ∈ ℝ)
4140recnd 10663 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) ∈ ℂ)
428recnd 10663 . . . . 5 (𝜑 → (abs‘𝐴) ∈ ℂ)
439eftlcvg 15454 . . . . 5 (((abs‘𝐴) ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐺) ∈ dom ⇝ )
4442, 3, 43syl2anc 584 . . . 4 (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ )
4520, 21, 34, 41, 44isumclim2 15108 . . 3 (𝜑 → seq𝑀( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
46 eftabs 15424 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (abs‘((𝐴𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
471, 46sylan 580 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (abs‘((𝐴𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
4826fveq2d 6673 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (abs‘(𝐹𝑘)) = (abs‘((𝐴𝑘) / (!‘𝑘))))
4947, 48, 363eqtr4rd 2872 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = (abs‘(𝐹𝑘)))
5024, 49syldan 591 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) = (abs‘(𝐹𝑘)))
5120, 33, 45, 21, 30, 50iserabs 15165 . 2 (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ≤ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
52 nn0uz 12274 . . . 4 0 = (ℤ‘0)
53 0zd 11987 . . . 4 (𝜑 → 0 ∈ ℤ)
542nncnd 11648 . . . . 5 (𝜑𝑀 ∈ ℂ)
55 nn0cn 11901 . . . . 5 (𝑗 ∈ ℕ0𝑗 ∈ ℂ)
56 nn0ex 11897 . . . . . . . 8 0 ∈ V
5756mptex 6983 . . . . . . 7 (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛))) ∈ V
589, 57eqeltri 2914 . . . . . 6 𝐺 ∈ V
5958shftval4 14431 . . . . 5 ((𝑀 ∈ ℂ ∧ 𝑗 ∈ ℂ) → ((𝐺 shift -𝑀)‘𝑗) = (𝐺‘(𝑀 + 𝑗)))
6054, 55, 59syl2an 595 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((𝐺 shift -𝑀)‘𝑗) = (𝐺‘(𝑀 + 𝑗)))
61 nn0addcl 11926 . . . . . . 7 ((𝑀 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ ℕ0)
623, 61sylan 580 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ ℕ0)
639eftval 15425 . . . . . 6 ((𝑀 + 𝑗) ∈ ℕ0 → (𝐺‘(𝑀 + 𝑗)) = (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))))
6462, 63syl 17 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) = (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))))
658adantr 481 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
66 reeftcl 15423 . . . . . 6 (((abs‘𝐴) ∈ ℝ ∧ (𝑀 + 𝑗) ∈ ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ∈ ℝ)
6765, 62, 66syl2anc 584 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ∈ ℝ)
6864, 67eqeltrd 2918 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) ∈ ℝ)
69 oveq2 7158 . . . . . . 7 (𝑛 = 𝑗 → ((1 / (𝑀 + 1))↑𝑛) = ((1 / (𝑀 + 1))↑𝑗))
7069oveq2d 7166 . . . . . 6 (𝑛 = 𝑗 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
71 eftl.3 . . . . . 6 𝐻 = (𝑛 ∈ ℕ0 ↦ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)))
72 ovex 7183 . . . . . 6 ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ V
7370, 71, 72fvmpt 6767 . . . . 5 (𝑗 ∈ ℕ0 → (𝐻𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
7473adantl 482 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐻𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
7512, 16nndivred 11685 . . . . . 6 (𝜑 → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℝ)
7675adantr 481 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℝ)
772peano2nnd 11649 . . . . . . 7 (𝜑 → (𝑀 + 1) ∈ ℕ)
7877nnrecred 11682 . . . . . 6 (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ)
79 reexpcl 13441 . . . . . 6 (((1 / (𝑀 + 1)) ∈ ℝ ∧ 𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ)
8078, 79sylan 580 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ)
8176, 80remulcld 10665 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ)
8265, 62reexpcld 13522 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑(𝑀 + 𝑗)) ∈ ℝ)
8312adantr 481 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ∈ ℝ)
8462faccld 13639 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (!‘(𝑀 + 𝑗)) ∈ ℕ)
8584nnred 11647 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (!‘(𝑀 + 𝑗)) ∈ ℝ)
8685, 81remulcld 10665 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) ∈ ℝ)
873adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝑀 ∈ ℕ0)
88 uzid 12252 . . . . . . . . . 10 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
8921, 88syl 17 . . . . . . . . 9 (𝜑𝑀 ∈ (ℤ𝑀))
90 uzaddcl 12298 . . . . . . . . 9 ((𝑀 ∈ (ℤ𝑀) ∧ 𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ (ℤ𝑀))
9189, 90sylan 580 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ (ℤ𝑀))
921absge0d 14799 . . . . . . . . 9 (𝜑 → 0 ≤ (abs‘𝐴))
9392adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (abs‘𝐴))
94 eftl.6 . . . . . . . . 9 (𝜑 → (abs‘𝐴) ≤ 1)
9594adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ≤ 1)
9665, 87, 91, 93, 95leexp2rd 13613 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((abs‘𝐴)↑𝑀))
9716adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑀) ∈ ℕ)
98 nnexpcl 13437 . . . . . . . . . . . . 13 (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℕ)
9977, 98sylan 580 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℕ)
10097, 99nnmulcld 11684 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℕ)
101100nnred 11647 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℝ)
1028, 3, 92expge0d 13523 . . . . . . . . . . . 12 (𝜑 → 0 ≤ ((abs‘𝐴)↑𝑀))
10312, 102jca 512 . . . . . . . . . . 11 (𝜑 → (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑀)))
104103adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑀)))
105 faclbnd6 13654 . . . . . . . . . . 11 ((𝑀 ∈ ℕ0𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗)))
1063, 105sylan 580 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗)))
107 lemul1a 11488 . . . . . . . . . 10 (((((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℝ ∧ (!‘(𝑀 + 𝑗)) ∈ ℝ ∧ (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑀))) ∧ ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗))) → (((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)))
108101, 85, 104, 106, 107syl31anc 1367 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)))
10985, 83remulcld 10665 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) ∈ ℝ)
110100nnrpd 12424 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℝ+)
11183, 109, 110lemuldiv2d 12476 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) ↔ ((abs‘𝐴)↑𝑀) ≤ (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))))
112108, 111mpbid 233 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ≤ (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))))
11384nncnd 11648 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (!‘(𝑀 + 𝑗)) ∈ ℂ)
11412recnd 10663 . . . . . . . . . . 11 (𝜑 → ((abs‘𝐴)↑𝑀) ∈ ℂ)
115114adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ∈ ℂ)
116100nncnd 11648 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℂ)
117100nnne0d 11681 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≠ 0)
118113, 115, 116, 117divassd 11445 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((!‘(𝑀 + 𝑗)) · (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))))
11977nncnd 11648 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 + 1) ∈ ℂ)
120119adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 1) ∈ ℂ)
12177adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 1) ∈ ℕ)
122121nnne0d 11681 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 1) ≠ 0)
123 nn0z 11999 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0𝑗 ∈ ℤ)
124123adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℤ)
125120, 122, 124exprecd 13513 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) = (1 / ((𝑀 + 1)↑𝑗)))
126125oveq2d 7166 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · (1 / ((𝑀 + 1)↑𝑗))))
12775recnd 10663 . . . . . . . . . . . . 13 (𝜑 → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℂ)
128127adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℂ)
12999nncnd 11648 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℂ)
13099nnne0d 11681 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ≠ 0)
131128, 129, 130divrecd 11413 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) / ((𝑀 + 1)↑𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · (1 / ((𝑀 + 1)↑𝑗))))
13216nncnd 11648 . . . . . . . . . . . . 13 (𝜑 → (!‘𝑀) ∈ ℂ)
133132adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑀) ∈ ℂ)
134 facne0 13641 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ0 → (!‘𝑀) ≠ 0)
1353, 134syl 17 . . . . . . . . . . . . 13 (𝜑 → (!‘𝑀) ≠ 0)
136135adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑀) ≠ 0)
137115, 133, 129, 136, 130divdiv1d 11441 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) / ((𝑀 + 1)↑𝑗)) = (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))))
138126, 131, 1373eqtr2rd 2868 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
139138oveq2d 7166 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((!‘(𝑀 + 𝑗)) · (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))) = ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
140118, 139eqtrd 2861 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
141112, 140breqtrd 5089 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
14282, 83, 86, 96, 141letrd 10791 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
14384nngt0d 11680 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → 0 < (!‘(𝑀 + 𝑗)))
144 ledivmul 11510 . . . . . . 7 ((((abs‘𝐴)↑(𝑀 + 𝑗)) ∈ ℝ ∧ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ ∧ ((!‘(𝑀 + 𝑗)) ∈ ℝ ∧ 0 < (!‘(𝑀 + 𝑗)))) → ((((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ↔ ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))))
14582, 81, 85, 143, 144syl112anc 1368 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ↔ ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))))
146142, 145mpbird 258 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
14764, 146eqbrtrd 5085 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
148 0z 11986 . . . . . 6 0 ∈ ℤ
14921znegcld 12083 . . . . . 6 (𝜑 → -𝑀 ∈ ℤ)
15058seqshft 14439 . . . . . 6 ((0 ∈ ℤ ∧ -𝑀 ∈ ℤ) → seq0( + , (𝐺 shift -𝑀)) = (seq(0 − -𝑀)( + , 𝐺) shift -𝑀))
151148, 149, 150sylancr 587 . . . . 5 (𝜑 → seq0( + , (𝐺 shift -𝑀)) = (seq(0 − -𝑀)( + , 𝐺) shift -𝑀))
152 0cn 10627 . . . . . . . . . . . 12 0 ∈ ℂ
153 subneg 10929 . . . . . . . . . . . 12 ((0 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (0 − -𝑀) = (0 + 𝑀))
154152, 153mpan 686 . . . . . . . . . . 11 (𝑀 ∈ ℂ → (0 − -𝑀) = (0 + 𝑀))
155 addid2 10817 . . . . . . . . . . 11 (𝑀 ∈ ℂ → (0 + 𝑀) = 𝑀)
156154, 155eqtrd 2861 . . . . . . . . . 10 (𝑀 ∈ ℂ → (0 − -𝑀) = 𝑀)
15754, 156syl 17 . . . . . . . . 9 (𝜑 → (0 − -𝑀) = 𝑀)
158157seqeq1d 13370 . . . . . . . 8 (𝜑 → seq(0 − -𝑀)( + , 𝐺) = seq𝑀( + , 𝐺))
159158, 45eqbrtrd 5085 . . . . . . 7 (𝜑 → seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
160 seqex 13366 . . . . . . . 8 seq(0 − -𝑀)( + , 𝐺) ∈ V
161 climshft 14928 . . . . . . . 8 ((-𝑀 ∈ ℤ ∧ seq(0 − -𝑀)( + , 𝐺) ∈ V) → ((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ↔ seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘)))
162149, 160, 161sylancl 586 . . . . . . 7 (𝜑 → ((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ↔ seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘)))
163159, 162mpbird 258 . . . . . 6 (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
164 ovex 7183 . . . . . . 7 (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ V
165 sumex 15039 . . . . . . 7 Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ V
166164, 165breldm 5776 . . . . . 6 ((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ dom ⇝ )
167163, 166syl 17 . . . . 5 (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ dom ⇝ )
168151, 167eqeltrd 2918 . . . 4 (𝜑 → seq0( + , (𝐺 shift -𝑀)) ∈ dom ⇝ )
1692nnge1d 11679 . . . . . . . . . 10 (𝜑 → 1 ≤ 𝑀)
170 1nn 11643 . . . . . . . . . . 11 1 ∈ ℕ
171 nnleltp1 12031 . . . . . . . . . . 11 ((1 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (1 ≤ 𝑀 ↔ 1 < (𝑀 + 1)))
172170, 2, 171sylancr 587 . . . . . . . . . 10 (𝜑 → (1 ≤ 𝑀 ↔ 1 < (𝑀 + 1)))
173169, 172mpbid 233 . . . . . . . . 9 (𝜑 → 1 < (𝑀 + 1))
17414nn0ge0d 11952 . . . . . . . . . 10 (𝜑 → 0 ≤ (𝑀 + 1))
17515, 174absidd 14777 . . . . . . . . 9 (𝜑 → (abs‘(𝑀 + 1)) = (𝑀 + 1))
176173, 175breqtrrd 5091 . . . . . . . 8 (𝜑 → 1 < (abs‘(𝑀 + 1)))
177 eqid 2826 . . . . . . . . . 10 (𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))
178 ovex 7183 . . . . . . . . . 10 ((1 / (𝑀 + 1))↑𝑗) ∈ V
17969, 177, 178fvmpt 6767 . . . . . . . . 9 (𝑗 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) = ((1 / (𝑀 + 1))↑𝑗))
180179adantl 482 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) = ((1 / (𝑀 + 1))↑𝑗))
181119, 176, 180georeclim 15223 . . . . . . 7 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))) ⇝ ((𝑀 + 1) / ((𝑀 + 1) − 1)))
18280recnd 10663 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℂ)
183180, 182eqeltrd 2918 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) ∈ ℂ)
184180oveq2d 7166 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
18574, 184eqtr4d 2864 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (𝐻𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗)))
18652, 53, 127, 181, 183, 185isermulc2 15009 . . . . . 6 (𝜑 → seq0( + , 𝐻) ⇝ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))))
187 ax-1cn 10589 . . . . . . . . . . 11 1 ∈ ℂ
188 pncan 10886 . . . . . . . . . . 11 ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
18954, 187, 188sylancl 586 . . . . . . . . . 10 (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
190189oveq2d 7166 . . . . . . . . 9 (𝜑 → ((𝑀 + 1) / ((𝑀 + 1) − 1)) = ((𝑀 + 1) / 𝑀))
191190oveq2d 7166 . . . . . . . 8 (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / 𝑀)))
19215, 2nndivred 11685 . . . . . . . . . 10 (𝜑 → ((𝑀 + 1) / 𝑀) ∈ ℝ)
193192recnd 10663 . . . . . . . . 9 (𝜑 → ((𝑀 + 1) / 𝑀) ∈ ℂ)
194114, 193, 132, 135div23d 11447 . . . . . . . 8 (𝜑 → ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / 𝑀)))
195191, 194eqtr4d 2864 . . . . . . 7 (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)))
196114, 193, 132, 135divassd 11445 . . . . . . 7 (𝜑 → ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)) = (((abs‘𝐴)↑𝑀) · (((𝑀 + 1) / 𝑀) / (!‘𝑀))))
1972nnne0d 11681 . . . . . . . . . 10 (𝜑𝑀 ≠ 0)
198119, 54, 132, 197, 135divdiv1d 11441 . . . . . . . . 9 (𝜑 → (((𝑀 + 1) / 𝑀) / (!‘𝑀)) = ((𝑀 + 1) / (𝑀 · (!‘𝑀))))
19954, 132mulcomd 10656 . . . . . . . . . 10 (𝜑 → (𝑀 · (!‘𝑀)) = ((!‘𝑀) · 𝑀))
200199oveq2d 7166 . . . . . . . . 9 (𝜑 → ((𝑀 + 1) / (𝑀 · (!‘𝑀))) = ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))
201198, 200eqtrd 2861 . . . . . . . 8 (𝜑 → (((𝑀 + 1) / 𝑀) / (!‘𝑀)) = ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))
202201oveq2d 7166 . . . . . . 7 (𝜑 → (((abs‘𝐴)↑𝑀) · (((𝑀 + 1) / 𝑀) / (!‘𝑀))) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
203195, 196, 2023eqtrd 2865 . . . . . 6 (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
204186, 203breqtrd 5089 . . . . 5 (𝜑 → seq0( + , 𝐻) ⇝ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
205 seqex 13366 . . . . . 6 seq0( + , 𝐻) ∈ V
206 ovex 7183 . . . . . 6 (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) ∈ V
207205, 206breldm 5776 . . . . 5 (seq0( + , 𝐻) ⇝ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) → seq0( + , 𝐻) ∈ dom ⇝ )
208204, 207syl 17 . . . 4 (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ )
20952, 53, 60, 68, 74, 81, 147, 168, 208isumle 15194 . . 3 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)) ≤ Σ𝑗 ∈ ℕ0 ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
210 eqid 2826 . . . . 5 (ℤ‘(0 + 𝑀)) = (ℤ‘(0 + 𝑀))
211 fveq2 6669 . . . . 5 (𝑘 = (𝑀 + 𝑗) → (𝐺𝑘) = (𝐺‘(𝑀 + 𝑗)))
21254addid2d 10835 . . . . . . . . 9 (𝜑 → (0 + 𝑀) = 𝑀)
213212fveq2d 6673 . . . . . . . 8 (𝜑 → (ℤ‘(0 + 𝑀)) = (ℤ𝑀))
214213eleq2d 2903 . . . . . . 7 (𝜑 → (𝑘 ∈ (ℤ‘(0 + 𝑀)) ↔ 𝑘 ∈ (ℤ𝑀)))
215214biimpa 477 . . . . . 6 ((𝜑𝑘 ∈ (ℤ‘(0 + 𝑀))) → 𝑘 ∈ (ℤ𝑀))
216215, 41syldan 591 . . . . 5 ((𝜑𝑘 ∈ (ℤ‘(0 + 𝑀))) → (𝐺𝑘) ∈ ℂ)
21752, 210, 211, 21, 53, 216isumshft 15189 . . . 4 (𝜑 → Σ𝑘 ∈ (ℤ‘(0 + 𝑀))(𝐺𝑘) = Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)))
218213sumeq1d 15053 . . . 4 (𝜑 → Σ𝑘 ∈ (ℤ‘(0 + 𝑀))(𝐺𝑘) = Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
219217, 218eqtr3d 2863 . . 3 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)) = Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
22081recnd 10663 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℂ)
22152, 53, 74, 220, 204isumclim 15107 . . 3 (𝜑 → Σ𝑗 ∈ ℕ0 ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
222209, 219, 2213brtr3d 5094 . 2 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
2237, 11, 19, 51, 222letrd 10791 1 (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530  wcel 2107  wne 3021  Vcvv 3500   class class class wbr 5063  cmpt 5143  dom cdm 5554  cfv 6354  (class class class)co 7150  cc 10529  cr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536   < clt 10669  cle 10670  cmin 10864  -cneg 10865   / cdiv 11291  cn 11632  0cn0 11891  cz 11975  cuz 12237  seqcseq 13364  cexp 13424  !cfa 13628   shift cshi 14420  abscabs 14588  cli 14836  Σcsu 15037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-inf2 9098  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609  ax-addf 10610  ax-mulf 10611
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7574  df-1st 7685  df-2nd 7686  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-oadd 8102  df-er 8284  df-pm 8404  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-sup 8900  df-inf 8901  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-n0 11892  df-z 11976  df-uz 12238  df-rp 12385  df-ico 12739  df-fz 12888  df-fzo 13029  df-fl 13157  df-seq 13365  df-exp 13425  df-fac 13629  df-hash 13686  df-shft 14421  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-limsup 14823  df-clim 14840  df-rlim 14841  df-sum 15038
This theorem is referenced by:  ef01bndlem  15532  eirrlem  15552  dveflem  24510  subfaclim  32338
  Copyright terms: Public domain W3C validator