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 
|- ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` N ) = ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( ( ( FermatNo ` ( N - 2 ) ) - 1 ) ^ 2 ) ) ) )

Proof

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