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

Theorem wallispi2lem1 44774
Description: An intermediate step between the first version of the Wallis' formula for ฯ€ and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
Assertion
Ref Expression
wallispi2lem1 (๐‘ โˆˆ โ„• โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘) = ((1 / ((2 ยท ๐‘) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘)))

Proof of Theorem wallispi2lem1
Dummy variables ๐‘ค ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6889 . . 3 (๐‘ฅ = 1 โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฅ) = (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜1))
2 oveq2 7414 . . . . . 6 (๐‘ฅ = 1 โ†’ (2 ยท ๐‘ฅ) = (2 ยท 1))
32oveq1d 7421 . . . . 5 (๐‘ฅ = 1 โ†’ ((2 ยท ๐‘ฅ) + 1) = ((2 ยท 1) + 1))
43oveq2d 7422 . . . 4 (๐‘ฅ = 1 โ†’ (1 / ((2 ยท ๐‘ฅ) + 1)) = (1 / ((2 ยท 1) + 1)))
5 fveq2 6889 . . . 4 (๐‘ฅ = 1 โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฅ) = (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜1))
64, 5oveq12d 7424 . . 3 (๐‘ฅ = 1 โ†’ ((1 / ((2 ยท ๐‘ฅ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฅ)) = ((1 / ((2 ยท 1) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜1)))
71, 6eqeq12d 2749 . 2 (๐‘ฅ = 1 โ†’ ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฅ) = ((1 / ((2 ยท ๐‘ฅ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฅ)) โ†” (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜1) = ((1 / ((2 ยท 1) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜1))))
8 fveq2 6889 . . 3 (๐‘ฅ = ๐‘ฆ โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฅ) = (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ))
9 oveq2 7414 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ (2 ยท ๐‘ฅ) = (2 ยท ๐‘ฆ))
109oveq1d 7421 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ ((2 ยท ๐‘ฅ) + 1) = ((2 ยท ๐‘ฆ) + 1))
1110oveq2d 7422 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ (1 / ((2 ยท ๐‘ฅ) + 1)) = (1 / ((2 ยท ๐‘ฆ) + 1)))
12 fveq2 6889 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฅ) = (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ))
1311, 12oveq12d 7424 . . 3 (๐‘ฅ = ๐‘ฆ โ†’ ((1 / ((2 ยท ๐‘ฅ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฅ)) = ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)))
148, 13eqeq12d 2749 . 2 (๐‘ฅ = ๐‘ฆ โ†’ ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฅ) = ((1 / ((2 ยท ๐‘ฅ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฅ)) โ†” (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ) = ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ))))
15 fveq2 6889 . . 3 (๐‘ฅ = (๐‘ฆ + 1) โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฅ) = (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜(๐‘ฆ + 1)))
16 oveq2 7414 . . . . . 6 (๐‘ฅ = (๐‘ฆ + 1) โ†’ (2 ยท ๐‘ฅ) = (2 ยท (๐‘ฆ + 1)))
1716oveq1d 7421 . . . . 5 (๐‘ฅ = (๐‘ฆ + 1) โ†’ ((2 ยท ๐‘ฅ) + 1) = ((2 ยท (๐‘ฆ + 1)) + 1))
1817oveq2d 7422 . . . 4 (๐‘ฅ = (๐‘ฆ + 1) โ†’ (1 / ((2 ยท ๐‘ฅ) + 1)) = (1 / ((2 ยท (๐‘ฆ + 1)) + 1)))
19 fveq2 6889 . . . 4 (๐‘ฅ = (๐‘ฆ + 1) โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฅ) = (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜(๐‘ฆ + 1)))
2018, 19oveq12d 7424 . . 3 (๐‘ฅ = (๐‘ฆ + 1) โ†’ ((1 / ((2 ยท ๐‘ฅ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฅ)) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜(๐‘ฆ + 1))))
2115, 20eqeq12d 2749 . 2 (๐‘ฅ = (๐‘ฆ + 1) โ†’ ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฅ) = ((1 / ((2 ยท ๐‘ฅ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฅ)) โ†” (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜(๐‘ฆ + 1)) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜(๐‘ฆ + 1)))))
22 fveq2 6889 . . 3 (๐‘ฅ = ๐‘ โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฅ) = (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘))
23 oveq2 7414 . . . . . 6 (๐‘ฅ = ๐‘ โ†’ (2 ยท ๐‘ฅ) = (2 ยท ๐‘))
2423oveq1d 7421 . . . . 5 (๐‘ฅ = ๐‘ โ†’ ((2 ยท ๐‘ฅ) + 1) = ((2 ยท ๐‘) + 1))
2524oveq2d 7422 . . . 4 (๐‘ฅ = ๐‘ โ†’ (1 / ((2 ยท ๐‘ฅ) + 1)) = (1 / ((2 ยท ๐‘) + 1)))
26 fveq2 6889 . . . 4 (๐‘ฅ = ๐‘ โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฅ) = (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘))
2725, 26oveq12d 7424 . . 3 (๐‘ฅ = ๐‘ โ†’ ((1 / ((2 ยท ๐‘ฅ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฅ)) = ((1 / ((2 ยท ๐‘) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘)))
2822, 27eqeq12d 2749 . 2 (๐‘ฅ = ๐‘ โ†’ ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฅ) = ((1 / ((2 ยท ๐‘ฅ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฅ)) โ†” (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘) = ((1 / ((2 ยท ๐‘) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘))))
29 1z 12589 . . . 4 1 โˆˆ โ„ค
30 seq1 13976 . . . 4 (1 โˆˆ โ„ค โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜1) = ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜1))
3129, 30ax-mp 5 . . 3 (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜1) = ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜1)
32 1nn 12220 . . . 4 1 โˆˆ โ„•
33 oveq2 7414 . . . . . . 7 (๐‘˜ = 1 โ†’ (2 ยท ๐‘˜) = (2 ยท 1))
3433oveq1d 7421 . . . . . . 7 (๐‘˜ = 1 โ†’ ((2 ยท ๐‘˜) โˆ’ 1) = ((2 ยท 1) โˆ’ 1))
3533, 34oveq12d 7424 . . . . . 6 (๐‘˜ = 1 โ†’ ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) = ((2 ยท 1) / ((2 ยท 1) โˆ’ 1)))
3633oveq1d 7421 . . . . . . 7 (๐‘˜ = 1 โ†’ ((2 ยท ๐‘˜) + 1) = ((2 ยท 1) + 1))
3733, 36oveq12d 7424 . . . . . 6 (๐‘˜ = 1 โ†’ ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)) = ((2 ยท 1) / ((2 ยท 1) + 1)))
3835, 37oveq12d 7424 . . . . 5 (๐‘˜ = 1 โ†’ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))) = (((2 ยท 1) / ((2 ยท 1) โˆ’ 1)) ยท ((2 ยท 1) / ((2 ยท 1) + 1))))
39 eqid 2733 . . . . 5 (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))) = (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))
40 ovex 7439 . . . . 5 (((2 ยท 1) / ((2 ยท 1) โˆ’ 1)) ยท ((2 ยท 1) / ((2 ยท 1) + 1))) โˆˆ V
4138, 39, 40fvmpt 6996 . . . 4 (1 โˆˆ โ„• โ†’ ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜1) = (((2 ยท 1) / ((2 ยท 1) โˆ’ 1)) ยท ((2 ยท 1) / ((2 ยท 1) + 1))))
4232, 41ax-mp 5 . . 3 ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜1) = (((2 ยท 1) / ((2 ยท 1) โˆ’ 1)) ยท ((2 ยท 1) / ((2 ยท 1) + 1)))
43 2t1e2 12372 . . . . . . 7 (2 ยท 1) = 2
4443oveq1i 7416 . . . . . . . 8 ((2 ยท 1) โˆ’ 1) = (2 โˆ’ 1)
45 2m1e1 12335 . . . . . . . 8 (2 โˆ’ 1) = 1
4644, 45eqtri 2761 . . . . . . 7 ((2 ยท 1) โˆ’ 1) = 1
4743, 46oveq12i 7418 . . . . . 6 ((2 ยท 1) / ((2 ยท 1) โˆ’ 1)) = (2 / 1)
4843oveq1i 7416 . . . . . . . 8 ((2 ยท 1) + 1) = (2 + 1)
49 2p1e3 12351 . . . . . . . 8 (2 + 1) = 3
5048, 49eqtri 2761 . . . . . . 7 ((2 ยท 1) + 1) = 3
5143, 50oveq12i 7418 . . . . . 6 ((2 ยท 1) / ((2 ยท 1) + 1)) = (2 / 3)
5247, 51oveq12i 7418 . . . . 5 (((2 ยท 1) / ((2 ยท 1) โˆ’ 1)) ยท ((2 ยท 1) / ((2 ยท 1) + 1))) = ((2 / 1) ยท (2 / 3))
53 2cn 12284 . . . . . 6 2 โˆˆ โ„‚
54 ax-1cn 11165 . . . . . 6 1 โˆˆ โ„‚
55 3cn 12290 . . . . . 6 3 โˆˆ โ„‚
56 ax-1ne0 11176 . . . . . 6 1 โ‰  0
57 3ne0 12315 . . . . . 6 3 โ‰  0
5853, 54, 53, 55, 56, 57divmuldivi 11971 . . . . 5 ((2 / 1) ยท (2 / 3)) = ((2 ยท 2) / (1 ยท 3))
59 2t2e4 12373 . . . . . 6 (2 ยท 2) = 4
6055mullidi 11216 . . . . . 6 (1 ยท 3) = 3
6159, 60oveq12i 7418 . . . . 5 ((2 ยท 2) / (1 ยท 3)) = (4 / 3)
6252, 58, 613eqtri 2765 . . . 4 (((2 ยท 1) / ((2 ยท 1) โˆ’ 1)) ยท ((2 ยท 1) / ((2 ยท 1) + 1))) = (4 / 3)
63 4cn 12294 . . . . 5 4 โˆˆ โ„‚
64 divrec2 11886 . . . . 5 ((4 โˆˆ โ„‚ โˆง 3 โˆˆ โ„‚ โˆง 3 โ‰  0) โ†’ (4 / 3) = ((1 / 3) ยท 4))
6563, 55, 57, 64mp3an 1462 . . . 4 (4 / 3) = ((1 / 3) ยท 4)
6650eqcomi 2742 . . . . . 6 3 = ((2 ยท 1) + 1)
6766oveq2i 7417 . . . . 5 (1 / 3) = (1 / ((2 ยท 1) + 1))
68 seq1 13976 . . . . . . . 8 (1 โˆˆ โ„ค โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜1) = ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜1))
6929, 68ax-mp 5 . . . . . . 7 (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜1) = ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜1)
7033oveq1d 7421 . . . . . . . . . 10 (๐‘˜ = 1 โ†’ ((2 ยท ๐‘˜)โ†‘4) = ((2 ยท 1)โ†‘4))
7133, 34oveq12d 7424 . . . . . . . . . . 11 (๐‘˜ = 1 โ†’ ((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1)) = ((2 ยท 1) ยท ((2 ยท 1) โˆ’ 1)))
7271oveq1d 7421 . . . . . . . . . 10 (๐‘˜ = 1 โ†’ (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2) = (((2 ยท 1) ยท ((2 ยท 1) โˆ’ 1))โ†‘2))
7370, 72oveq12d 7424 . . . . . . . . 9 (๐‘˜ = 1 โ†’ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)) = (((2 ยท 1)โ†‘4) / (((2 ยท 1) ยท ((2 ยท 1) โˆ’ 1))โ†‘2)))
74 eqid 2733 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))) = (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))
75 ovex 7439 . . . . . . . . 9 (((2 ยท 1)โ†‘4) / (((2 ยท 1) ยท ((2 ยท 1) โˆ’ 1))โ†‘2)) โˆˆ V
7673, 74, 75fvmpt 6996 . . . . . . . 8 (1 โˆˆ โ„• โ†’ ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜1) = (((2 ยท 1)โ†‘4) / (((2 ยท 1) ยท ((2 ยท 1) โˆ’ 1))โ†‘2)))
7732, 76ax-mp 5 . . . . . . 7 ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜1) = (((2 ยท 1)โ†‘4) / (((2 ยท 1) ยท ((2 ยท 1) โˆ’ 1))โ†‘2))
7843oveq1i 7416 . . . . . . . . 9 ((2 ยท 1)โ†‘4) = (2โ†‘4)
7943, 46oveq12i 7418 . . . . . . . . . . 11 ((2 ยท 1) ยท ((2 ยท 1) โˆ’ 1)) = (2 ยท 1)
8079, 43eqtri 2761 . . . . . . . . . 10 ((2 ยท 1) ยท ((2 ยท 1) โˆ’ 1)) = 2
8180oveq1i 7416 . . . . . . . . 9 (((2 ยท 1) ยท ((2 ยท 1) โˆ’ 1))โ†‘2) = (2โ†‘2)
8278, 81oveq12i 7418 . . . . . . . 8 (((2 ยท 1)โ†‘4) / (((2 ยท 1) ยท ((2 ยท 1) โˆ’ 1))โ†‘2)) = ((2โ†‘4) / (2โ†‘2))
83 2exp4 17015 . . . . . . . . . 10 (2โ†‘4) = 16
84 sq2 14158 . . . . . . . . . 10 (2โ†‘2) = 4
8583, 84oveq12i 7418 . . . . . . . . 9 ((2โ†‘4) / (2โ†‘2)) = (16 / 4)
86 4t4e16 12773 . . . . . . . . . . 11 (4 ยท 4) = 16
8786eqcomi 2742 . . . . . . . . . 10 16 = (4 ยท 4)
8887oveq1i 7416 . . . . . . . . 9 (16 / 4) = ((4 ยท 4) / 4)
89 4ne0 12317 . . . . . . . . . 10 4 โ‰  0
9063, 63, 89divcan3i 11957 . . . . . . . . 9 ((4 ยท 4) / 4) = 4
9185, 88, 903eqtri 2765 . . . . . . . 8 ((2โ†‘4) / (2โ†‘2)) = 4
9282, 91eqtri 2761 . . . . . . 7 (((2 ยท 1)โ†‘4) / (((2 ยท 1) ยท ((2 ยท 1) โˆ’ 1))โ†‘2)) = 4
9369, 77, 923eqtri 2765 . . . . . 6 (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜1) = 4
9493eqcomi 2742 . . . . 5 4 = (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜1)
9567, 94oveq12i 7418 . . . 4 ((1 / 3) ยท 4) = ((1 / ((2 ยท 1) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜1))
9662, 65, 953eqtri 2765 . . 3 (((2 ยท 1) / ((2 ยท 1) โˆ’ 1)) ยท ((2 ยท 1) / ((2 ยท 1) + 1))) = ((1 / ((2 ยท 1) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜1))
9731, 42, 963eqtri 2765 . 2 (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜1) = ((1 / ((2 ยท 1) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜1))
98 elnnuz 12863 . . . . . . 7 (๐‘ฆ โˆˆ โ„• โ†” ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜1))
9998biimpi 215 . . . . . 6 (๐‘ฆ โˆˆ โ„• โ†’ ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜1))
10099adantr 482 . . . . 5 ((๐‘ฆ โˆˆ โ„• โˆง (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ) = ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ))) โ†’ ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜1))
101 seqp1 13978 . . . . 5 (๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜(๐‘ฆ + 1)) = ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜(๐‘ฆ + 1))))
102100, 101syl 17 . . . 4 ((๐‘ฆ โˆˆ โ„• โˆง (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ) = ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ))) โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜(๐‘ฆ + 1)) = ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜(๐‘ฆ + 1))))
103 simpr 486 . . . . 5 ((๐‘ฆ โˆˆ โ„• โˆง (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ) = ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ))) โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ) = ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)))
104103oveq1d 7421 . . . 4 ((๐‘ฆ โˆˆ โ„• โˆง (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ) = ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ))) โ†’ ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜(๐‘ฆ + 1))) = (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜(๐‘ฆ + 1))))
105 eqidd 2734 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))) = (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))
106 oveq2 7414 . . . . . . . . . . . 12 (๐‘˜ = (๐‘ฆ + 1) โ†’ (2 ยท ๐‘˜) = (2 ยท (๐‘ฆ + 1)))
107106oveq1d 7421 . . . . . . . . . . . 12 (๐‘˜ = (๐‘ฆ + 1) โ†’ ((2 ยท ๐‘˜) โˆ’ 1) = ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))
108106, 107oveq12d 7424 . . . . . . . . . . 11 (๐‘˜ = (๐‘ฆ + 1) โ†’ ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) = ((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)))
109106oveq1d 7421 . . . . . . . . . . . 12 (๐‘˜ = (๐‘ฆ + 1) โ†’ ((2 ยท ๐‘˜) + 1) = ((2 ยท (๐‘ฆ + 1)) + 1))
110106, 109oveq12d 7424 . . . . . . . . . . 11 (๐‘˜ = (๐‘ฆ + 1) โ†’ ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)) = ((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) + 1)))
111108, 110oveq12d 7424 . . . . . . . . . 10 (๐‘˜ = (๐‘ฆ + 1) โ†’ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))) = (((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) ยท ((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) + 1))))
112111adantl 483 . . . . . . . . 9 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘˜ = (๐‘ฆ + 1)) โ†’ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))) = (((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) ยท ((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) + 1))))
113 peano2nn 12221 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘ฆ + 1) โˆˆ โ„•)
114 2rp 12976 . . . . . . . . . . . . 13 2 โˆˆ โ„+
115114a1i 11 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ 2 โˆˆ โ„+)
116 nnre 12216 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ ๐‘ฆ โˆˆ โ„)
117 nnnn0 12476 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ ๐‘ฆ โˆˆ โ„•0)
118117nn0ge0d 12532 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ 0 โ‰ค ๐‘ฆ)
119116, 118ge0p1rpd 13043 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘ฆ + 1) โˆˆ โ„+)
120115, 119rpmulcld 13029 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„• โ†’ (2 ยท (๐‘ฆ + 1)) โˆˆ โ„+)
121 2re 12283 . . . . . . . . . . . . . . 15 2 โˆˆ โ„
122121a1i 11 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ 2 โˆˆ โ„)
123 1red 11212 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„• โ†’ 1 โˆˆ โ„)
124116, 123readdcld 11240 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘ฆ + 1) โˆˆ โ„)
125122, 124remulcld 11241 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ (2 ยท (๐‘ฆ + 1)) โˆˆ โ„)
126125, 123resubcld 11639 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) โˆ’ 1) โˆˆ โ„)
127 1lt2 12380 . . . . . . . . . . . . . . 15 1 < 2
128127a1i 11 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ 1 < 2)
129 nnrp 12982 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„• โ†’ ๐‘ฆ โˆˆ โ„+)
130123, 129ltaddrp2d 13047 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ 1 < (๐‘ฆ + 1))
131122, 124, 128, 130mulgt1d 12147 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ 1 < (2 ยท (๐‘ฆ + 1)))
132123, 125posdifd 11798 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ (1 < (2 ยท (๐‘ฆ + 1)) โ†” 0 < ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)))
133131, 132mpbid 231 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ 0 < ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))
134126, 133elrpd 13010 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) โˆ’ 1) โˆˆ โ„+)
135120, 134rpdivcld 13030 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) โˆˆ โ„+)
136115rpge0d 13017 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ 0 โ‰ค 2)
137 0le1 11734 . . . . . . . . . . . . . . 15 0 โ‰ค 1
138137a1i 11 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ 0 โ‰ค 1)
139116, 123, 118, 138addge0d 11787 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ 0 โ‰ค (๐‘ฆ + 1))
140122, 124, 136, 139mulge0d 11788 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ 0 โ‰ค (2 ยท (๐‘ฆ + 1)))
141125, 140ge0p1rpd 13043 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) + 1) โˆˆ โ„+)
142120, 141rpdivcld 13030 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) + 1)) โˆˆ โ„+)
143135, 142rpmulcld 13029 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) ยท ((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) + 1))) โˆˆ โ„+)
144105, 112, 113, 143fvmptd 7003 . . . . . . . 8 (๐‘ฆ โˆˆ โ„• โ†’ ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜(๐‘ฆ + 1)) = (((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) ยท ((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) + 1))))
145144oveq2d 7422 . . . . . . 7 (๐‘ฆ โˆˆ โ„• โ†’ (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜(๐‘ฆ + 1))) = (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท (((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) ยท ((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) + 1)))))
146125recnd 11239 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ (2 ยท (๐‘ฆ + 1)) โˆˆ โ„‚)
147126recnd 11239 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) โˆ’ 1) โˆˆ โ„‚)
148141rpcnd 13015 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) + 1) โˆˆ โ„‚)
149133gt0ne0d 11775 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) โˆ’ 1) โ‰  0)
150141rpne0d 13018 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) + 1) โ‰  0)
151146, 147, 146, 148, 149, 150divmuldivd 12028 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) ยท ((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) + 1))) = (((2 ยท (๐‘ฆ + 1)) ยท (2 ยท (๐‘ฆ + 1))) / (((2 ยท (๐‘ฆ + 1)) โˆ’ 1) ยท ((2 ยท (๐‘ฆ + 1)) + 1))))
152146, 146mulcld 11231 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) ยท (2 ยท (๐‘ฆ + 1))) โˆˆ โ„‚)
153152, 147, 148, 149, 150divdiv1d 12018 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„• โ†’ ((((2 ยท (๐‘ฆ + 1)) ยท (2 ยท (๐‘ฆ + 1))) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) / ((2 ยท (๐‘ฆ + 1)) + 1)) = (((2 ยท (๐‘ฆ + 1)) ยท (2 ยท (๐‘ฆ + 1))) / (((2 ยท (๐‘ฆ + 1)) โˆ’ 1) ยท ((2 ยท (๐‘ฆ + 1)) + 1))))
154146sqvald 14105 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1))โ†‘2) = ((2 ยท (๐‘ฆ + 1)) ยท (2 ยท (๐‘ฆ + 1))))
155154eqcomd 2739 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) ยท (2 ยท (๐‘ฆ + 1))) = ((2 ยท (๐‘ฆ + 1))โ†‘2))
156155oveq1d 7421 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1)) ยท (2 ยท (๐‘ฆ + 1))) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) = (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)))
157156oveq1d 7421 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„• โ†’ ((((2 ยท (๐‘ฆ + 1)) ยท (2 ยท (๐‘ฆ + 1))) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) / ((2 ยท (๐‘ฆ + 1)) + 1)) = ((((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) / ((2 ยท (๐‘ฆ + 1)) + 1)))
158151, 153, 1573eqtr2d 2779 . . . . . . . 8 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) ยท ((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) + 1))) = ((((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) / ((2 ยท (๐‘ฆ + 1)) + 1)))
159158oveq2d 7422 . . . . . . 7 (๐‘ฆ โˆˆ โ„• โ†’ (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท (((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) ยท ((2 ยท (๐‘ฆ + 1)) / ((2 ยท (๐‘ฆ + 1)) + 1)))) = (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท ((((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) / ((2 ยท (๐‘ฆ + 1)) + 1))))
160146sqcld 14106 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1))โ†‘2) โˆˆ โ„‚)
161160, 147, 149divcld 11987 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) โˆˆ โ„‚)
162161, 148, 150divrec2d 11991 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„• โ†’ ((((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) / ((2 ยท (๐‘ฆ + 1)) + 1)) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))))
163162oveq2d 7422 . . . . . . . 8 (๐‘ฆ โˆˆ โ„• โ†’ (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท ((((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) / ((2 ยท (๐‘ฆ + 1)) + 1))) = (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)))))
164 2cnd 12287 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ 2 โˆˆ โ„‚)
165 nncn 12217 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ ๐‘ฆ โˆˆ โ„‚)
166164, 165mulcld 11231 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„‚)
167 1cnd 11206 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ 1 โˆˆ โ„‚)
168166, 167addcld 11230 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท ๐‘ฆ) + 1) โˆˆ โ„‚)
169 2nn 12282 . . . . . . . . . . . . . . 15 2 โˆˆ โ„•
170169a1i 11 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ 2 โˆˆ โ„•)
171 id 22 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ ๐‘ฆ โˆˆ โ„•)
172170, 171nnmulcld 12262 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„•)
173172peano2nnd 12226 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท ๐‘ฆ) + 1) โˆˆ โ„•)
174173nnne0d 12259 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท ๐‘ฆ) + 1) โ‰  0)
175168, 174reccld 11980 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ (1 / ((2 ยท ๐‘ฆ) + 1)) โˆˆ โ„‚)
176 eqidd 2734 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘ฅ โˆˆ (1...๐‘ฆ)) โ†’ (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))) = (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))
177 oveq2 7414 . . . . . . . . . . . . . . . 16 (๐‘˜ = ๐‘ฅ โ†’ (2 ยท ๐‘˜) = (2 ยท ๐‘ฅ))
178177oveq1d 7421 . . . . . . . . . . . . . . 15 (๐‘˜ = ๐‘ฅ โ†’ ((2 ยท ๐‘˜)โ†‘4) = ((2 ยท ๐‘ฅ)โ†‘4))
179177oveq1d 7421 . . . . . . . . . . . . . . . . 17 (๐‘˜ = ๐‘ฅ โ†’ ((2 ยท ๐‘˜) โˆ’ 1) = ((2 ยท ๐‘ฅ) โˆ’ 1))
180177, 179oveq12d 7424 . . . . . . . . . . . . . . . 16 (๐‘˜ = ๐‘ฅ โ†’ ((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1)) = ((2 ยท ๐‘ฅ) ยท ((2 ยท ๐‘ฅ) โˆ’ 1)))
181180oveq1d 7421 . . . . . . . . . . . . . . 15 (๐‘˜ = ๐‘ฅ โ†’ (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2) = (((2 ยท ๐‘ฅ) ยท ((2 ยท ๐‘ฅ) โˆ’ 1))โ†‘2))
182178, 181oveq12d 7424 . . . . . . . . . . . . . 14 (๐‘˜ = ๐‘ฅ โ†’ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)) = (((2 ยท ๐‘ฅ)โ†‘4) / (((2 ยท ๐‘ฅ) ยท ((2 ยท ๐‘ฅ) โˆ’ 1))โ†‘2)))
183182adantl 483 . . . . . . . . . . . . 13 (((๐‘ฆ โˆˆ โ„• โˆง ๐‘ฅ โˆˆ (1...๐‘ฆ)) โˆง ๐‘˜ = ๐‘ฅ) โ†’ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)) = (((2 ยท ๐‘ฅ)โ†‘4) / (((2 ยท ๐‘ฅ) ยท ((2 ยท ๐‘ฅ) โˆ’ 1))โ†‘2)))
184 elfznn 13527 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ (1...๐‘ฆ) โ†’ ๐‘ฅ โˆˆ โ„•)
185184adantl 483 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘ฅ โˆˆ (1...๐‘ฆ)) โ†’ ๐‘ฅ โˆˆ โ„•)
186169a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ โ„• โ†’ 2 โˆˆ โ„•)
187 id 22 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ โ„• โ†’ ๐‘ฅ โˆˆ โ„•)
188186, 187nnmulcld 12262 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ โ„• โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„•)
189 4nn0 12488 . . . . . . . . . . . . . . . . . . 19 4 โˆˆ โ„•0
190189a1i 11 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ โ„• โ†’ 4 โˆˆ โ„•0)
191188, 190nnexpcld 14205 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ โ„• โ†’ ((2 ยท ๐‘ฅ)โ†‘4) โˆˆ โ„•)
192191nncnd 12225 . . . . . . . . . . . . . . . 16 (๐‘ฅ โˆˆ โ„• โ†’ ((2 ยท ๐‘ฅ)โ†‘4) โˆˆ โ„‚)
193 2cnd 12287 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ โ„• โ†’ 2 โˆˆ โ„‚)
194 nncn 12217 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ โ„• โ†’ ๐‘ฅ โˆˆ โ„‚)
195193, 194mulcld 11231 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ โ„• โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„‚)
196 1cnd 11206 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ โ„• โ†’ 1 โˆˆ โ„‚)
197195, 196subcld 11568 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ โ„• โ†’ ((2 ยท ๐‘ฅ) โˆ’ 1) โˆˆ โ„‚)
198195, 197mulcld 11231 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ โ„• โ†’ ((2 ยท ๐‘ฅ) ยท ((2 ยท ๐‘ฅ) โˆ’ 1)) โˆˆ โ„‚)
199198sqcld 14106 . . . . . . . . . . . . . . . 16 (๐‘ฅ โˆˆ โ„• โ†’ (((2 ยท ๐‘ฅ) ยท ((2 ยท ๐‘ฅ) โˆ’ 1))โ†‘2) โˆˆ โ„‚)
200186nnne0d 12259 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ โ„• โ†’ 2 โ‰  0)
201 nnne0 12243 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ โ„• โ†’ ๐‘ฅ โ‰  0)
202193, 194, 200, 201mulne0d 11863 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ โ„• โ†’ (2 ยท ๐‘ฅ) โ‰  0)
203 1red 11212 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ โˆˆ โ„• โ†’ 1 โˆˆ โ„)
204121a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ โ„• โ†’ 2 โˆˆ โ„)
205204, 203remulcld 11241 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ โˆˆ โ„• โ†’ (2 ยท 1) โˆˆ โ„)
206 nnre 12216 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ โ„• โ†’ ๐‘ฅ โˆˆ โ„)
207204, 206remulcld 11241 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ โˆˆ โ„• โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„)
20843a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ โ„• โ†’ (2 ยท 1) = 2)
209127, 208breqtrrid 5186 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ โˆˆ โ„• โ†’ 1 < (2 ยท 1))
210 0le2 12311 . . . . . . . . . . . . . . . . . . . . . . 23 0 โ‰ค 2
211210a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ โ„• โ†’ 0 โ‰ค 2)
212 nnge1 12237 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ โ„• โ†’ 1 โ‰ค ๐‘ฅ)
213203, 206, 204, 211, 212lemul2ad 12151 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ โˆˆ โ„• โ†’ (2 ยท 1) โ‰ค (2 ยท ๐‘ฅ))
214203, 205, 207, 209, 213ltletrd 11371 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ โˆˆ โ„• โ†’ 1 < (2 ยท ๐‘ฅ))
215203, 214gtned 11346 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ โ„• โ†’ (2 ยท ๐‘ฅ) โ‰  1)
216195, 196, 215subne0d 11577 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ โ„• โ†’ ((2 ยท ๐‘ฅ) โˆ’ 1) โ‰  0)
217195, 197, 202, 216mulne0d 11863 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ โ„• โ†’ ((2 ยท ๐‘ฅ) ยท ((2 ยท ๐‘ฅ) โˆ’ 1)) โ‰  0)
218 2z 12591 . . . . . . . . . . . . . . . . . 18 2 โˆˆ โ„ค
219218a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ โ„• โ†’ 2 โˆˆ โ„ค)
220198, 217, 219expne0d 14114 . . . . . . . . . . . . . . . 16 (๐‘ฅ โˆˆ โ„• โ†’ (((2 ยท ๐‘ฅ) ยท ((2 ยท ๐‘ฅ) โˆ’ 1))โ†‘2) โ‰  0)
221192, 199, 220divcld 11987 . . . . . . . . . . . . . . 15 (๐‘ฅ โˆˆ โ„• โ†’ (((2 ยท ๐‘ฅ)โ†‘4) / (((2 ยท ๐‘ฅ) ยท ((2 ยท ๐‘ฅ) โˆ’ 1))โ†‘2)) โˆˆ โ„‚)
222184, 221syl 17 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ (1...๐‘ฆ) โ†’ (((2 ยท ๐‘ฅ)โ†‘4) / (((2 ยท ๐‘ฅ) ยท ((2 ยท ๐‘ฅ) โˆ’ 1))โ†‘2)) โˆˆ โ„‚)
223222adantl 483 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘ฅ โˆˆ (1...๐‘ฆ)) โ†’ (((2 ยท ๐‘ฅ)โ†‘4) / (((2 ยท ๐‘ฅ) ยท ((2 ยท ๐‘ฅ) โˆ’ 1))โ†‘2)) โˆˆ โ„‚)
224176, 183, 185, 223fvmptd 7003 . . . . . . . . . . . 12 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘ฅ โˆˆ (1...๐‘ฆ)) โ†’ ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜๐‘ฅ) = (((2 ยท ๐‘ฅ)โ†‘4) / (((2 ยท ๐‘ฅ) ยท ((2 ยท ๐‘ฅ) โˆ’ 1))โ†‘2)))
225224, 223eqeltrd 2834 . . . . . . . . . . 11 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘ฅ โˆˆ (1...๐‘ฆ)) โ†’ ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜๐‘ฅ) โˆˆ โ„‚)
226 mulcl 11191 . . . . . . . . . . . 12 ((๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ค โˆˆ โ„‚) โ†’ (๐‘ฅ ยท ๐‘ค) โˆˆ โ„‚)
227226adantl 483 . . . . . . . . . . 11 ((๐‘ฆ โˆˆ โ„• โˆง (๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ค โˆˆ โ„‚)) โ†’ (๐‘ฅ ยท ๐‘ค) โˆˆ โ„‚)
22899, 225, 227seqcl 13985 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) โˆˆ โ„‚)
229175, 228mulcld 11231 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„• โ†’ ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) โˆˆ โ„‚)
230148, 150reccld 11980 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„• โ†’ (1 / ((2 ยท (๐‘ฆ + 1)) + 1)) โˆˆ โ„‚)
231229, 230, 161mul12d 11420 . . . . . . . 8 (๐‘ฆ โˆˆ โ„• โ†’ (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)))) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)))))
232175, 228mulcomd 11232 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„• โ†’ ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) = ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท (1 / ((2 ยท ๐‘ฆ) + 1))))
233232oveq1d 7421 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))) = (((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท (1 / ((2 ยท ๐‘ฆ) + 1))) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))))
234228, 175, 161mulassd 11234 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ (((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท (1 / ((2 ยท ๐‘ฆ) + 1))) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))) = ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)))))
235167, 168, 160, 147, 174, 149divmuldivd 12028 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))) = ((1 ยท ((2 ยท (๐‘ฆ + 1))โ†‘2)) / (((2 ยท ๐‘ฆ) + 1) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))))
236160mullidd 11229 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ (1 ยท ((2 ยท (๐‘ฆ + 1))โ†‘2)) = ((2 ยท (๐‘ฆ + 1))โ†‘2))
237164, 165, 167adddid 11235 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ โˆˆ โ„• โ†’ (2 ยท (๐‘ฆ + 1)) = ((2 ยท ๐‘ฆ) + (2 ยท 1)))
23843a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐‘ฆ โˆˆ โ„• โ†’ (2 ยท 1) = 2)
239238oveq2d 7422 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท ๐‘ฆ) + (2 ยท 1)) = ((2 ยท ๐‘ฆ) + 2))
240237, 239eqtrd 2773 . . . . . . . . . . . . . . . . 17 (๐‘ฆ โˆˆ โ„• โ†’ (2 ยท (๐‘ฆ + 1)) = ((2 ยท ๐‘ฆ) + 2))
241240oveq1d 7421 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) โˆ’ 1) = (((2 ยท ๐‘ฆ) + 2) โˆ’ 1))
242166, 164, 167addsubassd 11588 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท ๐‘ฆ) + 2) โˆ’ 1) = ((2 ยท ๐‘ฆ) + (2 โˆ’ 1)))
24345a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘ฆ โˆˆ โ„• โ†’ (2 โˆ’ 1) = 1)
244243oveq2d 7422 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท ๐‘ฆ) + (2 โˆ’ 1)) = ((2 ยท ๐‘ฆ) + 1))
245241, 242, 2443eqtrd 2777 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) โˆ’ 1) = ((2 ยท ๐‘ฆ) + 1))
246245oveq2d 7422 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท ๐‘ฆ) + 1) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) = (((2 ยท ๐‘ฆ) + 1) ยท ((2 ยท ๐‘ฆ) + 1)))
247168sqvald 14105 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท ๐‘ฆ) + 1)โ†‘2) = (((2 ยท ๐‘ฆ) + 1) ยท ((2 ยท ๐‘ฆ) + 1)))
248246, 247eqtr4d 2776 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท ๐‘ฆ) + 1) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) = (((2 ยท ๐‘ฆ) + 1)โ†‘2))
249236, 248oveq12d 7424 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ ((1 ยท ((2 ยท (๐‘ฆ + 1))โ†‘2)) / (((2 ยท ๐‘ฆ) + 1) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))) = (((2 ยท (๐‘ฆ + 1))โ†‘2) / (((2 ยท ๐‘ฆ) + 1)โ†‘2)))
250 2p2e4 12344 . . . . . . . . . . . . . . . . . 18 (2 + 2) = 4
25153, 53, 250mvlladdi 11475 . . . . . . . . . . . . . . . . 17 2 = (4 โˆ’ 2)
252251a1i 11 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„• โ†’ 2 = (4 โˆ’ 2))
253252oveq2d 7422 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1))โ†‘2) = ((2 ยท (๐‘ฆ + 1))โ†‘(4 โˆ’ 2)))
254120rpne0d 13018 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„• โ†’ (2 ยท (๐‘ฆ + 1)) โ‰  0)
255218a1i 11 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„• โ†’ 2 โˆˆ โ„ค)
256 4z 12593 . . . . . . . . . . . . . . . . 17 4 โˆˆ โ„ค
257256a1i 11 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„• โ†’ 4 โˆˆ โ„ค)
258146, 254, 255, 257expsubd 14119 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1))โ†‘(4 โˆ’ 2)) = (((2 ยท (๐‘ฆ + 1))โ†‘4) / ((2 ยท (๐‘ฆ + 1))โ†‘2)))
259253, 258eqtrd 2773 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1))โ†‘2) = (((2 ยท (๐‘ฆ + 1))โ†‘4) / ((2 ยท (๐‘ฆ + 1))โ†‘2)))
260245eqcomd 2739 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท ๐‘ฆ) + 1) = ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))
261260oveq1d 7421 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท ๐‘ฆ) + 1)โ†‘2) = (((2 ยท (๐‘ฆ + 1)) โˆ’ 1)โ†‘2))
262259, 261oveq12d 7424 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1))โ†‘2) / (((2 ยท ๐‘ฆ) + 1)โ†‘2)) = ((((2 ยท (๐‘ฆ + 1))โ†‘4) / ((2 ยท (๐‘ฆ + 1))โ†‘2)) / (((2 ยท (๐‘ฆ + 1)) โˆ’ 1)โ†‘2)))
263146, 254, 257expclzd 14113 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1))โ†‘4) โˆˆ โ„‚)
264147sqcld 14106 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1)) โˆ’ 1)โ†‘2) โˆˆ โ„‚)
265165, 167addcld 11230 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘ฆ + 1) โˆˆ โ„‚)
266170nnne0d 12259 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„• โ†’ 2 โ‰  0)
267113nnne0d 12259 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘ฆ + 1) โ‰  0)
268164, 265, 266, 267mulne0d 11863 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„• โ†’ (2 ยท (๐‘ฆ + 1)) โ‰  0)
269146, 268, 255expne0d 14114 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1))โ†‘2) โ‰  0)
270147, 149, 255expne0d 14114 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1)) โˆ’ 1)โ†‘2) โ‰  0)
271263, 160, 264, 269, 270divdiv1d 12018 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ ((((2 ยท (๐‘ฆ + 1))โ†‘4) / ((2 ยท (๐‘ฆ + 1))โ†‘2)) / (((2 ยท (๐‘ฆ + 1)) โˆ’ 1)โ†‘2)) = (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1))โ†‘2) ยท (((2 ยท (๐‘ฆ + 1)) โˆ’ 1)โ†‘2))))
272146, 147sqmuld 14120 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2) = (((2 ยท (๐‘ฆ + 1))โ†‘2) ยท (((2 ยท (๐‘ฆ + 1)) โˆ’ 1)โ†‘2)))
273272eqcomd 2739 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1))โ†‘2) ยท (((2 ยท (๐‘ฆ + 1)) โˆ’ 1)โ†‘2)) = (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2))
274273oveq2d 7422 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1))โ†‘2) ยท (((2 ยท (๐‘ฆ + 1)) โˆ’ 1)โ†‘2))) = (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2)))
275262, 271, 2743eqtrd 2777 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1))โ†‘2) / (((2 ยท ๐‘ฆ) + 1)โ†‘2)) = (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2)))
276235, 249, 2753eqtrd 2777 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„• โ†’ ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))) = (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2)))
277276oveq2d 7422 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)))) = ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2))))
278233, 234, 2773eqtrd 2777 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„• โ†’ (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))) = ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2))))
279278oveq2d 7422 . . . . . . . 8 (๐‘ฆ โˆˆ โ„• โ†’ ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท (((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)))) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2)))))
280163, 231, 2793eqtrd 2777 . . . . . . 7 (๐‘ฆ โˆˆ โ„• โ†’ (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท ((((2 ยท (๐‘ฆ + 1))โ†‘2) / ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) / ((2 ยท (๐‘ฆ + 1)) + 1))) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2)))))
281145, 159, 2803eqtrd 2777 . . . . . 6 (๐‘ฆ โˆˆ โ„• โ†’ (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜(๐‘ฆ + 1))) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2)))))
282 eqidd 2734 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))) = (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))
283 simpr 486 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘˜ = (๐‘ฆ + 1)) โ†’ ๐‘˜ = (๐‘ฆ + 1))
284283oveq2d 7422 . . . . . . . . . . . 12 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘˜ = (๐‘ฆ + 1)) โ†’ (2 ยท ๐‘˜) = (2 ยท (๐‘ฆ + 1)))
285284oveq1d 7421 . . . . . . . . . . 11 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘˜ = (๐‘ฆ + 1)) โ†’ ((2 ยท ๐‘˜)โ†‘4) = ((2 ยท (๐‘ฆ + 1))โ†‘4))
286284oveq1d 7421 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘˜ = (๐‘ฆ + 1)) โ†’ ((2 ยท ๐‘˜) โˆ’ 1) = ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))
287284, 286oveq12d 7424 . . . . . . . . . . . 12 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘˜ = (๐‘ฆ + 1)) โ†’ ((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1)) = ((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)))
288287oveq1d 7421 . . . . . . . . . . 11 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘˜ = (๐‘ฆ + 1)) โ†’ (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2) = (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2))
289285, 288oveq12d 7424 . . . . . . . . . 10 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘˜ = (๐‘ฆ + 1)) โ†’ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)) = (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2)))
290146, 147mulcld 11231 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) โˆˆ โ„‚)
291290sqcld 14106 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2) โˆˆ โ„‚)
292146, 147, 254, 149mulne0d 11863 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„• โ†’ ((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1)) โ‰  0)
293290, 292, 255expne0d 14114 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2) โ‰  0)
294263, 291, 293divcld 11987 . . . . . . . . . 10 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2)) โˆˆ โ„‚)
295282, 289, 113, 294fvmptd 7003 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„• โ†’ ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜(๐‘ฆ + 1)) = (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2)))
296295eqcomd 2739 . . . . . . . 8 (๐‘ฆ โˆˆ โ„• โ†’ (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2)) = ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜(๐‘ฆ + 1)))
297296oveq2d 7422 . . . . . . 7 (๐‘ฆ โˆˆ โ„• โ†’ ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2))) = ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜(๐‘ฆ + 1))))
298297oveq2d 7422 . . . . . 6 (๐‘ฆ โˆˆ โ„• โ†’ ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท (((2 ยท (๐‘ฆ + 1))โ†‘4) / (((2 ยท (๐‘ฆ + 1)) ยท ((2 ยท (๐‘ฆ + 1)) โˆ’ 1))โ†‘2)))) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜(๐‘ฆ + 1)))))
299 seqp1 13978 . . . . . . . . 9 (๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜(๐‘ฆ + 1)) = ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜(๐‘ฆ + 1))))
30099, 299syl 17 . . . . . . . 8 (๐‘ฆ โˆˆ โ„• โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜(๐‘ฆ + 1)) = ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜(๐‘ฆ + 1))))
301300eqcomd 2739 . . . . . . 7 (๐‘ฆ โˆˆ โ„• โ†’ ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜(๐‘ฆ + 1))) = (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜(๐‘ฆ + 1)))
302301oveq2d 7422 . . . . . 6 (๐‘ฆ โˆˆ โ„• โ†’ ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2)))โ€˜(๐‘ฆ + 1)))) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜(๐‘ฆ + 1))))
303281, 298, 3023eqtrd 2777 . . . . 5 (๐‘ฆ โˆˆ โ„• โ†’ (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜(๐‘ฆ + 1))) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜(๐‘ฆ + 1))))
304303adantr 482 . . . 4 ((๐‘ฆ โˆˆ โ„• โˆง (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ) = ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ))) โ†’ (((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) ยท ((๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1))))โ€˜(๐‘ฆ + 1))) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜(๐‘ฆ + 1))))
305102, 104, 3043eqtrd 2777 . . 3 ((๐‘ฆ โˆˆ โ„• โˆง (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ) = ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ))) โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜(๐‘ฆ + 1)) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜(๐‘ฆ + 1))))
306305ex 414 . 2 (๐‘ฆ โˆˆ โ„• โ†’ ((seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘ฆ) = ((1 / ((2 ยท ๐‘ฆ) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘ฆ)) โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜(๐‘ฆ + 1)) = ((1 / ((2 ยท (๐‘ฆ + 1)) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜(๐‘ฆ + 1)))))
3077, 14, 21, 28, 97, 306nnind 12227 1 (๐‘ โˆˆ โ„• โ†’ (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) โˆ’ 1)) ยท ((2 ยท ๐‘˜) / ((2 ยท ๐‘˜) + 1)))))โ€˜๐‘) = ((1 / ((2 ยท ๐‘) + 1)) ยท (seq1( ยท , (๐‘˜ โˆˆ โ„• โ†ฆ (((2 ยท ๐‘˜)โ†‘4) / (((2 ยท ๐‘˜) ยท ((2 ยท ๐‘˜) โˆ’ 1))โ†‘2))))โ€˜๐‘)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941   class class class wbr 5148   โ†ฆ cmpt 5231  โ€˜cfv 6541  (class class class)co 7406  โ„‚cc 11105  โ„cr 11106  0cc0 11107  1c1 11108   + caddc 11110   ยท cmul 11112   < clt 11245   โ‰ค cle 11246   โˆ’ cmin 11441   / cdiv 11868  โ„•cn 12209  2c2 12264  3c3 12265  4c4 12266  6c6 12268  โ„•0cn0 12469  โ„คcz 12555  cdc 12674  โ„คโ‰ฅcuz 12819  โ„+crp 12971  ...cfz 13481  seqcseq 13963  โ†‘cexp 14024
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-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
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 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-rp 12972  df-fz 13482  df-seq 13964  df-exp 14025
This theorem is referenced by:  wallispi2  44776
  Copyright terms: Public domain W3C validator