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 44391
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 12427 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•0)
3 faccl 14190 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„•0 โ†’ (!โ€˜๐‘›) โˆˆ โ„•)
4 nncn 12168 . . . . . . . . . . . . 13 ((!โ€˜๐‘›) โˆˆ โ„• โ†’ (!โ€˜๐‘›) โˆˆ โ„‚)
52, 3, 43syl 18 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (!โ€˜๐‘›) โˆˆ โ„‚)
6 2cnd 12238 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„‚)
7 nncn 12168 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„‚)
86, 7mulcld 11182 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„‚)
98sqrtcld 15329 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (โˆšโ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
10 ere 15978 . . . . . . . . . . . . . . . . 17 e โˆˆ โ„
1110recni 11176 . . . . . . . . . . . . . . . 16 e โˆˆ โ„‚
1211a1i 11 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ e โˆˆ โ„‚)
13 epos 16096 . . . . . . . . . . . . . . . . 17 0 < e
1410, 13gt0ne0ii 11698 . . . . . . . . . . . . . . . 16 e โ‰  0
1514a1i 11 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ e โ‰  0)
167, 12, 15divcld 11938 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (๐‘› / e) โˆˆ โ„‚)
1716, 2expcld 14058 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘๐‘›) โˆˆ โ„‚)
189, 17mulcld 11182 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)) โˆˆ โ„‚)
19 2rp 12927 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„+
2019a1i 11 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„+)
21 nnrp 12933 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„+)
2220, 21rpmulcld 12980 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„+)
2322sqrtgt0d 15304 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ 0 < (โˆšโ€˜(2 ยท ๐‘›)))
2423gt0ne0d 11726 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (โˆšโ€˜(2 ยท ๐‘›)) โ‰  0)
25 nnne0 12194 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ๐‘› โ‰  0)
267, 12, 25, 15divne0d 11954 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (๐‘› / e) โ‰  0)
27 nnz 12527 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„ค)
2816, 26, 27expne0d 14064 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘๐‘›) โ‰  0)
299, 17, 24, 28mulne0d 11814 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)) โ‰  0)
305, 18, 29divcld 11938 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) โˆˆ โ„‚)
31 stirlinglem3.1 . . . . . . . . . . . 12 ๐ด = (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
3231fvmpt2 6964 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) โˆˆ โ„‚) โ†’ (๐ดโ€˜๐‘›) = ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
3330, 32mpdan 686 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜๐‘›) = ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
3433oveq1d 7377 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((๐ดโ€˜๐‘›)โ†‘4) = (((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ†‘4))
35 stirlinglem3.3 . . . . . . . . . . . 12 ๐ธ = (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))
3635fvmpt2 6964 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)) โˆˆ โ„‚) โ†’ (๐ธโ€˜๐‘›) = ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))
3718, 36mpdan 686 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜๐‘›) = ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))
3837oveq1d 7377 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜๐‘›)โ†‘4) = (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4))
3934, 38oveq12d 7380 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) = ((((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ†‘4) ยท (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)))
40 4nn0 12439 . . . . . . . . . . 11 4 โˆˆ โ„•0
4140a1i 11 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ 4 โˆˆ โ„•0)
425, 18, 29, 41expdivd 14072 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ†‘4) = (((!โ€˜๐‘›)โ†‘4) / (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)))
4342oveq1d 7377 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ†‘4) ยท (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)) = ((((!โ€˜๐‘›)โ†‘4) / (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)) ยท (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)))
445, 41expcld 14058 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜๐‘›)โ†‘4) โˆˆ โ„‚)
4518, 41expcld 14058 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) โˆˆ โ„‚)
4641nn0zd 12532 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ 4 โˆˆ โ„ค)
4718, 29, 46expne0d 14064 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) โ‰  0)
4844, 45, 47divcan1d 11939 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜๐‘›)โ†‘4) / (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)) ยท (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4)) = ((!โ€˜๐‘›)โ†‘4))
4939, 43, 483eqtrd 2781 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) = ((!โ€˜๐‘›)โ†‘4))
5049eqcomd 2743 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜๐‘›)โ†‘4) = (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)))
5150oveq2d 7378 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) = ((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))))
52 2nn0 12437 . . . . . . . . . . . . 13 2 โˆˆ โ„•0
5352a1i 11 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„•0)
5453, 2nn0mulcld 12485 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„•0)
55 faccl 14190 . . . . . . . . . . 11 ((2 ยท ๐‘›) โˆˆ โ„•0 โ†’ (!โ€˜(2 ยท ๐‘›)) โˆˆ โ„•)
56 nncn 12168 . . . . . . . . . . 11 ((!โ€˜(2 ยท ๐‘›)) โˆˆ โ„• โ†’ (!โ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
5754, 55, 563syl 18 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
5857sqcld 14056 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›))โ†‘2) โˆˆ โ„‚)
596, 8mulcld 11182 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (2 ยท (2 ยท ๐‘›)) โˆˆ โ„‚)
6059sqrtcld 15329 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (โˆšโ€˜(2 ยท (2 ยท ๐‘›))) โˆˆ โ„‚)
618, 12, 15divcld 11938 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) / e) โˆˆ โ„‚)
6261, 54expcld 14058 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)) โˆˆ โ„‚)
6360, 62mulcld 11182 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))) โˆˆ โ„‚)
6463sqcld 14056 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2) โˆˆ โ„‚)
6520, 22rpmulcld 12980 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (2 ยท (2 ยท ๐‘›)) โˆˆ โ„+)
6665sqrtgt0d 15304 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 0 < (โˆšโ€˜(2 ยท (2 ยท ๐‘›))))
6766gt0ne0d 11726 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (โˆšโ€˜(2 ยท (2 ยท ๐‘›))) โ‰  0)
6820rpne0d 12969 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ 2 โ‰  0)
696, 7, 68, 25mulne0d 11814 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โ‰  0)
708, 12, 69, 15divne0d 11954 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) / e) โ‰  0)
71 2z 12542 . . . . . . . . . . . . . 14 2 โˆˆ โ„ค
7271a1i 11 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„ค)
7372, 27zmulcld 12620 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„ค)
7461, 70, 73expne0d 14064 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)) โ‰  0)
7560, 62, 67, 74mulne0d 11814 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))) โ‰  0)
7663, 75, 72expne0d 14064 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2) โ‰  0)
7758, 64, 76divcan1d 11939 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜(2 ยท ๐‘›))โ†‘2) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = ((!โ€˜(2 ยท ๐‘›))โ†‘2))
7857, 63, 75, 53expdivd 14072 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) = (((!โ€˜(2 ยท ๐‘›))โ†‘2) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
7978eqcomd 2743 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((!โ€˜(2 ยท ๐‘›))โ†‘2) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = (((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2))
8079oveq1d 7377 . . . . . . . 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 2779 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›))โ†‘2) = ((((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
82 fveq2 6847 . . . . . . . . . . . . . 14 (๐‘› = ๐‘š โ†’ (!โ€˜๐‘›) = (!โ€˜๐‘š))
83 oveq2 7370 . . . . . . . . . . . . . . . 16 (๐‘› = ๐‘š โ†’ (2 ยท ๐‘›) = (2 ยท ๐‘š))
8483fveq2d 6851 . . . . . . . . . . . . . . 15 (๐‘› = ๐‘š โ†’ (โˆšโ€˜(2 ยท ๐‘›)) = (โˆšโ€˜(2 ยท ๐‘š)))
85 oveq1 7369 . . . . . . . . . . . . . . . 16 (๐‘› = ๐‘š โ†’ (๐‘› / e) = (๐‘š / e))
86 id 22 . . . . . . . . . . . . . . . 16 (๐‘› = ๐‘š โ†’ ๐‘› = ๐‘š)
8785, 86oveq12d 7380 . . . . . . . . . . . . . . 15 (๐‘› = ๐‘š โ†’ ((๐‘› / e)โ†‘๐‘›) = ((๐‘š / e)โ†‘๐‘š))
8884, 87oveq12d 7380 . . . . . . . . . . . . . 14 (๐‘› = ๐‘š โ†’ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)) = ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))
8982, 88oveq12d 7380 . . . . . . . . . . . . 13 (๐‘› = ๐‘š โ†’ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) = ((!โ€˜๐‘š) / ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
9089cbvmptv 5223 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†ฆ ((!โ€˜๐‘›) / ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))) = (๐‘š โˆˆ โ„• โ†ฆ ((!โ€˜๐‘š) / ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
9131, 90eqtri 2765 . . . . . . . . . . 11 ๐ด = (๐‘š โˆˆ โ„• โ†ฆ ((!โ€˜๐‘š) / ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
92 fveq2 6847 . . . . . . . . . . . 12 (๐‘š = (2 ยท ๐‘›) โ†’ (!โ€˜๐‘š) = (!โ€˜(2 ยท ๐‘›)))
93 oveq2 7370 . . . . . . . . . . . . . 14 (๐‘š = (2 ยท ๐‘›) โ†’ (2 ยท ๐‘š) = (2 ยท (2 ยท ๐‘›)))
9493fveq2d 6851 . . . . . . . . . . . . 13 (๐‘š = (2 ยท ๐‘›) โ†’ (โˆšโ€˜(2 ยท ๐‘š)) = (โˆšโ€˜(2 ยท (2 ยท ๐‘›))))
95 oveq1 7369 . . . . . . . . . . . . . 14 (๐‘š = (2 ยท ๐‘›) โ†’ (๐‘š / e) = ((2 ยท ๐‘›) / e))
96 id 22 . . . . . . . . . . . . . 14 (๐‘š = (2 ยท ๐‘›) โ†’ ๐‘š = (2 ยท ๐‘›))
9795, 96oveq12d 7380 . . . . . . . . . . . . 13 (๐‘š = (2 ยท ๐‘›) โ†’ ((๐‘š / e)โ†‘๐‘š) = (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))
9894, 97oveq12d 7380 . . . . . . . . . . . 12 (๐‘š = (2 ยท ๐‘›) โ†’ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)) = ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))
9992, 98oveq12d 7380 . . . . . . . . . . 11 (๐‘š = (2 ยท ๐‘›) โ†’ ((!โ€˜๐‘š) / ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))) = ((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))))
100 2nn 12233 . . . . . . . . . . . . 13 2 โˆˆ โ„•
101100a1i 11 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„•)
102 id 22 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•)
103101, 102nnmulcld 12213 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„•)
10457, 63, 75divcld 11938 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))) โˆˆ โ„‚)
10591, 99, 103, 104fvmptd3 6976 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜(2 ยท ๐‘›)) = ((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))))
106105oveq1d 7377 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) = (((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2))
107106eqcomd 2743 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) = ((๐ดโ€˜(2 ยท ๐‘›))โ†‘2))
108107oveq1d 7377 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
109 eqidd 2738 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))) = (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
11098adantl 483 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„• โˆง ๐‘š = (2 ยท ๐‘›)) โ†’ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)) = ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))
111109, 110, 103, 63fvmptd 6960 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›)) = ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))
112111oveq1d 7377 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2) = (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2))
113112eqcomd 2743 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2) = (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2))
114113oveq2d 7378 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2)))
11581, 108, 1143eqtrd 2781 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›))โ†‘2) = (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2)))
11688cbvmptv 5223 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) = (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))
117116a1i 11 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))) = (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
118117fveq1d 6849 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›)) = ((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›)))
119118eqcomd 2743 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›)) = ((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›)))
120119oveq1d 7377 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2) = (((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›))โ†‘2))
121120oveq2d 7378 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š)))โ€˜(2 ยท ๐‘›))โ†‘2)) = (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›))โ†‘2)))
122105, 104eqeltrd 2838 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
123 stirlinglem3.2 . . . . . . . . . . 11 ๐ท = (๐‘› โˆˆ โ„• โ†ฆ (๐ดโ€˜(2 ยท ๐‘›)))
124123fvmpt2 6964 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง (๐ดโ€˜(2 ยท ๐‘›)) โˆˆ โ„‚) โ†’ (๐ทโ€˜๐‘›) = (๐ดโ€˜(2 ยท ๐‘›)))
125122, 124mpdan 686 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ทโ€˜๐‘›) = (๐ดโ€˜(2 ยท ๐‘›)))
126125eqcomd 2743 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜(2 ยท ๐‘›)) = (๐ทโ€˜๐‘›))
127126oveq1d 7377 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) = ((๐ทโ€˜๐‘›)โ†‘2))
12835a1i 11 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ๐ธ = (๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))))
129128fveq1d 6849 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜(2 ยท ๐‘›)) = ((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›)))
130129eqcomd 2743 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›)) = (๐ธโ€˜(2 ยท ๐‘›)))
131130oveq1d 7377 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›))โ†‘2) = ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))
132127, 131oveq12d 7380 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜(2 ยท ๐‘›))โ†‘2) ยท (((๐‘› โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›)))โ€˜(2 ยท ๐‘›))โ†‘2)) = (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))
133115, 121, 1323eqtrd 2781 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›))โ†‘2) = (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))
13451, 133oveq12d 7380 . . . 4 (๐‘› โˆˆ โ„• โ†’ (((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) = (((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
135134oveq1d 7377 . . 3 (๐‘› โˆˆ โ„• โ†’ ((((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) / ((2 ยท ๐‘›) + 1)) = ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
136135mpteq2ia 5213 . 2 (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท ((!โ€˜๐‘›)โ†‘4)) / ((!โ€˜(2 ยท ๐‘›))โ†‘2)) / ((2 ยท ๐‘›) + 1))) = (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
13741, 2nn0mulcld 12485 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (4 ยท ๐‘›) โˆˆ โ„•0)
1386, 137expcld 14058 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (2โ†‘(4 ยท ๐‘›)) โˆˆ โ„‚)
13949, 44eqeltrd 2838 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) โˆˆ โ„‚)
140138, 139mulcomd 11183 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) = ((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))))
141140oveq1d 7377 . . . . 5 (๐‘› โˆˆ โ„• โ†’ (((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
142141oveq1d 7377 . . . 4 (๐‘› โˆˆ โ„• โ†’ ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
143125, 122eqeltrd 2838 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ทโ€˜๐‘›) โˆˆ โ„‚)
144143sqcld 14056 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ทโ€˜๐‘›)โ†‘2) โˆˆ โ„‚)
145128, 117eqtrd 2777 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ๐ธ = (๐‘š โˆˆ โ„• โ†ฆ ((โˆšโ€˜(2 ยท ๐‘š)) ยท ((๐‘š / e)โ†‘๐‘š))))
146145, 110, 103, 63fvmptd 6960 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜(2 ยท ๐‘›)) = ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))))
147146, 63eqeltrd 2838 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜(2 ยท ๐‘›)) โˆˆ โ„‚)
148147sqcld 14056 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2) โˆˆ โ„‚)
149 nnne0 12194 . . . . . . . . . . . 12 ((!โ€˜(2 ยท ๐‘›)) โˆˆ โ„• โ†’ (!โ€˜(2 ยท ๐‘›)) โ‰  0)
15054, 55, 1493syl 18 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (!โ€˜(2 ยท ๐‘›)) โ‰  0)
15157, 63, 150, 75divne0d 11954 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((!โ€˜(2 ยท ๐‘›)) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))) โ‰  0)
152105, 151eqnetrd 3012 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜(2 ยท ๐‘›)) โ‰  0)
153125, 152eqnetrd 3012 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ทโ€˜๐‘›) โ‰  0)
154143, 153, 72expne0d 14064 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ทโ€˜๐‘›)โ†‘2) โ‰  0)
155146, 75eqnetrd 3012 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐ธโ€˜(2 ยท ๐‘›)) โ‰  0)
156147, 155, 72expne0d 14064 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2) โ‰  0)
157139, 144, 138, 148, 154, 156divmuldivd 11979 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
158157eqcomd 2743 . . . . 5 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
159158oveq1d 7377 . . . 4 (๐‘› โˆˆ โ„• โ†’ ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท (2โ†‘(4 ยท ๐‘›))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
16033, 30eqeltrd 2838 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐ดโ€˜๐‘›) โˆˆ โ„‚)
161160, 41expcld 14058 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐ดโ€˜๐‘›)โ†‘4) โˆˆ โ„‚)
16238, 45eqeltrd 2838 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜๐‘›)โ†‘4) โˆˆ โ„‚)
163161, 162, 144, 154div23d 11975 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)))
164163oveq1d 7377 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
165164oveq1d 7377 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)))
166161, 144, 154divcld 11938 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) โˆˆ โ„‚)
167138, 148, 156divcld 11938 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)) โˆˆ โ„‚)
168166, 162, 167mulassd 11185 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))))
169168oveq1d 7377 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐ธโ€˜๐‘›)โ†‘4)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))) / ((2 ยท ๐‘›) + 1)))
170162, 167mulcld 11182 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) โˆˆ โ„‚)
171 1cnd 11157 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ 1 โˆˆ โ„‚)
1728, 171addcld 11181 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โˆˆ โ„‚)
173 0red 11165 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ 0 โˆˆ โ„)
174103nnred 12175 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„)
175 2re 12234 . . . . . . . . . . . 12 2 โˆˆ โ„
176175a1i 11 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„)
177 nnre 12167 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„)
178176, 177remulcld 11192 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„)
179 1red 11163 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ 1 โˆˆ โ„)
180178, 179readdcld 11191 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โˆˆ โ„)
181103nngt0d 12209 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ 0 < (2 ยท ๐‘›))
182174ltp1d 12092 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) < ((2 ยท ๐‘›) + 1))
183173, 174, 180, 181, 182lttrd 11323 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ 0 < ((2 ยท ๐‘›) + 1))
184183gt0ne0d 11726 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โ‰  0)
185166, 170, 172, 184divassd 11973 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))) / ((2 ยท ๐‘›) + 1)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1))))
186162, 138, 148, 156div12d 11974 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = ((2โ†‘(4 ยท ๐‘›)) ยท (((๐ธโ€˜๐‘›)โ†‘4) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))))
1879, 17, 41mulexpd 14073 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) = (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) ยท (((๐‘› / e)โ†‘๐‘›)โ†‘4)))
18860, 62sqmuld 14070 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2) = (((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) ยท ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)))
189187, 188oveq12d 7380 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)) = ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) ยท (((๐‘› / e)โ†‘๐‘›)โ†‘4)) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) ยท ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))))
190146oveq1d 7377 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2) = (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2))
19138, 190oveq12d 7380 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)) = ((((โˆšโ€˜(2 ยท ๐‘›)) ยท ((๐‘› / e)โ†‘๐‘›))โ†‘4) / (((โˆšโ€˜(2 ยท (2 ยท ๐‘›))) ยท (((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›)))โ†‘2)))
1929, 41expcld 14058 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) โˆˆ โ„‚)
19360sqcld 14056 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) โˆˆ โ„‚)
19417, 41expcld 14058 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (((๐‘› / e)โ†‘๐‘›)โ†‘4) โˆˆ โ„‚)
19562sqcld 14056 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2) โˆˆ โ„‚)
19660, 67, 72expne0d 14064 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) โ‰  0)
19762, 74, 72expne0d 14064 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2) โ‰  0)
198192, 193, 194, 195, 196, 197divmuldivd 11979 . . . . . . . . . . . 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 2787 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)) = ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))))
200199oveq2d 7378 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (((๐ธโ€˜๐‘›)โ†‘4) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = ((2โ†‘(4 ยท ๐‘›)) ยท ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)))))
20165rprege0d 12971 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท (2 ยท ๐‘›)) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท (2 ยท ๐‘›))))
202 resqrtth 15147 . . . . . . . . . . . . . . . 16 (((2 ยท (2 ยท ๐‘›)) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท (2 ยท ๐‘›))) โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) = (2 ยท (2 ยท ๐‘›)))
203201, 202syl 17 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2) = (2 ยท (2 ยท ๐‘›)))
204203oveq2d 7378 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) = (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / (2 ยท (2 ยท ๐‘›))))
205 2t2e4 12324 . . . . . . . . . . . . . . . . . . 19 (2 ยท 2) = 4
206205eqcomi 2746 . . . . . . . . . . . . . . . . . 18 4 = (2 ยท 2)
207206a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ 4 = (2 ยท 2))
208207oveq2d 7378 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) = ((โˆšโ€˜(2 ยท ๐‘›))โ†‘(2 ยท 2)))
2099, 53, 53expmuld 14061 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘(2 ยท 2)) = (((โˆšโ€˜(2 ยท ๐‘›))โ†‘2)โ†‘2))
21022rprege0d 12971 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท ๐‘›)))
211 resqrtth 15147 . . . . . . . . . . . . . . . . . 18 (((2 ยท ๐‘›) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท ๐‘›)) โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘2) = (2 ยท ๐‘›))
212210, 211syl 17 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘2) = (2 ยท ๐‘›))
213212oveq1d 7377 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›))โ†‘2)โ†‘2) = ((2 ยท ๐‘›)โ†‘2))
214208, 209, 2133eqtrd 2781 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) = ((2 ยท ๐‘›)โ†‘2))
2156, 6, 7mulassd 11185 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท 2) ยท ๐‘›) = (2 ยท (2 ยท ๐‘›)))
216205a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (2 ยท 2) = 4)
217216oveq1d 7377 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท 2) ยท ๐‘›) = (4 ยท ๐‘›))
218215, 217eqtr3d 2779 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (2 ยท (2 ยท ๐‘›)) = (4 ยท ๐‘›))
219214, 218oveq12d 7380 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / (2 ยท (2 ยท ๐‘›))) = (((2 ยท ๐‘›)โ†‘2) / (4 ยท ๐‘›)))
2206, 7sqmuld 14070 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘2) = ((2โ†‘2) ยท (๐‘›โ†‘2)))
221 sq2 14108 . . . . . . . . . . . . . . . . . . 19 (2โ†‘2) = 4
222221a1i 11 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ (2โ†‘2) = 4)
223222oveq1d 7377 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘2) ยท (๐‘›โ†‘2)) = (4 ยท (๐‘›โ†‘2)))
224220, 223eqtrd 2777 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘2) = (4 ยท (๐‘›โ†‘2)))
225224oveq1d 7377 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›)โ†‘2) / (4 ยท ๐‘›)) = ((4 ยท (๐‘›โ†‘2)) / (4 ยท ๐‘›)))
226 4cn 12245 . . . . . . . . . . . . . . . . . . 19 4 โˆˆ โ„‚
227 4ne0 12268 . . . . . . . . . . . . . . . . . . 19 4 โ‰  0
228226, 227dividi 11895 . . . . . . . . . . . . . . . . . 18 (4 / 4) = 1
229228a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (4 / 4) = 1)
2307sqvald 14055 . . . . . . . . . . . . . . . . . . 19 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘2) = (๐‘› ยท ๐‘›))
231230oveq1d 7377 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘2) / ๐‘›) = ((๐‘› ยท ๐‘›) / ๐‘›))
2327, 7, 25divcan4d 11944 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ ((๐‘› ยท ๐‘›) / ๐‘›) = ๐‘›)
233231, 232eqtrd 2777 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘2) / ๐‘›) = ๐‘›)
234229, 233oveq12d 7380 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((4 / 4) ยท ((๐‘›โ†‘2) / ๐‘›)) = (1 ยท ๐‘›))
23541nn0cnd 12482 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ 4 โˆˆ โ„‚)
2367sqcld 14056 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘2) โˆˆ โ„‚)
237227a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ 4 โ‰  0)
238235, 235, 236, 7, 237, 25divmuldivd 11979 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((4 / 4) ยท ((๐‘›โ†‘2) / ๐‘›)) = ((4 ยท (๐‘›โ†‘2)) / (4 ยท ๐‘›)))
2397mulid2d 11180 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (1 ยท ๐‘›) = ๐‘›)
240234, 238, 2393eqtr3d 2785 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((4 ยท (๐‘›โ†‘2)) / (4 ยท ๐‘›)) = ๐‘›)
241225, 240eqtrd 2777 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›)โ†‘2) / (4 ยท ๐‘›)) = ๐‘›)
242204, 219, 2413eqtrd 2781 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) = ๐‘›)
2437, 235mulcomd 11183 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (๐‘› ยท 4) = (4 ยท ๐‘›))
244243oveq2d 7378 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘(๐‘› ยท 4)) = ((๐‘› / e)โ†‘(4 ยท ๐‘›)))
24516, 41, 2expmuld 14061 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘(๐‘› ยท 4)) = (((๐‘› / e)โ†‘๐‘›)โ†‘4))
2467, 12, 15, 137expdivd 14072 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((๐‘› / e)โ†‘(4 ยท ๐‘›)) = ((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))))
247244, 245, 2463eqtr3d 2785 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (((๐‘› / e)โ†‘๐‘›)โ†‘4) = ((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))))
2486, 7, 6mul32d 11372 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) ยท 2) = ((2 ยท 2) ยท ๐‘›))
249248, 217eqtrd 2777 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) ยท 2) = (4 ยท ๐‘›))
250249oveq2d 7378 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘((2 ยท ๐‘›) ยท 2)) = (((2 ยท ๐‘›) / e)โ†‘(4 ยท ๐‘›)))
25161, 53, 54expmuld 14061 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘((2 ยท ๐‘›) ยท 2)) = ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))
2528, 12, 15, 137expdivd 14072 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / e)โ†‘(4 ยท ๐‘›)) = (((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))))
253250, 251, 2523eqtr3d 2785 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2) = (((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))))
254247, 253oveq12d 7380 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)) = (((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) / (((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›)))))
255247, 194eqeltrrd 2839 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) โˆˆ โ„‚)
2568, 137expcld 14058 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) โˆˆ โ„‚)
25712, 137expcld 14058 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (eโ†‘(4 ยท ๐‘›)) โˆˆ โ„‚)
25846, 27zmulcld 12620 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (4 ยท ๐‘›) โˆˆ โ„ค)
2598, 69, 258expne0d 14064 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) โ‰  0)
26012, 15, 258expne0d 14064 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (eโ†‘(4 ยท ๐‘›)) โ‰  0)
261255, 256, 257, 259, 260divdiv2d 11970 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) / (((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›)))) = ((((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) ยท (eโ†‘(4 ยท ๐‘›))) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))))
2627, 137expcld 14058 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘(4 ยท ๐‘›)) โˆˆ โ„‚)
263262, 257, 260divcan1d 11939 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) ยท (eโ†‘(4 ยท ๐‘›))) = (๐‘›โ†‘(4 ยท ๐‘›)))
264263oveq1d 7377 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) ยท (eโ†‘(4 ยท ๐‘›))) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))) = ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))))
2656, 7, 137mulexpd 14073 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›)) = ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›))))
266265oveq2d 7378 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))) = ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›)))))
267138, 262mulcomd 11183 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›))) = ((๐‘›โ†‘(4 ยท ๐‘›)) ยท (2โ†‘(4 ยท ๐‘›))))
268267oveq2d 7378 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›)))) = ((๐‘›โ†‘(4 ยท ๐‘›)) / ((๐‘›โ†‘(4 ยท ๐‘›)) ยท (2โ†‘(4 ยท ๐‘›)))))
2697, 25, 258expne0d 14064 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (๐‘›โ†‘(4 ยท ๐‘›)) โ‰  0)
2706, 68, 258expne0d 14064 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ (2โ†‘(4 ยท ๐‘›)) โ‰  0)
271262, 262, 138, 269, 270divdiv1d 11969 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘(4 ยท ๐‘›)) / (๐‘›โ†‘(4 ยท ๐‘›))) / (2โ†‘(4 ยท ๐‘›))) = ((๐‘›โ†‘(4 ยท ๐‘›)) / ((๐‘›โ†‘(4 ยท ๐‘›)) ยท (2โ†‘(4 ยท ๐‘›)))))
272262, 269dividd 11936 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / (๐‘›โ†‘(4 ยท ๐‘›))) = 1)
273272oveq1d 7377 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘(4 ยท ๐‘›)) / (๐‘›โ†‘(4 ยท ๐‘›))) / (2โ†‘(4 ยท ๐‘›))) = (1 / (2โ†‘(4 ยท ๐‘›))))
274268, 271, 2733eqtr2d 2783 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ ((๐‘›โ†‘(4 ยท ๐‘›)) / ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘›โ†‘(4 ยท ๐‘›)))) = (1 / (2โ†‘(4 ยท ๐‘›))))
275264, 266, 2743eqtrd 2781 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ ((((๐‘›โ†‘(4 ยท ๐‘›)) / (eโ†‘(4 ยท ๐‘›))) ยท (eโ†‘(4 ยท ๐‘›))) / ((2 ยท ๐‘›)โ†‘(4 ยท ๐‘›))) = (1 / (2โ†‘(4 ยท ๐‘›))))
276254, 261, 2753eqtrd 2781 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)) = (1 / (2โ†‘(4 ยท ๐‘›))))
277242, 276oveq12d 7380 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2))) = (๐‘› ยท (1 / (2โ†‘(4 ยท ๐‘›)))))
278277oveq2d 7378 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)))) = ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘› ยท (1 / (2โ†‘(4 ยท ๐‘›))))))
279138, 270reccld 11931 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (1 / (2โ†‘(4 ยท ๐‘›))) โˆˆ โ„‚)
280138, 7, 279mul12d 11371 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (๐‘› ยท (1 / (2โ†‘(4 ยท ๐‘›))))) = (๐‘› ยท ((2โ†‘(4 ยท ๐‘›)) ยท (1 / (2โ†‘(4 ยท ๐‘›))))))
2817mulid1d 11179 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (๐‘› ยท 1) = ๐‘›)
282138, 270recidd 11933 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท (1 / (2โ†‘(4 ยท ๐‘›)))) = 1)
283282oveq2d 7378 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„• โ†’ (๐‘› ยท ((2โ†‘(4 ยท ๐‘›)) ยท (1 / (2โ†‘(4 ยท ๐‘›))))) = (๐‘› ยท 1))
284281, 283, 2333eqtr4d 2787 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (๐‘› ยท ((2โ†‘(4 ยท ๐‘›)) ยท (1 / (2โ†‘(4 ยท ๐‘›))))) = ((๐‘›โ†‘2) / ๐‘›))
285278, 280, 2843eqtrd 2781 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((2โ†‘(4 ยท ๐‘›)) ยท ((((โˆšโ€˜(2 ยท ๐‘›))โ†‘4) / ((โˆšโ€˜(2 ยท (2 ยท ๐‘›)))โ†‘2)) ยท ((((๐‘› / e)โ†‘๐‘›)โ†‘4) / ((((2 ยท ๐‘›) / e)โ†‘(2 ยท ๐‘›))โ†‘2)))) = ((๐‘›โ†‘2) / ๐‘›))
286186, 200, 2853eqtrd 2781 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) = ((๐‘›โ†‘2) / ๐‘›))
287286oveq1d 7377 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = (((๐‘›โ†‘2) / ๐‘›) / ((2 ยท ๐‘›) + 1)))
288236, 7, 172, 25, 184divdiv1d 11969 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((๐‘›โ†‘2) / ๐‘›) / ((2 ยท ๐‘›) + 1)) = ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1))))
289287, 288eqtrd 2777 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1))))
290289oveq2d 7378 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1))) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
291185, 290eqtrd 2777 . . . . 5 (๐‘› โˆˆ โ„• โ†’ (((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท (((๐ธโ€˜๐‘›)โ†‘4) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2)))) / ((2 ยท ๐‘›) + 1)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
292165, 169, 2913eqtrd 2781 . . . 4 (๐‘› โˆˆ โ„• โ†’ ((((((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4)) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((2โ†‘(4 ยท ๐‘›)) / ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
293142, 159, 2923eqtrd 2781 . . 3 (๐‘› โˆˆ โ„• โ†’ ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1)) = ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
294293mpteq2ia 5213 . 2 (๐‘› โˆˆ โ„• โ†ฆ ((((2โ†‘(4 ยท ๐‘›)) ยท (((๐ดโ€˜๐‘›)โ†‘4) ยท ((๐ธโ€˜๐‘›)โ†‘4))) / (((๐ทโ€˜๐‘›)โ†‘2) ยท ((๐ธโ€˜(2 ยท ๐‘›))โ†‘2))) / ((2 ยท ๐‘›) + 1))) = (๐‘› โˆˆ โ„• โ†ฆ ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
2951, 136, 2943eqtri 2769 1 ๐‘‰ = (๐‘› โˆˆ โ„• โ†ฆ ((((๐ดโ€˜๐‘›)โ†‘4) / ((๐ทโ€˜๐‘›)โ†‘2)) ยท ((๐‘›โ†‘2) / (๐‘› ยท ((2 ยท ๐‘›) + 1)))))
Colors of variables: wff setvar class
Syntax hints:   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944   class class class wbr 5110   โ†ฆ cmpt 5193  โ€˜cfv 6501  (class class class)co 7362  โ„‚cc 11056  โ„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   ยท cmul 11063   โ‰ค cle 11197   / cdiv 11819  โ„•cn 12160  2c2 12215  4c4 12217  โ„•0cn0 12420  โ„คcz 12506  โ„+crp 12922  โ†‘cexp 13974  !cfa 14180  โˆšcsqrt 15125  eceu 15952
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-n0 12421  df-z 12507  df-uz 12771  df-q 12881  df-rp 12923  df-ico 13277  df-fz 13432  df-fzo 13575  df-fl 13704  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-ef 15957  df-e 15958
This theorem is referenced by:  stirlinglem15  44403
  Copyright terms: Public domain W3C validator