Metamath Proof Explorer

Theorem fmtnorec3

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

Ref Expression
Assertion fmtnorec3 
|- ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` N ) = ( ( FermatNo ` ( N - 1 ) ) + ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. prod_ n e. ( 0 ... ( N - 2 ) ) ( FermatNo ` n ) ) ) )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 0 ... ( N - 2 ) ) e. Fin )
2 elfznn0 
 |-  ( n e. ( 0 ... ( N - 2 ) ) -> n e. NN0 )
3 fmtnonn 
 |-  ( n e. NN0 -> ( FermatNo ` n ) e. NN )
4 2 3 syl 
 |-  ( n e. ( 0 ... ( N - 2 ) ) -> ( FermatNo ` n ) e. NN )
5 4 nncnd 
 |-  ( n e. ( 0 ... ( N - 2 ) ) -> ( FermatNo ` n ) e. CC )
6 5 adantl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ n e. ( 0 ... ( N - 2 ) ) ) -> ( FermatNo ` n ) e. CC )
7 1 6 fprodcl 
 |-  ( N e. ( ZZ>= ` 2 ) -> prod_ n e. ( 0 ... ( N - 2 ) ) ( FermatNo ` n ) e. CC )
8 2cn 
 |-  2 e. CC
9 8 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. CC )
10 uznn0sub 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. NN0 )
11 fmtnorec2 
 |-  ( ( N - 2 ) e. NN0 -> ( FermatNo ` ( ( N - 2 ) + 1 ) ) = ( prod_ n e. ( 0 ... ( N - 2 ) ) ( FermatNo ` n ) + 2 ) )
12 10 11 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` ( ( N - 2 ) + 1 ) ) = ( prod_ n e. ( 0 ... ( N - 2 ) ) ( FermatNo ` n ) + 2 ) )
13 12 eqcomd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( prod_ n e. ( 0 ... ( N - 2 ) ) ( FermatNo ` n ) + 2 ) = ( FermatNo ` ( ( N - 2 ) + 1 ) ) )
14 7 9 13 mvlraddd 
 |-  ( N e. ( ZZ>= ` 2 ) -> prod_ n e. ( 0 ... ( N - 2 ) ) ( FermatNo ` n ) = ( ( FermatNo ` ( ( N - 2 ) + 1 ) ) - 2 ) )
15 14 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. prod_ n e. ( 0 ... ( N - 2 ) ) ( FermatNo ` n ) ) = ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( ( FermatNo ` ( ( N - 2 ) + 1 ) ) - 2 ) ) )
16 15 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( FermatNo ` ( N - 1 ) ) + ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. prod_ n e. ( 0 ... ( N - 2 ) ) ( FermatNo ` n ) ) ) = ( ( FermatNo ` ( N - 1 ) ) + ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( ( FermatNo ` ( ( N - 2 ) + 1 ) ) - 2 ) ) ) )
17 2nn0 
 |-  2 e. NN0
18 17 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. NN0 )
19 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
20 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
21 19 20 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN0 )
22 18 21 nn0expcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N - 1 ) ) e. NN0 )
23 18 22 nn0expcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( 2 ^ ( N - 1 ) ) ) e. NN0 )
24 23 nn0cnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( 2 ^ ( N - 1 ) ) ) e. CC )
25 peano2nn0 
 |-  ( ( N - 2 ) e. NN0 -> ( ( N - 2 ) + 1 ) e. NN0 )
26 10 25 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N - 2 ) + 1 ) e. NN0 )
27 fmtnonn 
 |-  ( ( ( N - 2 ) + 1 ) e. NN0 -> ( FermatNo ` ( ( N - 2 ) + 1 ) ) e. NN )
28 26 27 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` ( ( N - 2 ) + 1 ) ) e. NN )
29 28 nncnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` ( ( N - 2 ) + 1 ) ) e. CC )
30 24 29 9 subdid 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( ( FermatNo ` ( ( N - 2 ) + 1 ) ) - 2 ) ) = ( ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( ( N - 2 ) + 1 ) ) ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) )
31 eluzelcn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. CC )
32 ax-1cn 
 |-  1 e. CC
33 32 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 e. CC )
34 subsub 
 |-  ( ( N e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( N - ( 2 - 1 ) ) = ( ( N - 2 ) + 1 ) )
35 34 eqcomd 
 |-  ( ( N e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( N - 2 ) + 1 ) = ( N - ( 2 - 1 ) ) )
36 31 9 33 35 syl3anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N - 2 ) + 1 ) = ( N - ( 2 - 1 ) ) )
37 2m1e1 
 |-  ( 2 - 1 ) = 1
38 37 oveq2i 
 |-  ( N - ( 2 - 1 ) ) = ( N - 1 )
