Metamath Proof Explorer


Theorem faclbnd

Description: A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005)

Ref Expression
Assertion faclbnd ( ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ( ๐‘ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘ ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 โŠข ( ๐‘€ โˆˆ โ„•0 โ†” ( ๐‘€ โˆˆ โ„• โˆจ ๐‘€ = 0 ) )
2 oveq1 โŠข ( ๐‘— = 0 โ†’ ( ๐‘— + 1 ) = ( 0 + 1 ) )
3 2 oveq2d โŠข ( ๐‘— = 0 โ†’ ( ๐‘€ โ†‘ ( ๐‘— + 1 ) ) = ( ๐‘€ โ†‘ ( 0 + 1 ) ) )
4 fveq2 โŠข ( ๐‘— = 0 โ†’ ( ! โ€˜ ๐‘— ) = ( ! โ€˜ 0 ) )
5 4 oveq2d โŠข ( ๐‘— = 0 โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘— ) ) = ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ 0 ) ) )
6 3 5 breq12d โŠข ( ๐‘— = 0 โ†’ ( ( ๐‘€ โ†‘ ( ๐‘— + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘— ) ) โ†” ( ๐‘€ โ†‘ ( 0 + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ 0 ) ) ) )
7 6 imbi2d โŠข ( ๐‘— = 0 โ†’ ( ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( ๐‘— + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘— ) ) ) โ†” ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( 0 + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ 0 ) ) ) ) )
8 oveq1 โŠข ( ๐‘— = ๐‘˜ โ†’ ( ๐‘— + 1 ) = ( ๐‘˜ + 1 ) )
9 8 oveq2d โŠข ( ๐‘— = ๐‘˜ โ†’ ( ๐‘€ โ†‘ ( ๐‘— + 1 ) ) = ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) )
10 fveq2 โŠข ( ๐‘— = ๐‘˜ โ†’ ( ! โ€˜ ๐‘— ) = ( ! โ€˜ ๐‘˜ ) )
11 10 oveq2d โŠข ( ๐‘— = ๐‘˜ โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘— ) ) = ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) )
12 9 11 breq12d โŠข ( ๐‘— = ๐‘˜ โ†’ ( ( ๐‘€ โ†‘ ( ๐‘— + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘— ) ) โ†” ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) )
13 12 imbi2d โŠข ( ๐‘— = ๐‘˜ โ†’ ( ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( ๐‘— + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘— ) ) ) โ†” ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) ) )
14 oveq1 โŠข ( ๐‘— = ( ๐‘˜ + 1 ) โ†’ ( ๐‘— + 1 ) = ( ( ๐‘˜ + 1 ) + 1 ) )
15 14 oveq2d โŠข ( ๐‘— = ( ๐‘˜ + 1 ) โ†’ ( ๐‘€ โ†‘ ( ๐‘— + 1 ) ) = ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) )
16 fveq2 โŠข ( ๐‘— = ( ๐‘˜ + 1 ) โ†’ ( ! โ€˜ ๐‘— ) = ( ! โ€˜ ( ๐‘˜ + 1 ) ) )
17 16 oveq2d โŠข ( ๐‘— = ( ๐‘˜ + 1 ) โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘— ) ) = ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) )
18 15 17 breq12d โŠข ( ๐‘— = ( ๐‘˜ + 1 ) โ†’ ( ( ๐‘€ โ†‘ ( ๐‘— + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘— ) ) โ†” ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
19 18 imbi2d โŠข ( ๐‘— = ( ๐‘˜ + 1 ) โ†’ ( ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( ๐‘— + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘— ) ) ) โ†” ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) ) ) )
20 oveq1 โŠข ( ๐‘— = ๐‘ โ†’ ( ๐‘— + 1 ) = ( ๐‘ + 1 ) )
21 20 oveq2d โŠข ( ๐‘— = ๐‘ โ†’ ( ๐‘€ โ†‘ ( ๐‘— + 1 ) ) = ( ๐‘€ โ†‘ ( ๐‘ + 1 ) ) )
22 fveq2 โŠข ( ๐‘— = ๐‘ โ†’ ( ! โ€˜ ๐‘— ) = ( ! โ€˜ ๐‘ ) )
23 22 oveq2d โŠข ( ๐‘— = ๐‘ โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘— ) ) = ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘ ) ) )
24 21 23 breq12d โŠข ( ๐‘— = ๐‘ โ†’ ( ( ๐‘€ โ†‘ ( ๐‘— + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘— ) ) โ†” ( ๐‘€ โ†‘ ( ๐‘ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘ ) ) ) )
25 24 imbi2d โŠข ( ๐‘— = ๐‘ โ†’ ( ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( ๐‘— + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘— ) ) ) โ†” ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( ๐‘ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘ ) ) ) ) )
26 nnre โŠข ( ๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„ )
27 nnge1 โŠข ( ๐‘€ โˆˆ โ„• โ†’ 1 โ‰ค ๐‘€ )
28 elnnuz โŠข ( ๐‘€ โˆˆ โ„• โ†” ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) )
29 28 biimpi โŠข ( ๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) )
30 26 27 29 leexp2ad โŠข ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ 1 ) โ‰ค ( ๐‘€ โ†‘ ๐‘€ ) )
31 0p1e1 โŠข ( 0 + 1 ) = 1
32 31 oveq2i โŠข ( ๐‘€ โ†‘ ( 0 + 1 ) ) = ( ๐‘€ โ†‘ 1 )
33 32 a1i โŠข ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( 0 + 1 ) ) = ( ๐‘€ โ†‘ 1 ) )
34 fac0 โŠข ( ! โ€˜ 0 ) = 1
35 34 oveq2i โŠข ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ 0 ) ) = ( ( ๐‘€ โ†‘ ๐‘€ ) ยท 1 )
36 nnnn0 โŠข ( ๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„•0 )
37 26 36 reexpcld โŠข ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ๐‘€ ) โˆˆ โ„ )
38 37 recnd โŠข ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ๐‘€ ) โˆˆ โ„‚ )
39 38 mulid1d โŠข ( ๐‘€ โˆˆ โ„• โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท 1 ) = ( ๐‘€ โ†‘ ๐‘€ ) )
40 35 39 eqtrid โŠข ( ๐‘€ โˆˆ โ„• โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ 0 ) ) = ( ๐‘€ โ†‘ ๐‘€ ) )
41 30 33 40 3brtr4d โŠข ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( 0 + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ 0 ) ) )
42 26 ad3antrrr โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ๐‘€ โˆˆ โ„ )
43 simpllr โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ๐‘˜ โˆˆ โ„•0 )
44 peano2nn0 โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„•0 )
45 43 44 syl โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„•0 )
46 42 45 reexpcld โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โˆˆ โ„ )
47 36 ad3antrrr โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ๐‘€ โˆˆ โ„•0 )
48 42 47 reexpcld โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ๐‘€ โ†‘ ๐‘€ ) โˆˆ โ„ )
49 43 faccld โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ! โ€˜ ๐‘˜ ) โˆˆ โ„• )
50 49 nnred โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ! โ€˜ ๐‘˜ ) โˆˆ โ„ )
51 48 50 remulcld โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) โˆˆ โ„ )
52 nn0re โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„ )
53 peano2re โŠข ( ๐‘˜ โˆˆ โ„ โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„ )
54 43 52 53 3syl โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„ )
55 nngt0 โŠข ( ๐‘€ โˆˆ โ„• โ†’ 0 < ๐‘€ )
56 55 ad3antrrr โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ 0 < ๐‘€ )
57 0re โŠข 0 โˆˆ โ„
58 ltle โŠข ( ( 0 โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„ ) โ†’ ( 0 < ๐‘€ โ†’ 0 โ‰ค ๐‘€ ) )
59 57 58 mpan โŠข ( ๐‘€ โˆˆ โ„ โ†’ ( 0 < ๐‘€ โ†’ 0 โ‰ค ๐‘€ ) )
60 42 56 59 sylc โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ 0 โ‰ค ๐‘€ )
61 42 45 60 expge0d โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ 0 โ‰ค ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) )
62 simplr โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) )
63 simprr โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ๐‘€ โ‰ค ( ๐‘˜ + 1 ) )
64 46 51 42 54 61 60 62 63 lemul12ad โŠข ( ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โˆง ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) ยท ๐‘€ ) โ‰ค ( ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ยท ( ๐‘˜ + 1 ) ) )
65 64 anandis โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) ยท ๐‘€ ) โ‰ค ( ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ยท ( ๐‘˜ + 1 ) ) )
66 nncn โŠข ( ๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„‚ )
67 expp1 โŠข ( ( ๐‘€ โˆˆ โ„‚ โˆง ( ๐‘˜ + 1 ) โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) = ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) ยท ๐‘€ ) )
68 66 44 67 syl2an โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) = ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) ยท ๐‘€ ) )
69 68 adantr โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) = ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) ยท ๐‘€ ) )
70 facp1 โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ! โ€˜ ( ๐‘˜ + 1 ) ) = ( ( ! โ€˜ ๐‘˜ ) ยท ( ๐‘˜ + 1 ) ) )
71 70 adantl โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ! โ€˜ ( ๐‘˜ + 1 ) ) = ( ( ! โ€˜ ๐‘˜ ) ยท ( ๐‘˜ + 1 ) ) )
72 71 oveq2d โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) = ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ( ! โ€˜ ๐‘˜ ) ยท ( ๐‘˜ + 1 ) ) ) )
73 38 adantr โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ๐‘€ ) โˆˆ โ„‚ )
74 faccl โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ! โ€˜ ๐‘˜ ) โˆˆ โ„• )
75 74 nncnd โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ! โ€˜ ๐‘˜ ) โˆˆ โ„‚ )
76 75 adantl โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ! โ€˜ ๐‘˜ ) โˆˆ โ„‚ )
77 nn0cn โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„‚ )
78 peano2cn โŠข ( ๐‘˜ โˆˆ โ„‚ โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„‚ )
79 77 78 syl โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„‚ )
80 79 adantl โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„‚ )
81 73 76 80 mulassd โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ยท ( ๐‘˜ + 1 ) ) = ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ( ! โ€˜ ๐‘˜ ) ยท ( ๐‘˜ + 1 ) ) ) )
82 72 81 eqtr4d โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) = ( ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ยท ( ๐‘˜ + 1 ) ) )
83 82 adantr โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) = ( ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ยท ( ๐‘˜ + 1 ) ) )
84 65 69 83 3brtr4d โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) โˆง ๐‘€ โ‰ค ( ๐‘˜ + 1 ) ) ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) )
85 84 exp32 โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) โ†’ ( ๐‘€ โ‰ค ( ๐‘˜ + 1 ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) ) ) )
86 85 com23 โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ‰ค ( ๐‘˜ + 1 ) โ†’ ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) ) ) )
87 nn0ltp1le โŠข ( ( ( ๐‘˜ + 1 ) โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( ๐‘˜ + 1 ) < ๐‘€ โ†” ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) )
88 44 36 87 syl2anr โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘˜ + 1 ) < ๐‘€ โ†” ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) )
89 peano2nn0 โŠข ( ( ๐‘˜ + 1 ) โˆˆ โ„•0 โ†’ ( ( ๐‘˜ + 1 ) + 1 ) โˆˆ โ„•0 )
90 44 89 syl โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ( ๐‘˜ + 1 ) + 1 ) โˆˆ โ„•0 )
91 reexpcl โŠข ( ( ๐‘€ โˆˆ โ„ โˆง ( ( ๐‘˜ + 1 ) + 1 ) โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โˆˆ โ„ )
92 26 90 91 syl2an โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โˆˆ โ„ )
93 92 adantr โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โˆˆ โ„ )
94 37 ad2antrr โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ( ๐‘€ โ†‘ ๐‘€ ) โˆˆ โ„ )
95 44 faccld โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ! โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„• )
96 95 nnred โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ! โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„ )
97 remulcl โŠข ( ( ( ๐‘€ โ†‘ ๐‘€ ) โˆˆ โ„ โˆง ( ! โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„ ) โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) โˆˆ โ„ )
98 37 96 97 syl2an โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) โˆˆ โ„ )
99 98 adantr โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) โˆˆ โ„ )
100 26 ad2antrr โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ๐‘€ โˆˆ โ„ )
101 27 ad2antrr โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ 1 โ‰ค ๐‘€ )
102 simpr โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ )
103 90 ad2antlr โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ( ( ๐‘˜ + 1 ) + 1 ) โˆˆ โ„•0 )
104 103 nn0zd โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ( ( ๐‘˜ + 1 ) + 1 ) โˆˆ โ„ค )
105 nnz โŠข ( ๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„ค )
106 105 ad2antrr โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ๐‘€ โˆˆ โ„ค )
107 eluz โŠข ( ( ( ( ๐‘˜ + 1 ) + 1 ) โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค ) โ†’ ( ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘˜ + 1 ) + 1 ) ) โ†” ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) )
108 104 106 107 syl2anc โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ( ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘˜ + 1 ) + 1 ) ) โ†” ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) )
109 102 108 mpbird โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘˜ + 1 ) + 1 ) ) )
110 100 101 109 leexp2ad โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ๐‘€ โ†‘ ๐‘€ ) )
111 37 96 anim12i โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) โˆˆ โ„ โˆง ( ! โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„ ) )
112 nn0re โŠข ( ๐‘€ โˆˆ โ„•0 โ†’ ๐‘€ โˆˆ โ„ )
113 id โŠข ( ๐‘€ โˆˆ โ„•0 โ†’ ๐‘€ โˆˆ โ„•0 )
114 nn0ge0 โŠข ( ๐‘€ โˆˆ โ„•0 โ†’ 0 โ‰ค ๐‘€ )
115 112 113 114 expge0d โŠข ( ๐‘€ โˆˆ โ„•0 โ†’ 0 โ‰ค ( ๐‘€ โ†‘ ๐‘€ ) )
116 36 115 syl โŠข ( ๐‘€ โˆˆ โ„• โ†’ 0 โ‰ค ( ๐‘€ โ†‘ ๐‘€ ) )
117 95 nnge1d โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ 1 โ‰ค ( ! โ€˜ ( ๐‘˜ + 1 ) ) )
118 116 117 anim12i โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( 0 โ‰ค ( ๐‘€ โ†‘ ๐‘€ ) โˆง 1 โ‰ค ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) )
119 lemulge11 โŠข ( ( ( ( ๐‘€ โ†‘ ๐‘€ ) โˆˆ โ„ โˆง ( ! โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„ ) โˆง ( 0 โ‰ค ( ๐‘€ โ†‘ ๐‘€ ) โˆง 1 โ‰ค ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) ) โ†’ ( ๐‘€ โ†‘ ๐‘€ ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) )
120 111 118 119 syl2anc โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ๐‘€ ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) )
121 120 adantr โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ( ๐‘€ โ†‘ ๐‘€ ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) )
122 93 94 99 110 121 letrd โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โˆง ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) )
123 122 ex โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ๐‘˜ + 1 ) + 1 ) โ‰ค ๐‘€ โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
124 88 123 sylbid โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘˜ + 1 ) < ๐‘€ โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
125 124 a1dd โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘˜ + 1 ) < ๐‘€ โ†’ ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) ) ) )
126 52 53 syl โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„ )
127 lelttric โŠข ( ( ๐‘€ โˆˆ โ„ โˆง ( ๐‘˜ + 1 ) โˆˆ โ„ ) โ†’ ( ๐‘€ โ‰ค ( ๐‘˜ + 1 ) โˆจ ( ๐‘˜ + 1 ) < ๐‘€ ) )
128 26 126 127 syl2an โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ‰ค ( ๐‘˜ + 1 ) โˆจ ( ๐‘˜ + 1 ) < ๐‘€ ) )
129 86 125 128 mpjaod โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
130 129 expcom โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ๐‘€ โˆˆ โ„• โ†’ ( ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) ) ) )
131 130 a2d โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( ๐‘˜ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘˜ ) ) ) โ†’ ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( ( ๐‘˜ + 1 ) + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ( ๐‘˜ + 1 ) ) ) ) ) )
132 7 13 19 25 41 131 nn0ind โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ๐‘€ โˆˆ โ„• โ†’ ( ๐‘€ โ†‘ ( ๐‘ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘ ) ) ) )
133 132 impcom โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ( ๐‘ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘ ) ) )
134 faccl โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ! โ€˜ ๐‘ ) โˆˆ โ„• )
135 134 nnnn0d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ! โ€˜ ๐‘ ) โˆˆ โ„•0 )
136 135 nn0ge0d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ 0 โ‰ค ( ! โ€˜ ๐‘ ) )
137 nn0p1nn โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ๐‘ + 1 ) โˆˆ โ„• )
138 137 0expd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 0 โ†‘ ( ๐‘ + 1 ) ) = 0 )
139 0exp0e1 โŠข ( 0 โ†‘ 0 ) = 1
140 139 oveq1i โŠข ( ( 0 โ†‘ 0 ) ยท ( ! โ€˜ ๐‘ ) ) = ( 1 ยท ( ! โ€˜ ๐‘ ) )
141 134 nncnd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ! โ€˜ ๐‘ ) โˆˆ โ„‚ )
142 141 mulid2d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 1 ยท ( ! โ€˜ ๐‘ ) ) = ( ! โ€˜ ๐‘ ) )
143 140 142 eqtrid โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( 0 โ†‘ 0 ) ยท ( ! โ€˜ ๐‘ ) ) = ( ! โ€˜ ๐‘ ) )
144 136 138 143 3brtr4d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 0 โ†‘ ( ๐‘ + 1 ) ) โ‰ค ( ( 0 โ†‘ 0 ) ยท ( ! โ€˜ ๐‘ ) ) )
145 oveq1 โŠข ( ๐‘€ = 0 โ†’ ( ๐‘€ โ†‘ ( ๐‘ + 1 ) ) = ( 0 โ†‘ ( ๐‘ + 1 ) ) )
146 oveq12 โŠข ( ( ๐‘€ = 0 โˆง ๐‘€ = 0 ) โ†’ ( ๐‘€ โ†‘ ๐‘€ ) = ( 0 โ†‘ 0 ) )
147 146 anidms โŠข ( ๐‘€ = 0 โ†’ ( ๐‘€ โ†‘ ๐‘€ ) = ( 0 โ†‘ 0 ) )
148 147 oveq1d โŠข ( ๐‘€ = 0 โ†’ ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘ ) ) = ( ( 0 โ†‘ 0 ) ยท ( ! โ€˜ ๐‘ ) ) )
149 145 148 breq12d โŠข ( ๐‘€ = 0 โ†’ ( ( ๐‘€ โ†‘ ( ๐‘ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘ ) ) โ†” ( 0 โ†‘ ( ๐‘ + 1 ) ) โ‰ค ( ( 0 โ†‘ 0 ) ยท ( ! โ€˜ ๐‘ ) ) ) )
150 144 149 syl5ibr โŠข ( ๐‘€ = 0 โ†’ ( ๐‘ โˆˆ โ„•0 โ†’ ( ๐‘€ โ†‘ ( ๐‘ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘ ) ) ) )
151 150 imp โŠข ( ( ๐‘€ = 0 โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ( ๐‘ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘ ) ) )
152 133 151 jaoian โŠข ( ( ( ๐‘€ โˆˆ โ„• โˆจ ๐‘€ = 0 ) โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ( ๐‘ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘ ) ) )
153 1 152 sylanb โŠข ( ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐‘€ โ†‘ ( ๐‘ + 1 ) ) โ‰ค ( ( ๐‘€ โ†‘ ๐‘€ ) ยท ( ! โ€˜ ๐‘ ) ) )