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

Theorem climcnds 14627
 Description: The Cauchy condensation test. If 𝑎(𝑘) is a decreasing sequence of nonnegative terms, then Σ𝑘 ∈ ℕ𝑎(𝑘) converges iff Σ𝑛 ∈ ℕ02↑𝑛 · 𝑎(2↑𝑛) converges. (Contributed by Mario Carneiro, 18-Jul-2014.)
Hypotheses
Ref Expression
climcnds.1 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
climcnds.2 ((𝜑𝑘 ∈ ℕ) → 0 ≤ (𝐹𝑘))
climcnds.3 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
climcnds.4 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
Assertion
Ref Expression
climcnds (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq0( + , 𝐺) ∈ dom ⇝ ))
Distinct variable groups:   𝑘,𝑛,𝐹   𝑘,𝐺,𝑛   𝜑,𝑘,𝑛

Proof of Theorem climcnds
Dummy variables 𝑗 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11761 . . . . 5 ℕ = (ℤ‘1)
2 1zzd 11446 . . . . 5 ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → 1 ∈ ℤ)
3 1zzd 11446 . . . . . . 7 (𝜑 → 1 ∈ ℤ)
4 nnnn0 11337 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
5 climcnds.4 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
6 2nn 11223 . . . . . . . . . . . 12 2 ∈ ℕ
7 simpr 476 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
8 nnexpcl 12913 . . . . . . . . . . . 12 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
96, 7, 8sylancr 696 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
109nnred 11073 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℝ)
11 climcnds.1 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
1211ralrimiva 2995 . . . . . . . . . . . 12 (𝜑 → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
1312adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
14 fveq2 6229 . . . . . . . . . . . . 13 (𝑘 = (2↑𝑛) → (𝐹𝑘) = (𝐹‘(2↑𝑛)))
1514eleq1d 2715 . . . . . . . . . . . 12 (𝑘 = (2↑𝑛) → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘(2↑𝑛)) ∈ ℝ))
1615rspcv 3336 . . . . . . . . . . 11 ((2↑𝑛) ∈ ℕ → (∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ → (𝐹‘(2↑𝑛)) ∈ ℝ))
179, 13, 16sylc 65 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (𝐹‘(2↑𝑛)) ∈ ℝ)
1810, 17remulcld 10108 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) ∈ ℝ)
195, 18eqeltrd 2730 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) ∈ ℝ)
204, 19sylan2 490 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ ℝ)
211, 3, 20serfre 12870 . . . . . 6 (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ)
2221adantr 480 . . . . 5 ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq1( + , 𝐺):ℕ⟶ℝ)
23 simpr 476 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
2423, 1syl6eleq 2740 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
25 nnz 11437 . . . . . . . . 9 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
2625adantl 481 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
27 uzid 11740 . . . . . . . 8 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
28 peano2uz 11779 . . . . . . . 8 (𝑗 ∈ (ℤ𝑗) → (𝑗 + 1) ∈ (ℤ𝑗))
2926, 27, 283syl 18 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝑗 + 1) ∈ (ℤ𝑗))
30 simpl 472 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝜑)
31 elfznn 12408 . . . . . . . 8 (𝑛 ∈ (1...(𝑗 + 1)) → 𝑛 ∈ ℕ)
3230, 31, 20syl2an 493 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...(𝑗 + 1))) → (𝐺𝑛) ∈ ℝ)
33 simpll 805 . . . . . . . 8 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝜑)
34 elfz1eq 12390 . . . . . . . . . 10 (𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1)) → 𝑛 = (𝑗 + 1))
3534adantl 481 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝑛 = (𝑗 + 1))
36 nnnn0 11337 . . . . . . . . . . 11 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ0)
37 peano2nn0 11371 . . . . . . . . . . 11 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ0)
3836, 37syl 17 . . . . . . . . . 10 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ0)
3938ad2antlr 763 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → (𝑗 + 1) ∈ ℕ0)
4035, 39eqeltrd 2730 . . . . . . . 8 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝑛 ∈ ℕ0)
419nnnn0d 11389 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ0)
4241nn0ge0d 11392 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (2↑𝑛))
43 climcnds.2 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 0 ≤ (𝐹𝑘))
4443ralrimiva 2995 . . . . . . . . . . . 12 (𝜑 → ∀𝑘 ∈ ℕ 0 ≤ (𝐹𝑘))
4544adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → ∀𝑘 ∈ ℕ 0 ≤ (𝐹𝑘))
4614breq2d 4697 . . . . . . . . . . . 12 (𝑘 = (2↑𝑛) → (0 ≤ (𝐹𝑘) ↔ 0 ≤ (𝐹‘(2↑𝑛))))
4746rspcv 3336 . . . . . . . . . . 11 ((2↑𝑛) ∈ ℕ → (∀𝑘 ∈ ℕ 0 ≤ (𝐹𝑘) → 0 ≤ (𝐹‘(2↑𝑛))))
489, 45, 47sylc 65 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (𝐹‘(2↑𝑛)))
4910, 17, 42, 48mulge0d 10642 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ ((2↑𝑛) · (𝐹‘(2↑𝑛))))
5049, 5breqtrrd 4713 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (𝐺𝑛))
5133, 40, 50syl2anc 694 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 0 ≤ (𝐺𝑛))
5224, 29, 32, 51sermono 12873 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ≤ (seq1( + , 𝐺)‘(𝑗 + 1)))
5352adantlr 751 . . . . 5 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ≤ (seq1( + , 𝐺)‘(𝑗 + 1)))
54 2re 11128 . . . . . . 7 2 ∈ ℝ
55 eqidd 2652 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (𝐹𝑘))
5611adantlr 751 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
57 simpr 476 . . . . . . . 8 ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq1( + , 𝐹) ∈ dom ⇝ )
581, 2, 55, 56, 57isumrecl 14540 . . . . . . 7 ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → Σ𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
59 remulcl 10059 . . . . . . 7 ((2 ∈ ℝ ∧ Σ𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ) → (2 · Σ𝑘 ∈ ℕ (𝐹𝑘)) ∈ ℝ)
6054, 58, 59sylancr 696 . . . . . 6 ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → (2 · Σ𝑘 ∈ ℕ (𝐹𝑘)) ∈ ℝ)
6122ffvelrnda 6399 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ∈ ℝ)
621, 3, 11serfre 12870 . . . . . . . . . . 11 (𝜑 → seq1( + , 𝐹):ℕ⟶ℝ)
6362ad2antrr 762 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → seq1( + , 𝐹):ℕ⟶ℝ)
6436adantl 481 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0)
65 nnexpcl 12913 . . . . . . . . . . 11 ((2 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2↑𝑗) ∈ ℕ)
666, 64, 65sylancr 696 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈ ℕ)
6763, 66ffvelrnd 6400 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ)
68 remulcl 10059 . . . . . . . . 9 ((2 ∈ ℝ ∧ (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ) → (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ∈ ℝ)
6954, 67, 68sylancr 696 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ∈ ℝ)
7060adantr 480 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2 · Σ𝑘 ∈ ℕ (𝐹𝑘)) ∈ ℝ)
71 climcnds.3 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
7211, 43, 71, 5climcndslem2 14626 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))))
7372adantlr 751 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))))
74 eqidd 2652 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹𝑘) = (𝐹𝑘))
7566, 1syl6eleq 2740 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈ (ℤ‘1))
76 simpll 805 . . . . . . . . . . . 12 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝜑)
77 elfznn 12408 . . . . . . . . . . . 12 (𝑘 ∈ (1...(2↑𝑗)) → 𝑘 ∈ ℕ)
7811recnd 10106 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
7976, 77, 78syl2an 493 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹𝑘) ∈ ℂ)
8074, 75, 79fsumser 14505 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑𝑗))(𝐹𝑘) = (seq1( + , 𝐹)‘(2↑𝑗)))
81 1zzd 11446 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 1 ∈ ℤ)
82 fzfid 12812 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (1...(2↑𝑗)) ∈ Fin)
8377ssriv 3640 . . . . . . . . . . . 12 (1...(2↑𝑗)) ⊆ ℕ
8483a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (1...(2↑𝑗)) ⊆ ℕ)
85 eqidd 2652 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (𝐹𝑘))
8656adantlr 751 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
8776, 43sylan 487 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐹𝑘))
88 simplr 807 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → seq1( + , 𝐹) ∈ dom ⇝ )
891, 81, 82, 84, 85, 86, 87, 88isumless 14621 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑𝑗))(𝐹𝑘) ≤ Σ𝑘 ∈ ℕ (𝐹𝑘))
9080, 89eqbrtrrd 4709 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ≤ Σ𝑘 ∈ ℕ (𝐹𝑘))
9158adantr 480 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
9254a1i 11 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 2 ∈ ℝ)
93 2pos 11150 . . . . . . . . . . 11 0 < 2
9493a1i 11 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 0 < 2)
95 lemul2 10914 . . . . . . . . . 10 (((seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ ∧ Σ𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((seq1( + , 𝐹)‘(2↑𝑗)) ≤ Σ𝑘 ∈ ℕ (𝐹𝑘) ↔ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹𝑘))))
9667, 91, 92, 94, 95syl112anc 1370 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → ((seq1( + , 𝐹)‘(2↑𝑗)) ≤ Σ𝑘 ∈ ℕ (𝐹𝑘) ↔ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹𝑘))))
9790, 96mpbid 222 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹𝑘)))
9861, 69, 70, 73, 97letrd 10232 . . . . . . 7 (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹𝑘)))
9998ralrimiva 2995 . . . . . 6 ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → ∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹𝑘)))
100 breq2 4689 . . . . . . . 8 (𝑥 = (2 · Σ𝑘 ∈ ℕ (𝐹𝑘)) → ((seq1( + , 𝐺)‘𝑗) ≤ 𝑥 ↔ (seq1( + , 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹𝑘))))
101100ralbidv 3015 . . . . . . 7 (𝑥 = (2 · Σ𝑘 ∈ ℕ (𝐹𝑘)) → (∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹𝑘))))
102101rspcev 3340 . . . . . 6 (((2 · Σ𝑘 ∈ ℕ (𝐹𝑘)) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹𝑘))) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ 𝑥)
10360, 99, 102syl2anc 694 . . . . 5 ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ 𝑥)
1041, 2, 22, 53, 103climsup 14444 . . . 4 ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq1( + , 𝐺) ⇝ sup(ran seq1( + , 𝐺), ℝ, < ))
105 climrel 14267 . . . . 5 Rel ⇝
106105releldmi 5394 . . . 4 (seq1( + , 𝐺) ⇝ sup(ran seq1( + , 𝐺), ℝ, < ) → seq1( + , 𝐺) ∈ dom ⇝ )
107104, 106syl 17 . . 3 ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq1( + , 𝐺) ∈ dom ⇝ )
108 nn0uz 11760 . . . . 5 0 = (ℤ‘0)
109 1nn0 11346 . . . . . 6 1 ∈ ℕ0
110109a1i 11 . . . . 5 (𝜑 → 1 ∈ ℕ0)
11119recnd 10106 . . . . 5 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) ∈ ℂ)
112108, 110, 111iserex 14431 . . . 4 (𝜑 → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq1( + , 𝐺) ∈ dom ⇝ ))
113112biimpar 501 . . 3 ((𝜑 ∧ seq1( + , 𝐺) ∈ dom ⇝ ) → seq0( + , 𝐺) ∈ dom ⇝ )
114107, 113syldan 486 . 2 ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq0( + , 𝐺) ∈ dom ⇝ )
115 1zzd 11446 . . . 4 ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → 1 ∈ ℤ)
11662adantr 480 . . . 4 ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq1( + , 𝐹):ℕ⟶ℝ)
117 elfznn 12408 . . . . . . 7 (𝑘 ∈ (1...(𝑗 + 1)) → 𝑘 ∈ ℕ)
11830, 117, 11syl2an 493 . . . . . 6 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(𝑗 + 1))) → (𝐹𝑘) ∈ ℝ)
119 simpll 805 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝜑)
120 peano2nn 11070 . . . . . . . . 9 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
121120adantl 481 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
122 elfz1eq 12390 . . . . . . . 8 (𝑘 ∈ ((𝑗 + 1)...(𝑗 + 1)) → 𝑘 = (𝑗 + 1))
123 eleq1 2718 . . . . . . . . 9 (𝑘 = (𝑗 + 1) → (𝑘 ∈ ℕ ↔ (𝑗 + 1) ∈ ℕ))
124123biimparc 503 . . . . . . . 8 (((𝑗 + 1) ∈ ℕ ∧ 𝑘 = (𝑗 + 1)) → 𝑘 ∈ ℕ)
125121, 122, 124syl2an 493 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝑘 ∈ ℕ)
126119, 125, 43syl2anc 694 . . . . . 6 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 0 ≤ (𝐹𝑘))
12724, 29, 118, 126sermono 12873 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘𝑗) ≤ (seq1( + , 𝐹)‘(𝑗 + 1)))
128127adantlr 751 . . . 4 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘𝑗) ≤ (seq1( + , 𝐹)‘(𝑗 + 1)))
129 0zd 11427 . . . . . 6 ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → 0 ∈ ℤ)
130 eqidd 2652 . . . . . 6 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ0) → (𝐺𝑛) = (𝐺𝑛))
13119adantlr 751 . . . . . 6 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ0) → (𝐺𝑛) ∈ ℝ)
132 simpr 476 . . . . . 6 ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq0( + , 𝐺) ∈ dom ⇝ )
133108, 129, 130, 131, 132isumrecl 14540 . . . . 5 ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → Σ𝑛 ∈ ℕ0 (𝐺𝑛) ∈ ℝ)
134116ffvelrnda 6399 . . . . . . 7 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘𝑗) ∈ ℝ)
135 0zd 11427 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
136108, 135, 19serfre 12870 . . . . . . . . 9 (𝜑 → seq0( + , 𝐺):ℕ0⟶ℝ)
137136adantr 480 . . . . . . . 8 ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq0( + , 𝐺):ℕ0⟶ℝ)
138 ffvelrn 6397 . . . . . . . 8 ((seq0( + , 𝐺):ℕ0⟶ℝ ∧ 𝑗 ∈ ℕ0) → (seq0( + , 𝐺)‘𝑗) ∈ ℝ)
139137, 36, 138syl2an 493 . . . . . . 7 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq0( + , 𝐺)‘𝑗) ∈ ℝ)
140133adantr 480 . . . . . . 7 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → Σ𝑛 ∈ ℕ0 (𝐺𝑛) ∈ ℝ)
141116adantr 480 . . . . . . . . 9 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → seq1( + , 𝐹):ℕ⟶ℝ)
142 simpr 476 . . . . . . . . . 10 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
14325adantl 481 . . . . . . . . . . 11 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
14438adantl 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ0)
145144nn0red 11390 . . . . . . . . . . . . 13 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℝ)
146 nnexpcl 12913 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ ∧ (𝑗 + 1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ)
1476, 144, 146sylancr 696 . . . . . . . . . . . . . 14 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈ ℕ)
148147nnred 11073 . . . . . . . . . . . . 13 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈ ℝ)
149 2z 11447 . . . . . . . . . . . . . . 15 2 ∈ ℤ
150 uzid 11740 . . . . . . . . . . . . . . 15 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
151149, 150ax-mp 5 . . . . . . . . . . . . . 14 2 ∈ (ℤ‘2)
152 bernneq3 13032 . . . . . . . . . . . . . 14 ((2 ∈ (ℤ‘2) ∧ (𝑗 + 1) ∈ ℕ0) → (𝑗 + 1) < (2↑(𝑗 + 1)))
153151, 144, 152sylancr 696 . . . . . . . . . . . . 13 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) < (2↑(𝑗 + 1)))
154145, 148, 153ltled 10223 . . . . . . . . . . . 12 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ≤ (2↑(𝑗 + 1)))
155143peano2zd 11523 . . . . . . . . . . . . 13 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℤ)
156147nnzd 11519 . . . . . . . . . . . . 13 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈ ℤ)
157 eluz 11739 . . . . . . . . . . . . 13 (((𝑗 + 1) ∈ ℤ ∧ (2↑(𝑗 + 1)) ∈ ℤ) → ((2↑(𝑗 + 1)) ∈ (ℤ‘(𝑗 + 1)) ↔ (𝑗 + 1) ≤ (2↑(𝑗 + 1))))
158155, 156, 157syl2anc 694 . . . . . . . . . . . 12 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → ((2↑(𝑗 + 1)) ∈ (ℤ‘(𝑗 + 1)) ↔ (𝑗 + 1) ≤ (2↑(𝑗 + 1))))
159154, 158mpbird 247 . . . . . . . . . . 11 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈ (ℤ‘(𝑗 + 1)))
160 eluzp1m1 11749 . . . . . . . . . . 11 ((𝑗 ∈ ℤ ∧ (2↑(𝑗 + 1)) ∈ (ℤ‘(𝑗 + 1))) → ((2↑(𝑗 + 1)) − 1) ∈ (ℤ𝑗))
161143, 159, 160syl2anc 694 . . . . . . . . . 10 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → ((2↑(𝑗 + 1)) − 1) ∈ (ℤ𝑗))
162 eluznn 11796 . . . . . . . . . 10 ((𝑗 ∈ ℕ ∧ ((2↑(𝑗 + 1)) − 1) ∈ (ℤ𝑗)) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ)
163142, 161, 162syl2anc 694 . . . . . . . . 9 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ)
164141, 163ffvelrnd 6400 . . . . . . . 8 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ∈ ℝ)
16524adantlr 751 . . . . . . . . 9 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
166 simpll 805 . . . . . . . . . 10 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝜑)
167 elfznn 12408 . . . . . . . . . 10 (𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈ ℕ)
168166, 167, 11syl2an 493 . . . . . . . . 9 ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹𝑘) ∈ ℝ)
169166adantr 480 . . . . . . . . . 10 ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...((2↑(𝑗 + 1)) − 1))) → 𝜑)
170120adantl 481 . . . . . . . . . . 11 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
171 elfzuz 12376 . . . . . . . . . . 11 (𝑘 ∈ ((𝑗 + 1)...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈ (ℤ‘(𝑗 + 1)))
172 eluznn 11796 . . . . . . . . . . 11 (((𝑗 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝑗 + 1))) → 𝑘 ∈ ℕ)
173170, 171, 172syl2an 493 . . . . . . . . . 10 ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...((2↑(𝑗 + 1)) − 1))) → 𝑘 ∈ ℕ)
174169, 173, 43syl2anc 694 . . . . . . . . 9 ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...((2↑(𝑗 + 1)) − 1))) → 0 ≤ (𝐹𝑘))
175165, 161, 168, 174sermono 12873 . . . . . . . 8 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘𝑗) ≤ (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)))
17636adantl 481 . . . . . . . . 9 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0)
17711, 43, 71, 5climcndslem1 14625 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗))
178166, 176, 177syl2anc 694 . . . . . . . 8 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗))
179134, 164, 139, 175, 178letrd 10232 . . . . . . 7 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘𝑗) ≤ (seq0( + , 𝐺)‘𝑗))
180 eqidd 2652 . . . . . . . . 9 ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑗)) → (𝐺𝑛) = (𝐺𝑛))
181176, 108syl6eleq 2740 . . . . . . . . 9 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘0))
182 elfznn0 12471 . . . . . . . . . 10 (𝑛 ∈ (0...𝑗) → 𝑛 ∈ ℕ0)
183166, 182, 111syl2an 493 . . . . . . . . 9 ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑗)) → (𝐺𝑛) ∈ ℂ)
184180, 181, 183fsumser 14505 . . . . . . . 8 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → Σ𝑛 ∈ (0...𝑗)(𝐺𝑛) = (seq0( + , 𝐺)‘𝑗))
185 0zd 11427 . . . . . . . . 9 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 0 ∈ ℤ)
186 fzfid 12812 . . . . . . . . 9 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (0...𝑗) ∈ Fin)
187182ssriv 3640 . . . . . . . . . 10 (0...𝑗) ⊆ ℕ0
188187a1i 11 . . . . . . . . 9 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (0...𝑗) ⊆ ℕ0)
189 eqidd 2652 . . . . . . . . 9 ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ0) → (𝐺𝑛) = (𝐺𝑛))
190166, 19sylan 487 . . . . . . . . 9 ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ0) → (𝐺𝑛) ∈ ℝ)
191166, 50sylan 487 . . . . . . . . 9 ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ0) → 0 ≤ (𝐺𝑛))
192 simplr 807 . . . . . . . . 9 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → seq0( + , 𝐺) ∈ dom ⇝ )
193108, 185, 186, 188, 189, 190, 191, 192isumless 14621 . . . . . . . 8 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → Σ𝑛 ∈ (0...𝑗)(𝐺𝑛) ≤ Σ𝑛 ∈ ℕ0 (𝐺𝑛))
194184, 193eqbrtrrd 4709 . . . . . . 7 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq0( + , 𝐺)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺𝑛))
195134, 139, 140, 179, 194letrd 10232 . . . . . 6 (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺𝑛))
196195ralrimiva 2995 . . . . 5 ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺𝑛))
197 breq2 4689 . . . . . . 7 (𝑥 = Σ𝑛 ∈ ℕ0 (𝐺𝑛) → ((seq1( + , 𝐹)‘𝑗) ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺𝑛)))
198197ralbidv 3015 . . . . . 6 (𝑥 = Σ𝑛 ∈ ℕ0 (𝐺𝑛) → (∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺𝑛)))
199198rspcev 3340 . . . . 5 ((Σ𝑛 ∈ ℕ0 (𝐺𝑛) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺𝑛)) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ 𝑥)
200133, 196, 199syl2anc 694 . . . 4 ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ 𝑥)
2011, 115, 116, 128, 200climsup 14444 . . 3 ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq1( + , 𝐹) ⇝ sup(ran seq1( + , 𝐹), ℝ, < ))
202105releldmi 5394 . . 3 (seq1( + , 𝐹) ⇝ sup(ran seq1( + , 𝐹), ℝ, < ) → seq1( + , 𝐹) ∈ dom ⇝ )
203201, 202syl 17 . 2 ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq1( + , 𝐹) ∈ dom ⇝ )
204114, 203impbida 895 1 (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq0( + , 𝐺) ∈ dom ⇝ ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942   ⊆ wss 3607   class class class wbr 4685  dom cdm 5143  ran crn 5144  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  supcsup 8387  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112   ≤ cle 10113   − cmin 10304  ℕcn 11058  2c2 11108  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ...cfz 12364  seqcseq 12841  ↑cexp 12900   ⇝ cli 14259  Σcsu 14460 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-ico 12219  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461 This theorem is referenced by:  harmonic  14635  zetacvg  24786
 Copyright terms: Public domain W3C validator