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

Theorem iseralt 14352
Description: The alternating series test. If 𝐺(𝑘) is a decreasing sequence that converges to 0, then Σ𝑘𝑍(-1↑𝑘) · 𝐺(𝑘) is a convergent series. (Note that the first term is positive if 𝑀 is even, and negative if 𝑀 is odd. If the parity of your series does not match up with this, you will need to post-compose the series with multiplication by -1 using isermulc2 14325.) (Contributed by Mario Carneiro, 7-Apr-2015.)
Hypotheses
Ref Expression
iseralt.1 𝑍 = (ℤ𝑀)
iseralt.2 (𝜑𝑀 ∈ ℤ)
iseralt.3 (𝜑𝐺:𝑍⟶ℝ)
iseralt.4 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
iseralt.5 (𝜑𝐺 ⇝ 0)
iseralt.6 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
Assertion
Ref Expression
iseralt (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Distinct variable groups:   𝑘,𝐹   𝑘,𝐺   𝑘,𝑀   𝜑,𝑘   𝑘,𝑍

Proof of Theorem iseralt
Dummy variables 𝑗 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iseralt.1 . 2 𝑍 = (ℤ𝑀)
2 seqex 12746 . . 3 seq𝑀( + , 𝐹) ∈ V
32a1i 11 . 2 (𝜑 → seq𝑀( + , 𝐹) ∈ V)
4 iseralt.5 . . . 4 (𝜑𝐺 ⇝ 0)
5 iseralt.2 . . . . 5 (𝜑𝑀 ∈ ℤ)
6 climrel 14160 . . . . . . 7 Rel ⇝
76brrelexi 5120 . . . . . 6 (𝐺 ⇝ 0 → 𝐺 ∈ V)
84, 7syl 17 . . . . 5 (𝜑𝐺 ∈ V)
9 eqidd 2622 . . . . 5 ((𝜑𝑛𝑍) → (𝐺𝑛) = (𝐺𝑛))
10 iseralt.3 . . . . . . 7 (𝜑𝐺:𝑍⟶ℝ)
1110ffvelrnda 6317 . . . . . 6 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ ℝ)
1211recnd 10015 . . . . 5 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ ℂ)
131, 5, 8, 9, 12clim0c 14175 . . . 4 (𝜑 → (𝐺 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥))
144, 13mpbid 222 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥)
15 simpr 477 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗𝑍)
1615, 1syl6eleq 2708 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
17 eluzelz 11644 . . . . . . . 8 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℤ)
18 uzid 11649 . . . . . . . 8 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
1916, 17, 183syl 18 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗 ∈ (ℤ𝑗))
20 peano2uz 11688 . . . . . . 7 (𝑗 ∈ (ℤ𝑗) → (𝑗 + 1) ∈ (ℤ𝑗))
21 fveq2 6150 . . . . . . . . . 10 (𝑛 = (𝑗 + 1) → (𝐺𝑛) = (𝐺‘(𝑗 + 1)))
2221fveq2d 6154 . . . . . . . . 9 (𝑛 = (𝑗 + 1) → (abs‘(𝐺𝑛)) = (abs‘(𝐺‘(𝑗 + 1))))
2322breq1d 4625 . . . . . . . 8 (𝑛 = (𝑗 + 1) → ((abs‘(𝐺𝑛)) < 𝑥 ↔ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
2423rspcv 3291 . . . . . . 7 ((𝑗 + 1) ∈ (ℤ𝑗) → (∀𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
2519, 20, 243syl 18 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
26 eluzelz 11644 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (ℤ𝑗) → 𝑛 ∈ ℤ)
2726ad2antll 764 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ ℤ)
2827zcnd 11430 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ ℂ)
2917, 1eleq2s 2716 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑍𝑗 ∈ ℤ)
3029ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℤ)
3130zcnd 11430 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℂ)
3228, 31subcld 10339 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℂ)
33 2cnd 11040 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 2 ∈ ℂ)
34 2ne0 11060 . . . . . . . . . . . . . . . . . . . . . 22 2 ≠ 0
3534a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 2 ≠ 0)
3632, 33, 35divcan2d 10750 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · ((𝑛𝑗) / 2)) = (𝑛𝑗))
3736oveq2d 6623 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (2 · ((𝑛𝑗) / 2))) = (𝑗 + (𝑛𝑗)))
3831, 28pncan3d 10342 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (𝑛𝑗)) = 𝑛)
3937, 38eqtr2d 2656 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 = (𝑗 + (2 · ((𝑛𝑗) / 2))))
4039adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 𝑛 = (𝑗 + (2 · ((𝑛𝑗) / 2))))
4140fveq2d 6154 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))))
4241oveq1d 6622 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) = ((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗)))
4342fveq2d 6154 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))))
44 simpll 789 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 𝜑)
45 simpl 473 . . . . . . . . . . . . . . . 16 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → 𝑗𝑍)
4645ad2antlr 762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 𝑗𝑍)
47 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → ((𝑛𝑗) / 2) ∈ ℤ)
4827, 30zsubcld 11434 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℤ)
4948zred 11429 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℝ)
50 eluzle 11647 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ𝑗) → 𝑗𝑛)
5150ad2antll 764 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗𝑛)
5227zred 11429 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ ℝ)
5330zred 11429 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℝ)
5452, 53subge0d 10564 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (0 ≤ (𝑛𝑗) ↔ 𝑗𝑛))
5551, 54mpbird 247 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 ≤ (𝑛𝑗))
56 2re 11037 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ
5756a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 2 ∈ ℝ)
58 2pos 11059 . . . . . . . . . . . . . . . . . . 19 0 < 2
5958a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 < 2)
60 divge0 10839 . . . . . . . . . . . . . . . . . 18 ((((𝑛𝑗) ∈ ℝ ∧ 0 ≤ (𝑛𝑗)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑛𝑗) / 2))
6149, 55, 57, 59, 60syl22anc 1324 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 ≤ ((𝑛𝑗) / 2))
6261adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → 0 ≤ ((𝑛𝑗) / 2))
63 elnn0z 11337 . . . . . . . . . . . . . . . 16 (((𝑛𝑗) / 2) ∈ ℕ0 ↔ (((𝑛𝑗) / 2) ∈ ℤ ∧ 0 ≤ ((𝑛𝑗) / 2)))
6447, 62, 63sylanbrc 697 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → ((𝑛𝑗) / 2) ∈ ℕ0)
65 iseralt.4 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
66 iseralt.6 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
671, 5, 10, 65, 4, 66iseraltlem3 14351 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑍 ∧ ((𝑛𝑗) / 2) ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((𝑛𝑗) / 2))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))))
6867simpld 475 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑍 ∧ ((𝑛𝑗) / 2) ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
6944, 46, 64, 68syl3anc 1323 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
7043, 69eqbrtrd 4637 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ ((𝑛𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
71 2div2e1 11097 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (2 / 2) = 1
7271oveq2i 6618 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑛𝑗) + 1) / 2) − (2 / 2)) = ((((𝑛𝑗) + 1) / 2) − 1)
73 peano2cn 10155 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑛𝑗) ∈ ℂ → ((𝑛𝑗) + 1) ∈ ℂ)
7432, 73syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) + 1) ∈ ℂ)
7574, 33, 33, 35divsubdird 10787 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) − 2) / 2) = ((((𝑛𝑗) + 1) / 2) − (2 / 2)))
76 df-2 11026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 = (1 + 1)
7776oveq2i 6618 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑛𝑗) + 1) − 2) = (((𝑛𝑗) + 1) − (1 + 1))
78 ax-1cn 9941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ∈ ℂ
7978a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 1 ∈ ℂ)
8032, 79, 79pnpcan2d 10377 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) + 1) − (1 + 1)) = ((𝑛𝑗) − 1))
8177, 80syl5eq 2667 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) + 1) − 2) = ((𝑛𝑗) − 1))
8281oveq1d 6622 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) − 2) / 2) = (((𝑛𝑗) − 1) / 2))
8375, 82eqtr3d 2657 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) / 2) − (2 / 2)) = (((𝑛𝑗) − 1) / 2))
8472, 83syl5eqr 2669 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((((𝑛𝑗) + 1) / 2) − 1) = (((𝑛𝑗) − 1) / 2))
8584oveq2d 6623 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · ((((𝑛𝑗) + 1) / 2) − 1)) = (2 · (((𝑛𝑗) − 1) / 2)))
86 subcl 10227 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛𝑗) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛𝑗) − 1) ∈ ℂ)
8732, 78, 86sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) − 1) ∈ ℂ)
8887, 33, 35divcan2d 10750 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · (((𝑛𝑗) − 1) / 2)) = ((𝑛𝑗) − 1))
8928, 31, 79sub32d 10371 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) − 1) = ((𝑛 − 1) − 𝑗))
9085, 88, 893eqtrd 2659 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (2 · ((((𝑛𝑗) + 1) / 2) − 1)) = ((𝑛 − 1) − 𝑗))
9190oveq2d 6623 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) = (𝑗 + ((𝑛 − 1) − 𝑗)))
92 subcl 10227 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑛 − 1) ∈ ℂ)
9328, 78, 92sylancl 693 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛 − 1) ∈ ℂ)
9431, 93pncan3d 10342 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + ((𝑛 − 1) − 𝑗)) = (𝑛 − 1))
9591, 94eqtrd 2655 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) = (𝑛 − 1))
9695oveq1d 6622 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1) = ((𝑛 − 1) + 1))
97 npcan 10237 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
9828, 78, 97sylancl 693 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛 − 1) + 1) = 𝑛)
9996, 98eqtr2d 2656 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑛 = ((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1))
10099adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 𝑛 = ((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1))
101100fveq2d 6154 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)))
102101oveq1d 6622 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) = ((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗)))
103102fveq2d 6154 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))))
104 simpll 789 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 𝜑)
10545ad2antlr 762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 𝑗𝑍)
106 simpr 477 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (((𝑛𝑗) + 1) / 2) ∈ ℤ)
107 uznn0sub 11666 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℤ𝑗) → (𝑛𝑗) ∈ ℕ0)
108107ad2antll 764 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝑛𝑗) ∈ ℕ0)
109 nn0p1nn 11279 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛𝑗) ∈ ℕ0 → ((𝑛𝑗) + 1) ∈ ℕ)
110108, 109syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) + 1) ∈ ℕ)
111110nnrpd 11817 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((𝑛𝑗) + 1) ∈ ℝ+)
112111rphalfcld 11831 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) + 1) / 2) ∈ ℝ+)
113112rpgt0d 11822 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 < (((𝑛𝑗) + 1) / 2))
114113adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → 0 < (((𝑛𝑗) + 1) / 2))
115 elnnz 11334 . . . . . . . . . . . . . . . . 17 ((((𝑛𝑗) + 1) / 2) ∈ ℕ ↔ ((((𝑛𝑗) + 1) / 2) ∈ ℤ ∧ 0 < (((𝑛𝑗) + 1) / 2)))
116106, 114, 115sylanbrc 697 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (((𝑛𝑗) + 1) / 2) ∈ ℕ)
117 nnm1nn0 11281 . . . . . . . . . . . . . . . 16 ((((𝑛𝑗) + 1) / 2) ∈ ℕ → ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0)
118116, 117syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0)
1191, 5, 10, 65, 4, 66iseraltlem3 14351 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑍 ∧ ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))))
120119simprd 479 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑍 ∧ ((((𝑛𝑗) + 1) / 2) − 1) ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
121104, 105, 118, 120syl3anc 1323 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
122103, 121eqbrtrd 4637 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) ∧ (((𝑛𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
123 zeo 11410 . . . . . . . . . . . . . 14 ((𝑛𝑗) ∈ ℤ → (((𝑛𝑗) / 2) ∈ ℤ ∨ (((𝑛𝑗) + 1) / 2) ∈ ℤ))
12448, 123syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((𝑛𝑗) / 2) ∈ ℤ ∨ (((𝑛𝑗) + 1) / 2) ∈ ℤ))
12570, 122, 124mpjaodan 826 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
1261peano2uzs 11689 . . . . . . . . . . . . . . 15 (𝑗𝑍 → (𝑗 + 1) ∈ 𝑍)
127126adantr 481 . . . . . . . . . . . . . 14 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → (𝑗 + 1) ∈ 𝑍)
128 ffvelrn 6315 . . . . . . . . . . . . . 14 ((𝐺:𝑍⟶ℝ ∧ (𝑗 + 1) ∈ 𝑍) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
12910, 127, 128syl2an 494 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
1301, 5, 10, 65, 4iseraltlem1 14349 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑗 + 1)))
131127, 130sylan2 491 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 0 ≤ (𝐺‘(𝑗 + 1)))
132129, 131absidd 14098 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) = (𝐺‘(𝑗 + 1)))
133125, 132breqtrrd 4643 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))))
134133adantlr 750 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))))
135 neg1rr 11072 . . . . . . . . . . . . . . . . . . . . 21 -1 ∈ ℝ
136135a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → -1 ∈ ℝ)
137 neg1ne0 11073 . . . . . . . . . . . . . . . . . . . . 21 -1 ≠ 0
138137a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → -1 ≠ 0)
139 eluzelz 11644 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
140139, 1eleq2s 2716 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑍𝑘 ∈ ℤ)
141140adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
142136, 138, 141reexpclzd 12977 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
14310ffvelrnda 6317 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
144142, 143remulcld 10017 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
14566, 144eqeltrd 2698 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
1461, 5, 145serfre 12773 . . . . . . . . . . . . . . . 16 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
1471uztrn2 11652 . . . . . . . . . . . . . . . 16 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → 𝑛𝑍)
148 ffvelrn 6315 . . . . . . . . . . . . . . . 16 ((seq𝑀( + , 𝐹):𝑍⟶ℝ ∧ 𝑛𝑍) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
149146, 147, 148syl2an 494 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
150 ffvelrn 6315 . . . . . . . . . . . . . . . 16 ((seq𝑀( + , 𝐹):𝑍⟶ℝ ∧ 𝑗𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
151146, 45, 150syl2an 494 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
152149, 151resubcld 10405 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) ∈ ℝ)
153152recnd 10015 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) ∈ ℂ)
154153abscld 14112 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ)
155154adantlr 750 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ)
156132, 129eqeltrd 2698 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ)
157156adantlr 750 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ)
158 rpre 11786 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
159158ad2antlr 762 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → 𝑥 ∈ ℝ)
160 lelttr 10075 . . . . . . . . . . 11 (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ ∧ (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))) ∧ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
161155, 157, 159, 160syl3anc 1323 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))) ∧ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
162134, 161mpand 710 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
163146adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
164163, 147, 148syl2an 494 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
165162, 164jctild 565 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
166165anassrs 679 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑛 ∈ (ℤ𝑗)) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
167166ralrimdva 2963 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ∀𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
16825, 167syld 47 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → ∀𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
169168reximdva 3011 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (∃𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → ∃𝑗𝑍𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
170169ralimdva 2956 . . 3 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(𝐺𝑛)) < 𝑥 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
17114, 170mpd 15 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
1721, 3, 171caurcvg2 14345 1 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3186   class class class wbr 4615  dom cdm 5076  wf 5845  cfv 5849  (class class class)co 6607  cc 9881  cr 9882  0cc0 9883  1c1 9884   + caddc 9886   · cmul 9888   < clt 10021  cle 10022  cmin 10213  -cneg 10214   / cdiv 10631  cn 10967  2c2 11017  0cn0 11239  cz 11324  cuz 11634  +crp 11779  seqcseq 12744  cexp 12803  abscabs 13911  cli 14152
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 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-inf2 8485  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960  ax-pre-sup 9961
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 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-er 7690  df-pm 7808  df-en 7903  df-dom 7904  df-sdom 7905  df-sup 8295  df-inf 8296  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-div 10632  df-nn 10968  df-2 11026  df-3 11027  df-n0 11240  df-z 11325  df-uz 11635  df-rp 11780  df-ico 12126  df-fz 12272  df-fl 12536  df-seq 12745  df-exp 12804  df-cj 13776  df-re 13777  df-im 13778  df-sqrt 13912  df-abs 13913  df-limsup 14139  df-clim 14156  df-rlim 14157
This theorem is referenced by:  leibpi  24576
  Copyright terms: Public domain W3C validator