39 36 38 eqtrdi 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N - 2 ) + 1 ) = ( N - 1 ) )
40 39 fveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` ( ( N - 2 ) + 1 ) ) = ( FermatNo ` ( N - 1 ) ) )
41 40 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( ( N - 2 ) + 1 ) ) ) = ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) )
42 41 oveq1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( ( N - 2 ) + 1 ) ) ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) = ( ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) )
43 30 42 eqtrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( ( FermatNo ` ( ( N - 2 ) + 1 ) ) - 2 ) ) = ( ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) )
44 43 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( FermatNo ` ( N - 1 ) ) + ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( ( FermatNo ` ( ( N - 2 ) + 1 ) ) - 2 ) ) ) = ( ( FermatNo ` ( N - 1 ) ) + ( ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) ) )
45 fmtnonn 
 |-  ( ( N - 1 ) e. NN0 -> ( FermatNo ` ( N - 1 ) ) e. NN )
46 21 45 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` ( N - 1 ) ) e. NN )
47 46 nncnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` ( N - 1 ) ) e. CC )
48 47 mullidd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 x. ( FermatNo ` ( N - 1 ) ) ) = ( FermatNo ` ( N - 1 ) ) )
49 48 eqcomd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` ( N - 1 ) ) = ( 1 x. ( FermatNo ` ( N - 1 ) ) ) )
50 49 oveq1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( FermatNo ` ( N - 1 ) ) + ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) ) = ( ( 1 x. ( FermatNo ` ( N - 1 ) ) ) + ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) ) )
51 33 24 47 adddird 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 1 + ( 2 ^ ( 2 ^ ( N - 1 ) ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) = ( ( 1 x. ( FermatNo ` ( N - 1 ) ) ) + ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) ) )
52 33 24 addcomd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 + ( 2 ^ ( 2 ^ ( N - 1 ) ) ) ) = ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) + 1 ) )
53 fmtno 
 |-  ( ( N - 1 ) e. NN0 -> ( FermatNo ` ( N - 1 ) ) = ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) + 1 ) )
54 21 53 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` ( N - 1 ) ) = ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) + 1 ) )
55 52 54 eqtr4d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 + ( 2 ^ ( 2 ^ ( N - 1 ) ) ) ) = ( FermatNo ` ( N - 1 ) ) )
56 55 oveq1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 1 + ( 2 ^ ( 2 ^ ( N - 1 ) ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) = ( ( FermatNo ` ( N - 1 ) ) x. ( FermatNo ` ( N - 1 ) ) ) )
57 47 sqvald 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) = ( ( FermatNo ` ( N - 1 ) ) x. ( FermatNo ` ( N - 1 ) ) ) )
58 56 57 eqtr4d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 1 + ( 2 ^ ( 2 ^ ( N - 1 ) ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) = ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) )
59 50 51 58 3eqtr2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( FermatNo ` ( N - 1 ) ) + ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) ) = ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) )
60 59 oveq1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( FermatNo ` ( N - 1 ) ) + ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) = ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) )
61 24 47 mulcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) e. CC )
62 24 9 mulcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) e. CC )
63 47 61 62 addsubassd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( FermatNo ` ( N - 1 ) ) + ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) = ( ( FermatNo ` ( N - 1 ) ) + ( ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) ) )
64 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
65 31 64 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N - 1 ) + 1 ) = N )
66 65 eqcomd 
 |-  ( N e. ( ZZ>= ` 2 ) -> N = ( ( N - 1 ) + 1 ) )
67 66 fveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` N ) = ( FermatNo ` ( ( N - 1 ) + 1 ) ) )
68 fmtnorec1 
 |-  ( ( N - 1 ) e. NN0 -> ( FermatNo ` ( ( N - 1 ) + 1 ) ) = ( ( ( ( FermatNo ` ( N - 1 ) ) - 1 ) ^ 2 ) + 1 ) )
69 21 68 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` ( ( N - 1 ) + 1 ) ) = ( ( ( ( FermatNo ` ( N - 1 ) ) - 1 ) ^ 2 ) + 1 ) )
70 binom2sub1 
 |-  ( ( FermatNo ` ( N - 1 ) ) e. CC -> ( ( ( FermatNo ` ( N - 1 ) ) - 1 ) ^ 2 ) = ( ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) + 1 ) )
