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

Theorem iseraltlem2 14457
Description: Lemma for iseralt 14459. The terms of an alternating series form a chain of inequalities in alternate terms, so that for example 𝑆(1) ≤ 𝑆(3) ≤ 𝑆(5) ≤ ... and ... ≤ 𝑆(4) ≤ 𝑆(2) ≤ 𝑆(0) (assuming 𝑀 = 0 so that these terms are defined). (Contributed by Mario Carneiro, 6-Apr-2015.)
Hypotheses
Ref Expression
iseralt.1 𝑍 = (ℤ𝑀)
iseralt.2 (𝜑𝑀 ∈ ℤ)
iseralt.3 (𝜑𝐺:𝑍⟶ℝ)
iseralt.4 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
iseralt.5 (𝜑𝐺 ⇝ 0)
iseralt.6 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
Assertion
Ref Expression
iseraltlem2 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
Distinct variable groups:   𝑘,𝐹   𝑘,𝐺   𝑘,𝑀   𝜑,𝑘   𝑘,𝐾   𝑘,𝑁   𝑘,𝑍

Proof of Theorem iseraltlem2
Dummy variables 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6698 . . . . . . . . . 10 (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
2 2t0e0 11221 . . . . . . . . . 10 (2 · 0) = 0
31, 2syl6eq 2701 . . . . . . . . 9 (𝑥 = 0 → (2 · 𝑥) = 0)
43oveq2d 6706 . . . . . . . 8 (𝑥 = 0 → (𝑁 + (2 · 𝑥)) = (𝑁 + 0))
54fveq2d 6233 . . . . . . 7 (𝑥 = 0 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + 0)))
65oveq2d 6706 . . . . . 6 (𝑥 = 0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))))
76breq1d 4695 . . . . 5 (𝑥 = 0 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
87imbi2d 329 . . . 4 (𝑥 = 0 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
9 oveq2 6698 . . . . . . . . 9 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
109oveq2d 6706 . . . . . . . 8 (𝑥 = 𝑛 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝑛)))
1110fveq2d 6233 . . . . . . 7 (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))))
1211oveq2d 6706 . . . . . 6 (𝑥 = 𝑛 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
1312breq1d 4695 . . . . 5 (𝑥 = 𝑛 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
1413imbi2d 329 . . . 4 (𝑥 = 𝑛 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
15 oveq2 6698 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
1615oveq2d 6706 . . . . . . . 8 (𝑥 = (𝑛 + 1) → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · (𝑛 + 1))))
1716fveq2d 6233 . . . . . . 7 (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
1817oveq2d 6706 . . . . . 6 (𝑥 = (𝑛 + 1) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
1918breq1d 4695 . . . . 5 (𝑥 = (𝑛 + 1) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
2019imbi2d 329 . . . 4 (𝑥 = (𝑛 + 1) → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
21 oveq2 6698 . . . . . . . . 9 (𝑥 = 𝐾 → (2 · 𝑥) = (2 · 𝐾))
2221oveq2d 6706 . . . . . . . 8 (𝑥 = 𝐾 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝐾)))
2322fveq2d 6233 . . . . . . 7 (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))
2423oveq2d 6706 . . . . . 6 (𝑥 = 𝐾 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
2524breq1d 4695 . . . . 5 (𝑥 = 𝐾 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
2625imbi2d 329 . . . 4 (𝑥 = 𝐾 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
27 iseralt.1 . . . . . . . . . . . 12 𝑍 = (ℤ𝑀)
28 uzssz 11745 . . . . . . . . . . . 12 (ℤ𝑀) ⊆ ℤ
2927, 28eqsstri 3668 . . . . . . . . . . 11 𝑍 ⊆ ℤ
3029a1i 11 . . . . . . . . . 10 (𝜑𝑍 ⊆ ℤ)
3130sselda 3636 . . . . . . . . 9 ((𝜑𝑁𝑍) → 𝑁 ∈ ℤ)
3231zcnd 11521 . . . . . . . 8 ((𝜑𝑁𝑍) → 𝑁 ∈ ℂ)
3332addid1d 10274 . . . . . . 7 ((𝜑𝑁𝑍) → (𝑁 + 0) = 𝑁)
3433fveq2d 6233 . . . . . 6 ((𝜑𝑁𝑍) → (seq𝑀( + , 𝐹)‘(𝑁 + 0)) = (seq𝑀( + , 𝐹)‘𝑁))
3534oveq2d 6706 . . . . 5 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
36 neg1rr 11163 . . . . . . . . 9 -1 ∈ ℝ
37 neg1ne0 11164 . . . . . . . . 9 -1 ≠ 0
38 reexpclz 12920 . . . . . . . . 9 ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (-1↑𝑁) ∈ ℝ)
3936, 37, 38mp3an12 1454 . . . . . . . 8 (𝑁 ∈ ℤ → (-1↑𝑁) ∈ ℝ)
4031, 39syl 17 . . . . . . 7 ((𝜑𝑁𝑍) → (-1↑𝑁) ∈ ℝ)
41 iseralt.2 . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
42 iseralt.6 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
4330sselda 3636 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
44 reexpclz 12920 . . . . . . . . . . . . 13 ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈ ℝ)
4536, 37, 44mp3an12 1454 . . . . . . . . . . . 12 (𝑘 ∈ ℤ → (-1↑𝑘) ∈ ℝ)
4643, 45syl 17 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
47 iseralt.3 . . . . . . . . . . . 12 (𝜑𝐺:𝑍⟶ℝ)
4847ffvelrnda 6399 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
4946, 48remulcld 10108 . . . . . . . . . 10 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
5042, 49eqeltrd 2730 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
5127, 41, 50serfre 12870 . . . . . . . 8 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
5251ffvelrnda 6399 . . . . . . 7 ((𝜑𝑁𝑍) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
5340, 52remulcld 10108 . . . . . 6 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
5453leidd 10632 . . . . 5 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
5535, 54eqbrtrd 4707 . . . 4 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
5647ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
57 ax-1cn 10032 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
58572timesi 11185 . . . . . . . . . . . . . . 15 (2 · 1) = (1 + 1)
5958oveq2i 6701 . . . . . . . . . . . . . 14 ((𝑁 + (2 · 𝑛)) + (2 · 1)) = ((𝑁 + (2 · 𝑛)) + (1 + 1))
60 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑁𝑍) → 𝑁𝑍)
6160, 27syl6eleq 2740 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑁𝑍) → 𝑁 ∈ (ℤ𝑀))
6261adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ (ℤ𝑀))
63 eluzelz 11735 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
6462, 63syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℤ)
6564zcnd 11521 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℂ)
66 2cn 11129 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
67 nn0cn 11340 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
6867adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℂ)
69 mulcl 10058 . . . . . . . . . . . . . . . 16 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
7066, 68, 69sylancr 696 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℂ)
7166, 57mulcli 10083 . . . . . . . . . . . . . . . 16 (2 · 1) ∈ ℂ
7271a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 1) ∈ ℂ)
7365, 70, 72addassd 10100 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (2 · 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
7459, 73syl5eqr 2699 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (1 + 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
75 2nn0 11347 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ0
76 simpr 476 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
77 nn0mulcl 11367 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℕ0𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
7875, 76, 77sylancr 696 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
79 uzaddcl 11782 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · 𝑛) ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀))
8062, 78, 79syl2anc 694 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀))
8128, 80sseldi 3634 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℤ)
8281zcnd 11521 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℂ)
83 1cnd 10094 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 1 ∈ ℂ)
8482, 83, 83addassd 10100 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = ((𝑁 + (2 · 𝑛)) + (1 + 1)))
85 2cnd 11131 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
8685, 68, 83adddid 10102 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
8786oveq2d 6706 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
8874, 84, 873eqtr4d 2695 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = (𝑁 + (2 · (𝑛 + 1))))
89 peano2nn0 11371 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
9089adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑛 + 1) ∈ ℕ0)
91 nn0mulcl 11367 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
9275, 90, 91sylancr 696 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
93 uzaddcl 11782 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · (𝑛 + 1)) ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ𝑀))
9462, 92, 93syl2anc 694 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ𝑀))
9594, 27syl6eleqr 2741 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ 𝑍)
9688, 95eqeltrd 2730 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) ∈ 𝑍)
9756, 96ffvelrnd 6400 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
98 peano2uz 11779 . . . . . . . . . . . . 13 ((𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ𝑀))
9980, 98syl 17 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ𝑀))
10099, 27syl6eleqr 2741 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍)
10156, 100ffvelrnd 6400 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
10297, 101resubcld 10496 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
103 0red 10079 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 0 ∈ ℝ)
10440adantr 480 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℝ)
10551ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
10680, 27syl6eleqr 2741 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ 𝑍)
107105, 106ffvelrnd 6400 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℝ)
108104, 107remulcld 10108 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℝ)
109 iseralt.4 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
110109ralrimiva 2995 . . . . . . . . . . . 12 (𝜑 → ∀𝑘𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
111110ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
112 oveq1 6697 . . . . . . . . . . . . . 14 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝑘 + 1) = (((𝑁 + (2 · 𝑛)) + 1) + 1))
113112fveq2d 6233 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘(𝑘 + 1)) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
114 fveq2 6229 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺𝑘) = (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
115113, 114breq12d 4698 . . . . . . . . . . . 12 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘) ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
116115rspcv 3336 . . . . . . . . . . 11 (((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍 → (∀𝑘𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
117100, 111, 116sylc 65 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
11897, 101suble0d 10656 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ≤ 0 ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
119117, 118mpbird 247 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ≤ 0)
120102, 103, 108, 119leadd2dd 10680 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0))
121 seqp1 12856 . . . . . . . . . . . . 13 (((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
12299, 121syl 17 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
123 seqp1 12856 . . . . . . . . . . . . . 14 ((𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))))
12480, 123syl 17 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))))
125124oveq1d 6705 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
126122, 125eqtrd 2685 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
12788fveq2d 6233 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
128107recnd 10106 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℂ)
12942ralrimiva 2995 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
130129ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
131 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐹𝑘) = (𝐹‘((𝑁 + (2 · 𝑛)) + 1)))
132 oveq2 6698 . . . . . . . . . . . . . . . . . . 19 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝑛)) + 1)))
133132, 114oveq12d 6708 . . . . . . . . . . . . . . . . . 18 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
134131, 133eqeq12d 2666 . . . . . . . . . . . . . . . . 17 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
135134rspcv 3336 . . . . . . . . . . . . . . . 16 (((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍 → (∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
136100, 130, 135sylc 65 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
137 neg1cn 11162 . . . . . . . . . . . . . . . . . . 19 -1 ∈ ℂ
138137a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℂ)
13937a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ≠ 0)
140138, 139, 81expp1zd 13057 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -1))
14136a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℝ)
142141, 139, 81reexpclzd 13074 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℝ)
143142recnd 10106 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ)
144 mulcom 10060 . . . . . . . . . . . . . . . . . 18 (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ -1 ∈ ℂ) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
145143, 137, 144sylancl 695 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
146143mulm1d 10520 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1 · (-1↑(𝑁 + (2 · 𝑛)))) = -(-1↑(𝑁 + (2 · 𝑛))))
147140, 145, 1463eqtrd 2689 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = -(-1↑(𝑁 + (2 · 𝑛))))
148147oveq1d 6705 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
149101recnd 10106 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
150 mulneg12 10506 . . . . . . . . . . . . . . . 16 (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
151143, 149, 150syl2anc 694 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
152136, 148, 1513eqtrd 2689 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
153101renegcld 10495 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
154142, 153remulcld 10108 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
155152, 154eqeltrd 2730 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
156155recnd 10106 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
157 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐹𝑘) = (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
158 oveq2 6698 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (-1↑𝑘) = (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)))
159 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐺𝑘) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
160158, 159oveq12d 6708 . . . . . . . . . . . . . . . . . 18 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
161157, 160eqeq12d 2666 . . . . . . . . . . . . . . . . 17 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
162161rspcv 3336 . . . . . . . . . . . . . . . 16 ((((𝑁 + (2 · 𝑛)) + 1) + 1) ∈ 𝑍 → (∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
16396, 130, 162sylc 65 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
16481peano2zd 11523 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ ℤ)
165138, 139, 164expp1zd 13057 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1))
166147oveq1d 6705 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1) = (-(-1↑(𝑁 + (2 · 𝑛))) · -1))
167 mul2neg 10507 . . . . . . . . . . . . . . . . . . 19 (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ 1 ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
168143, 57, 167sylancl 695 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
169143mulid1d 10095 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · 1) = (-1↑(𝑁 + (2 · 𝑛))))
170168, 169eqtrd 2685 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1↑(𝑁 + (2 · 𝑛))))
171165, 166, 1703eqtrd 2689 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (-1↑(𝑁 + (2 · 𝑛))))
172171oveq1d 6705 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
173163, 172eqtrd 2685 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
174142, 97remulcld 10108 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
175173, 174eqeltrd 2730 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
176175recnd 10106 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
177128, 156, 176addassd 10100 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
178126, 127, 1773eqtr3d 2693 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
179178oveq2d 6706 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
180104recnd 10106 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℂ)
181155, 175readdcld 10107 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
182181recnd 10106 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℂ)
183180, 128, 182adddid 10102 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
184180, 156, 176adddid 10102 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
185152oveq2d 6706 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
186153recnd 10106 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
187180, 143, 186mulassd 10101 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
188185, 187eqtr4d 2688 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
18985, 65, 68adddid 10102 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑁 + 𝑛)) = ((2 · 𝑁) + (2 · 𝑛)))
190652timesd 11313 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
191190oveq1d 6705 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑁) + (2 · 𝑛)) = ((𝑁 + 𝑁) + (2 · 𝑛)))
19265, 65, 70addassd 10100 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + 𝑁) + (2 · 𝑛)) = (𝑁 + (𝑁 + (2 · 𝑛))))
193189, 191, 1923eqtrrd 2690 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (𝑁 + (2 · 𝑛))) = (2 · (𝑁 + 𝑛)))
194193oveq2d 6706 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = (-1↑(2 · (𝑁 + 𝑛))))
195 expaddz 12944 . . . . . . . . . . . . . . . 16 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ (𝑁 + (2 · 𝑛)) ∈ ℤ)) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
196138, 139, 64, 81, 195syl22anc 1367 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
197 2z 11447 . . . . . . . . . . . . . . . . . 18 2 ∈ ℤ
198197a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℤ)
199 nn0z 11438 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
200 zaddcl 11455 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 + 𝑛) ∈ ℤ)
20131, 199, 200syl2an 493 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + 𝑛) ∈ ℤ)
202 expmulz 12946 . . . . . . . . . . . . . . . . 17 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑁 + 𝑛) ∈ ℤ)) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
203138, 139, 198, 201, 202syl22anc 1367 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
204 neg1sqe1 12999 . . . . . . . . . . . . . . . . . 18 (-1↑2) = 1
205204oveq1i 6700 . . . . . . . . . . . . . . . . 17 ((-1↑2)↑(𝑁 + 𝑛)) = (1↑(𝑁 + 𝑛))
206 1exp 12929 . . . . . . . . . . . . . . . . . 18 ((𝑁 + 𝑛) ∈ ℤ → (1↑(𝑁 + 𝑛)) = 1)
207201, 206syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (1↑(𝑁 + 𝑛)) = 1)
208205, 207syl5eq 2697 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑2)↑(𝑁 + 𝑛)) = 1)
209203, 208eqtrd 2685 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = 1)
210194, 196, 2093eqtr3d 2693 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) = 1)
211210oveq1d 6705 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
212186mulid2d 10096 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
213188, 211, 2123eqtrd 2689 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
214173oveq2d 6706 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
21597recnd 10106 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
216180, 143, 215mulassd 10101 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
217214, 216eqtr4d 2688 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
218210oveq1d 6705 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
219215mulid2d 10096 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
220217, 218, 2193eqtrd 2689 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
221213, 220oveq12d 6708 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
222149negcld 10417 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
223222, 215addcomd 10276 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
224215, 149negsubd 10436 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
225223, 224eqtrd 2685 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
226184, 221, 2253eqtrd 2689 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
227226oveq2d 6706 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
228179, 183, 2273eqtrrd 2690 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
229108recnd 10106 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℂ)
230229addid1d 10274 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
231120, 228, 2303brtr3d 4716 . . . . . . 7 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
232105, 95ffvelrnd 6400 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) ∈ ℝ)
233104, 232remulcld 10108 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ∈ ℝ)
23453adantr 480 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
235 letr 10169 . . . . . . . 8 ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ∈ ℝ ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℝ ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ) → ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
236233, 108, 234, 235syl3anc 1366 . . . . . . 7 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
237231, 236mpand 711 . . . . . 6 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
238237expcom 450 . . . . 5 (𝑛 ∈ ℕ0 → ((𝜑𝑁𝑍) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
239238a2d 29 . . . 4 (𝑛 ∈ ℕ0 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
2408, 14, 20, 26, 55, 239nn0ind 11510 . . 3 (𝐾 ∈ ℕ0 → ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
241240com12 32 . 2 ((𝜑𝑁𝑍) → (𝐾 ∈ ℕ0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
2422413impia 1280 1 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wss 3607   class class class wbr 4685  wf 5922  cfv 5926  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  cle 10113  cmin 10304  -cneg 10305  2c2 11108  0cn0 11330  cz 11415  cuz 11725  seqcseq 12841  cexp 12900  cli 14259
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-seq 12842  df-exp 12901
This theorem is referenced by:  iseraltlem3  14458
  Copyright terms: Public domain W3C validator