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

Theorem stirlinglem3 45387
Description: Long but simple algebraic transformations are applied to show that ๐‘‰, the Wallis formula for ฯ€ , can be expressed in terms of ๐ด, the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the ๐ด, in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
stirlinglem3.1 ๐ด = (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
stirlinglem3.2 ๐ท = (๐‘› โˆˆ โ„• โ†ฆ (๐ดโ€˜(2 ยท ๐‘›)))
stirlinglem3.3 ๐ธ = (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))
stirlinglem3.4 ๐‘‰ = (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) / ((2 ยท ๐‘›) + 1)))
Assertion
Ref Expression
stirlinglem3 ๐‘‰ = (๐‘› โˆˆ โ„• โ†ฆ ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))

Proof of Theorem stirlinglem3
Dummy variable ๐‘š is distinct from all other variables.
StepHypRef Expression
1 stirlinglem3.4 . 2 ๐‘‰ = (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) / ((2 ยท ๐‘›) + 1)))
2 nnnn0 12501 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•0)
3 faccl 14266 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„•0 โ†’ (!โ€˜๐‘›) โˆˆ โ„•)
4 nncn 12242 . . . . . . . . . . . . 13 ((!โ€˜๐‘›) โˆˆ โ„• โ†’ (!โ€˜๐‘›) โˆˆ โ„‚)
52, 3, 43syl 18 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (!โ€˜๐‘›) โˆˆ โ„‚)
6 2cnd 12312 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„‚)
7 nncn 12242 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„‚)
86, 7mulcld 11256 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„‚)
98sqrtcld 15408 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (โˆšโ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
10 ere 16057 . . . . . . . . . . . . . . . . 17 e โˆˆ โ„
1110recni 11250 . . . . . . . . . . . . . . . 16 e โˆˆ โ„‚
1211a1i 11 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ e โˆˆ โ„‚)
13 epos 16175 . . . . . . . . . . . . . . . . 17 0 < e
1410, 13gt0ne0ii 11772 . . . . . . . . . . . . . . . 16 e โ‰  0
1514a1i 11 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ e โ‰  0)
167, 12, 15divcld 12012 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (๐‘› / e) โˆˆ โ„‚)
1716, 2expcld 14134 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘๐‘›) โˆˆ โ„‚)
189, 17mulcld 11256 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)) โˆˆ โ„‚)
19 2rp 13003 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„+
2019a1i 11 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„+)
21 nnrp 13009 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„+)
2220, 21rpmulcld 13056 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„+)
2322sqrtgt0d 15383 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ 0 < (โˆšโ€˜(2 ยท ๐‘›)))
2423gt0ne0d 11800 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (โˆšโ€˜(2 ยท ๐‘›)) โ‰  0)
25 nnne0 12268 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ๐‘› โ‰  0)
267, 12, 25, 15divne0d 12028 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (๐‘› / e) โ‰  0)
27 nnz 12601 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„ค)
2816, 26, 27expne0d 14140 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘๐‘›) โ‰  0)
299, 17, 24, 28mulne0d 11888 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)) โ‰  0)
305, 18, 29divcld 12012 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) โˆˆ โ„‚)
31 stirlinglem3.1 . . . . . . . . . . . 12 ๐ด = (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
3231fvmpt2 7010 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) โˆˆ โ„‚) โ†’ (๐ดโ€˜๐‘›) = ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
3330, 32mpdan 686 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜๐‘›) = ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
3433oveq1d 7429 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((๐ดโ€˜๐‘›)โ†‘4) = (((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ†‘4))
35 stirlinglem3.3 . . . . . . . . . . . 12 ๐ธ = (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))
3635fvmpt2 7010 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)) โˆˆ โ„‚) โ†’ (๐ธโ€˜๐‘›) = ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))
3718, 36mpdan 686 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜๐‘›) = ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))
3837oveq1d 7429 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜๐‘›)โ†‘4) = (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4))
3934, 38oveq12d 7432 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) = ((((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ†‘4) ยท (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)))
40 4nn0 12513 . . . . . . . . . . 11 4 โˆˆ โ„•0
4140a1i 11 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ 4 โˆˆ โ„•0)
425, 18, 29, 41expdivd 14148 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ†‘4) = (((!โ€˜๐‘›)โ†‘4) / (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)))
4342oveq1d 7429 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ†‘4) ยท (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)) = ((((!โ€˜๐‘›)โ†‘4) / (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)) ยท (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)))
445, 41expcld 14134 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜๐‘›)โ†‘4) โˆˆ โ„‚)
4518, 41expcld 14134 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) โˆˆ โ„‚)
4641nn0zd 12606 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ 4 โˆˆ โ„ค)
4718, 29, 46expne0d 14140 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) โ‰  0)
4844, 45, 47divcan1d 12013 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜๐‘›)โ†‘4) / (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)) ยท (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)) = ((!โ€˜๐‘›)โ†‘4))
4939, 43, 483eqtrd 2771 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) = ((!โ€˜๐‘›)โ†‘4))
5049eqcomd 2733 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜๐‘›)โ†‘4) = (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)))
5150oveq2d 7430 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) = ((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))))
52 2nn0 12511 . . . . . . . . . . . . 13 2 โˆˆ โ„•0
5352a1i 11 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„•0)
5453, 2nn0mulcld 12559 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„•0)
55 faccl 14266 . . . . . . . . . . 11 ((2 ยท ๐‘›) โˆˆ โ„•0 โ†’ (!โ€˜(2 ยท ๐‘›)) โˆˆ โ„•)
56 nncn 12242 . . . . . . . . . . 11 ((!โ€˜(2 ยท ๐‘›)) โˆˆ โ„• โ†’ (!โ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
5754, 55, 563syl 18 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
5857sqcld 14132 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›))โ†‘2) โˆˆ โ„‚)
596, 8mulcld 11256 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (2 ยท (2 ยท ๐‘›)) โˆˆ โ„‚)
6059sqrtcld 15408 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (โˆšโ€˜(2 ยท (2 ยท ๐‘›))) โˆˆ โ„‚)
618, 12, 15divcld 12012 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) / e) โˆˆ โ„‚)
6261, 54expcld 14134 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)) โˆˆ โ„‚)
6360, 62mulcld 11256 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))) โˆˆ โ„‚)
6463sqcld 14132 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2) โˆˆ โ„‚)
6520, 22rpmulcld 13056 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (2 ยท (2 ยท ๐‘›)) โˆˆ โ„+)
6665sqrtgt0d 15383 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 0 < (โˆšโ€˜(2 ยท (2 ยท ๐‘›))))
6766gt0ne0d 11800 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (โˆšโ€˜(2 ยท (2 ยท ๐‘›))) โ‰  0)
6820rpne0d 13045 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ 2 โ‰  0)
696, 7, 68, 25mulne0d 11888 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โ‰  0)
708, 12, 69, 15divne0d 12028 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) / e) โ‰  0)
71 2z 12616 . . . . . . . . . . . . . 14 2 โˆˆ โ„ค
7271a1i 11 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„ค)
7372, 27zmulcld 12694 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„ค)
7461, 70, 73expne0d 14140 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)) โ‰  0)
7560, 62, 67, 74mulne0d 11888 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))) โ‰  0)
7663, 75, 72expne0d 14140 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2) โ‰  0)
7758, 64, 76divcan1d 12013 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜(2 ยท ๐‘›))โ†‘2) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = ((!โ€˜(2 ยท ๐‘›))โ†‘2))
7857, 63, 75, 53expdivd 14148 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) = (((!โ€˜(2 ยท ๐‘›))โ†‘2) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
7978eqcomd 2733 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((!โ€˜(2 ยท ๐‘›))โ†‘2) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = (((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2))
8079oveq1d 7429 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜(2 ยท ๐‘›))โ†‘2) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = ((((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
8177, 80eqtr3d 2769 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›))โ†‘2) = ((((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
82 fveq2 6891 . . . . . . . . . . . . . 14 (๐‘› = ๐‘š โ†’ (!โ€˜๐‘›) = (!โ€˜๐‘š))
83 oveq2 7422 . . . . . . . . . . . . . . . 16 (๐‘› = ๐‘š โ†’ (2 ยท ๐‘›) = (2 ยท ๐‘š))
8483fveq2d 6895 . . . . . . . . . . . . . . 15 (๐‘› = ๐‘š โ†’ (โˆšโ€˜(2 ยท ๐‘›)) = (โˆšโ€˜(2 ยท ๐‘š)))
85 oveq1 7421 . . . . . . . . . . . . . . . 16 (๐‘› = ๐‘š โ†’ (๐‘› / e) = (๐‘š / e))
86 id 22 . . . . . . . . . . . . . . . 16 (๐‘› = ๐‘š โ†’ ๐‘› = ๐‘š)
8785, 86oveq12d 7432 . . . . . . . . . . . . . . 15 (๐‘› = ๐‘š โ†’ ((๐‘› / e)โ†‘๐‘›) = ((๐‘š / e)โ†‘๐‘š))
8884, 87oveq12d 7432 . . . . . . . . . . . . . 14 (๐‘› = ๐‘š โ†’ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)) = ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))
8982, 88oveq12d 7432 . . . . . . . . . . . . 13 (๐‘› = ๐‘š โ†’ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) = ((!โ€˜๐‘š) / ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
9089cbvmptv 5255 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))) = (๐‘š โˆˆ โ„• โ†ฆ ((!โ€˜๐‘š) / ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
9131, 90eqtri 2755 . . . . . . . . . . 11 ๐ด = (๐‘š โˆˆ โ„• โ†ฆ ((!โ€˜๐‘š) / ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
92 fveq2 6891 . . . . . . . . . . . 12 (๐‘š = (2 ยท ๐‘›) โ†’ (!โ€˜๐‘š) = (!โ€˜(2 ยท ๐‘›)))
93 oveq2 7422 . . . . . . . . . . . . . 14 (๐‘š = (2 ยท ๐‘›) โ†’ (2 ยท ๐‘š) = (2 ยท (2 ยท ๐‘›)))
9493fveq2d 6895 . . . . . . . . . . . . 13 (๐‘š = (2 ยท ๐‘›) โ†’ (โˆšโ€˜(2 ยท ๐‘š)) = (โˆšโ€˜(2 ยท (2 ยท ๐‘›))))
95 oveq1 7421 . . . . . . . . . . . . . 14 (๐‘š = (2 ยท ๐‘›) โ†’ (๐‘š / e) = ((2 ยท ๐‘›) / e))
96 id 22 . . . . . . . . . . . . . 14 (๐‘š = (2 ยท ๐‘›) โ†’ ๐‘š = (2 ยท ๐‘›))
9795, 96oveq12d 7432 . . . . . . . . . . . . 13 (๐‘š = (2 ยท ๐‘›) โ†’ ((๐‘š / e)โ†‘๐‘š) = (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))
9894, 97oveq12d 7432 . . . . . . . . . . . 12 (๐‘š = (2 ยท ๐‘›) โ†’ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)) = ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))
9992, 98oveq12d 7432 . . . . . . . . . . 11 (๐‘š = (2 ยท ๐‘›) โ†’ ((!โ€˜๐‘š) / ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))) = ((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))))
100 2nn 12307 . . . . . . . . . . . . 13 2 โˆˆ โ„•
101100a1i 11 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„•)
102 id 22 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•)
103101, 102nnmulcld 12287 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„•)
10457, 63, 75divcld 12012 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))) โˆˆ โ„‚)
10591, 99, 103, 104fvmptd3 7022 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜(2 ยท ๐‘›)) = ((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))))
106105oveq1d 7429 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) = (((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2))
107106eqcomd 2733 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) = ((๐ดโ€˜(2 ยท ๐‘›))โ†‘2))
108107oveq1d 7429 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
109 eqidd 2728 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))) = (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
11098adantl 481 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘š = (2 ยท ๐‘›)) โ†’ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)) = ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))
111109, 110, 103, 63fvmptd 7006 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›)) = ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))
112111oveq1d 7429 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2) = (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2))
113112eqcomd 2733 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2) = (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2))
114113oveq2d 7430 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2)))
11581, 108, 1143eqtrd 2771 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›))โ†‘2) = (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2)))
11688cbvmptv 5255 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) = (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))
117116a1i 11 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) = (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
118117fveq1d 6893 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›)) = ((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›)))
119118eqcomd 2733 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›)) = ((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›)))
120119oveq1d 7429 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2) = (((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›))โ†‘2))
121120oveq2d 7430 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2)) = (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›))โ†‘2)))
122105, 104eqeltrd 2828 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
123 stirlinglem3.2 . . . . . . . . . . 11 ๐ท = (๐‘› โˆˆ โ„• โ†ฆ (๐ดโ€˜(2 ยท ๐‘›)))
124123fvmpt2 7010 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง (๐ดโ€˜(2 ยท ๐‘›)) โˆˆ โ„‚) โ†’ (๐ทโ€˜๐‘›) = (๐ดโ€˜(2 ยท ๐‘›)))
125122, 124mpdan 686 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ทโ€˜๐‘›) = (๐ดโ€˜(2 ยท ๐‘›)))
126125eqcomd 2733 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜(2 ยท ๐‘›)) = (๐ทโ€˜๐‘›))
127126oveq1d 7429 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) = ((๐ทโ€˜๐‘›)โ†‘2))
12835a1i 11 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ๐ธ = (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
129128fveq1d 6893 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜(2 ยท ๐‘›)) = ((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›)))
130129eqcomd 2733 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›)) = (๐ธโ€˜(2 ยท ๐‘›)))
131130oveq1d 7429 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›))โ†‘2) = ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))
132127, 131oveq12d 7432 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›))โ†‘2)) = (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))
133115, 121, 1323eqtrd 2771 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›))โ†‘2) = (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))
13451, 133oveq12d 7432 . . . 4 (๐‘› โˆˆ โ„• โ†’ (((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) = (((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
135134oveq1d 7429 . . 3 (๐‘› โˆˆ โ„• โ†’ ((((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) / ((2 ยท ๐‘›) + 1)) = ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
136135mpteq2ia 5245 . 2 (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) / ((2 ยท ๐‘›) + 1))) = (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
13741, 2nn0mulcld 12559 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (4 ยท ๐‘›) โˆˆ โ„•0)
1386, 137expcld 14134 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (2โ†‘(4 ยท ๐‘›)) โˆˆ โ„‚)
13949, 44eqeltrd 2828 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) โˆˆ โ„‚)
140138, 139mulcomd 11257 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) = ((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))))
141140oveq1d 7429 . . . . 5 (๐‘› โˆˆ โ„• โ†’ (((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
142141oveq1d 7429 . . . 4 (๐‘› โˆˆ โ„• โ†’ ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
143125, 122eqeltrd 2828 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ทโ€˜๐‘›) โˆˆ โ„‚)
144143sqcld 14132 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ทโ€˜๐‘›)โ†‘2) โˆˆ โ„‚)
145128, 117eqtrd 2767 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ๐ธ = (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
146145, 110, 103, 63fvmptd 7006 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜(2 ยท ๐‘›)) = ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))
147146, 63eqeltrd 2828 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
148147sqcld 14132 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2) โˆˆ โ„‚)
149 nnne0 12268 . . . . . . . . . . . 12 ((!โ€˜(2 ยท ๐‘›)) โˆˆ โ„• โ†’ (!โ€˜(2 ยท ๐‘›)) โ‰  0)
15054, 55, 1493syl 18 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(2 ยท ๐‘›)) โ‰  0)
15157, 63, 150, 75divne0d 12028 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))) โ‰  0)
152105, 151eqnetrd 3003 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜(2 ยท ๐‘›)) โ‰  0)
153125, 152eqnetrd 3003 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ทโ€˜๐‘›) โ‰  0)
154143, 153, 72expne0d 14140 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ทโ€˜๐‘›)โ†‘2) โ‰  0)
155146, 75eqnetrd 3003 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜(2 ยท ๐‘›)) โ‰  0)
156147, 155, 72expne0d 14140 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2) โ‰  0)
157139, 144, 138, 148, 154, 156divmuldivd 12053 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
158157eqcomd 2733 . . . . 5 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
159158oveq1d 7429 . . . 4 (๐‘› โˆˆ โ„• โ†’ ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
16033, 30eqeltrd 2828 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜๐‘›) โˆˆ โ„‚)
161160, 41expcld 14134 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐ดโ€˜๐‘›)โ†‘4) โˆˆ โ„‚)
16238, 45eqeltrd 2828 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜๐‘›)โ†‘4) โˆˆ โ„‚)
163161, 162, 144, 154div23d 12049 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)))
164163oveq1d 7429 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
165164oveq1d 7429 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
166161, 144, 154divcld 12012 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) โˆˆ โ„‚)
167138, 148, 156divcld 12012 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)) โˆˆ โ„‚)
168166, 162, 167mulassd 11259 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))))
169168oveq1d 7429 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))) / ((2 ยท ๐‘›) + 1)))
170162, 167mulcld 11256 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) โˆˆ โ„‚)
171 1cnd 11231 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ 1 โˆˆ โ„‚)
1728, 171addcld 11255 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โˆˆ โ„‚)
173 0red 11239 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ 0 โˆˆ โ„)
174103nnred 12249 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„)
175 2re 12308 . . . . . . . . . . . 12 2 โˆˆ โ„
176175a1i 11 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„)
177 nnre 12241 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„)
178176, 177remulcld 11266 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„)
179 1red 11237 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ 1 โˆˆ โ„)
180178, 179readdcld 11265 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โˆˆ โ„)
181103nngt0d 12283 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ 0 < (2 ยท ๐‘›))
182174ltp1d 12166 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) < ((2 ยท ๐‘›) + 1))
183173, 174, 180, 181, 182lttrd 11397 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ 0 < ((2 ยท ๐‘›) + 1))
184183gt0ne0d 11800 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โ‰  0)
185166, 170, 172, 184divassd 12047 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))) / ((2 ยท ๐‘›) + 1)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1))))
186162, 138, 148, 156div12d 12048 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = ((2โ†‘(4 ยท ๐‘›)) ยท (((๐ธโ€˜๐‘›)โ†‘4) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
1879, 17, 41mulexpd 14149 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) = (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) ยท (((๐‘› / e)โ†‘๐‘›)โ†‘4)))
18860, 62sqmuld 14146 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2) = (((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) ยท ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)))
189187, 188oveq12d 7432 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) ยท (((๐‘› / e)โ†‘๐‘›)โ†‘4)) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) ยท ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))))
190146oveq1d 7429 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2) = (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2))
19138, 190oveq12d 7432 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)) = ((((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
1929, 41expcld 14134 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) โˆˆ โ„‚)
19360sqcld 14132 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) โˆˆ โ„‚)
19417, 41expcld 14134 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (((๐‘› / e)โ†‘๐‘›)โ†‘4) โˆˆ โ„‚)
19562sqcld 14132 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2) โˆˆ โ„‚)
19660, 67, 72expne0d 14140 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) โ‰  0)
19762, 74, 72expne0d 14140 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2) โ‰  0)
198192, 193, 194, 195, 196, 197divmuldivd 12053 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))) = ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) ยท (((๐‘› / e)โ†‘๐‘›)โ†‘4)) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) ยท ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))))
199189, 191, 1983eqtr4d 2777 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)) = ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))))
200199oveq2d 7430 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (((๐ธโ€˜๐‘›)โ†‘4) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = ((2โ†‘(4 ยท ๐‘›)) ยท ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)))))
20165rprege0d 13047 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท (2 ยท ๐‘›)) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท (2 ยท ๐‘›))))
202 resqrtth 15226 . . . . . . . . . . . . . . . 16 (((2 ยท (2 ยท ๐‘›)) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท (2 ยท ๐‘›))) โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) = (2 ยท (2 ยท ๐‘›)))
203201, 202syl 17 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) = (2 ยท (2 ยท ๐‘›)))
204203oveq2d 7430 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) = (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / (2 ยท (2 ยท ๐‘›))))
205 2t2e4 12398 . . . . . . . . . . . . . . . . . . 19 (2 ยท 2) = 4
206205eqcomi 2736 . . . . . . . . . . . . . . . . . 18 4 = (2 ยท 2)
207206a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ 4 = (2 ยท 2))
208207oveq2d 7430 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) = ((โˆšโ€˜(2 ยท ๐‘›))โ†‘(2 ยท 2)))
2099, 53, 53expmuld 14137 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘(2 ยท 2)) = (((โˆšโ€˜(2 ยท ๐‘›))โ†‘2)โ†‘2))
21022rprege0d 13047 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท ๐‘›)))
211 resqrtth 15226 . . . . . . . . . . . . . . . . . 18 (((2 ยท ๐‘›) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท ๐‘›)) โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘2) = (2 ยท ๐‘›))
212210, 211syl 17 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘2) = (2 ยท ๐‘›))
213212oveq1d 7429 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›))โ†‘2)โ†‘2) = ((2 ยท ๐‘›)โ†‘2))
214208, 209, 2133eqtrd 2771 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) = ((2 ยท ๐‘›)โ†‘2))
2156, 6, 7mulassd 11259 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท 2) ยท ๐‘›) = (2 ยท (2 ยท ๐‘›)))
216205a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (2 ยท 2) = 4)
217216oveq1d 7429 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท 2) ยท ๐‘›) = (4 ยท ๐‘›))
218215, 217eqtr3d 2769 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (2 ยท (2 ยท ๐‘›)) = (4 ยท ๐‘›))
219214, 218oveq12d 7432 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / (2 ยท (2 ยท ๐‘›))) = (((2 ยท ๐‘›)โ†‘2) / (4 ยท ๐‘›)))
2206, 7sqmuld 14146 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘2) = ((2โ†‘2) ยท (๐‘›โ†‘2)))
221 sq2 14184 . . . . . . . . . . . . . . . . . . 19 (2โ†‘2) = 4
222221a1i 11 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ (2โ†‘2) = 4)
223222oveq1d 7429 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘2) ยท (๐‘›โ†‘2)) = (4 ยท (๐‘›โ†‘2)))
224220, 223eqtrd 2767 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘2) = (4 ยท (๐‘›โ†‘2)))
225224oveq1d 7429 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›)โ†‘2) / (4 ยท ๐‘›)) = ((4 ยท (๐‘›โ†‘2)) / (4 ยท ๐‘›)))
226 4cn 12319 . . . . . . . . . . . . . . . . . . 19 4 โˆˆ โ„‚
227 4ne0 12342 . . . . . . . . . . . . . . . . . . 19 4 โ‰  0
228226, 227dividi 11969 . . . . . . . . . . . . . . . . . 18 (4 / 4) = 1
229228a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (4 / 4) = 1)
2307sqvald 14131 . . . . . . . . . . . . . . . . . . 19 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘2) = (๐‘› ยท ๐‘›))
231230oveq1d 7429 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘2) / ๐‘›) = ((๐‘› ยท ๐‘›) / ๐‘›))
2327, 7, 25divcan4d 12018 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ ((๐‘› ยท ๐‘›) / ๐‘›) = ๐‘›)
233231, 232eqtrd 2767 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘2) / ๐‘›) = ๐‘›)
234229, 233oveq12d 7432 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((4 / 4) ยท ((๐‘›โ†‘2) / ๐‘›)) = (1 ยท ๐‘›))
23541nn0cnd 12556 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ 4 โˆˆ โ„‚)
2367sqcld 14132 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘2) โˆˆ โ„‚)
237227a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ 4 โ‰  0)
238235, 235, 236, 7, 237, 25divmuldivd 12053 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((4 / 4) ยท ((๐‘›โ†‘2) / ๐‘›)) = ((4 ยท (๐‘›โ†‘2)) / (4 ยท ๐‘›)))
2397mullidd 11254 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (1 ยท ๐‘›) = ๐‘›)
240234, 238, 2393eqtr3d 2775 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((4 ยท (๐‘›โ†‘2)) / (4 ยท ๐‘›)) = ๐‘›)
241225, 240eqtrd 2767 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›)โ†‘2) / (4 ยท ๐‘›)) = ๐‘›)
242204, 219, 2413eqtrd 2771 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) = ๐‘›)
2437, 235mulcomd 11257 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (๐‘› ยท 4) = (4 ยท ๐‘›))
244243oveq2d 7430 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘(๐‘› ยท 4)) = ((๐‘› / e)โ†‘(4 ยท ๐‘›)))
24516, 41, 2expmuld 14137 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘(๐‘› ยท 4)) = (((๐‘› / e)โ†‘๐‘›)โ†‘4))
2467, 12, 15, 137expdivd 14148 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘(4 ยท ๐‘›)) = ((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))))
247244, 245, 2463eqtr3d 2775 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (((๐‘› / e)โ†‘๐‘›)โ†‘4) = ((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))))
2486, 7, 6mul32d 11446 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) ยท 2) = ((2 ยท 2) ยท ๐‘›))
249248, 217eqtrd 2767 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) ยท 2) = (4 ยท ๐‘›))
250249oveq2d 7430 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘((2 ยท ๐‘›) ยท 2)) = (((2 ยท ๐‘›) / e)โ†‘(4 ยท ๐‘›)))
25161, 53, 54expmuld 14137 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘((2 ยท ๐‘›) ยท 2)) = ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))
2528, 12, 15, 137expdivd 14148 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘(4 ยท ๐‘›)) = (((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))))
253250, 251, 2523eqtr3d 2775 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2) = (((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))))
254247, 253oveq12d 7432 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)) = (((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) / (((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›)))))
255247, 194eqeltrrd 2829 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) โˆˆ โ„‚)
2568, 137expcld 14134 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) โˆˆ โ„‚)
25712, 137expcld 14134 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (eโ†‘(4 ยท ๐‘›)) โˆˆ โ„‚)
25846, 27zmulcld 12694 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (4 ยท ๐‘›) โˆˆ โ„ค)
2598, 69, 258expne0d 14140 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) โ‰  0)
26012, 15, 258expne0d 14140 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (eโ†‘(4 ยท ๐‘›)) โ‰  0)
261255, 256, 257, 259, 260divdiv2d 12044 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) / (((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›)))) = ((((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) ยท (eโ†‘(4 ยท ๐‘›))) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))))
2627, 137expcld 14134 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘(4 ยท ๐‘›)) โˆˆ โ„‚)
263262, 257, 260divcan1d 12013 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) ยท (eโ†‘(4 ยท ๐‘›))) = (๐‘›โ†‘(4 ยท ๐‘›)))
264263oveq1d 7429 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) ยท (eโ†‘(4 ยท ๐‘›))) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))) = ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))))
2656, 7, 137mulexpd 14149 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) = ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›))))
266265oveq2d 7430 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))) = ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›)))))
267138, 262mulcomd 11257 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›))) = ((๐‘›โ†‘(4 ยท ๐‘›)) ยท (2โ†‘(4 ยท ๐‘›))))
268267oveq2d 7430 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›)))) = ((๐‘›โ†‘(4 ยท ๐‘›)) / ((๐‘›โ†‘(4 ยท ๐‘›)) ยท (2โ†‘(4 ยท ๐‘›)))))
2697, 25, 258expne0d 14140 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘(4 ยท ๐‘›)) โ‰  0)
2706, 68, 258expne0d 14140 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (2โ†‘(4 ยท ๐‘›)) โ‰  0)
271262, 262, 138, 269, 270divdiv1d 12043 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘(4 ยท ๐‘›)) / (๐‘›โ†‘(4 ยท ๐‘›))) / (2โ†‘(4 ยท ๐‘›))) = ((๐‘›โ†‘(4 ยท ๐‘›)) / ((๐‘›โ†‘(4 ยท ๐‘›)) ยท (2โ†‘(4 ยท ๐‘›)))))
272262, 269dividd 12010 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / (๐‘›โ†‘(4 ยท ๐‘›))) = 1)
273272oveq1d 7429 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘(4 ยท ๐‘›)) / (๐‘›โ†‘(4 ยท ๐‘›))) / (2โ†‘(4 ยท ๐‘›))) = (1 / (2โ†‘(4 ยท ๐‘›))))
274268, 271, 2733eqtr2d 2773 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›)))) = (1 / (2โ†‘(4 ยท ๐‘›))))
275264, 266, 2743eqtrd 2771 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ((((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) ยท (eโ†‘(4 ยท ๐‘›))) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))) = (1 / (2โ†‘(4 ยท ๐‘›))))
276254, 261, 2753eqtrd 2771 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)) = (1 / (2โ†‘(4 ยท ๐‘›))))
277242, 276oveq12d 7432 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))) = (๐‘› ยท (1 / (2โ†‘(4 ยท ๐‘›)))))
278277oveq2d 7430 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)))) = ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘› ยท (1 / (2โ†‘(4 ยท ๐‘›))))))
279138, 270reccld 12005 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (1 / (2โ†‘(4 ยท ๐‘›))) โˆˆ โ„‚)
280138, 7, 279mul12d 11445 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘› ยท (1 / (2โ†‘(4 ยท ๐‘›))))) = (๐‘› ยท ((2โ†‘(4 ยท ๐‘›)) ยท (1 / (2โ†‘(4 ยท ๐‘›))))))
2817mulridd 11253 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (๐‘› ยท 1) = ๐‘›)
282138, 270recidd 12007 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (1 / (2โ†‘(4 ยท ๐‘›)))) = 1)
283282oveq2d 7430 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (๐‘› ยท ((2โ†‘(4 ยท ๐‘›)) ยท (1 / (2โ†‘(4 ยท ๐‘›))))) = (๐‘› ยท 1))
284281, 283, 2333eqtr4d 2777 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (๐‘› ยท ((2โ†‘(4 ยท ๐‘›)) ยท (1 / (2โ†‘(4 ยท ๐‘›))))) = ((๐‘›โ†‘2) / ๐‘›))
285278, 280, 2843eqtrd 2771 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)))) = ((๐‘›โ†‘2) / ๐‘›))
286186, 200, 2853eqtrd 2771 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = ((๐‘›โ†‘2) / ๐‘›))
287286oveq1d 7429 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = (((๐‘›โ†‘2) / ๐‘›) / ((2 ยท ๐‘›) + 1)))
288236, 7, 172, 25, 184divdiv1d 12043 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘2) / ๐‘›) / ((2 ยท ๐‘›) + 1)) = ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1))))
289287, 288eqtrd 2767 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1))))
290289oveq2d 7430 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1))) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
291185, 290eqtrd 2767 . . . . 5 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))) / ((2 ยท ๐‘›) + 1)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
292165, 169, 2913eqtrd 2771 . . . 4 (๐‘› โˆˆ โ„• โ†’ ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
293142, 159, 2923eqtrd 2771 . . 3 (๐‘› โˆˆ โ„• โ†’ ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
294293mpteq2ia 5245 . 2 (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1))) = (๐‘› โˆˆ โ„• โ†ฆ ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
2951, 136, 2943eqtri 2759 1 ๐‘‰ = (๐‘› โˆˆ โ„• โ†ฆ ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
Colors of variables: wff setvar class
Syntax hints:   โˆง wa 395   = wceq 1534   โˆˆ wcel 2099   โ‰  wne 2935   class class class wbr 5142   โ†ฆ cmpt 5225  โ€˜cfv 6542  (class class class)co 7414  โ„‚cc 11128  โ„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   ยท cmul 11135   โ‰ค cle 11271   / cdiv 11893  โ„•cn 12234  2c2 12289  4c4 12291  โ„•0cn0 12494  โ„คcz 12580  โ„+crp 12998  โ†‘cexp 14050  !cfa 14256  โˆšcsqrt 15204  eceu 16030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-pm 8839  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-sup 9457  df-inf 9458  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-n0 12495  df-z 12581  df-uz 12845  df-q 12955  df-rp 12999  df-ico 13354  df-fz 13509  df-fzo 13652  df-fl 13781  df-seq 13991  df-exp 14051  df-fac 14257  df-bc 14286  df-hash 14314  df-shft 15038  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-limsup 15439  df-clim 15456  df-rlim 15457  df-sum 15657  df-ef 16035  df-e 16036
This theorem is referenced by:  stirlinglem15  45399
  Copyright terms: Public domain W3C validator