Metamath Proof Explorer

Theorem fmtnorec4

Description: The fourth recurrence relation for Fermat numbers, see Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties . (Contributed by AV, 31-Jul-2021)

Ref Expression
Assertion fmtnorec4 ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( FermatNo โ€˜ ๐‘ ) = ( ( ( FermatNo โ€˜ ( ๐‘ โˆ’ 1 ) ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ( ( FermatNo โ€˜ ( ๐‘ โˆ’ 2 ) ) โˆ’ 1 ) โ†‘ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 eluz2nn โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ โˆˆ โ„• )
2 nnm1nn0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ โˆ’ 1 ) โˆˆ โ„•0 )
3 1 2 syl โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ๐‘ โˆ’ 1 ) โˆˆ โ„•0 )
4 fmtno โŠข ( ( ๐‘ โˆ’ 1 ) โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ( ๐‘ โˆ’ 1 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) )
5 3 4 syl โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( FermatNo โ€˜ ( ๐‘ โˆ’ 1 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) )
6 5 oveq1d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( FermatNo โ€˜ ( ๐‘ โˆ’ 1 ) ) โ†‘ 2 ) = ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) )
7 2nn โŠข 2 โˆˆ โ„•
8 7 a1i โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ 2 โˆˆ โ„• )
9 2nn0 โŠข 2 โˆˆ โ„•0
10 9 a1i โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ 2 โˆˆ โ„•0 )
11 10 3 nn0expcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) โˆˆ โ„•0 )
12 8 11 nnexpcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„• )
13 12 nncnd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„‚ )
14 binom21 โŠข ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„‚ โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) = ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) )
15 13 14 syl โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) = ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) )
16 2cn โŠข 2 โˆˆ โ„‚
17 16 a1i โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ 2 โˆˆ โ„‚ )
18 17 10 11 expmuld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ยท 2 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) )
19 17 3 expp1d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ( ๐‘ โˆ’ 1 ) + 1 ) ) = ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ยท 2 ) )
20 1 nncnd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ โˆˆ โ„‚ )
21 npcan1 โŠข ( ๐‘ โˆˆ โ„‚ โ†’ ( ( ๐‘ โˆ’ 1 ) + 1 ) = ๐‘ )
22 20 21 syl โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ๐‘ โˆ’ 1 ) + 1 ) = ๐‘ )
23 22 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ( ๐‘ โˆ’ 1 ) + 1 ) ) = ( 2 โ†‘ ๐‘ ) )
24 19 23 eqtr3d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ยท 2 ) = ( 2 โ†‘ ๐‘ ) )
25 24 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ยท 2 ) ) = ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) )
26 18 25 eqtr3d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) = ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) )
27 26 oveq1d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) )
28 27 oveq1d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) = ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) )
29 6 15 28 3eqtrd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( FermatNo โ€˜ ( ๐‘ โˆ’ 1 ) ) โ†‘ 2 ) = ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) )
30 uznn0sub โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ๐‘ โˆ’ 2 ) โˆˆ โ„•0 )
31 fmtno โŠข ( ( ๐‘ โˆ’ 2 ) โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ( ๐‘ โˆ’ 2 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) )
32 30 31 syl โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( FermatNo โ€˜ ( ๐‘ โˆ’ 2 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) )
33 32 oveq1d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( FermatNo โ€˜ ( ๐‘ โˆ’ 2 ) ) โˆ’ 1 ) = ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โˆ’ 1 ) )
34 33 oveq1d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( FermatNo โ€˜ ( ๐‘ โˆ’ 2 ) ) โˆ’ 1 ) โ†‘ 2 ) = ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โˆ’ 1 ) โ†‘ 2 ) )
35 10 30 nn0expcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) โˆˆ โ„•0 )
36 8 35 nnexpcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โˆˆ โ„• )
37 36 nncnd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โˆˆ โ„‚ )
38 peano2cn โŠข ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โˆˆ โ„‚ โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โˆˆ โ„‚ )
39 37 38 syl โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โˆˆ โ„‚ )
40 binom2sub1 โŠข ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โˆˆ โ„‚ โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โˆ’ 1 ) โ†‘ 2 ) = ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) + 1 ) )
41 39 40 syl โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โˆ’ 1 ) โ†‘ 2 ) = ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) + 1 ) )
42 binom21 โŠข ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โˆˆ โ„‚ โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โ†‘ 2 ) = ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) )
43 37 42 syl โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โ†‘ 2 ) = ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) )
44 43 oveq1d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) = ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) )
45 44 oveq1d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) + 1 ) = ( ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) + 1 ) )
46 34 41 45 3eqtrd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( FermatNo โ€˜ ( ๐‘ โˆ’ 2 ) ) โˆ’ 1 ) โ†‘ 2 ) = ( ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) + 1 ) )
47 46 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( ( FermatNo โ€˜ ( ๐‘ โˆ’ 2 ) ) โˆ’ 1 ) โ†‘ 2 ) ) = ( 2 ยท ( ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) + 1 ) ) )
48 29 47 oveq12d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( FermatNo โ€˜ ( ๐‘ โˆ’ 1 ) ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ( ( FermatNo โ€˜ ( ๐‘ โˆ’ 2 ) ) โˆ’ 1 ) โ†‘ 2 ) ) ) = ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) + 1 ) ) ) )
49 36 10 nnexpcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) โˆˆ โ„• )
50 49 nncnd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) โˆˆ โ„‚ )
51 17 37 mulcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) โˆˆ โ„‚ )
52 50 51 addcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) โˆˆ โ„‚ )
53 peano2cn โŠข ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) โˆˆ โ„‚ โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆˆ โ„‚ )
54 52 53 syl โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆˆ โ„‚ )
55 17 39 mulcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) โˆˆ โ„‚ )
56 54 55 subcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) โˆˆ โ„‚ )
57 1cnd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ 1 โˆˆ โ„‚ )
58 17 56 57 adddid โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) + 1 ) ) = ( ( 2 ยท ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) ) + ( 2 ยท 1 ) ) )
59 52 57 addcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆˆ โ„‚ )
60 17 59 55 subdid โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) ) = ( ( 2 ยท ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) ) โˆ’ ( 2 ยท ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) ) )
61 17 52 57 adddid โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) ) = ( ( 2 ยท ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) ) + ( 2 ยท 1 ) ) )
62 17 50 51 adddid โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) ) = ( ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) ) + ( 2 ยท ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) ) )
63 17 10 35 expmuld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ยท 2 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) )
64 17 30 expp1d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ( ๐‘ โˆ’ 2 ) + 1 ) ) = ( ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ยท 2 ) )
65 20 17 57 subsubd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ๐‘ โˆ’ ( 2 โˆ’ 1 ) ) = ( ( ๐‘ โˆ’ 2 ) + 1 ) )
66 65 eqcomd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ๐‘ โˆ’ 2 ) + 1 ) = ( ๐‘ โˆ’ ( 2 โˆ’ 1 ) ) )
67 66 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ( ๐‘ โˆ’ 2 ) + 1 ) ) = ( 2 โ†‘ ( ๐‘ โˆ’ ( 2 โˆ’ 1 ) ) ) )
68 64 67 eqtr3d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ยท 2 ) = ( 2 โ†‘ ( ๐‘ โˆ’ ( 2 โˆ’ 1 ) ) ) )
69 68 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ยท 2 ) ) = ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ ( 2 โˆ’ 1 ) ) ) ) )
70 63 69 eqtr3d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) = ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ ( 2 โˆ’ 1 ) ) ) ) )
71 70 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) ) = ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ ( 2 โˆ’ 1 ) ) ) ) ) )
72 2m1e1 โŠข ( 2 โˆ’ 1 ) = 1
73 72 a1i โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โˆ’ 1 ) = 1 )
74 73 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ๐‘ โˆ’ ( 2 โˆ’ 1 ) ) = ( ๐‘ โˆ’ 1 ) )
75 74 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( ๐‘ โˆ’ ( 2 โˆ’ 1 ) ) ) = ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) )
76 75 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ ( 2 โˆ’ 1 ) ) ) ) = ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) )
77 76 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ ( 2 โˆ’ 1 ) ) ) ) ) = ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) )
78 71 77 eqtrd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) ) = ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) )
79 17 17 37 mulassd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) = ( 2 ยท ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) )
80 79 eqcomd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) = ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) )
81 78 80 oveq12d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) ) + ( 2 ยท ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) ) = ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) )
82 62 81 eqtrd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) ) = ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) )
83 2t1e2 โŠข ( 2 ยท 1 ) = 2
84 83 a1i โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท 1 ) = 2 )
85 82 84 oveq12d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 ยท ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) ) + ( 2 ยท 1 ) ) = ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) )
86 61 85 eqtrd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) ) = ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) )
87 17 37 57 adddid โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) = ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + ( 2 ยท 1 ) ) )
88 84 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + ( 2 ยท 1 ) ) = ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 2 ) )
89 87 88 eqtrd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) = ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 2 ) )
90 89 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) = ( 2 ยท ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 2 ) ) )
91 17 51 17 adddid โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 2 ) ) = ( ( 2 ยท ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + ( 2 ยท 2 ) ) )
92 2t2e4 โŠข ( 2 ยท 2 ) = 4
93 92 a1i โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท 2 ) = 4 )
94 80 93 oveq12d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 ยท ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + ( 2 ยท 2 ) ) = ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) )
95 90 91 94 3eqtrd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) = ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) )
96 86 95 oveq12d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 ยท ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) ) โˆ’ ( 2 ยท ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) ) = ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) )
97 60 96 eqtrd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) ) = ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) )
98 97 84 oveq12d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 ยท ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) ) + ( 2 ยท 1 ) ) = ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) )
99 58 98 eqtrd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) + 1 ) ) = ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) )
100 99 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 1 ) โˆ’ ( 2 ยท ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) + 1 ) ) ) + 1 ) ) ) = ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) โˆ’ ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) ) )
101 17 13 mulcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) โˆˆ โ„‚ )
102 16 16 mulcli โŠข ( 2 ยท 2 ) โˆˆ โ„‚
103 102 a1i โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 ยท 2 ) โˆˆ โ„‚ )
104 103 37 mulcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) โˆˆ โ„‚ )
105 101 104 addcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) โˆˆ โ„‚ )
106 105 17 addcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆˆ โ„‚ )
107 4cn โŠข 4 โˆˆ โ„‚
108 107 a1i โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ 4 โˆˆ โ„‚ )
109 104 108 addcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) โˆˆ โ„‚ )
110 105 17 17 addassd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) + 2 ) = ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + ( 2 + 2 ) ) )
111 2p2e4 โŠข ( 2 + 2 ) = 4
112 111 a1i โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 + 2 ) = 4 )
113 112 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + ( 2 + 2 ) ) = ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 4 ) )
114 101 104 108 addassd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 4 ) = ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) )
115 110 113 114 3eqtrd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) + 2 ) = ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) )
116 106 17 101 109 115 subaddeqd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) = ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) โˆ’ 2 ) )
117 116 eqcomd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) โˆ’ 2 ) = ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) )
118 106 109 subcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) โˆˆ โ„‚ )
119 101 17 118 subadd2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) โˆ’ 2 ) = ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) โ†” ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) = ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) )
120 117 119 mpbid โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) = ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) )
121 120 oveq2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) )
122 eluzge2nn0 โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ โˆˆ โ„•0 )
123 10 122 nn0expcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ๐‘ ) โˆˆ โ„•0 )
124 8 123 nnexpcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„• )
125 124 nncnd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„‚ )
126 125 101 addcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) โˆˆ โ„‚ )
127 118 17 addcld โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) โˆˆ โ„‚ )
128 126 127 125 subadd2d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) โˆ’ ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) ) = ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†” ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) ) )
129 121 128 mpbird โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) โˆ’ ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) ) = ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) )
130 129 oveq1d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) โˆ’ ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) ) + 1 ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) )
131 126 57 127 addsubd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) โˆ’ ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) ) = ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) โˆ’ ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) ) + 1 ) )
132 fmtno โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ๐‘ ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) )
133 122 132 syl โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( FermatNo โ€˜ ๐‘ ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) )
134 130 131 133 3eqtr4d โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) โˆ’ ( ( ( ( ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) + ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) ) + 2 ) โˆ’ ( ( ( 2 ยท 2 ) ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 2 ) ) ) ) + 4 ) ) + 2 ) ) = ( FermatNo โ€˜ ๐‘ ) )
135 48 100 134 3eqtrrd โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( FermatNo โ€˜ ๐‘ ) = ( ( ( FermatNo โ€˜ ( ๐‘ โˆ’ 1 ) ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ( ( FermatNo โ€˜ ( ๐‘ โˆ’ 2 ) ) โˆ’ 1 ) โ†‘ 2 ) ) ) )