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

Theorem wallispilem4 44395
Description: 𝐹 maps to explicit expression for the ratio of two consecutive values of 𝐼. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
Hypotheses
Ref Expression
wallispilem4.1 𝐹 = (π‘˜ ∈ β„• ↦ (((2 Β· π‘˜) / ((2 Β· π‘˜) βˆ’ 1)) Β· ((2 Β· π‘˜) / ((2 Β· π‘˜) + 1))))
wallispilem4.2 𝐼 = (𝑛 ∈ β„•0 ↦ ∫(0(,)Ο€)((sinβ€˜π‘§)↑𝑛) d𝑧)
wallispilem4.3 𝐺 = (𝑛 ∈ β„• ↦ ((πΌβ€˜(2 Β· 𝑛)) / (πΌβ€˜((2 Β· 𝑛) + 1))))
wallispilem4.4 𝐻 = (𝑛 ∈ β„• ↦ ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘›))))
Assertion
Ref Expression
wallispilem4 𝐺 = 𝐻
Distinct variable groups:   𝑧,𝑛   𝑧,𝐹
Allowed substitution hints:   𝐹(π‘˜,𝑛)   𝐺(𝑧,π‘˜,𝑛)   𝐻(𝑧,π‘˜,𝑛)   𝐼(𝑧,π‘˜,𝑛)

