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

Theorem iseraltlem2 15719
Description: Lemma for iseralt 15721. 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 7439 . . . . . . . . . 10 (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
2 2t0e0 12435 . . . . . . . . . 10 (2 · 0) = 0
31, 2eqtrdi 2793 . . . . . . . . 9 (𝑥 = 0 → (2 · 𝑥) = 0)
43oveq2d 7447 . . . . . . . 8 (𝑥 = 0 → (𝑁 + (2 · 𝑥)) = (𝑁 + 0))
54fveq2d 6910 . . . . . . 7 (𝑥 = 0 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + 0)))
65oveq2d 7447 . . . . . 6 (𝑥 = 0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))))
76breq1d 5153 . . . . 5 (𝑥 = 0 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
87imbi2d 340 . . . 4 (𝑥 = 0 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
9 oveq2 7439 . . . . . . . . 9 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
109oveq2d 7447 . . . . . . . 8 (𝑥 = 𝑛 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝑛)))
1110fveq2d 6910 . . . . . . 7 (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))))
1211oveq2d 7447 . . . . . 6 (𝑥 = 𝑛 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
1312breq1d 5153 . . . . 5 (𝑥 = 𝑛 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
1413imbi2d 340 . . . 4 (𝑥 = 𝑛 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
15 oveq2 7439 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
1615oveq2d 7447 . . . . . . . 8 (𝑥 = (𝑛 + 1) → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · (𝑛 + 1))))
1716fveq2d 6910 . . . . . . 7 (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
1817oveq2d 7447 . . . . . 6 (𝑥 = (𝑛 + 1) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
1918breq1d 5153 . . . . 5 (𝑥 = (𝑛 + 1) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
2019imbi2d 340 . . . 4 (𝑥 = (𝑛 + 1) → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
21 oveq2 7439 . . . . . . . . 9 (𝑥 = 𝐾 → (2 · 𝑥) = (2 · 𝐾))
2221oveq2d 7447 . . . . . . . 8 (𝑥 = 𝐾 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝐾)))
2322fveq2d 6910 . . . . . . 7 (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))
2423oveq2d 7447 . . . . . 6 (𝑥 = 𝐾 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
2524breq1d 5153 . . . . 5 (𝑥 = 𝐾 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
2625imbi2d 340 . . . 4 (𝑥 = 𝐾 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
27 iseralt.1 . . . . . . . . . . . 12 𝑍 = (ℤ𝑀)
28 uzssz 12899 . . . . . . . . . . . 12 (ℤ𝑀) ⊆ ℤ
2927, 28eqsstri 4030 . . . . . . . . . . 11 𝑍 ⊆ ℤ
3029a1i 11 . . . . . . . . . 10 (𝜑𝑍 ⊆ ℤ)
3130sselda 3983 . . . . . . . . 9 ((𝜑𝑁𝑍) → 𝑁 ∈ ℤ)
3231zcnd 12723 . . . . . . . 8 ((𝜑𝑁𝑍) → 𝑁 ∈ ℂ)
3332addridd 11461 . . . . . . 7 ((𝜑𝑁𝑍) → (𝑁 + 0) = 𝑁)
3433fveq2d 6910 . . . . . 6 ((𝜑𝑁𝑍) → (seq𝑀( + , 𝐹)‘(𝑁 + 0)) = (seq𝑀( + , 𝐹)‘𝑁))
3534oveq2d 7447 . . . . 5 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
36 neg1rr 12381 . . . . . . . 8 -1 ∈ ℝ
37 neg1ne0 12382 . . . . . . . 8 -1 ≠ 0
38 reexpclz 14123 . . . . . . . 8 ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (-1↑𝑁) ∈ ℝ)
3936, 37, 31, 38mp3an12i 1467 . . . . . . 7 ((𝜑𝑁𝑍) → (-1↑𝑁) ∈ ℝ)
40 iseralt.2 . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
41 iseralt.6 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
4230sselda 3983 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
43 reexpclz 14123 . . . . . . . . . . . 12 ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈ ℝ)
4436, 37, 42, 43mp3an12i 1467 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
45 iseralt.3 . . . . . . . . . . . 12 (𝜑𝐺:𝑍⟶ℝ)
4645ffvelcdmda 7104 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
4744, 46remulcld 11291 . . . . . . . . . 10 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
4841, 47eqeltrd 2841 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
4927, 40, 48serfre 14072 . . . . . . . 8 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
5049ffvelcdmda 7104 . . . . . . 7 ((𝜑𝑁𝑍) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
5139, 50remulcld 11291 . . . . . 6 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
5251leidd 11829 . . . . 5 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
5335, 52eqbrtrd 5165 . . . 4 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
5445ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
55 ax-1cn 11213 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
56552timesi 12404 . . . . . . . . . . . . . . 15 (2 · 1) = (1 + 1)
5756oveq2i 7442 . . . . . . . . . . . . . 14 ((𝑁 + (2 · 𝑛)) + (2 · 1)) = ((𝑁 + (2 · 𝑛)) + (1 + 1))
58 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑁𝑍) → 𝑁𝑍)
5958, 27eleqtrdi 2851 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑁𝑍) → 𝑁 ∈ (ℤ𝑀))
6059adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ (ℤ𝑀))
61 eluzelz 12888 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
6260, 61syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℤ)
6362zcnd 12723 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℂ)
64 2cn 12341 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
65 nn0cn 12536 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
6665adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℂ)
67 mulcl 11239 . . . . . . . . . . . . . . . 16 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
6864, 66, 67sylancr 587 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℂ)
6964, 55mulcli 11268 . . . . . . . . . . . . . . . 16 (2 · 1) ∈ ℂ
7069a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 1) ∈ ℂ)
7163, 68, 70addassd 11283 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (2 · 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
7257, 71eqtr3id 2791 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (1 + 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
73 2nn0 12543 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ0
74 simpr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
75 nn0mulcl 12562 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℕ0𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
7673, 74, 75sylancr 587 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
77 uzaddcl 12946 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · 𝑛) ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀))
7860, 76, 77syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀))
7928, 78sselid 3981 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℤ)
8079zcnd 12723 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℂ)
81 1cnd 11256 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 1 ∈ ℂ)
8280, 81, 81addassd 11283 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = ((𝑁 + (2 · 𝑛)) + (1 + 1)))
83 2cnd 12344 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
8483, 66, 81adddid 11285 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
8584oveq2d 7447 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
8672, 82, 853eqtr4d 2787 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = (𝑁 + (2 · (𝑛 + 1))))
87 peano2nn0 12566 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
8887adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑛 + 1) ∈ ℕ0)
89 nn0mulcl 12562 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
9073, 88, 89sylancr 587 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
91 uzaddcl 12946 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · (𝑛 + 1)) ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ𝑀))
9260, 90, 91syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ𝑀))
9392, 27eleqtrrdi 2852 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ 𝑍)
9486, 93eqeltrd 2841 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) ∈ 𝑍)
9554, 94ffvelcdmd 7105 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
96 peano2uz 12943 . . . . . . . . . . . . 13 ((𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ𝑀))
9778, 96syl 17 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ𝑀))
9897, 27eleqtrrdi 2852 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍)
9954, 98ffvelcdmd 7105 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
10095, 99resubcld 11691 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
101 0red 11264 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 0 ∈ ℝ)
10239adantr 480 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℝ)
10349ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
10478, 27eleqtrrdi 2852 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ 𝑍)
105103, 104ffvelcdmd 7105 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℝ)
106102, 105remulcld 11291 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℝ)
107 fvoveq1 7454 . . . . . . . . . . . 12 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘(𝑘 + 1)) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
108 fveq2 6906 . . . . . . . . . . . 12 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺𝑘) = (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
109107, 108breq12d 5156 . . . . . . . . . . 11 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘) ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
110 iseralt.4 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
111110ralrimiva 3146 . . . . . . . . . . . 12 (𝜑 → ∀𝑘𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
112111ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
113109, 112, 98rspcdva 3623 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
11495, 99suble0d 11854 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ≤ 0 ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
115113, 114mpbird 257 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ≤ 0)
116100, 101, 106, 115leadd2dd 11878 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0))
117 seqp1 14057 . . . . . . . . . . . . 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 14057 . . . . . . . . . . . . . 14 ((𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))))
12078, 119syl 17 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))))
121120oveq1d 7446 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
122118, 121eqtrd 2777 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
12386fveq2d 6910 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
124105recnd 11289 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℂ)
125 fveq2 6906 . . . . . . . . . . . . . . . . 17 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐹𝑘) = (𝐹‘((𝑁 + (2 · 𝑛)) + 1)))
126 oveq2 7439 . . . . . . . . . . . . . . . . . 18 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝑛)) + 1)))
127126, 108oveq12d 7449 . . . . . . . . . . . . . . . . 17 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
128125, 127eqeq12d 2753 . . . . . . . . . . . . . . . 16 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
12941ralrimiva 3146 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
130129ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
131128, 130, 98rspcdva 3623 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
132 neg1cn 12380 . . . . . . . . . . . . . . . . . . 19 -1 ∈ ℂ
133132a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℂ)
13437a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ≠ 0)
135133, 134, 79expp1zd 14195 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -1))
13636a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℝ)
137136, 134, 79reexpclzd 14288 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℝ)
138137recnd 11289 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ)
139 mulcom 11241 . . . . . . . . . . . . . . . . . 18 (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ -1 ∈ ℂ) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
140138, 132, 139sylancl 586 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
141138mulm1d 11715 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1 · (-1↑(𝑁 + (2 · 𝑛)))) = -(-1↑(𝑁 + (2 · 𝑛))))
142135, 140, 1413eqtrd 2781 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = -(-1↑(𝑁 + (2 · 𝑛))))
143142oveq1d 7446 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
14499recnd 11289 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
145 mulneg12 11701 . . . . . . . . . . . . . . . 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 2781 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
14899renegcld 11690 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
149137, 148remulcld 11291 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
150147, 149eqeltrd 2841 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
151150recnd 11289 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
152 fveq2 6906 . . . . . . . . . . . . . . . . 17 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐹𝑘) = (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
153 oveq2 7439 . . . . . . . . . . . . . . . . . 18 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (-1↑𝑘) = (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)))
154 fveq2 6906 . . . . . . . . . . . . . . . . . 18 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐺𝑘) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
155153, 154oveq12d 7449 . . . . . . . . . . . . . . . . 17 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
156152, 155eqeq12d 2753 . . . . . . . . . . . . . . . 16 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
157156, 130, 94rspcdva 3623 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
15879peano2zd 12725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ ℤ)
159133, 134, 158expp1zd 14195 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1))
160142oveq1d 7446 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1) = (-(-1↑(𝑁 + (2 · 𝑛))) · -1))
161 mul2neg 11702 . . . . . . . . . . . . . . . . . . 19 (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ 1 ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
162138, 55, 161sylancl 586 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
163138mulridd 11278 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · 1) = (-1↑(𝑁 + (2 · 𝑛))))
164162, 163eqtrd 2777 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1↑(𝑁 + (2 · 𝑛))))
165159, 160, 1643eqtrd 2781 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (-1↑(𝑁 + (2 · 𝑛))))
166165oveq1d 7446 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
167157, 166eqtrd 2777 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
168137, 95remulcld 11291 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
169167, 168eqeltrd 2841 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
170169recnd 11289 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
171124, 151, 170addassd 11283 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
172122, 123, 1713eqtr3d 2785 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
173172oveq2d 7447 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
174102recnd 11289 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℂ)
175150, 169readdcld 11290 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
176175recnd 11289 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℂ)
177174, 124, 176adddid 11285 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
178174, 151, 170adddid 11285 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
179147oveq2d 7447 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
180148recnd 11289 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
181174, 138, 180mulassd 11284 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
182179, 181eqtr4d 2780 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
18383, 63, 66adddid 11285 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑁 + 𝑛)) = ((2 · 𝑁) + (2 · 𝑛)))
184632timesd 12509 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
185184oveq1d 7446 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑁) + (2 · 𝑛)) = ((𝑁 + 𝑁) + (2 · 𝑛)))
18663, 63, 68addassd 11283 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + 𝑁) + (2 · 𝑛)) = (𝑁 + (𝑁 + (2 · 𝑛))))
187183, 185, 1863eqtrrd 2782 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (𝑁 + (2 · 𝑛))) = (2 · (𝑁 + 𝑛)))
188187oveq2d 7447 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = (-1↑(2 · (𝑁 + 𝑛))))
189 expaddz 14147 . . . . . . . . . . . . . . . 16 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ (𝑁 + (2 · 𝑛)) ∈ ℤ)) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
190133, 134, 62, 79, 189syl22anc 839 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
191 2z 12649 . . . . . . . . . . . . . . . . . 18 2 ∈ ℤ
192191a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℤ)
193 nn0z 12638 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
194 zaddcl 12657 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 + 𝑛) ∈ ℤ)
19531, 193, 194syl2an 596 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + 𝑛) ∈ ℤ)
196 expmulz 14149 . . . . . . . . . . . . . . . . 17 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑁 + 𝑛) ∈ ℤ)) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
197133, 134, 192, 195, 196syl22anc 839 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
198 neg1sqe1 14235 . . . . . . . . . . . . . . . . . 18 (-1↑2) = 1
199198oveq1i 7441 . . . . . . . . . . . . . . . . 17 ((-1↑2)↑(𝑁 + 𝑛)) = (1↑(𝑁 + 𝑛))
200 1exp 14132 . . . . . . . . . . . . . . . . . 18 ((𝑁 + 𝑛) ∈ ℤ → (1↑(𝑁 + 𝑛)) = 1)
201195, 200syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (1↑(𝑁 + 𝑛)) = 1)
202199, 201eqtrid 2789 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑2)↑(𝑁 + 𝑛)) = 1)
203197, 202eqtrd 2777 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = 1)
204188, 190, 2033eqtr3d 2785 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) = 1)
205204oveq1d 7446 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
206180mullidd 11279 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
207182, 205, 2063eqtrd 2781 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
208167oveq2d 7447 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
20995recnd 11289 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
210174, 138, 209mulassd 11284 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
211208, 210eqtr4d 2780 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
212204oveq1d 7446 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
213209mullidd 11279 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
214211, 212, 2133eqtrd 2781 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
215207, 214oveq12d 7449 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
216144negcld 11607 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
217216, 209addcomd 11463 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
218209, 144negsubd 11626 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
219217, 218eqtrd 2777 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
220178, 215, 2193eqtrd 2781 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
221220oveq2d 7447 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
222173, 177, 2213eqtrrd 2782 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
223106recnd 11289 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℂ)
224223addridd 11461 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
225116, 222, 2243brtr3d 5174 . . . . . . 7 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
226103, 93ffvelcdmd 7105 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) ∈ ℝ)
227102, 226remulcld 11291 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ∈ ℝ)
22851adantr 480 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
229 letr 11355 . . . . . . . 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 1373 . . . . . . 7 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
231225, 230mpand 695 . . . . . 6 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
232231expcom 413 . . . . 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 12713 . . 3 (𝐾 ∈ ℕ0 → ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
235234com12 32 . 2 ((𝜑𝑁𝑍) → (𝐾 ∈ ℕ0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
2362353impia 1118 1 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wral 3061  wss 3951   class class class wbr 5143  wf 6557  cfv 6561  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  cle 11296  cmin 11492  -cneg 11493  2c2 12321  0cn0 12526  cz 12613  cuz 12878  seqcseq 14042  cexp 14102  cli 15520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-seq 14043  df-exp 14103
This theorem is referenced by:  iseraltlem3  15720
  Copyright terms: Public domain W3C validator