71 47 70 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( FermatNo ` ( N - 1 ) ) - 1 ) ^ 2 ) = ( ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) + 1 ) )
72 71 oveq1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( ( FermatNo ` ( N - 1 ) ) - 1 ) ^ 2 ) + 1 ) = ( ( ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) + 1 ) + 1 ) )
73 46 nnsqcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) e. NN )
74 73 nncnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) e. CC )
75 9 47 mulcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 x. ( FermatNo ` ( N - 1 ) ) ) e. CC )
76 74 75 subcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) e. CC )
77 76 33 33 addassd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) + 1 ) + 1 ) = ( ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) + ( 1 + 1 ) ) )
78 32 2timesi 
 |-  ( 2 x. 1 ) = ( 1 + 1 )
79 78 eqcomi 
 |-  ( 1 + 1 ) = ( 2 x. 1 )
80 79 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 + 1 ) = ( 2 x. 1 ) )
81 80 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) + ( 1 + 1 ) ) = ( ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) + ( 2 x. 1 ) ) )
82 77 81 eqtrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) + 1 ) + 1 ) = ( ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) + ( 2 x. 1 ) ) )
83 8 32 mulcli 
 |-  ( 2 x. 1 ) e. CC
84 83 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 x. 1 ) e. CC )
85 74 75 84 subadd23d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) + ( 2 x. 1 ) ) = ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) + ( ( 2 x. 1 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) ) )
86 9 33 47 subdid 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 x. ( 1 - ( FermatNo ` ( N - 1 ) ) ) ) = ( ( 2 x. 1 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) )
87 86 eqcomd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 x. 1 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) = ( 2 x. ( 1 - ( FermatNo ` ( N - 1 ) ) ) ) )
88 87 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) + ( ( 2 x. 1 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) ) = ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) + ( 2 x. ( 1 - ( FermatNo ` ( N - 1 ) ) ) ) ) )
89 33 47 subcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 - ( FermatNo ` ( N - 1 ) ) ) e. CC )
90 9 89 mulneg2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 x. -u ( 1 - ( FermatNo ` ( N - 1 ) ) ) ) = -u ( 2 x. ( 1 - ( FermatNo ` ( N - 1 ) ) ) ) )
91 33 47 negsubdi2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> -u ( 1 - ( FermatNo ` ( N - 1 ) ) ) = ( ( FermatNo ` ( N - 1 ) ) - 1 ) )
92 fmtnom1nn 
 |-  ( ( N - 1 ) e. NN0 -> ( ( FermatNo ` ( N - 1 ) ) - 1 ) = ( 2 ^ ( 2 ^ ( N - 1 ) ) ) )
93 21 92 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( FermatNo ` ( N - 1 ) ) - 1 ) = ( 2 ^ ( 2 ^ ( N - 1 ) ) ) )
94 91 93 eqtrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> -u ( 1 - ( FermatNo ` ( N - 1 ) ) ) = ( 2 ^ ( 2 ^ ( N - 1 ) ) ) )
95 94 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 x. -u ( 1 - ( FermatNo ` ( N - 1 ) ) ) ) = ( 2 x. ( 2 ^ ( 2 ^ ( N - 1 ) ) ) ) )
96 90 95 eqtr3d 
 |-  ( N e. ( ZZ>= ` 2 ) -> -u ( 2 x. ( 1 - ( FermatNo ` ( N - 1 ) ) ) ) = ( 2 x. ( 2 ^ ( 2 ^ ( N - 1 ) ) ) ) )
97 96 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - -u ( 2 x. ( 1 - ( FermatNo ` ( N - 1 ) ) ) ) ) = ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( 2 ^ ( 2 ^ ( N - 1 ) ) ) ) ) )
98 9 89 mulcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 x. ( 1 - ( FermatNo ` ( N - 1 ) ) ) ) e. CC )
99 74 98 subnegd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - -u ( 2 x. ( 1 - ( FermatNo ` ( N - 1 ) ) ) ) ) = ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) + ( 2 x. ( 1 - ( FermatNo ` ( N - 1 ) ) ) ) ) )
100 9 24 mulcomd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 x. ( 2 ^ ( 2 ^ ( N - 1 ) ) ) ) = ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) )
101 100 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( 2 ^ ( 2 ^ ( N - 1 ) ) ) ) ) = ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) )
102 97 99 101 3eqtr3d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) + ( 2 x. ( 1 - ( FermatNo ` ( N - 1 ) ) ) ) ) = ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) )
103 85 88 102 3eqtrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( FermatNo ` ( N - 1 ) ) ) ) + ( 2 x. 1 ) ) = ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) )
104 72 82 103 3eqtrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( ( FermatNo ` ( N - 1 ) ) - 1 ) ^ 2 ) + 1 ) = ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) )
105 67 69 104 3eqtrrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( FermatNo ` ( N - 1 ) ) ^ 2 ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) = ( FermatNo ` N ) )
106 60 63 105 3eqtr3d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( FermatNo ` ( N - 1 ) ) + ( ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. ( FermatNo ` ( N - 1 ) ) ) - ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. 2 ) ) ) = ( FermatNo ` N ) )
107 16 44 106 3eqtrrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( FermatNo ` N ) = ( ( FermatNo ` ( N - 1 ) ) + ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. prod_ n e. ( 0 ... ( N - 2 ) ) ( FermatNo ` n ) ) ) )