Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wallispilem3 Structured version   Visualization version   GIF version

Theorem wallispilem3 42218
Description: I maps to real values. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypothesis
Ref Expression
wallispilem3.1 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
Assertion
Ref Expression
wallispilem3 (𝑁 ∈ ℕ0 → (𝐼𝑁) ∈ ℝ+)
Distinct variable group:   𝑥,𝑛
Allowed substitution hints:   𝐼(𝑥,𝑛)   𝑁(𝑥,𝑛)

Proof of Theorem wallispilem3
Dummy variables 𝑘 𝑚 𝑦 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 5067 . . . . . 6 (𝑤 = 0 → (𝑚𝑤𝑚 ≤ 0))
21imbi1d 343 . . . . 5 (𝑤 = 0 → ((𝑚𝑤 → (𝐼𝑚) ∈ ℝ+) ↔ (𝑚 ≤ 0 → (𝐼𝑚) ∈ ℝ+)))
32ralbidv 3202 . . . 4 (𝑤 = 0 → (∀𝑚 ∈ ℕ0 (𝑚𝑤 → (𝐼𝑚) ∈ ℝ+) ↔ ∀𝑚 ∈ ℕ0 (𝑚 ≤ 0 → (𝐼𝑚) ∈ ℝ+)))
4 breq2 5067 . . . . . 6 (𝑤 = 𝑦 → (𝑚𝑤𝑚𝑦))
54imbi1d 343 . . . . 5 (𝑤 = 𝑦 → ((𝑚𝑤 → (𝐼𝑚) ∈ ℝ+) ↔ (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)))
65ralbidv 3202 . . . 4 (𝑤 = 𝑦 → (∀𝑚 ∈ ℕ0 (𝑚𝑤 → (𝐼𝑚) ∈ ℝ+) ↔ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)))
7 breq2 5067 . . . . . 6 (𝑤 = (𝑦 + 1) → (𝑚𝑤𝑚 ≤ (𝑦 + 1)))
87imbi1d 343 . . . . 5 (𝑤 = (𝑦 + 1) → ((𝑚𝑤 → (𝐼𝑚) ∈ ℝ+) ↔ (𝑚 ≤ (𝑦 + 1) → (𝐼𝑚) ∈ ℝ+)))
98ralbidv 3202 . . . 4 (𝑤 = (𝑦 + 1) → (∀𝑚 ∈ ℕ0 (𝑚𝑤 → (𝐼𝑚) ∈ ℝ+) ↔ ∀𝑚 ∈ ℕ0 (𝑚 ≤ (𝑦 + 1) → (𝐼𝑚) ∈ ℝ+)))
10 breq2 5067 . . . . . 6 (𝑤 = 𝑁 → (𝑚𝑤𝑚𝑁))
1110imbi1d 343 . . . . 5 (𝑤 = 𝑁 → ((𝑚𝑤 → (𝐼𝑚) ∈ ℝ+) ↔ (𝑚𝑁 → (𝐼𝑚) ∈ ℝ+)))
1211ralbidv 3202 . . . 4 (𝑤 = 𝑁 → (∀𝑚 ∈ ℕ0 (𝑚𝑤 → (𝐼𝑚) ∈ ℝ+) ↔ ∀𝑚 ∈ ℕ0 (𝑚𝑁 → (𝐼𝑚) ∈ ℝ+)))
13 simpr 485 . . . . . . . . 9 ((𝑚 ∈ ℕ0𝑚 ≤ 0) → 𝑚 ≤ 0)
14 nn0ge0 11911 . . . . . . . . . 10 (𝑚 ∈ ℕ0 → 0 ≤ 𝑚)
1514adantr 481 . . . . . . . . 9 ((𝑚 ∈ ℕ0𝑚 ≤ 0) → 0 ≤ 𝑚)
16 nn0re 11895 . . . . . . . . . . 11 (𝑚 ∈ ℕ0𝑚 ∈ ℝ)
1716adantr 481 . . . . . . . . . 10 ((𝑚 ∈ ℕ0𝑚 ≤ 0) → 𝑚 ∈ ℝ)
18 0red 10633 . . . . . . . . . 10 ((𝑚 ∈ ℕ0𝑚 ≤ 0) → 0 ∈ ℝ)
1917, 18letri3d 10771 . . . . . . . . 9 ((𝑚 ∈ ℕ0𝑚 ≤ 0) → (𝑚 = 0 ↔ (𝑚 ≤ 0 ∧ 0 ≤ 𝑚)))
2013, 15, 19mpbir2and 709 . . . . . . . 8 ((𝑚 ∈ ℕ0𝑚 ≤ 0) → 𝑚 = 0)
2120fveq2d 6671 . . . . . . 7 ((𝑚 ∈ ℕ0𝑚 ≤ 0) → (𝐼𝑚) = (𝐼‘0))
22 wallispilem3.1 . . . . . . . . . 10 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
2322wallispilem2 42217 . . . . . . . . 9 ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (𝑚 ∈ (ℤ‘2) → (𝐼𝑚) = (((𝑚 − 1) / 𝑚) · (𝐼‘(𝑚 − 2)))))
2423simp1i 1133 . . . . . . . 8 (𝐼‘0) = π
25 pirp 24962 . . . . . . . 8 π ∈ ℝ+
2624, 25eqeltri 2914 . . . . . . 7 (𝐼‘0) ∈ ℝ+
2721, 26syl6eqel 2926 . . . . . 6 ((𝑚 ∈ ℕ0𝑚 ≤ 0) → (𝐼𝑚) ∈ ℝ+)
2827ex 413 . . . . 5 (𝑚 ∈ ℕ0 → (𝑚 ≤ 0 → (𝐼𝑚) ∈ ℝ+))
2928rgen 3153 . . . 4 𝑚 ∈ ℕ0 (𝑚 ≤ 0 → (𝐼𝑚) ∈ ℝ+)
30 nfv 1908 . . . . . . 7 𝑚 𝑦 ∈ ℕ0
31 nfra1 3224 . . . . . . 7 𝑚𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)
3230, 31nfan 1893 . . . . . 6 𝑚(𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+))
33 simpllr 772 . . . . . . . . 9 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ (𝑦 + 1)) → ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+))
34 simplr 765 . . . . . . . . 9 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ (𝑦 + 1)) → 𝑚 ∈ ℕ0)
35 rsp 3210 . . . . . . . . 9 (∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+) → (𝑚 ∈ ℕ0 → (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)))
3633, 34, 35sylc 65 . . . . . . . 8 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ (𝑦 + 1)) → (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+))
37 fveq2 6667 . . . . . . . . . . . . 13 (𝑚 = 1 → (𝐼𝑚) = (𝐼‘1))
3823simp2i 1134 . . . . . . . . . . . . . 14 (𝐼‘1) = 2
39 2rp 12384 . . . . . . . . . . . . . 14 2 ∈ ℝ+
4038, 39eqeltri 2914 . . . . . . . . . . . . 13 (𝐼‘1) ∈ ℝ+
4137, 40syl6eqel 2926 . . . . . . . . . . . 12 (𝑚 = 1 → (𝐼𝑚) ∈ ℝ+)
4241a1i 11 . . . . . . . . . . 11 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = (𝑦 + 1)) → (𝑚 = 1 → (𝐼𝑚) ∈ ℝ+))
4323simp3i 1135 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ℤ‘2) → (𝐼𝑚) = (((𝑚 − 1) / 𝑚) · (𝐼‘(𝑚 − 2))))
4443adantl 482 . . . . . . . . . . . . . 14 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → (𝐼𝑚) = (((𝑚 − 1) / 𝑚) · (𝐼‘(𝑚 − 2))))
45 eluz2nn 12273 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ (ℤ‘2) → 𝑚 ∈ ℕ)
46 nnre 11634 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
47 1red 10631 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ → 1 ∈ ℝ)
4846, 47resubcld 11057 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ → (𝑚 − 1) ∈ ℝ)
4945, 48syl 17 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (ℤ‘2) → (𝑚 − 1) ∈ ℝ)
50 1m1e0 11698 . . . . . . . . . . . . . . . . . . 19 (1 − 1) = 0
51 1red 10631 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ (ℤ‘2) → 1 ∈ ℝ)
52 eluzelre 12243 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ (ℤ‘2) → 𝑚 ∈ ℝ)
53 eluz2b2 12310 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ (ℤ‘2) ↔ (𝑚 ∈ ℕ ∧ 1 < 𝑚))
5453simprbi 497 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ (ℤ‘2) → 1 < 𝑚)
5551, 52, 51, 54ltsub1dd 11241 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ (ℤ‘2) → (1 − 1) < (𝑚 − 1))
5650, 55eqbrtrrid 5099 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (ℤ‘2) → 0 < (𝑚 − 1))
5749, 56elrpd 12418 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (ℤ‘2) → (𝑚 − 1) ∈ ℝ+)
5845nnrpd 12419 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (ℤ‘2) → 𝑚 ∈ ℝ+)
5957, 58rpdivcld 12438 . . . . . . . . . . . . . . . 16 (𝑚 ∈ (ℤ‘2) → ((𝑚 − 1) / 𝑚) ∈ ℝ+)
6059adantl 482 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → ((𝑚 − 1) / 𝑚) ∈ ℝ+)
61 breq1 5066 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑘 → (𝑚𝑦𝑘𝑦))
62 fveq2 6667 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑘 → (𝐼𝑚) = (𝐼𝑘))
6362eleq1d 2902 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑘 → ((𝐼𝑚) ∈ ℝ+ ↔ (𝐼𝑘) ∈ ℝ+))
6461, 63imbi12d 346 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑘 → ((𝑚𝑦 → (𝐼𝑚) ∈ ℝ+) ↔ (𝑘𝑦 → (𝐼𝑘) ∈ ℝ+)))
6564cbvralv 3458 . . . . . . . . . . . . . . . . . . 19 (∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+) ↔ ∀𝑘 ∈ ℕ0 (𝑘𝑦 → (𝐼𝑘) ∈ ℝ+))
6665biimpi 217 . . . . . . . . . . . . . . . . . 18 (∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+) → ∀𝑘 ∈ ℕ0 (𝑘𝑦 → (𝐼𝑘) ∈ ℝ+))
6766ad3antlr 727 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → ∀𝑘 ∈ ℕ0 (𝑘𝑦 → (𝐼𝑘) ∈ ℝ+))
68 uznn0sub 12266 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (ℤ‘2) → (𝑚 − 2) ∈ ℕ0)
6968adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → (𝑚 − 2) ∈ ℕ0)
7067, 69jca 512 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → (∀𝑘 ∈ ℕ0 (𝑘𝑦 → (𝐼𝑘) ∈ ℝ+) ∧ (𝑚 − 2) ∈ ℕ0))
71 simplll 771 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → 𝑦 ∈ ℕ0)
72 simplr 765 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → 𝑚 = (𝑦 + 1))
73 simpr 485 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → 𝑚 ∈ (ℤ‘2))
74 simp2 1131 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℕ0𝑚 = (𝑦 + 1) ∧ 𝑚 ∈ (ℤ‘2)) → 𝑚 = (𝑦 + 1))
7574oveq1d 7163 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ0𝑚 = (𝑦 + 1) ∧ 𝑚 ∈ (ℤ‘2)) → (𝑚 − 2) = ((𝑦 + 1) − 2))
76 nn0re 11895 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℕ0𝑦 ∈ ℝ)
77763ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℕ0𝑚 = (𝑦 + 1) ∧ 𝑚 ∈ (ℤ‘2)) → 𝑦 ∈ ℝ)
7877recnd 10658 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℕ0𝑚 = (𝑦 + 1) ∧ 𝑚 ∈ (ℤ‘2)) → 𝑦 ∈ ℂ)
79 df-2 11689 . . . . . . . . . . . . . . . . . . . . . . 23 2 = (1 + 1)
8079a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℂ → 2 = (1 + 1))
8180oveq2d 7164 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → ((𝑦 + 1) − 2) = ((𝑦 + 1) − (1 + 1)))
82 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
83 1cnd 10625 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℂ → 1 ∈ ℂ)
8482, 83, 83pnpcan2d 11024 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → ((𝑦 + 1) − (1 + 1)) = (𝑦 − 1))
8581, 84eqtrd 2861 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℂ → ((𝑦 + 1) − 2) = (𝑦 − 1))
8678, 85syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ0𝑚 = (𝑦 + 1) ∧ 𝑚 ∈ (ℤ‘2)) → ((𝑦 + 1) − 2) = (𝑦 − 1))
8775, 86eqtrd 2861 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℕ0𝑚 = (𝑦 + 1) ∧ 𝑚 ∈ (ℤ‘2)) → (𝑚 − 2) = (𝑦 − 1))
8877lem1d 11562 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℕ0𝑚 = (𝑦 + 1) ∧ 𝑚 ∈ (ℤ‘2)) → (𝑦 − 1) ≤ 𝑦)
8987, 88eqbrtrd 5085 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ0𝑚 = (𝑦 + 1) ∧ 𝑚 ∈ (ℤ‘2)) → (𝑚 − 2) ≤ 𝑦)
9071, 72, 73, 89syl3anc 1365 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → (𝑚 − 2) ≤ 𝑦)
91 breq1 5066 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝑚 − 2) → (𝑘𝑦 ↔ (𝑚 − 2) ≤ 𝑦))
92 fveq2 6667 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (𝑚 − 2) → (𝐼𝑘) = (𝐼‘(𝑚 − 2)))
9392eleq1d 2902 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝑚 − 2) → ((𝐼𝑘) ∈ ℝ+ ↔ (𝐼‘(𝑚 − 2)) ∈ ℝ+))
9491, 93imbi12d 346 . . . . . . . . . . . . . . . . 17 (𝑘 = (𝑚 − 2) → ((𝑘𝑦 → (𝐼𝑘) ∈ ℝ+) ↔ ((𝑚 − 2) ≤ 𝑦 → (𝐼‘(𝑚 − 2)) ∈ ℝ+)))
9594rspccva 3626 . . . . . . . . . . . . . . . 16 ((∀𝑘 ∈ ℕ0 (𝑘𝑦 → (𝐼𝑘) ∈ ℝ+) ∧ (𝑚 − 2) ∈ ℕ0) → ((𝑚 − 2) ≤ 𝑦 → (𝐼‘(𝑚 − 2)) ∈ ℝ+))
9670, 90, 95sylc 65 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → (𝐼‘(𝑚 − 2)) ∈ ℝ+)
9760, 96rpmulcld 12437 . . . . . . . . . . . . . 14 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → (((𝑚 − 1) / 𝑚) · (𝐼‘(𝑚 − 2))) ∈ ℝ+)
9844, 97eqeltrd 2918 . . . . . . . . . . . . 13 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → (𝐼𝑚) ∈ ℝ+)
9998adantllr 715 . . . . . . . . . . . 12 (((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = (𝑦 + 1)) ∧ 𝑚 ∈ (ℤ‘2)) → (𝐼𝑚) ∈ ℝ+)
10099ex 413 . . . . . . . . . . 11 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = (𝑦 + 1)) → (𝑚 ∈ (ℤ‘2) → (𝐼𝑚) ∈ ℝ+))
101 simplll 771 . . . . . . . . . . . 12 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = (𝑦 + 1)) → 𝑦 ∈ ℕ0)
102 simplr 765 . . . . . . . . . . . 12 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = (𝑦 + 1)) → 𝑚 ∈ ℕ0)
103 simpr 485 . . . . . . . . . . . 12 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = (𝑦 + 1)) → 𝑚 = (𝑦 + 1))
104 simp3 1132 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 = (𝑦 + 1)) → 𝑚 = (𝑦 + 1))
105 nn0p1nn 11925 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ0 → (𝑦 + 1) ∈ ℕ)
1061053ad2ant1 1127 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 = (𝑦 + 1)) → (𝑦 + 1) ∈ ℕ)
107104, 106eqeltrd 2918 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 = (𝑦 + 1)) → 𝑚 ∈ ℕ)
108 elnnuz 12271 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ‘1))
109107, 108sylib 219 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 = (𝑦 + 1)) → 𝑚 ∈ (ℤ‘1))
110 uzp1 12268 . . . . . . . . . . . . . 14 (𝑚 ∈ (ℤ‘1) → (𝑚 = 1 ∨ 𝑚 ∈ (ℤ‘(1 + 1))))
111 1p1e2 11751 . . . . . . . . . . . . . . . . 17 (1 + 1) = 2
112111fveq2i 6670 . . . . . . . . . . . . . . . 16 (ℤ‘(1 + 1)) = (ℤ‘2)
113112eleq2i 2909 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ℤ‘(1 + 1)) ↔ 𝑚 ∈ (ℤ‘2))
114113orbi2i 908 . . . . . . . . . . . . . 14 ((𝑚 = 1 ∨ 𝑚 ∈ (ℤ‘(1 + 1))) ↔ (𝑚 = 1 ∨ 𝑚 ∈ (ℤ‘2)))
115110, 114sylib 219 . . . . . . . . . . . . 13 (𝑚 ∈ (ℤ‘1) → (𝑚 = 1 ∨ 𝑚 ∈ (ℤ‘2)))
116109, 115syl 17 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 = (𝑦 + 1)) → (𝑚 = 1 ∨ 𝑚 ∈ (ℤ‘2)))
117101, 102, 103, 116syl3anc 1365 . . . . . . . . . . 11 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = (𝑦 + 1)) → (𝑚 = 1 ∨ 𝑚 ∈ (ℤ‘2)))
11842, 100, 117mpjaod 856 . . . . . . . . . 10 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = (𝑦 + 1)) → (𝐼𝑚) ∈ ℝ+)
119118adantlr 711 . . . . . . . . 9 (((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ (𝑦 + 1)) ∧ 𝑚 = (𝑦 + 1)) → (𝐼𝑚) ∈ ℝ+)
120119ex 413 . . . . . . . 8 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ (𝑦 + 1)) → (𝑚 = (𝑦 + 1) → (𝐼𝑚) ∈ ℝ+))
121 simplll 771 . . . . . . . . 9 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ (𝑦 + 1)) → 𝑦 ∈ ℕ0)
122 simpr 485 . . . . . . . . 9 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ (𝑦 + 1)) → 𝑚 ≤ (𝑦 + 1))
123 simpl1 1185 . . . . . . . . . . 11 (((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) ∧ 𝑚 < (𝑦 + 1)) → 𝑦 ∈ ℕ0)
124 simpl2 1186 . . . . . . . . . . 11 (((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) ∧ 𝑚 < (𝑦 + 1)) → 𝑚 ∈ ℕ0)
125 simpr 485 . . . . . . . . . . 11 (((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) ∧ 𝑚 < (𝑦 + 1)) → 𝑚 < (𝑦 + 1))
126 simpr 485 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0𝑚 = 0) → 𝑚 = 0)
127 nn0ge0 11911 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ0 → 0 ≤ 𝑦)
128127adantr 481 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0𝑚 = 0) → 0 ≤ 𝑦)
129126, 128eqbrtrd 5085 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0𝑚 = 0) → 𝑚𝑦)
1301293ad2antl1 1179 . . . . . . . . . . . . 13 (((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 < (𝑦 + 1)) ∧ 𝑚 = 0) → 𝑚𝑦)
131 simpl1 1185 . . . . . . . . . . . . . 14 (((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 < (𝑦 + 1)) ∧ 𝑚 ∈ ℕ) → 𝑦 ∈ ℕ0)
132 simpr 485 . . . . . . . . . . . . . 14 (((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 < (𝑦 + 1)) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
133 simpl3 1187 . . . . . . . . . . . . . 14 (((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 < (𝑦 + 1)) ∧ 𝑚 ∈ ℕ) → 𝑚 < (𝑦 + 1))
134 simp3 1132 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → 𝑚 < (𝑦 + 1))
135 simp2 1131 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → 𝑚 ∈ ℕ)
136 simp1 1130 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → 𝑦 ∈ ℕ0)
137 0red 10633 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → 0 ∈ ℝ)
138483ad2ant2 1128 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → (𝑚 − 1) ∈ ℝ)
139763ad2ant1 1127 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → 𝑦 ∈ ℝ)
140 nnm1ge0 12039 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ → 0 ≤ (𝑚 − 1))
1411403ad2ant2 1128 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → 0 ≤ (𝑚 − 1))
142463ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → 𝑚 ∈ ℝ)
143 1red 10631 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → 1 ∈ ℝ)
144142, 143, 139ltsubaddd 11225 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → ((𝑚 − 1) < 𝑦𝑚 < (𝑦 + 1)))
145134, 144mpbird 258 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → (𝑚 − 1) < 𝑦)
146137, 138, 139, 141, 145lelttrd 10787 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → 0 < 𝑦)
147146gt0ne0d 11193 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → 𝑦 ≠ 0)
148 elnnne0 11900 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ ↔ (𝑦 ∈ ℕ0𝑦 ≠ 0))
149136, 147, 148sylanbrc 583 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → 𝑦 ∈ ℕ)
150 nnleltp1 12026 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑚𝑦𝑚 < (𝑦 + 1)))
151135, 149, 150syl2anc 584 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → (𝑚𝑦𝑚 < (𝑦 + 1)))
152134, 151mpbird 258 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ ∧ 𝑚 < (𝑦 + 1)) → 𝑚𝑦)
153131, 132, 133, 152syl3anc 1365 . . . . . . . . . . . . 13 (((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 < (𝑦 + 1)) ∧ 𝑚 ∈ ℕ) → 𝑚𝑦)
154 elnn0 11888 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ0 ↔ (𝑚 ∈ ℕ ∨ 𝑚 = 0))
155154biimpi 217 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → (𝑚 ∈ ℕ ∨ 𝑚 = 0))
156155orcomd 867 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 → (𝑚 = 0 ∨ 𝑚 ∈ ℕ))
1571563ad2ant2 1128 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 < (𝑦 + 1)) → (𝑚 = 0 ∨ 𝑚 ∈ ℕ))
158130, 153, 157mpjaodan 954 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 < (𝑦 + 1)) → 𝑚𝑦)
159158orcd 871 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 < (𝑦 + 1)) → (𝑚𝑦𝑚 = (𝑦 + 1)))
160123, 124, 125, 159syl3anc 1365 . . . . . . . . . 10 (((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) ∧ 𝑚 < (𝑦 + 1)) → (𝑚𝑦𝑚 = (𝑦 + 1)))
161 simpr 485 . . . . . . . . . . 11 (((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) ∧ 𝑚 = (𝑦 + 1)) → 𝑚 = (𝑦 + 1))
162161olcd 872 . . . . . . . . . 10 (((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) ∧ 𝑚 = (𝑦 + 1)) → (𝑚𝑦𝑚 = (𝑦 + 1)))
163 simp3 1132 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) → 𝑚 ≤ (𝑦 + 1))
164163ad2ant2 1128 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) → 𝑚 ∈ ℝ)
165763ad2ant1 1127 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) → 𝑦 ∈ ℝ)
166 1red 10631 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) → 1 ∈ ℝ)
167165, 166readdcld 10659 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) → (𝑦 + 1) ∈ ℝ)
168164, 167leloed 10772 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) → (𝑚 ≤ (𝑦 + 1) ↔ (𝑚 < (𝑦 + 1) ∨ 𝑚 = (𝑦 + 1))))
169163, 168mpbid 233 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) → (𝑚 < (𝑦 + 1) ∨ 𝑚 = (𝑦 + 1)))
170160, 162, 169mpjaodan 954 . . . . . . . . 9 ((𝑦 ∈ ℕ0𝑚 ∈ ℕ0𝑚 ≤ (𝑦 + 1)) → (𝑚𝑦𝑚 = (𝑦 + 1)))
171121, 34, 122, 170syl3anc 1365 . . . . . . . 8 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ (𝑦 + 1)) → (𝑚𝑦𝑚 = (𝑦 + 1)))
17236, 120, 171mpjaod 856 . . . . . . 7 ((((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ (𝑦 + 1)) → (𝐼𝑚) ∈ ℝ+)
173172exp31 420 . . . . . 6 ((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) → (𝑚 ∈ ℕ0 → (𝑚 ≤ (𝑦 + 1) → (𝐼𝑚) ∈ ℝ+)))
17432, 173ralrimi 3221 . . . . 5 ((𝑦 ∈ ℕ0 ∧ ∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+)) → ∀𝑚 ∈ ℕ0 (𝑚 ≤ (𝑦 + 1) → (𝐼𝑚) ∈ ℝ+))
175174ex 413 . . . 4 (𝑦 ∈ ℕ0 → (∀𝑚 ∈ ℕ0 (𝑚𝑦 → (𝐼𝑚) ∈ ℝ+) → ∀𝑚 ∈ ℕ0 (𝑚 ≤ (𝑦 + 1) → (𝐼𝑚) ∈ ℝ+)))
1763, 6, 9, 12, 29, 175nn0ind 12066 . . 3 (𝑁 ∈ ℕ0 → ∀𝑚 ∈ ℕ0 (𝑚𝑁 → (𝐼𝑚) ∈ ℝ+))
177176ancri 550 . 2 (𝑁 ∈ ℕ0 → (∀𝑚 ∈ ℕ0 (𝑚𝑁 → (𝐼𝑚) ∈ ℝ+) ∧ 𝑁 ∈ ℕ0))
178 nn0re 11895 . . 3 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
179178leidd 11195 . 2 (𝑁 ∈ ℕ0𝑁𝑁)
180 breq1 5066 . . . 4 (𝑚 = 𝑁 → (𝑚𝑁𝑁𝑁))
181 fveq2 6667 . . . . 5 (𝑚 = 𝑁 → (𝐼𝑚) = (𝐼𝑁))
182181eleq1d 2902 . . . 4 (𝑚 = 𝑁 → ((𝐼𝑚) ∈ ℝ+ ↔ (𝐼𝑁) ∈ ℝ+))
183180, 182imbi12d 346 . . 3 (𝑚 = 𝑁 → ((𝑚𝑁 → (𝐼𝑚) ∈ ℝ+) ↔ (𝑁𝑁 → (𝐼𝑁) ∈ ℝ+)))
184183rspccva 3626 . 2 ((∀𝑚 ∈ ℕ0 (𝑚𝑁 → (𝐼𝑚) ∈ ℝ+) ∧ 𝑁 ∈ ℕ0) → (𝑁𝑁 → (𝐼𝑁) ∈ ℝ+))
185177, 179, 184sylc 65 1 (𝑁 ∈ ℕ0 → (𝐼𝑁) ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 843  w3a 1081   = wceq 1530  wcel 2107  wne 3021  wral 3143   class class class wbr 5063  cmpt 5143  cfv 6352  (class class class)co 7148  cc 10524  cr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531   < clt 10664  cle 10665  cmin 10859   / cdiv 11286  cn 11627  2c2 11681  0cn0 11886  cuz 12232  +crp 12379  (,)cioo 12728  cexp 13419  sincsin 15407  πcpi 15410  citg 24134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-inf2 9093  ax-cc 9846  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-symdif 4223  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-disj 5029  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-isom 6361  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7399  df-ofr 7400  df-om 7569  df-1st 7680  df-2nd 7681  df-supp 7822  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-2o 8094  df-oadd 8097  df-omul 8098  df-er 8279  df-map 8398  df-pm 8399  df-ixp 8451  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-fsupp 8823  df-fi 8864  df-sup 8895  df-inf 8896  df-oi 8963  df-dju 9319  df-card 9357  df-acn 9360  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11628  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696  df-n0 11887  df-z 11971  df-dec 12088  df-uz 12233  df-q 12338  df-rp 12380  df-xneg 12497  df-xadd 12498  df-xmul 12499  df-ioo 12732  df-ioc 12733  df-ico 12734  df-icc 12735  df-fz 12883  df-fzo 13024  df-fl 13152  df-mod 13228  df-seq 13360  df-exp 13420  df-fac 13624  df-bc 13653  df-hash 13681  df-shft 14416  df-cj 14448  df-re 14449  df-im 14450  df-sqrt 14584  df-abs 14585  df-limsup 14818  df-clim 14835  df-rlim 14836  df-sum 15033  df-ef 15411  df-sin 15413  df-cos 15414  df-pi 15416  df-struct 16475  df-ndx 16476  df-slot 16477  df-base 16479  df-sets 16480  df-ress 16481  df-plusg 16568  df-mulr 16569  df-starv 16570  df-sca 16571  df-vsca 16572  df-ip 16573  df-tset 16574  df-ple 16575  df-ds 16577  df-unif 16578  df-hom 16579  df-cco 16580  df-rest 16686  df-topn 16687  df-0g 16705  df-gsum 16706  df-topgen 16707  df-pt 16708  df-prds 16711  df-xrs 16765  df-qtop 16770  df-imas 16771  df-xps 16773  df-mre 16847  df-mrc 16848  df-acs 16850  df-mgm 17842  df-sgrp 17890  df-mnd 17901  df-submnd 17945  df-mulg 18155  df-cntz 18377  df-cmn 18828  df-psmet 20453  df-xmet 20454  df-met 20455  df-bl 20456  df-mopn 20457  df-fbas 20458  df-fg 20459  df-cnfld 20462  df-top 21418  df-topon 21435  df-topsp 21457  df-bases 21470  df-cld 21543  df-ntr 21544  df-cls 21545  df-nei 21622  df-lp 21660  df-perf 21661  df-cn 21751  df-cnp 21752  df-haus 21839  df-cmp 21911  df-tx 22086  df-hmeo 22279  df-fil 22370  df-fm 22462  df-flim 22463  df-flf 22464  df-xms 22845  df-ms 22846  df-tms 22847  df-cncf 23401  df-ovol 23980  df-vol 23981  df-mbf 24135  df-itg1 24136  df-itg2 24137  df-ibl 24138  df-itg 24139  df-0p 24186  df-limc 24379  df-dv 24380
This theorem is referenced by:  wallispilem4  42219  wallispilem5  42220
  Copyright terms: Public domain W3C validator