Proof of Theorem wallispilem4
Dummy variables 𝑀 𝑦 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7366 . . . . . . 7 (π‘₯ = 1 β†’ (2 Β· π‘₯) = (2 Β· 1))
21fveq2d 6847 . . . . . 6 (π‘₯ = 1 β†’ (πΌβ€˜(2 Β· π‘₯)) = (πΌβ€˜(2 Β· 1)))
31fvoveq1d 7380 . . . . . 6 (π‘₯ = 1 β†’ (πΌβ€˜((2 Β· π‘₯) + 1)) = (πΌβ€˜((2 Β· 1) + 1)))
42, 3oveq12d 7376 . . . . 5 (π‘₯ = 1 β†’ ((πΌβ€˜(2 Β· π‘₯)) / (πΌβ€˜((2 Β· π‘₯) + 1))) = ((πΌβ€˜(2 Β· 1)) / (πΌβ€˜((2 Β· 1) + 1))))
5 fveq2 6843 . . . . . . 7 (π‘₯ = 1 β†’ (seq1( Β· , 𝐹)β€˜π‘₯) = (seq1( Β· , 𝐹)β€˜1))
65oveq2d 7374 . . . . . 6 (π‘₯ = 1 β†’ (1 / (seq1( Β· , 𝐹)β€˜π‘₯)) = (1 / (seq1( Β· , 𝐹)β€˜1)))
76oveq2d 7374 . . . . 5 (π‘₯ = 1 β†’ ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘₯))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜1))))
84, 7eqeq12d 2749 . . . 4 (π‘₯ = 1 β†’ (((πΌβ€˜(2 Β· π‘₯)) / (πΌβ€˜((2 Β· π‘₯) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘₯))) ↔ ((πΌβ€˜(2 Β· 1)) / (πΌβ€˜((2 Β· 1) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜1)))))
9 oveq2 7366 . . . . . . 7 (π‘₯ = 𝑦 β†’ (2 Β· π‘₯) = (2 Β· 𝑦))
109fveq2d 6847 . . . . . 6 (π‘₯ = 𝑦 β†’ (πΌβ€˜(2 Β· π‘₯)) = (πΌβ€˜(2 Β· 𝑦)))
119fvoveq1d 7380 . . . . . 6 (π‘₯ = 𝑦 β†’ (πΌβ€˜((2 Β· π‘₯) + 1)) = (πΌβ€˜((2 Β· 𝑦) + 1)))
1210, 11oveq12d 7376 . . . . 5 (π‘₯ = 𝑦 β†’ ((πΌβ€˜(2 Β· π‘₯)) / (πΌβ€˜((2 Β· π‘₯) + 1))) = ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1))))
13 fveq2 6843 . . . . . . 7 (π‘₯ = 𝑦 β†’ (seq1( Β· , 𝐹)β€˜π‘₯) = (seq1( Β· , 𝐹)β€˜π‘¦))
1413oveq2d 7374 . . . . . 6 (π‘₯ = 𝑦 β†’ (1 / (seq1( Β· , 𝐹)β€˜π‘₯)) = (1 / (seq1( Β· , 𝐹)β€˜π‘¦)))
1514oveq2d 7374 . . . . 5 (π‘₯ = 𝑦 β†’ ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘₯))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))))
1612, 15eqeq12d 2749 . . . 4 (π‘₯ = 𝑦 β†’ (((πΌβ€˜(2 Β· π‘₯)) / (πΌβ€˜((2 Β· π‘₯) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘₯))) ↔ ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦)))))
17 oveq2 7366 . . . . . . 7 (π‘₯ = (𝑦 + 1) β†’ (2 Β· π‘₯) = (2 Β· (𝑦 + 1)))
1817fveq2d 6847 . . . . . 6 (π‘₯ = (𝑦 + 1) β†’ (πΌβ€˜(2 Β· π‘₯)) = (πΌβ€˜(2 Β· (𝑦 + 1))))
1917fvoveq1d 7380 . . . . . 6 (π‘₯ = (𝑦 + 1) β†’ (πΌβ€˜((2 Β· π‘₯) + 1)) = (πΌβ€˜((2 Β· (𝑦 + 1)) + 1)))
2018, 19oveq12d 7376 . . . . 5 (π‘₯ = (𝑦 + 1) β†’ ((πΌβ€˜(2 Β· π‘₯)) / (πΌβ€˜((2 Β· π‘₯) + 1))) = ((πΌβ€˜(2 Β· (𝑦 + 1))) / (πΌβ€˜((2 Β· (𝑦 + 1)) + 1))))
21 fveq2 6843 . . . . . . 7 (π‘₯ = (𝑦 + 1) β†’ (seq1( Β· , 𝐹)β€˜π‘₯) = (seq1( Β· , 𝐹)β€˜(𝑦 + 1)))
2221oveq2d 7374 . . . . . 6 (π‘₯ = (𝑦 + 1) β†’ (1 / (seq1( Β· , 𝐹)β€˜π‘₯)) = (1 / (seq1( Β· , 𝐹)β€˜(𝑦 + 1))))
2322oveq2d 7374 . . . . 5 (π‘₯ = (𝑦 + 1) β†’ ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘₯))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜(𝑦 + 1)))))
2420, 23eqeq12d 2749 . . . 4 (π‘₯ = (𝑦 + 1) β†’ (((πΌβ€˜(2 Β· π‘₯)) / (πΌβ€˜((2 Β· π‘₯) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘₯))) ↔ ((πΌβ€˜(2 Β· (𝑦 + 1))) / (πΌβ€˜((2 Β· (𝑦 + 1)) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜(𝑦 + 1))))))
25 oveq2 7366 . . . . . . 7 (π‘₯ = 𝑛 β†’ (2 Β· π‘₯) = (2 Β· 𝑛))
2625fveq2d 6847 . . . . . 6 (π‘₯ = 𝑛 β†’ (πΌβ€˜(2 Β· π‘₯)) = (πΌβ€˜(2 Β· 𝑛)))
2725fvoveq1d 7380 . . . . . 6 (π‘₯ = 𝑛 β†’ (πΌβ€˜((2 Β· π‘₯) + 1)) = (πΌβ€˜((2 Β· 𝑛) + 1)))
2826, 27oveq12d 7376 . . . . 5 (π‘₯ = 𝑛 β†’ ((πΌβ€˜(2 Β· π‘₯)) / (πΌβ€˜((2 Β· π‘₯) + 1))) = ((πΌβ€˜(2 Β· 𝑛)) / (πΌβ€˜((2 Β· 𝑛) + 1))))
29 fveq2 6843 . . . . . . 7 (π‘₯ = 𝑛 β†’ (seq1( Β· , 𝐹)β€˜π‘₯) = (seq1( Β· , 𝐹)β€˜π‘›))
3029oveq2d 7374 . . . . . 6 (π‘₯ = 𝑛 β†’ (1 / (seq1( Β· , 𝐹)β€˜π‘₯)) = (1 / (seq1( Β· , 𝐹)β€˜π‘›)))
3130oveq2d 7374 . . . . 5 (π‘₯ = 𝑛 β†’ ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘₯))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘›))))
3228, 31eqeq12d 2749 . . . 4 (π‘₯ = 𝑛 β†’ (((πΌβ€˜(2 Β· π‘₯)) / (πΌβ€˜((2 Β· π‘₯) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘₯))) ↔ ((πΌβ€˜(2 Β· 𝑛)) / (πΌβ€˜((2 Β· 𝑛) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘›)))))
33 2t1e2 12321 . . . . . . 7 (2 Β· 1) = 2
3433fveq2i 6846 . . . . . 6 (πΌβ€˜(2 Β· 1)) = (πΌβ€˜2)
3533oveq1i 7368 . . . . . . . 8 ((2 Β· 1) + 1) = (2 + 1)
36 2p1e3 12300 . . . . . . . 8 (2 + 1) = 3
3735, 36eqtri 2761 . . . . . . 7 ((2 Β· 1) + 1) = 3
3837fveq2i 6846 . . . . . 6 (πΌβ€˜((2 Β· 1) + 1)) = (πΌβ€˜3)
3934, 38oveq12i 7370 . . . . 5 ((πΌβ€˜(2 Β· 1)) / (πΌβ€˜((2 Β· 1) + 1))) = ((πΌβ€˜2) / (πΌβ€˜3))
40 2z 12540 . . . . . . . . 9 2 ∈ β„€
41 uzid 12783 . . . . . . . . 9 (2 ∈ β„€ β†’ 2 ∈ (β„€β‰₯β€˜2))
4240, 41ax-mp 5 . . . . . . . 8 2 ∈ (β„€β‰₯β€˜2)
43 wallispilem4.2 . . . . . . . . . 10 𝐼 = (𝑛 ∈ β„•0 ↦ ∫(0(,)Ο€)((sinβ€˜π‘§)↑𝑛) d𝑧)
4443wallispilem2 44393 . . . . . . . . 9 ((πΌβ€˜0) = Ο€ ∧ (πΌβ€˜1) = 2 ∧ (2 ∈ (β„€β‰₯β€˜2) β†’ (πΌβ€˜2) = (((2 βˆ’ 1) / 2) Β· (πΌβ€˜(2 βˆ’ 2)))))
4544simp3i 1142 . . . . . . . 8 (2 ∈ (β„€β‰₯β€˜2) β†’ (πΌβ€˜2) = (((2 βˆ’ 1) / 2) Β· (πΌβ€˜(2 βˆ’ 2))))
4642, 45ax-mp 5 . . . . . . 7 (πΌβ€˜2) = (((2 βˆ’ 1) / 2) Β· (πΌβ€˜(2 βˆ’ 2)))
47 2m1e1 12284 . . . . . . . . 9 (2 βˆ’ 1) = 1
4847oveq1i 7368 . . . . . . . 8 ((2 βˆ’ 1) / 2) = (1 / 2)
49 2cn 12233 . . . . . . . . . . 11 2 ∈ β„‚
5049subidi 11477 . . . . . . . . . 10 (2 βˆ’ 2) = 0
5150fveq2i 6846 . . . . . . . . 9 (πΌβ€˜(2 βˆ’ 2)) = (πΌβ€˜0)
5244simp1i 1140 . . . . . . . . 9 (πΌβ€˜0) = Ο€
5351, 52eqtri 2761 . . . . . . . 8 (πΌβ€˜(2 βˆ’ 2)) = Ο€
5448, 53oveq12i 7370 . . . . . . 7 (((2 βˆ’ 1) / 2) Β· (πΌβ€˜(2 βˆ’ 2))) = ((1 / 2) Β· Ο€)
55 ax-1cn 11114 . . . . . . . . 9 1 ∈ β„‚
56 2cnne0 12368 . . . . . . . . 9 (2 ∈ β„‚ ∧ 2 β‰  0)
57 picn 25832 . . . . . . . . 9 Ο€ ∈ β„‚
58 div32 11838 . . . . . . . . 9 ((1 ∈ β„‚ ∧ (2 ∈ β„‚ ∧ 2 β‰  0) ∧ Ο€ ∈ β„‚) β†’ ((1 / 2) Β· Ο€) = (1 Β· (Ο€ / 2)))
5955, 56, 57, 58mp3an 1462 . . . . . . . 8 ((1 / 2) Β· Ο€) = (1 Β· (Ο€ / 2))
60 2ne0 12262 . . . . . . . . . 10 2 β‰  0
6157, 49, 60divcli 11902 . . . . . . . . 9 (Ο€ / 2) ∈ β„‚
6261mulid2i 11165 . . . . . . . 8 (1 Β· (Ο€ / 2)) = (Ο€ / 2)
6359, 62eqtri 2761 . . . . . . 7 ((1 / 2) Β· Ο€) = (Ο€ / 2)
6446, 54, 633eqtri 2765 . . . . . 6 (πΌβ€˜2) = (Ο€ / 2)
65 3z 12541 . . . . . . . . 9 3 ∈ β„€
66 2re 12232 . . . . . . . . . 10 2 ∈ ℝ
67 3re 12238 . . . . . . . . . 10 3 ∈ ℝ
68 2lt3 12330 . . . . . . . . . 10 2 < 3
6966, 67, 68ltleii 11283 . . . . . . . . 9 2 ≀ 3
70 eluz2 12774 . . . . . . . . 9 (3 ∈ (β„€β‰₯β€˜2) ↔ (2 ∈ β„€ ∧ 3 ∈ β„€ ∧ 2 ≀ 3))
7140, 65, 69, 70mpbir3an 1342 . . . . . . . 8 3 ∈ (β„€β‰₯β€˜2)
7243wallispilem2 44393 . . . . . . . . 9 ((πΌβ€˜0) = Ο€ ∧ (πΌβ€˜1) = 2 ∧ (3 ∈ (β„€β‰₯β€˜2) β†’ (πΌβ€˜3) = (((3 βˆ’ 1) / 3) Β· (πΌβ€˜(3 βˆ’ 2)))))
7372simp3i 1142 . . . . . . . 8 (3 ∈ (β„€β‰₯β€˜2) β†’ (πΌβ€˜3) = (((3 βˆ’ 1) / 3) Β· (πΌβ€˜(3 βˆ’ 2))))
7471, 73ax-mp 5 . . . . . . 7 (πΌβ€˜3) = (((3 βˆ’ 1) / 3) Β· (πΌβ€˜(3 βˆ’ 2)))
75 3m1e2 12286 . . . . . . . . . 10 (3 βˆ’ 1) = 2
7675eqcomi 2742 . . . . . . . . 9 2 = (3 βˆ’ 1)
7776oveq1i 7368 . . . . . . . 8 (2 / 3) = ((3 βˆ’ 1) / 3)
78 3cn 12239 . . . . . . . . . . 11 3 ∈ β„‚
7978, 49, 55, 36subaddrii 11495 . . . . . . . . . 10 (3 βˆ’ 2) = 1
8079fveq2i 6846 . . . . . . . . 9 (πΌβ€˜(3 βˆ’ 2)) = (πΌβ€˜1)
8144simp2i 1141 . . . . . . . . 9 (πΌβ€˜1) = 2
8280, 81eqtr2i 2762 . . . . . . . 8 2 = (πΌβ€˜(3 βˆ’ 2))
8377, 82oveq12i 7370 . . . . . . 7 ((2 / 3) Β· 2) = (((3 βˆ’ 1) / 3) Β· (πΌβ€˜(3 βˆ’ 2)))
84 3ne0 12264 . . . . . . . . 9 3 β‰  0
8549, 78, 84divcli 11902 . . . . . . . 8 (2 / 3) ∈ β„‚
8685, 49mulcomi 11168 . . . . . . 7 ((2 / 3) Β· 2) = (2 Β· (2 / 3))
8774, 83, 863eqtr2i 2767 . . . . . 6 (πΌβ€˜3) = (2 Β· (2 / 3))
8864, 87oveq12i 7370 . . . . 5 ((πΌβ€˜2) / (πΌβ€˜3)) = ((Ο€ / 2) / (2 Β· (2 / 3)))
89 1z 12538 . . . . . . . . 9 1 ∈ β„€
90 seq1 13925 . . . . . . . . 9 (1 ∈ β„€ β†’ (seq1( Β· , 𝐹)β€˜1) = (πΉβ€˜1))
9189, 90ax-mp 5 . . . . . . . 8 (seq1( Β· , 𝐹)β€˜1) = (πΉβ€˜1)
92 1nn 12169 . . . . . . . . 9 1 ∈ β„•
93 oveq2 7366 . . . . . . . . . . . . . 14 (π‘˜ = 1 β†’ (2 Β· π‘˜) = (2 Β· 1))
9493, 33eqtrdi 2789 . . . . . . . . . . . . 13 (π‘˜ = 1 β†’ (2 Β· π‘˜) = 2)
9593oveq1d 7373 . . . . . . . . . . . . . 14 (π‘˜ = 1 β†’ ((2 Β· π‘˜) βˆ’ 1) = ((2 Β· 1) βˆ’ 1))
9633oveq1i 7368 . . . . . . . . . . . . . . 15 ((2 Β· 1) βˆ’ 1) = (2 βˆ’ 1)
9796, 47eqtri 2761 . . . . . . . . . . . . . 14 ((2 Β· 1) βˆ’ 1) = 1
9895, 97eqtrdi 2789 . . . . . . . . . . . . 13 (π‘˜ = 1 β†’ ((2 Β· π‘˜) βˆ’ 1) = 1)
9994, 98oveq12d 7376 . . . . . . . . . . . 12 (π‘˜ = 1 β†’ ((2 Β· π‘˜) / ((2 Β· π‘˜) βˆ’ 1)) = (2 / 1))
10049div1i 11888 . . . . . . . . . . . 12 (2 / 1) = 2
10199, 100eqtrdi 2789 . . . . . . . . . . 11 (π‘˜ = 1 β†’ ((2 Β· π‘˜) / ((2 Β· π‘˜) βˆ’ 1)) = 2)
10294oveq1d 7373 . . . . . . . . . . . . 13 (π‘˜ = 1 β†’ ((2 Β· π‘˜) + 1) = (2 + 1))
103102, 36eqtrdi 2789 . . . . . . . . . . . 12 (π‘˜ = 1 β†’ ((2 Β· π‘˜) + 1) = 3)
10494, 103oveq12d 7376 . . . . . . . . . . 11 (π‘˜ = 1 β†’ ((2 Β· π‘˜) / ((2 Β· π‘˜) + 1)) = (2 / 3))
105101, 104oveq12d 7376 . . . . . . . . . 10 (π‘˜ = 1 β†’ (((2 Β· π‘˜) / ((2 Β· π‘˜) βˆ’ 1)) Β· ((2 Β· π‘˜) / ((2 Β· π‘˜) + 1))) = (2 Β· (2 / 3)))
106 wallispilem4.1 . . . . . . . . . 10 𝐹 = (π‘˜ ∈ β„• ↦ (((2 Β· π‘˜) / ((2 Β· π‘˜) βˆ’ 1)) Β· ((2 Β· π‘˜) / ((2 Β· π‘˜) + 1))))
107 ovex 7391 . . . . . . . . . 10 (2 Β· (2 / 3)) ∈ V
108105, 106, 107fvmpt 6949 . . . . . . . . 9 (1 ∈ β„• β†’ (πΉβ€˜1) = (2 Β· (2 / 3)))
10992, 108ax-mp 5 . . . . . . . 8 (πΉβ€˜1) = (2 Β· (2 / 3))
11091, 109eqtr2i 2762 . . . . . . 7 (2 Β· (2 / 3)) = (seq1( Β· , 𝐹)β€˜1)
111110oveq2i 7369 . . . . . 6 ((Ο€ / 2) / (2 Β· (2 / 3))) = ((Ο€ / 2) / (seq1( Β· , 𝐹)β€˜1))
11249, 85mulcli 11167 . . . . . . . . 9 (2 Β· (2 / 3)) ∈ β„‚
113109, 112eqeltri 2830 . . . . . . . 8 (πΉβ€˜1) ∈ β„‚
11491, 113eqeltri 2830 . . . . . . 7 (seq1( Β· , 𝐹)β€˜1) ∈ β„‚
11549, 78, 60, 84divne0i 11908 . . . . . . . . 9 (2 / 3) β‰  0
11649, 85, 60, 115mulne0i 11803 . . . . . . . 8 (2 Β· (2 / 3)) β‰  0
117110, 116eqnetrri 3012 . . . . . . 7 (seq1( Β· , 𝐹)β€˜1) β‰  0
11861, 114, 117divreci 11905 . . . . . 6 ((Ο€ / 2) / (seq1( Β· , 𝐹)β€˜1)) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜1)))
119111, 118eqtri 2761 . . . . 5 ((Ο€ / 2) / (2 Β· (2 / 3))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜1)))
12039, 88, 1193eqtri 2765 . . . 4 ((πΌβ€˜(2 Β· 1)) / (πΌβ€˜((2 Β· 1) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜1)))
121 oveq2 7366 . . . . . . 7 (((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) β†’ (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1)))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦)))))
122121adantl 483 . . . . . 6 ((𝑦 ∈ β„• ∧ ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦)))) β†’ (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1)))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦)))))
123 2cnd 12236 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ 2 ∈ β„‚)
124 nncn 12166 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ 𝑦 ∈ β„‚)
12555a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ 1 ∈ β„‚)
126123, 124, 125adddid 11184 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ (2 Β· (𝑦 + 1)) = ((2 Β· 𝑦) + (2 Β· 1)))
127123mulid1d 11177 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ (2 Β· 1) = 2)
128127oveq2d 7374 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + (2 Β· 1)) = ((2 Β· 𝑦) + 2))
129126, 128eqtrd 2773 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (2 Β· (𝑦 + 1)) = ((2 Β· 𝑦) + 2))
130129oveq1d 7373 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) βˆ’ 1) = (((2 Β· 𝑦) + 2) βˆ’ 1))
131123, 124mulcld 11180 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (2 Β· 𝑦) ∈ β„‚)
132131, 123, 125addsubassd 11537 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ (((2 Β· 𝑦) + 2) βˆ’ 1) = ((2 Β· 𝑦) + (2 βˆ’ 1)))
13347a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (2 βˆ’ 1) = 1)
134133oveq2d 7374 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + (2 βˆ’ 1)) = ((2 Β· 𝑦) + 1))
135130, 132, 1343eqtrd 2777 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) βˆ’ 1) = ((2 Β· 𝑦) + 1))
136135oveq1d 7373 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (((2 Β· (𝑦 + 1)) βˆ’ 1) / (2 Β· (𝑦 + 1))) = (((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))))
137136oveq1d 7373 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ ((((2 Β· (𝑦 + 1)) βˆ’ 1) / (2 Β· (𝑦 + 1))) Β· (πΌβ€˜(2 Β· 𝑦))) = ((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) Β· (πΌβ€˜(2 Β· 𝑦))))
13875a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (3 βˆ’ 1) = 2)
139138oveq2d 7374 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + (3 βˆ’ 1)) = ((2 Β· 𝑦) + 2))
14078a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ 3 ∈ β„‚)
141131, 140, 125addsubassd 11537 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ (((2 Β· 𝑦) + 3) βˆ’ 1) = ((2 Β· 𝑦) + (3 βˆ’ 1)))
142139, 141, 1293eqtr4d 2783 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (((2 Β· 𝑦) + 3) βˆ’ 1) = (2 Β· (𝑦 + 1)))
143142oveq1d 7373 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ ((((2 Β· 𝑦) + 3) βˆ’ 1) / ((2 Β· 𝑦) + 3)) = ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))
144143oveq1d 7373 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ (((((2 Β· 𝑦) + 3) βˆ’ 1) / ((2 Β· 𝑦) + 3)) Β· (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2))) = (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)) Β· (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2))))
145137, 144oveq12d 7376 . . . . . . . . 9 (𝑦 ∈ β„• β†’ (((((2 Β· (𝑦 + 1)) βˆ’ 1) / (2 Β· (𝑦 + 1))) Β· (πΌβ€˜(2 Β· 𝑦))) / (((((2 Β· 𝑦) + 3) βˆ’ 1) / ((2 Β· 𝑦) + 3)) Β· (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) Β· (πΌβ€˜(2 Β· 𝑦))) / (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)) Β· (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)))))
14640a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ 2 ∈ β„€)
147 nnz 12525 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ 𝑦 ∈ β„€)
148147peano2zd 12615 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (𝑦 + 1) ∈ β„€)
149146, 148zmulcld 12618 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ (2 Β· (𝑦 + 1)) ∈ β„€)
15066a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ 2 ∈ ℝ)
151 nnre 12165 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ 𝑦 ∈ ℝ)
152 1red 11161 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ 1 ∈ ℝ)
153151, 152readdcld 11189 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (𝑦 + 1) ∈ ℝ)
154 0le2 12260 . . . . . . . . . . . . . . 15 0 ≀ 2
155154a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ 0 ≀ 2)
156 nnnn0 12425 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ 𝑦 ∈ β„•0)
157156nn0ge0d 12481 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ 0 ≀ 𝑦)
158152, 151addge02d 11749 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ (0 ≀ 𝑦 ↔ 1 ≀ (𝑦 + 1)))
159157, 158mpbid 231 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ 1 ≀ (𝑦 + 1))
160150, 153, 155, 159lemulge11d 12097 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ 2 ≀ (2 Β· (𝑦 + 1)))
16140eluz1i 12776 . . . . . . . . . . . . 13 ((2 Β· (𝑦 + 1)) ∈ (β„€β‰₯β€˜2) ↔ ((2 Β· (𝑦 + 1)) ∈ β„€ ∧ 2 ≀ (2 Β· (𝑦 + 1))))
162149, 160, 161sylanbrc 584 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (2 Β· (𝑦 + 1)) ∈ (β„€β‰₯β€˜2))
16343, 162itgsinexp 44282 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (πΌβ€˜(2 Β· (𝑦 + 1))) = ((((2 Β· (𝑦 + 1)) βˆ’ 1) / (2 Β· (𝑦 + 1))) Β· (πΌβ€˜((2 Β· (𝑦 + 1)) βˆ’ 2))))
164129oveq1d 7373 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) βˆ’ 2) = (((2 Β· 𝑦) + 2) βˆ’ 2))
165131, 123pncand 11518 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (((2 Β· 𝑦) + 2) βˆ’ 2) = (2 Β· 𝑦))
166164, 165eqtrd 2773 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) βˆ’ 2) = (2 Β· 𝑦))
167166fveq2d 6847 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (πΌβ€˜((2 Β· (𝑦 + 1)) βˆ’ 2)) = (πΌβ€˜(2 Β· 𝑦)))
168167oveq2d 7374 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ ((((2 Β· (𝑦 + 1)) βˆ’ 1) / (2 Β· (𝑦 + 1))) Β· (πΌβ€˜((2 Β· (𝑦 + 1)) βˆ’ 2))) = ((((2 Β· (𝑦 + 1)) βˆ’ 1) / (2 Β· (𝑦 + 1))) Β· (πΌβ€˜(2 Β· 𝑦))))
169163, 168eqtrd 2773 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ (πΌβ€˜(2 Β· (𝑦 + 1))) = ((((2 Β· (𝑦 + 1)) βˆ’ 1) / (2 Β· (𝑦 + 1))) Β· (πΌβ€˜(2 Β· 𝑦))))
170129oveq1d 7373 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) + 1) = (((2 Β· 𝑦) + 2) + 1))
171131, 123, 125addassd 11182 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ (((2 Β· 𝑦) + 2) + 1) = ((2 Β· 𝑦) + (2 + 1)))
17236a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (2 + 1) = 3)
173172oveq2d 7374 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + (2 + 1)) = ((2 Β· 𝑦) + 3))
174170, 171, 1733eqtrd 2777 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) + 1) = ((2 Β· 𝑦) + 3))
175174fveq2d 6847 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (πΌβ€˜((2 Β· (𝑦 + 1)) + 1)) = (πΌβ€˜((2 Β· 𝑦) + 3)))
176146, 147zmulcld 12618 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (2 Β· 𝑦) ∈ β„€)
17765a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ 3 ∈ β„€)
178176, 177zaddcld 12616 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + 3) ∈ β„€)
179150, 151remulcld 11190 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (2 Β· 𝑦) ∈ ℝ)
18067a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ 3 ∈ ℝ)
181179, 180readdcld 11189 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + 3) ∈ ℝ)
182 nnge1 12186 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ 1 ≀ 𝑦)
183150, 151, 155, 182lemulge11d 12097 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ 2 ≀ (2 Β· 𝑦))
184 0re 11162 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
185 3pos 12263 . . . . . . . . . . . . . . . 16 0 < 3
186184, 67, 185ltleii 11283 . . . . . . . . . . . . . . 15 0 ≀ 3
187179, 180addge01d 11748 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ (0 ≀ 3 ↔ (2 Β· 𝑦) ≀ ((2 Β· 𝑦) + 3)))
188186, 187mpbii 232 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (2 Β· 𝑦) ≀ ((2 Β· 𝑦) + 3))
189150, 179, 181, 183, 188letrd 11317 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ 2 ≀ ((2 Β· 𝑦) + 3))
19040eluz1i 12776 . . . . . . . . . . . . 13 (((2 Β· 𝑦) + 3) ∈ (β„€β‰₯β€˜2) ↔ (((2 Β· 𝑦) + 3) ∈ β„€ ∧ 2 ≀ ((2 Β· 𝑦) + 3)))
191178, 189, 190sylanbrc 584 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + 3) ∈ (β„€β‰₯β€˜2))
19243, 191itgsinexp 44282 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (πΌβ€˜((2 Β· 𝑦) + 3)) = (((((2 Β· 𝑦) + 3) βˆ’ 1) / ((2 Β· 𝑦) + 3)) Β· (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2))))
193175, 192eqtrd 2773 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ (πΌβ€˜((2 Β· (𝑦 + 1)) + 1)) = (((((2 Β· 𝑦) + 3) βˆ’ 1) / ((2 Β· 𝑦) + 3)) Β· (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2))))
194169, 193oveq12d 7376 . . . . . . . . 9 (𝑦 ∈ β„• β†’ ((πΌβ€˜(2 Β· (𝑦 + 1))) / (πΌβ€˜((2 Β· (𝑦 + 1)) + 1))) = (((((2 Β· (𝑦 + 1)) βˆ’ 1) / (2 Β· (𝑦 + 1))) Β· (πΌβ€˜(2 Β· 𝑦))) / (((((2 Β· 𝑦) + 3) βˆ’ 1) / ((2 Β· 𝑦) + 3)) Β· (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)))))
195131, 125addcld 11179 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + 1) ∈ β„‚)
196124, 125addcld 11179 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (𝑦 + 1) ∈ β„‚)
197123, 196mulcld 11180 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (2 Β· (𝑦 + 1)) ∈ β„‚)
19860a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ 2 β‰  0)
199 peano2nn 12170 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ (𝑦 + 1) ∈ β„•)
200199nnne0d 12208 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (𝑦 + 1) β‰  0)
201123, 196, 198, 200mulne0d 11812 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (2 Β· (𝑦 + 1)) β‰  0)
202195, 197, 201divcld 11936 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ (((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) ∈ β„‚)
203 2nn0 12435 . . . . . . . . . . . . 13 2 ∈ β„•0
204203a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ 2 ∈ β„•0)
205204, 156nn0mulcld 12483 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (2 Β· 𝑦) ∈ β„•0)
20643wallispilem3 44394 . . . . . . . . . . . 12 ((2 Β· 𝑦) ∈ β„•0 β†’ (πΌβ€˜(2 Β· 𝑦)) ∈ ℝ+)
207206rpcnd 12964 . . . . . . . . . . 11 ((2 Β· 𝑦) ∈ β„•0 β†’ (πΌβ€˜(2 Β· 𝑦)) ∈ β„‚)
208205, 207syl 17 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ (πΌβ€˜(2 Β· 𝑦)) ∈ β„‚)
209131, 140addcld 11179 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + 3) ∈ β„‚)
210 0red 11163 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ 0 ∈ ℝ)
211 2pos 12261 . . . . . . . . . . . . . . . 16 0 < 2
212211a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ 0 < 2)
213 nngt0 12189 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ 0 < 𝑦)
214150, 151, 212, 213mulgt0d 11315 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ 0 < (2 Β· 𝑦))
215180, 185jctir 522 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ (3 ∈ ℝ ∧ 0 < 3))
216 elrp 12922 . . . . . . . . . . . . . . . 16 (3 ∈ ℝ+ ↔ (3 ∈ ℝ ∧ 0 < 3))
217215, 216sylibr 233 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ 3 ∈ ℝ+)
218179, 217ltaddrpd 12995 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (2 Β· 𝑦) < ((2 Β· 𝑦) + 3))
219210, 179, 181, 214, 218lttrd 11321 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ 0 < ((2 Β· 𝑦) + 3))
220219gt0ne0d 11724 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + 3) β‰  0)
221197, 209, 220divcld 11936 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)) ∈ β„‚)
222197, 209, 201, 220divne0d 11952 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)) β‰  0)
223178, 146zsubcld 12617 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (((2 Β· 𝑦) + 3) βˆ’ 2) ∈ β„€)
224181, 150subge0d 11750 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ (0 ≀ (((2 Β· 𝑦) + 3) βˆ’ 2) ↔ 2 ≀ ((2 Β· 𝑦) + 3)))
225189, 224mpbird 257 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ 0 ≀ (((2 Β· 𝑦) + 3) βˆ’ 2))
226 elnn0z 12517 . . . . . . . . . . . . . 14 ((((2 Β· 𝑦) + 3) βˆ’ 2) ∈ β„•0 ↔ ((((2 Β· 𝑦) + 3) βˆ’ 2) ∈ β„€ ∧ 0 ≀ (((2 Β· 𝑦) + 3) βˆ’ 2)))
227223, 225, 226sylanbrc 584 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ (((2 Β· 𝑦) + 3) βˆ’ 2) ∈ β„•0)
22843wallispilem3 44394 . . . . . . . . . . . . 13 ((((2 Β· 𝑦) + 3) βˆ’ 2) ∈ β„•0 β†’ (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)) ∈ ℝ+)
229227, 228syl 17 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)) ∈ ℝ+)
230229rpcnne0d 12971 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ ((πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)) ∈ β„‚ ∧ (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)) β‰  0))
231221, 222, 230jca31 516 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ ((((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)) ∈ β„‚ ∧ ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)) β‰  0) ∧ ((πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)) ∈ β„‚ ∧ (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)) β‰  0)))
232 divmuldiv 11860 . . . . . . . . . 10 ((((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) ∈ β„‚ ∧ (πΌβ€˜(2 Β· 𝑦)) ∈ β„‚) ∧ ((((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)) ∈ β„‚ ∧ ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)) β‰  0) ∧ ((πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)) ∈ β„‚ ∧ (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)) β‰  0))) β†’ (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) Β· (πΌβ€˜(2 Β· 𝑦))) / (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)) Β· (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)))))
233202, 208, 231, 232syl21anc 837 . . . . . . . . 9 (𝑦 ∈ β„• β†’ (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) Β· (πΌβ€˜(2 Β· 𝑦))) / (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)) Β· (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)))))
234145, 194, 2333eqtr4d 2783 . . . . . . . 8 (𝑦 ∈ β„• β†’ ((πΌβ€˜(2 Β· (𝑦 + 1))) / (πΌβ€˜((2 Β· (𝑦 + 1)) + 1))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)))))
235131, 140, 123addsubassd 11537 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (((2 Β· 𝑦) + 3) βˆ’ 2) = ((2 Β· 𝑦) + (3 βˆ’ 2)))
23679a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ (3 βˆ’ 2) = 1)
237236oveq2d 7374 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + (3 βˆ’ 2)) = ((2 Β· 𝑦) + 1))
238235, 237eqtrd 2773 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (((2 Β· 𝑦) + 3) βˆ’ 2) = ((2 Β· 𝑦) + 1))
239238fveq2d 6847 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)) = (πΌβ€˜((2 Β· 𝑦) + 1)))
240239oveq2d 7374 . . . . . . . . 9 (𝑦 ∈ β„• β†’ ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2))) = ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1))))
241240oveq2d 7374 . . . . . . . 8 (𝑦 ∈ β„• β†’ (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜(((2 Β· 𝑦) + 3) βˆ’ 2)))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1)))))
242234, 241eqtrd 2773 . . . . . . 7 (𝑦 ∈ β„• β†’ ((πΌβ€˜(2 Β· (𝑦 + 1))) / (πΌβ€˜((2 Β· (𝑦 + 1)) + 1))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1)))))
243242adantr 482 . . . . . 6 ((𝑦 ∈ β„• ∧ ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦)))) β†’ ((πΌβ€˜(2 Β· (𝑦 + 1))) / (πΌβ€˜((2 Β· (𝑦 + 1)) + 1))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1)))))
244 elnnuz 12812 . . . . . . . . . . . . 13 (𝑦 ∈ β„• ↔ 𝑦 ∈ (β„€β‰₯β€˜1))
245244biimpi 215 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ 𝑦 ∈ (β„€β‰₯β€˜1))
246 seqp1 13927 . . . . . . . . . . . 12 (𝑦 ∈ (β„€β‰₯β€˜1) β†’ (seq1( Β· , 𝐹)β€˜(𝑦 + 1)) = ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (πΉβ€˜(𝑦 + 1))))
247245, 246syl 17 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜(𝑦 + 1)) = ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (πΉβ€˜(𝑦 + 1))))
248 oveq2 7366 . . . . . . . . . . . . . . 15 (π‘˜ = (𝑦 + 1) β†’ (2 Β· π‘˜) = (2 Β· (𝑦 + 1)))
249248oveq1d 7373 . . . . . . . . . . . . . . 15 (π‘˜ = (𝑦 + 1) β†’ ((2 Β· π‘˜) βˆ’ 1) = ((2 Β· (𝑦 + 1)) βˆ’ 1))
250248, 249oveq12d 7376 . . . . . . . . . . . . . 14 (π‘˜ = (𝑦 + 1) β†’ ((2 Β· π‘˜) / ((2 Β· π‘˜) βˆ’ 1)) = ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)))
251248oveq1d 7373 . . . . . . . . . . . . . . 15 (π‘˜ = (𝑦 + 1) β†’ ((2 Β· π‘˜) + 1) = ((2 Β· (𝑦 + 1)) + 1))
252248, 251oveq12d 7376 . . . . . . . . . . . . . 14 (π‘˜ = (𝑦 + 1) β†’ ((2 Β· π‘˜) / ((2 Β· π‘˜) + 1)) = ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1)))
253250, 252oveq12d 7376 . . . . . . . . . . . . 13 (π‘˜ = (𝑦 + 1) β†’ (((2 Β· π‘˜) / ((2 Β· π‘˜) βˆ’ 1)) Β· ((2 Β· π‘˜) / ((2 Β· π‘˜) + 1))) = (((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1))))
254150, 153remulcld 11190 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ (2 Β· (𝑦 + 1)) ∈ ℝ)
255254, 152resubcld 11588 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) βˆ’ 1) ∈ ℝ)
256 1lt2 12329 . . . . . . . . . . . . . . . . . . 19 1 < 2
257256a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ β„• β†’ 1 < 2)
258 nnrp 12931 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ β„• β†’ 𝑦 ∈ ℝ+)
259152, 258ltaddrp2d 12996 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ β„• β†’ 1 < (𝑦 + 1))
260150, 153, 257, 259mulgt1d 12096 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ β„• β†’ 1 < (2 Β· (𝑦 + 1)))
261152, 260gtned 11295 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ (2 Β· (𝑦 + 1)) β‰  1)
262197, 125, 261subne0d 11526 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) βˆ’ 1) β‰  0)
263254, 255, 262redivcld 11988 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) ∈ ℝ)
264174, 181eqeltrd 2834 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) + 1) ∈ ℝ)
265174, 220eqnetrd 3008 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) + 1) β‰  0)
266254, 264, 265redivcld 11988 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1)) ∈ ℝ)
267263, 266remulcld 11190 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ (((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1))) ∈ ℝ)
268106, 253, 199, 267fvmptd3 6972 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (πΉβ€˜(𝑦 + 1)) = (((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1))))
269268oveq2d 7374 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (πΉβ€˜(𝑦 + 1))) = ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1)))))
270247, 269eqtrd 2773 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜(𝑦 + 1)) = ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1)))))
271270oveq2d 7374 . . . . . . . . 9 (𝑦 ∈ β„• β†’ (1 / (seq1( Β· , 𝐹)β€˜(𝑦 + 1))) = (1 / ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1))))))
272271oveq2d 7374 . . . . . . . 8 (𝑦 ∈ β„• β†’ ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜(𝑦 + 1)))) = ((Ο€ / 2) Β· (1 / ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1)))))))
273135oveq2d 7374 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) = ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)))
274174oveq2d 7374 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1)) = ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))
275273, 274oveq12d 7376 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1))) = (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))))
276275oveq2d 7374 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1)))) = ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))))
277276oveq2d 7374 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ (1 / ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1))))) = (1 / ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))))))
278277oveq2d 7374 . . . . . . . . 9 (𝑦 ∈ β„• β†’ ((Ο€ / 2) Β· (1 / ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1)))))) = ((Ο€ / 2) Β· (1 / ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))))))
279 elfznn 13476 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (1...𝑦) β†’ 𝑀 ∈ β„•)
280279adantl 483 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ β„• ∧ 𝑀 ∈ (1...𝑦)) β†’ 𝑀 ∈ β„•)
281 oveq2 7366 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = 𝑀 β†’ (2 Β· π‘˜) = (2 Β· 𝑀))
282281oveq1d 7373 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = 𝑀 β†’ ((2 Β· π‘˜) βˆ’ 1) = ((2 Β· 𝑀) βˆ’ 1))
283281, 282oveq12d 7376 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑀 β†’ ((2 Β· π‘˜) / ((2 Β· π‘˜) βˆ’ 1)) = ((2 Β· 𝑀) / ((2 Β· 𝑀) βˆ’ 1)))
284281oveq1d 7373 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = 𝑀 β†’ ((2 Β· π‘˜) + 1) = ((2 Β· 𝑀) + 1))
285281, 284oveq12d 7376 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑀 β†’ ((2 Β· π‘˜) / ((2 Β· π‘˜) + 1)) = ((2 Β· 𝑀) / ((2 Β· 𝑀) + 1)))
286283, 285oveq12d 7376 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑀 β†’ (((2 Β· π‘˜) / ((2 Β· π‘˜) βˆ’ 1)) Β· ((2 Β· π‘˜) / ((2 Β· π‘˜) + 1))) = (((2 Β· 𝑀) / ((2 Β· 𝑀) βˆ’ 1)) Β· ((2 Β· 𝑀) / ((2 Β· 𝑀) + 1))))
287 id 22 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ β„• β†’ 𝑀 ∈ β„•)
288 2rp 12925 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℝ+
289288a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ β„• β†’ 2 ∈ ℝ+)
290 nnrp 12931 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ β„• β†’ 𝑀 ∈ ℝ+)
291289, 290rpmulcld 12978 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ β„• β†’ (2 Β· 𝑀) ∈ ℝ+)
29266a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ β„• β†’ 2 ∈ ℝ)
293 nnre 12165 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ β„• β†’ 𝑀 ∈ ℝ)
294292, 293remulcld 11190 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ β„• β†’ (2 Β· 𝑀) ∈ ℝ)
295 1red 11161 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ β„• β†’ 1 ∈ ℝ)
296294, 295resubcld 11588 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ β„• β†’ ((2 Β· 𝑀) βˆ’ 1) ∈ ℝ)
297 nnge1 12186 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ β„• β†’ 1 ≀ 𝑀)
298 nncn 12166 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ β„• β†’ 𝑀 ∈ β„‚)
299298mulid2d 11178 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 ∈ β„• β†’ (1 Β· 𝑀) = 𝑀)
300295, 292, 290ltmul1d 13003 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ β„• β†’ (1 < 2 ↔ (1 Β· 𝑀) < (2 Β· 𝑀)))
301256, 300mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 ∈ β„• β†’ (1 Β· 𝑀) < (2 Β· 𝑀))
302299, 301eqbrtrrd 5130 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ β„• β†’ 𝑀 < (2 Β· 𝑀))
303295, 293, 294, 297, 302lelttrd 11318 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ β„• β†’ 1 < (2 Β· 𝑀))
304295, 294posdifd 11747 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ β„• β†’ (1 < (2 Β· 𝑀) ↔ 0 < ((2 Β· 𝑀) βˆ’ 1)))
305303, 304mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ β„• β†’ 0 < ((2 Β· 𝑀) βˆ’ 1))
306296, 305elrpd 12959 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ β„• β†’ ((2 Β· 𝑀) βˆ’ 1) ∈ ℝ+)
307291, 306rpdivcld 12979 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ β„• β†’ ((2 Β· 𝑀) / ((2 Β· 𝑀) βˆ’ 1)) ∈ ℝ+)
308154a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ β„• β†’ 0 ≀ 2)
309290rpge0d 12966 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ β„• β†’ 0 ≀ 𝑀)
310292, 293, 308, 309mulge0d 11737 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ β„• β†’ 0 ≀ (2 Β· 𝑀))
311294, 310ge0p1rpd 12992 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ β„• β†’ ((2 Β· 𝑀) + 1) ∈ ℝ+)
312291, 311rpdivcld 12979 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ β„• β†’ ((2 Β· 𝑀) / ((2 Β· 𝑀) + 1)) ∈ ℝ+)
313307, 312rpmulcld 12978 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ β„• β†’ (((2 Β· 𝑀) / ((2 Β· 𝑀) βˆ’ 1)) Β· ((2 Β· 𝑀) / ((2 Β· 𝑀) + 1))) ∈ ℝ+)
314106, 286, 287, 313fvmptd3 6972 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ β„• β†’ (πΉβ€˜π‘€) = (((2 Β· 𝑀) / ((2 Β· 𝑀) βˆ’ 1)) Β· ((2 Β· 𝑀) / ((2 Β· 𝑀) + 1))))
315314, 313eqeltrd 2834 . . . . . . . . . . . . . . . 16 (𝑀 ∈ β„• β†’ (πΉβ€˜π‘€) ∈ ℝ+)
316280, 315syl 17 . . . . . . . . . . . . . . 15 ((𝑦 ∈ β„• ∧ 𝑀 ∈ (1...𝑦)) β†’ (πΉβ€˜π‘€) ∈ ℝ+)
317 rpmulcl 12943 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+) β†’ (𝑀 Β· 𝑧) ∈ ℝ+)
318317adantl 483 . . . . . . . . . . . . . . 15 ((𝑦 ∈ β„• ∧ (𝑀 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) β†’ (𝑀 Β· 𝑧) ∈ ℝ+)
319245, 316, 318seqcl 13934 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜π‘¦) ∈ ℝ+)
320319rpcnne0d 12971 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((seq1( Β· , 𝐹)β€˜π‘¦) ∈ β„‚ ∧ (seq1( Β· , 𝐹)β€˜π‘¦) β‰  0))
321288a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ β„• β†’ 2 ∈ ℝ+)
322151, 157ge0p1rpd 12992 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ β„• β†’ (𝑦 + 1) ∈ ℝ+)
323321, 322rpmulcld 12978 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ (2 Β· (𝑦 + 1)) ∈ ℝ+)
324150, 151, 155, 157mulge0d 11737 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ β„• β†’ 0 ≀ (2 Β· 𝑦))
325179, 324ge0p1rpd 12992 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + 1) ∈ ℝ+)
326323, 325rpdivcld 12979 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) ∈ ℝ+)
327321, 258rpmulcld 12978 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ β„• β†’ (2 Β· 𝑦) ∈ ℝ+)
328327, 217rpaddcld 12977 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + 3) ∈ ℝ+)
329323, 328rpdivcld 12979 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)) ∈ ℝ+)
330326, 329rpmulcld 12978 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) ∈ ℝ+)
331330rpcnne0d 12971 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) ∈ β„‚ ∧ (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) β‰  0))
332 divdiv1 11871 . . . . . . . . . . . . 13 ((1 ∈ β„‚ ∧ ((seq1( Β· , 𝐹)β€˜π‘¦) ∈ β„‚ ∧ (seq1( Β· , 𝐹)β€˜π‘¦) β‰  0) ∧ ((((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) ∈ β„‚ ∧ (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) β‰  0)) β†’ ((1 / (seq1( Β· , 𝐹)β€˜π‘¦)) / (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))) = (1 / ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))))))
333125, 320, 331, 332syl3anc 1372 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ ((1 / (seq1( Β· , 𝐹)β€˜π‘¦)) / (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))) = (1 / ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))))))
334333eqcomd 2739 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (1 / ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))))) = ((1 / (seq1( Β· , 𝐹)β€˜π‘¦)) / (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))))
335334oveq2d 7374 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ ((Ο€ / 2) Β· (1 / ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))))) = ((Ο€ / 2) Β· ((1 / (seq1( Β· , 𝐹)β€˜π‘¦)) / (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))))))
33661a1i 11 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (Ο€ / 2) ∈ β„‚)
337319rpcnd 12964 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜π‘¦) ∈ β„‚)
338319rpne0d 12967 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜π‘¦) β‰  0)
339337, 338reccld 11929 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (1 / (seq1( Β· , 𝐹)β€˜π‘¦)) ∈ β„‚)
340330rpcnd 12964 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) ∈ β„‚)
341330rpne0d 12967 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) β‰  0)
342336, 339, 340, 341divassd 11971 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) / (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))) = ((Ο€ / 2) Β· ((1 / (seq1( Β· , 𝐹)β€˜π‘¦)) / (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))))))
343135, 262eqnetrrd 3009 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((2 Β· 𝑦) + 1) β‰  0)
344197, 195, 197, 209, 343, 220divmuldivd 11977 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) = (((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1))) / (((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3))))
345344oveq2d 7374 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) / (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))) = (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) / (((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1))) / (((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3)))))
346336, 339mulcld 11180 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) ∈ β„‚)
347197, 197mulcld 11180 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1))) ∈ β„‚)
348195, 209mulcld 11180 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ (((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3)) ∈ β„‚)
349197, 197, 201, 201mulne0d 11812 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1))) β‰  0)
350195, 209, 343, 220mulne0d 11812 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ (((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3)) β‰  0)
351346, 347, 348, 349, 350divdiv2d 11968 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) / (((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1))) / (((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3)))) = ((((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) Β· (((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3))) / ((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1)))))
352346, 348, 347, 349divassd 11971 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ ((((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) Β· (((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3))) / ((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1)))) = (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) Β· ((((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3)) / ((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1))))))
353351, 352eqtrd 2773 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) / (((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1))) / (((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3)))) = (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) Β· ((((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3)) / ((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1))))))
354195, 197, 197, 209, 201, 220, 201divdivdivd 11983 . . . . . . . . . . . . 13 (𝑦 ∈ β„• β†’ ((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) = ((((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3)) / ((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1)))))
355354eqcomd 2739 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ ((((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3)) / ((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1)))) = ((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))))
356355oveq2d 7374 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) Β· ((((2 Β· 𝑦) + 1) Β· ((2 Β· 𝑦) + 3)) / ((2 Β· (𝑦 + 1)) Β· (2 Β· (𝑦 + 1))))) = (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) Β· ((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))))
357345, 353, 3563eqtrd 2777 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) / (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))) = (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) Β· ((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))))
358335, 342, 3573eqtr2d 2779 . . . . . . . . 9 (𝑦 ∈ β„• β†’ ((Ο€ / 2) Β· (1 / ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))))) = (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) Β· ((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))))
35957a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ β„• β†’ Ο€ ∈ β„‚)
360359halfcld 12403 . . . . . . . . . . 11 (𝑦 ∈ β„• β†’ (Ο€ / 2) ∈ β„‚)
361360, 339mulcld 11180 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) ∈ β„‚)
362202, 221, 222divcld 11936 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ ((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) ∈ β„‚)
363361, 362mulcomd 11181 . . . . . . . . 9 (𝑦 ∈ β„• β†’ (((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) Β· ((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3)))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦)))))
364278, 358, 3633eqtrd 2777 . . . . . . . 8 (𝑦 ∈ β„• β†’ ((Ο€ / 2) Β· (1 / ((seq1( Β· , 𝐹)β€˜π‘¦) Β· (((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) βˆ’ 1)) Β· ((2 Β· (𝑦 + 1)) / ((2 Β· (𝑦 + 1)) + 1)))))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦)))))
365272, 364eqtrd 2773 . . . . . . 7 (𝑦 ∈ β„• β†’ ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜(𝑦 + 1)))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦)))))
366365adantr 482 . . . . . 6 ((𝑦 ∈ β„• ∧ ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦)))) β†’ ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜(𝑦 + 1)))) = (((((2 Β· 𝑦) + 1) / (2 Β· (𝑦 + 1))) / ((2 Β· (𝑦 + 1)) / ((2 Β· 𝑦) + 3))) Β· ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦)))))
367122, 243, 3663eqtr4d 2783 . . . . 5 ((𝑦 ∈ β„• ∧ ((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦)))) β†’ ((πΌβ€˜(2 Β· (𝑦 + 1))) / (πΌβ€˜((2 Β· (𝑦 + 1)) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜(𝑦 + 1)))))
368367ex 414 . . . 4 (𝑦 ∈ β„• β†’ (((πΌβ€˜(2 Β· 𝑦)) / (πΌβ€˜((2 Β· 𝑦) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘¦))) β†’ ((πΌβ€˜(2 Β· (𝑦 + 1))) / (πΌβ€˜((2 Β· (𝑦 + 1)) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜(𝑦 + 1))))))
3698, 16, 24, 32, 120, 368nnind 12176 . . 3 (𝑛 ∈ β„• β†’ ((πΌβ€˜(2 Β· 𝑛)) / (πΌβ€˜((2 Β· 𝑛) + 1))) = ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘›))))
370369mpteq2ia 5209 . 2 (𝑛 ∈ β„• ↦ ((πΌβ€˜(2 Β· 𝑛)) / (πΌβ€˜((2 Β· 𝑛) + 1)))) = (𝑛 ∈ β„• ↦ ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘›))))
371 wallispilem4.3 . 2 𝐺 = (𝑛 ∈ β„• ↦ ((πΌβ€˜(2 Β· 𝑛)) / (πΌβ€˜((2 Β· 𝑛) + 1))))
372 wallispilem4.4 . 2 𝐻 = (𝑛 ∈ β„• ↦ ((Ο€ / 2) Β· (1 / (seq1( Β· , 𝐹)β€˜π‘›))))
373370, 371, 3723eqtr4i 2771 1 𝐺 = 𝐻
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2940   class class class wbr 5106   ↦ cmpt 5189  β€˜cfv 6497  (class class class)co 7358  β„‚cc 11054  β„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   Β· cmul 11061   < clt 11194   ≀ cle 11195   βˆ’ cmin 11390   / cdiv 11817  β„•cn 12158  2c2 12213  3c3 12214  β„•0cn0 12418  β„€cz 12504  β„€β‰₯cuz 12768  β„+crp 12920  (,)cioo 13270  ...cfz 13430  seqcseq 13912  β†‘cexp 13973  sincsin 15951  Ο€cpi 15954  βˆ«citg 24998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cc 10376  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-addf 11135  ax-mulf 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-symdif 4203  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-disj 5072  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-ofr 7619  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-omul 8418  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-fi 9352  df-sup 9383  df-inf 9384  df-oi 9451  df-dju 9842  df-card 9880  df-acn 9883  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-z 12505  df-dec 12624  df-uz 12769  df-q 12879  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13274  df-ioc 13275  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-fac 14180  df-bc 14209  df-hash 14237  df-shft 14958  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-limsup 15359  df-clim 15376  df-rlim 15377  df-sum 15577  df-ef 15955  df-sin 15957  df-cos 15958  df-pi 15960  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-rest 17309  df-topn 17310  df-0g 17328  df-gsum 17329  df-topgen 17330  df-pt 17331  df-prds 17334  df-xrs 17389  df-qtop 17394  df-imas 17395  df-xps 17397  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-submnd 18607  df-mulg 18878  df-cntz 19102  df-cmn 19569  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-ovol 24844  df-vol 24845  df-mbf 24999  df-itg1 25000  df-itg2 25001  df-ibl 25002  df-itg 25003  df-0p 25050  df-limc 25246  df-dv 25247
This theorem is referenced by:  wallispilem5  44396
  Copyright terms: Public domain W3C validator