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

Theorem iseraltlem2 15032
Description: Lemma for iseralt 15034. 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 7159 . . . . . . . . . 10 (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
2 2t0e0 11798 . . . . . . . . . 10 (2 · 0) = 0
31, 2syl6eq 2876 . . . . . . . . 9 (𝑥 = 0 → (2 · 𝑥) = 0)
43oveq2d 7167 . . . . . . . 8 (𝑥 = 0 → (𝑁 + (2 · 𝑥)) = (𝑁 + 0))
54fveq2d 6670 . . . . . . 7 (𝑥 = 0 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + 0)))
65oveq2d 7167 . . . . . 6 (𝑥 = 0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))))
76breq1d 5072 . . . . 5 (𝑥 = 0 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
87imbi2d 342 . . . 4 (𝑥 = 0 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
9 oveq2 7159 . . . . . . . . 9 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
109oveq2d 7167 . . . . . . . 8 (𝑥 = 𝑛 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝑛)))
1110fveq2d 6670 . . . . . . 7 (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))))
1211oveq2d 7167 . . . . . 6 (𝑥 = 𝑛 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
1312breq1d 5072 . . . . 5 (𝑥 = 𝑛 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
1413imbi2d 342 . . . 4 (𝑥 = 𝑛 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
15 oveq2 7159 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
1615oveq2d 7167 . . . . . . . 8 (𝑥 = (𝑛 + 1) → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · (𝑛 + 1))))
1716fveq2d 6670 . . . . . . 7 (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
1817oveq2d 7167 . . . . . 6 (𝑥 = (𝑛 + 1) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
1918breq1d 5072 . . . . 5 (𝑥 = (𝑛 + 1) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
2019imbi2d 342 . . . 4 (𝑥 = (𝑛 + 1) → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
21 oveq2 7159 . . . . . . . . 9 (𝑥 = 𝐾 → (2 · 𝑥) = (2 · 𝐾))
2221oveq2d 7167 . . . . . . . 8 (𝑥 = 𝐾 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝐾)))
2322fveq2d 6670 . . . . . . 7 (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))
2423oveq2d 7167 . . . . . 6 (𝑥 = 𝐾 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
2524breq1d 5072 . . . . 5 (𝑥 = 𝐾 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
2625imbi2d 342 . . . 4 (𝑥 = 𝐾 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
27 iseralt.1 . . . . . . . . . . . 12 𝑍 = (ℤ𝑀)
28 uzssz 12256 . . . . . . . . . . . 12 (ℤ𝑀) ⊆ ℤ
2927, 28eqsstri 4004 . . . . . . . . . . 11 𝑍 ⊆ ℤ
3029a1i 11 . . . . . . . . . 10 (𝜑𝑍 ⊆ ℤ)
3130sselda 3970 . . . . . . . . 9 ((𝜑𝑁𝑍) → 𝑁 ∈ ℤ)
3231zcnd 12080 . . . . . . . 8 ((𝜑𝑁𝑍) → 𝑁 ∈ ℂ)
3332addid1d 10832 . . . . . . 7 ((𝜑𝑁𝑍) → (𝑁 + 0) = 𝑁)
3433fveq2d 6670 . . . . . 6 ((𝜑𝑁𝑍) → (seq𝑀( + , 𝐹)‘(𝑁 + 0)) = (seq𝑀( + , 𝐹)‘𝑁))
3534oveq2d 7167 . . . . 5 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
36 neg1rr 11744 . . . . . . . 8 -1 ∈ ℝ
37 neg1ne0 11745 . . . . . . . 8 -1 ≠ 0
38 reexpclz 13442 . . . . . . . 8 ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (-1↑𝑁) ∈ ℝ)
3936, 37, 31, 38mp3an12i 1458 . . . . . . 7 ((𝜑𝑁𝑍) → (-1↑𝑁) ∈ ℝ)
40 iseralt.2 . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
41 iseralt.6 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
4230sselda 3970 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
43 reexpclz 13442 . . . . . . . . . . . 12 ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈ ℝ)
4436, 37, 42, 43mp3an12i 1458 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
45 iseralt.3 . . . . . . . . . . . 12 (𝜑𝐺:𝑍⟶ℝ)
4645ffvelrnda 6846 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
4744, 46remulcld 10663 . . . . . . . . . 10 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
4841, 47eqeltrd 2917 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
4927, 40, 48serfre 13392 . . . . . . . 8 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
5049ffvelrnda 6846 . . . . . . 7 ((𝜑𝑁𝑍) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
5139, 50remulcld 10663 . . . . . 6 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
5251leidd 11198 . . . . 5 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
5335, 52eqbrtrd 5084 . . . 4 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
5445ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
55 ax-1cn 10587 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
56552timesi 11767 . . . . . . . . . . . . . . 15 (2 · 1) = (1 + 1)
5756oveq2i 7162 . . . . . . . . . . . . . 14 ((𝑁 + (2 · 𝑛)) + (2 · 1)) = ((𝑁 + (2 · 𝑛)) + (1 + 1))
58 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑁𝑍) → 𝑁𝑍)
5958, 27syl6eleq 2927 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑁𝑍) → 𝑁 ∈ (ℤ𝑀))
6059adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ (ℤ𝑀))
61 eluzelz 12245 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
6260, 61syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℤ)
6362zcnd 12080 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℂ)
64 2cn 11704 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
65 nn0cn 11899 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
6665adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℂ)
67 mulcl 10613 . . . . . . . . . . . . . . . 16 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
6864, 66, 67sylancr 587 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℂ)
6964, 55mulcli 10640 . . . . . . . . . . . . . . . 16 (2 · 1) ∈ ℂ
7069a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 1) ∈ ℂ)
7163, 68, 70addassd 10655 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (2 · 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
7257, 71syl5eqr 2874 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (1 + 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
73 2nn0 11906 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ0
74 simpr 485 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
75 nn0mulcl 11925 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℕ0𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
7673, 74, 75sylancr 587 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
77 uzaddcl 12296 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · 𝑛) ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀))
7860, 76, 77syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀))
7928, 78sseldi 3968 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℤ)
8079zcnd 12080 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℂ)
81 1cnd 10628 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 1 ∈ ℂ)
8280, 81, 81addassd 10655 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = ((𝑁 + (2 · 𝑛)) + (1 + 1)))
83 2cnd 11707 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
8483, 66, 81adddid 10657 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
8584oveq2d 7167 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
8672, 82, 853eqtr4d 2870 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = (𝑁 + (2 · (𝑛 + 1))))
87 peano2nn0 11929 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
8887adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑛 + 1) ∈ ℕ0)
89 nn0mulcl 11925 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
9073, 88, 89sylancr 587 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
91 uzaddcl 12296 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · (𝑛 + 1)) ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ𝑀))
9260, 90, 91syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ𝑀))
9392, 27syl6eleqr 2928 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ 𝑍)
9486, 93eqeltrd 2917 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) ∈ 𝑍)
9554, 94ffvelrnd 6847 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
96 peano2uz 12293 . . . . . . . . . . . . 13 ((𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ𝑀))
9778, 96syl 17 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ𝑀))
9897, 27syl6eleqr 2928 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍)
9954, 98ffvelrnd 6847 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
10095, 99resubcld 11060 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
101 0red 10636 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 0 ∈ ℝ)
10239adantr 481 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℝ)
10349ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
10478, 27syl6eleqr 2928 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ 𝑍)
105103, 104ffvelrnd 6847 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℝ)
106102, 105remulcld 10663 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℝ)
107 fvoveq1 7174 . . . . . . . . . . . 12 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘(𝑘 + 1)) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
108 fveq2 6666 . . . . . . . . . . . 12 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺𝑘) = (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
109107, 108breq12d 5075 . . . . . . . . . . 11 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘) ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
110 iseralt.4 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
111110ralrimiva 3186 . . . . . . . . . . . 12 (𝜑 → ∀𝑘𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
112111ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
113109, 112, 98rspcdva 3628 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
11495, 99suble0d 11223 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ≤ 0 ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
115113, 114mpbird 258 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ≤ 0)
116100, 101, 106, 115leadd2dd 11247 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0))
117 seqp1 13377 . . . . . . . . . . . . 13 (((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
11897, 117syl 17 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
119 seqp1 13377 . . . . . . . . . . . . . 14 ((𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))))
12078, 119syl 17 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))))
121120oveq1d 7166 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
122118, 121eqtrd 2860 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
12386fveq2d 6670 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
124105recnd 10661 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℂ)
125 fveq2 6666 . . . . . . . . . . . . . . . . 17 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐹𝑘) = (𝐹‘((𝑁 + (2 · 𝑛)) + 1)))
126 oveq2 7159 . . . . . . . . . . . . . . . . . 18 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝑛)) + 1)))
127126, 108oveq12d 7169 . . . . . . . . . . . . . . . . 17 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
128125, 127eqeq12d 2841 . . . . . . . . . . . . . . . 16 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
12941ralrimiva 3186 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
130129ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
131128, 130, 98rspcdva 3628 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
132 neg1cn 11743 . . . . . . . . . . . . . . . . . . 19 -1 ∈ ℂ
133132a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℂ)
13437a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ≠ 0)
135133, 134, 79expp1zd 13512 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -1))
13636a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℝ)
137136, 134, 79reexpclzd 13603 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℝ)
138137recnd 10661 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ)
139 mulcom 10615 . . . . . . . . . . . . . . . . . 18 (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ -1 ∈ ℂ) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
140138, 132, 139sylancl 586 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
141138mulm1d 11084 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1 · (-1↑(𝑁 + (2 · 𝑛)))) = -(-1↑(𝑁 + (2 · 𝑛))))
142135, 140, 1413eqtrd 2864 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = -(-1↑(𝑁 + (2 · 𝑛))))
143142oveq1d 7166 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
14499recnd 10661 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
145 mulneg12 11070 . . . . . . . . . . . . . . . 16 (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
146138, 144, 145syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
147131, 143, 1463eqtrd 2864 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
14899renegcld 11059 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
149137, 148remulcld 10663 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
150147, 149eqeltrd 2917 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
151150recnd 10661 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
152 fveq2 6666 . . . . . . . . . . . . . . . . 17 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐹𝑘) = (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
153 oveq2 7159 . . . . . . . . . . . . . . . . . 18 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (-1↑𝑘) = (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)))
154 fveq2 6666 . . . . . . . . . . . . . . . . . 18 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐺𝑘) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
155153, 154oveq12d 7169 . . . . . . . . . . . . . . . . 17 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
156152, 155eqeq12d 2841 . . . . . . . . . . . . . . . 16 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
157156, 130, 94rspcdva 3628 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
15879peano2zd 12082 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ ℤ)
159133, 134, 158expp1zd 13512 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1))
160142oveq1d 7166 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1) = (-(-1↑(𝑁 + (2 · 𝑛))) · -1))
161 mul2neg 11071 . . . . . . . . . . . . . . . . . . 19 (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ 1 ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
162138, 55, 161sylancl 586 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
163138mulid1d 10650 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · 1) = (-1↑(𝑁 + (2 · 𝑛))))
164162, 163eqtrd 2860 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1↑(𝑁 + (2 · 𝑛))))
165159, 160, 1643eqtrd 2864 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (-1↑(𝑁 + (2 · 𝑛))))
166165oveq1d 7166 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
167157, 166eqtrd 2860 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
168137, 95remulcld 10663 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
169167, 168eqeltrd 2917 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
170169recnd 10661 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
171124, 151, 170addassd 10655 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
172122, 123, 1713eqtr3d 2868 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
173172oveq2d 7167 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
174102recnd 10661 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℂ)
175150, 169readdcld 10662 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
176175recnd 10661 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℂ)
177174, 124, 176adddid 10657 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
178174, 151, 170adddid 10657 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
179147oveq2d 7167 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
180148recnd 10661 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
181174, 138, 180mulassd 10656 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
182179, 181eqtr4d 2863 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
18383, 63, 66adddid 10657 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑁 + 𝑛)) = ((2 · 𝑁) + (2 · 𝑛)))
184632timesd 11872 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
185184oveq1d 7166 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑁) + (2 · 𝑛)) = ((𝑁 + 𝑁) + (2 · 𝑛)))
18663, 63, 68addassd 10655 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + 𝑁) + (2 · 𝑛)) = (𝑁 + (𝑁 + (2 · 𝑛))))
187183, 185, 1863eqtrrd 2865 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (𝑁 + (2 · 𝑛))) = (2 · (𝑁 + 𝑛)))
188187oveq2d 7167 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = (-1↑(2 · (𝑁 + 𝑛))))
189 expaddz 13466 . . . . . . . . . . . . . . . 16 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ (𝑁 + (2 · 𝑛)) ∈ ℤ)) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
190133, 134, 62, 79, 189syl22anc 836 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
191 2z 12006 . . . . . . . . . . . . . . . . . 18 2 ∈ ℤ
192191a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℤ)
193 nn0z 11997 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
194 zaddcl 12014 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 + 𝑛) ∈ ℤ)
19531, 193, 194syl2an 595 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + 𝑛) ∈ ℤ)
196 expmulz 13468 . . . . . . . . . . . . . . . . 17 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑁 + 𝑛) ∈ ℤ)) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
197133, 134, 192, 195, 196syl22anc 836 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
198 neg1sqe1 13552 . . . . . . . . . . . . . . . . . 18 (-1↑2) = 1
199198oveq1i 7161 . . . . . . . . . . . . . . . . 17 ((-1↑2)↑(𝑁 + 𝑛)) = (1↑(𝑁 + 𝑛))
200 1exp 13451 . . . . . . . . . . . . . . . . . 18 ((𝑁 + 𝑛) ∈ ℤ → (1↑(𝑁 + 𝑛)) = 1)
201195, 200syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (1↑(𝑁 + 𝑛)) = 1)
202199, 201syl5eq 2872 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑2)↑(𝑁 + 𝑛)) = 1)
203197, 202eqtrd 2860 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = 1)
204188, 190, 2033eqtr3d 2868 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) = 1)
205204oveq1d 7166 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
206180mulid2d 10651 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
207182, 205, 2063eqtrd 2864 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
208167oveq2d 7167 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
20995recnd 10661 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
210174, 138, 209mulassd 10656 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
211208, 210eqtr4d 2863 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
212204oveq1d 7166 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
213209mulid2d 10651 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
214211, 212, 2133eqtrd 2864 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
215207, 214oveq12d 7169 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
216144negcld 10976 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
217216, 209addcomd 10834 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
218209, 144negsubd 10995 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
219217, 218eqtrd 2860 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
220178, 215, 2193eqtrd 2864 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
221220oveq2d 7167 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
222173, 177, 2213eqtrrd 2865 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
223106recnd 10661 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℂ)
224223addid1d 10832 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
225116, 222, 2243brtr3d 5093 . . . . . . 7 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
226103, 93ffvelrnd 6847 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) ∈ ℝ)
227102, 226remulcld 10663 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ∈ ℝ)
22851adantr 481 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
229 letr 10726 . . . . . . . 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𝑀( + , 𝐹)‘𝑁))))
230227, 106, 228, 229syl3anc 1365 . . . . . . 7 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
231225, 230mpand 691 . . . . . 6 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
232231expcom 414 . . . . 5 (𝑛 ∈ ℕ0 → ((𝜑𝑁𝑍) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
233232a2d 29 . . . 4 (𝑛 ∈ ℕ0 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
2348, 14, 20, 26, 53, 233nn0ind 12069 . . 3 (𝐾 ∈ ℕ0 → ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
235234com12 32 . 2 ((𝜑𝑁𝑍) → (𝐾 ∈ ℕ0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
2362353impia 1111 1 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081   = wceq 1530  wcel 2107  wne 3020  wral 3142  wss 3939   class class class wbr 5062  wf 6347  cfv 6351  (class class class)co 7151  cc 10527  cr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  cle 10668  cmin 10862  -cneg 10863  2c2 11684  0cn0 11889  cz 11973  cuz 12235  seqcseq 13362  cexp 13422  cli 14834
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 2797  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8282  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-n0 11890  df-z 11974  df-uz 12236  df-fz 12886  df-seq 13363  df-exp 13423
This theorem is referenced by:  iseraltlem3  15033
  Copyright terms: Public domain W3C validator