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

Theorem iseraltlem2 14342
Description: Lemma for iseralt 14344. 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 6613 . . . . . . . . . 10 (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
2 2t0e0 11128 . . . . . . . . . 10 (2 · 0) = 0
31, 2syl6eq 2676 . . . . . . . . 9 (𝑥 = 0 → (2 · 𝑥) = 0)
43oveq2d 6621 . . . . . . . 8 (𝑥 = 0 → (𝑁 + (2 · 𝑥)) = (𝑁 + 0))
54fveq2d 6154 . . . . . . 7 (𝑥 = 0 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + 0)))
65oveq2d 6621 . . . . . 6 (𝑥 = 0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))))
76breq1d 4628 . . . . 5 (𝑥 = 0 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
87imbi2d 330 . . . 4 (𝑥 = 0 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
9 oveq2 6613 . . . . . . . . 9 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
109oveq2d 6621 . . . . . . . 8 (𝑥 = 𝑛 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝑛)))
1110fveq2d 6154 . . . . . . 7 (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))))
1211oveq2d 6621 . . . . . 6 (𝑥 = 𝑛 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
1312breq1d 4628 . . . . 5 (𝑥 = 𝑛 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
1413imbi2d 330 . . . 4 (𝑥 = 𝑛 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
15 oveq2 6613 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
1615oveq2d 6621 . . . . . . . 8 (𝑥 = (𝑛 + 1) → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · (𝑛 + 1))))
1716fveq2d 6154 . . . . . . 7 (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
1817oveq2d 6621 . . . . . 6 (𝑥 = (𝑛 + 1) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
1918breq1d 4628 . . . . 5 (𝑥 = (𝑛 + 1) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
2019imbi2d 330 . . . 4 (𝑥 = (𝑛 + 1) → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
21 oveq2 6613 . . . . . . . . 9 (𝑥 = 𝐾 → (2 · 𝑥) = (2 · 𝐾))
2221oveq2d 6621 . . . . . . . 8 (𝑥 = 𝐾 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝐾)))
2322fveq2d 6154 . . . . . . 7 (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))
2423oveq2d 6621 . . . . . 6 (𝑥 = 𝐾 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
2524breq1d 4628 . . . . 5 (𝑥 = 𝐾 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
2625imbi2d 330 . . . 4 (𝑥 = 𝐾 → (((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
27 iseralt.1 . . . . . . . . . . . 12 𝑍 = (ℤ𝑀)
28 uzssz 11651 . . . . . . . . . . . 12 (ℤ𝑀) ⊆ ℤ
2927, 28eqsstri 3619 . . . . . . . . . . 11 𝑍 ⊆ ℤ
3029a1i 11 . . . . . . . . . 10 (𝜑𝑍 ⊆ ℤ)
3130sselda 3588 . . . . . . . . 9 ((𝜑𝑁𝑍) → 𝑁 ∈ ℤ)
3231zcnd 11427 . . . . . . . 8 ((𝜑𝑁𝑍) → 𝑁 ∈ ℂ)
3332addid1d 10181 . . . . . . 7 ((𝜑𝑁𝑍) → (𝑁 + 0) = 𝑁)
3433fveq2d 6154 . . . . . 6 ((𝜑𝑁𝑍) → (seq𝑀( + , 𝐹)‘(𝑁 + 0)) = (seq𝑀( + , 𝐹)‘𝑁))
3534oveq2d 6621 . . . . 5 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
36 neg1rr 11070 . . . . . . . . 9 -1 ∈ ℝ
37 neg1ne0 11071 . . . . . . . . 9 -1 ≠ 0
38 reexpclz 12817 . . . . . . . . 9 ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (-1↑𝑁) ∈ ℝ)
3936, 37, 38mp3an12 1411 . . . . . . . 8 (𝑁 ∈ ℤ → (-1↑𝑁) ∈ ℝ)
4031, 39syl 17 . . . . . . 7 ((𝜑𝑁𝑍) → (-1↑𝑁) ∈ ℝ)
41 iseralt.2 . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
42 iseralt.6 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
4330sselda 3588 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
44 reexpclz 12817 . . . . . . . . . . . . 13 ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈ ℝ)
4536, 37, 44mp3an12 1411 . . . . . . . . . . . 12 (𝑘 ∈ ℤ → (-1↑𝑘) ∈ ℝ)
4643, 45syl 17 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
47 iseralt.3 . . . . . . . . . . . 12 (𝜑𝐺:𝑍⟶ℝ)
4847ffvelrnda 6316 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
4946, 48remulcld 10015 . . . . . . . . . 10 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
5042, 49eqeltrd 2704 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
5127, 41, 50serfre 12767 . . . . . . . 8 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
5251ffvelrnda 6316 . . . . . . 7 ((𝜑𝑁𝑍) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
5340, 52remulcld 10015 . . . . . 6 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
5453leidd 10539 . . . . 5 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
5535, 54eqbrtrd 4640 . . . 4 ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
5647ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
57 ax-1cn 9939 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
58572timesi 11092 . . . . . . . . . . . . . . 15 (2 · 1) = (1 + 1)
5958oveq2i 6616 . . . . . . . . . . . . . 14 ((𝑁 + (2 · 𝑛)) + (2 · 1)) = ((𝑁 + (2 · 𝑛)) + (1 + 1))
60 simpr 477 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑁𝑍) → 𝑁𝑍)
6160, 27syl6eleq 2714 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑁𝑍) → 𝑁 ∈ (ℤ𝑀))
6261adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ (ℤ𝑀))
63 eluzelz 11641 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
6462, 63syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℤ)
6564zcnd 11427 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℂ)
66 2cn 11036 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
67 nn0cn 11247 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
6867adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℂ)
69 mulcl 9965 . . . . . . . . . . . . . . . 16 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
7066, 68, 69sylancr 694 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℂ)
7166, 57mulcli 9990 . . . . . . . . . . . . . . . 16 (2 · 1) ∈ ℂ
7271a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 1) ∈ ℂ)
7365, 70, 72addassd 10007 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (2 · 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
7459, 73syl5eqr 2674 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (1 + 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
75 2nn0 11254 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ0
76 simpr 477 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
77 nn0mulcl 11274 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℕ0𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
7875, 76, 77sylancr 694 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
79 uzaddcl 11688 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · 𝑛) ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀))
8062, 78, 79syl2anc 692 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀))
8128, 80sseldi 3586 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℤ)
8281zcnd 11427 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℂ)
83 1cnd 10001 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 1 ∈ ℂ)
8482, 83, 83addassd 10007 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = ((𝑁 + (2 · 𝑛)) + (1 + 1)))
85 2cnd 11038 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
8685, 68, 83adddid 10009 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
8786oveq2d 6621 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
8874, 84, 873eqtr4d 2670 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = (𝑁 + (2 · (𝑛 + 1))))
89 peano2nn0 11278 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
9089adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑛 + 1) ∈ ℕ0)
91 nn0mulcl 11274 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
9275, 90, 91sylancr 694 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
93 uzaddcl 11688 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · (𝑛 + 1)) ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ𝑀))
9462, 92, 93syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ𝑀))
9594, 27syl6eleqr 2715 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ 𝑍)
9688, 95eqeltrd 2704 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) ∈ 𝑍)
9756, 96ffvelrnd 6317 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
98 peano2uz 11685 . . . . . . . . . . . . 13 ((𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ𝑀))
9980, 98syl 17 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ𝑀))
10099, 27syl6eleqr 2715 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍)
10156, 100ffvelrnd 6317 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
10297, 101resubcld 10403 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
103 0red 9986 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 0 ∈ ℝ)
10440adantr 481 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℝ)
10551ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
10680, 27syl6eleqr 2715 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ 𝑍)
107105, 106ffvelrnd 6317 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℝ)
108104, 107remulcld 10015 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℝ)
109 iseralt.4 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
110109ralrimiva 2965 . . . . . . . . . . . 12 (𝜑 → ∀𝑘𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
111110ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
112 oveq1 6612 . . . . . . . . . . . . . 14 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝑘 + 1) = (((𝑁 + (2 · 𝑛)) + 1) + 1))
113112fveq2d 6154 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘(𝑘 + 1)) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
114 fveq2 6150 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺𝑘) = (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
115113, 114breq12d 4631 . . . . . . . . . . . 12 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘) ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
116115rspcv 3296 . . . . . . . . . . 11 (((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍 → (∀𝑘𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
117100, 111, 116sylc 65 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
11897, 101suble0d 10563 . . . . . . . . . 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 10587 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0))
121 seqp1 12753 . . . . . . . . . . . . 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 12753 . . . . . . . . . . . . . 14 ((𝑁 + (2 · 𝑛)) ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))))
12480, 123syl 17 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))))
125124oveq1d 6620 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
126122, 125eqtrd 2660 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
12788fveq2d 6154 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
128107recnd 10013 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℂ)
12942ralrimiva 2965 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
130129ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
131 fveq2 6150 . . . . . . . . . . . . . . . . . 18 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐹𝑘) = (𝐹‘((𝑁 + (2 · 𝑛)) + 1)))
132 oveq2 6613 . . . . . . . . . . . . . . . . . . 19 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝑛)) + 1)))
133132, 114oveq12d 6623 . . . . . . . . . . . . . . . . . 18 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
134131, 133eqeq12d 2641 . . . . . . . . . . . . . . . . 17 (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
135134rspcv 3296 . . . . . . . . . . . . . . . 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 11069 . . . . . . . . . . . . . . . . . . 19 -1 ∈ ℂ
138137a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℂ)
13937a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ≠ 0)
140138, 139, 81expp1zd 12954 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -1))
14136a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℝ)
142141, 139, 81reexpclzd 12971 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℝ)
143142recnd 10013 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ)
144 mulcom 9967 . . . . . . . . . . . . . . . . . 18 (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ -1 ∈ ℂ) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
145143, 137, 144sylancl 693 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
146143mulm1d 10427 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1 · (-1↑(𝑁 + (2 · 𝑛)))) = -(-1↑(𝑁 + (2 · 𝑛))))
147140, 145, 1463eqtrd 2664 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = -(-1↑(𝑁 + (2 · 𝑛))))
148147oveq1d 6620 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
149101recnd 10013 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
150 mulneg12 10413 . . . . . . . . . . . . . . . 16 (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
151143, 149, 150syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
152136, 148, 1513eqtrd 2664 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
153101renegcld 10402 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
154142, 153remulcld 10015 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
155152, 154eqeltrd 2704 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
156155recnd 10013 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
157 fveq2 6150 . . . . . . . . . . . . . . . . . 18 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐹𝑘) = (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
158 oveq2 6613 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (-1↑𝑘) = (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)))
159 fveq2 6150 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐺𝑘) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
160158, 159oveq12d 6623 . . . . . . . . . . . . . . . . . 18 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
161157, 160eqeq12d 2641 . . . . . . . . . . . . . . . . 17 (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
162161rspcv 3296 . . . . . . . . . . . . . . . 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 11429 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ ℤ)
165138, 139, 164expp1zd 12954 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1))
166147oveq1d 6620 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1) = (-(-1↑(𝑁 + (2 · 𝑛))) · -1))
167 mul2neg 10414 . . . . . . . . . . . . . . . . . . 19 (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ 1 ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
168143, 57, 167sylancl 693 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
169143mulid1d 10002 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · 1) = (-1↑(𝑁 + (2 · 𝑛))))
170168, 169eqtrd 2660 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1↑(𝑁 + (2 · 𝑛))))
171165, 166, 1703eqtrd 2664 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (-1↑(𝑁 + (2 · 𝑛))))
172171oveq1d 6620 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
173163, 172eqtrd 2660 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
174142, 97remulcld 10015 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
175173, 174eqeltrd 2704 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
176175recnd 10013 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
177128, 156, 176addassd 10007 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
178126, 127, 1773eqtr3d 2668 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
179178oveq2d 6621 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
180104recnd 10013 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℂ)
181155, 175readdcld 10014 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
182181recnd 10013 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℂ)
183180, 128, 182adddid 10009 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
184180, 156, 176adddid 10009 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
185152oveq2d 6621 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
186153recnd 10013 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
187180, 143, 186mulassd 10008 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
188185, 187eqtr4d 2663 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
18985, 65, 68adddid 10009 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑁 + 𝑛)) = ((2 · 𝑁) + (2 · 𝑛)))
190652timesd 11220 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
191190oveq1d 6620 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑁) + (2 · 𝑛)) = ((𝑁 + 𝑁) + (2 · 𝑛)))
19265, 65, 70addassd 10007 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + 𝑁) + (2 · 𝑛)) = (𝑁 + (𝑁 + (2 · 𝑛))))
193189, 191, 1923eqtrrd 2665 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (𝑁 + (2 · 𝑛))) = (2 · (𝑁 + 𝑛)))
194193oveq2d 6621 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = (-1↑(2 · (𝑁 + 𝑛))))
195 expaddz 12841 . . . . . . . . . . . . . . . 16 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ (𝑁 + (2 · 𝑛)) ∈ ℤ)) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
196138, 139, 64, 81, 195syl22anc 1324 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
197 2z 11354 . . . . . . . . . . . . . . . . . 18 2 ∈ ℤ
198197a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℤ)
199 nn0z 11345 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
200 zaddcl 11362 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 + 𝑛) ∈ ℤ)
20131, 199, 200syl2an 494 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + 𝑛) ∈ ℤ)
202 expmulz 12843 . . . . . . . . . . . . . . . . 17 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑁 + 𝑛) ∈ ℤ)) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
203138, 139, 198, 201, 202syl22anc 1324 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
204 neg1sqe1 12896 . . . . . . . . . . . . . . . . . 18 (-1↑2) = 1
205204oveq1i 6615 . . . . . . . . . . . . . . . . 17 ((-1↑2)↑(𝑁 + 𝑛)) = (1↑(𝑁 + 𝑛))
206 1exp 12826 . . . . . . . . . . . . . . . . . 18 ((𝑁 + 𝑛) ∈ ℤ → (1↑(𝑁 + 𝑛)) = 1)
207201, 206syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (1↑(𝑁 + 𝑛)) = 1)
208205, 207syl5eq 2672 . . . . . . . . . . . . . . . 16 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑2)↑(𝑁 + 𝑛)) = 1)
209203, 208eqtrd 2660 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = 1)
210194, 196, 2093eqtr3d 2668 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) = 1)
211210oveq1d 6620 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
212186mulid2d 10003 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
213188, 211, 2123eqtrd 2664 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
214173oveq2d 6621 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
21597recnd 10013 . . . . . . . . . . . . . . 15 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
216180, 143, 215mulassd 10008 . . . . . . . . . . . . . 14 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
217214, 216eqtr4d 2663 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
218210oveq1d 6620 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
219215mulid2d 10003 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
220217, 218, 2193eqtrd 2664 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
221213, 220oveq12d 6623 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
222149negcld 10324 . . . . . . . . . . . . 13 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
223222, 215addcomd 10183 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
224215, 149negsubd 10343 . . . . . . . . . . . 12 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
225223, 224eqtrd 2660 . . . . . . . . . . 11 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
226184, 221, 2253eqtrd 2664 . . . . . . . . . 10 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
227226oveq2d 6621 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
228179, 183, 2273eqtrrd 2665 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
229108recnd 10013 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℂ)
230229addid1d 10181 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
231120, 228, 2303brtr3d 4649 . . . . . . 7 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
232105, 95ffvelrnd 6317 . . . . . . . . 9 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) ∈ ℝ)
233104, 232remulcld 10015 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ∈ ℝ)
23453adantr 481 . . . . . . . 8 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
235 letr 10076 . . . . . . . 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 1323 . . . . . . 7 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
237231, 236mpand 710 . . . . . 6 (((𝜑𝑁𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
238237expcom 451 . . . . 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 11416 . . 3 (𝐾 ∈ ℕ0 → ((𝜑𝑁𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
241240com12 32 . 2 ((𝜑𝑁𝑍) → (𝐾 ∈ ℕ0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
2422413impia 1258 1 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1992  wne 2796  wral 2912  wss 3560   class class class wbr 4618  wf 5846  cfv 5850  (class class class)co 6605  cc 9879  cr 9880  0cc0 9881  1c1 9882   + caddc 9884   · cmul 9886  cle 10020  cmin 10211  -cneg 10212  2c2 11015  0cn0 11237  cz 11322  cuz 11631  seqcseq 12738  cexp 12797  cli 14144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-er 7688  df-en 7901  df-dom 7902  df-sdom 7903  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-nn 10966  df-2 11024  df-n0 11238  df-z 11323  df-uz 11632  df-fz 12266  df-seq 12739  df-exp 12798
This theorem is referenced by:  iseraltlem3  14343
  Copyright terms: Public domain W3C validator