Metamath Proof Explorer

Theorem fmtnorec2lem

Description: Lemma for fmtnorec2 (induction step). (Contributed by AV, 29-Jul-2021)

Ref Expression
Assertion fmtnorec2lem 
|- ( y e. NN0 -> ( ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) -> ( FermatNo ` ( ( y + 1 ) + 1 ) ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) ) )

Proof

Step Hyp Ref Expression
1 peano2nn0 
 |-  ( y e. NN0 -> ( y + 1 ) e. NN0 )
2 peano2nn0 
 |-  ( ( y + 1 ) e. NN0 -> ( ( y + 1 ) + 1 ) e. NN0 )
3 fmtno 
 |-  ( ( ( y + 1 ) + 1 ) e. NN0 -> ( FermatNo ` ( ( y + 1 ) + 1 ) ) = ( ( 2 ^ ( 2 ^ ( ( y + 1 ) + 1 ) ) ) + 1 ) )
4 1 2 3 3syl 
 |-  ( y e. NN0 -> ( FermatNo ` ( ( y + 1 ) + 1 ) ) = ( ( 2 ^ ( 2 ^ ( ( y + 1 ) + 1 ) ) ) + 1 ) )
5 2cnd 
 |-  ( y e. NN0 -> 2 e. CC )
6 5 1 expp1d 
 |-  ( y e. NN0 -> ( 2 ^ ( ( y + 1 ) + 1 ) ) = ( ( 2 ^ ( y + 1 ) ) x. 2 ) )
7 6 oveq2d 
 |-  ( y e. NN0 -> ( 2 ^ ( 2 ^ ( ( y + 1 ) + 1 ) ) ) = ( 2 ^ ( ( 2 ^ ( y + 1 ) ) x. 2 ) ) )
8 2nn0 
 |-  2 e. NN0
9 8 a1i 
 |-  ( y e. NN0 -> 2 e. NN0 )
10 9 1 nn0expcld 
 |-  ( y e. NN0 -> ( 2 ^ ( y + 1 ) ) e. NN0 )
11 9 10 nn0expcld 
 |-  ( y e. NN0 -> ( 2 ^ ( 2 ^ ( y + 1 ) ) ) e. NN0 )
12 11 nn0cnd 
 |-  ( y e. NN0 -> ( 2 ^ ( 2 ^ ( y + 1 ) ) ) e. CC )
13 12 sqvald 
 |-  ( y e. NN0 -> ( ( 2 ^ ( 2 ^ ( y + 1 ) ) ) ^ 2 ) = ( ( 2 ^ ( 2 ^ ( y + 1 ) ) ) x. ( 2 ^ ( 2 ^ ( y + 1 ) ) ) ) )
14 5 9 10 expmuld 
 |-  ( y e. NN0 -> ( 2 ^ ( ( 2 ^ ( y + 1 ) ) x. 2 ) ) = ( ( 2 ^ ( 2 ^ ( y + 1 ) ) ) ^ 2 ) )
15 fmtnom1nn 
 |-  ( ( y + 1 ) e. NN0 -> ( ( FermatNo ` ( y + 1 ) ) - 1 ) = ( 2 ^ ( 2 ^ ( y + 1 ) ) ) )
16 1 15 syl 
 |-  ( y e. NN0 -> ( ( FermatNo ` ( y + 1 ) ) - 1 ) = ( 2 ^ ( 2 ^ ( y + 1 ) ) ) )
17 16 16 oveq12d 
 |-  ( y e. NN0 -> ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) = ( ( 2 ^ ( 2 ^ ( y + 1 ) ) ) x. ( 2 ^ ( 2 ^ ( y + 1 ) ) ) ) )
18 13 14 17 3eqtr4d 
 |-  ( y e. NN0 -> ( 2 ^ ( ( 2 ^ ( y + 1 ) ) x. 2 ) ) = ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) )
19 7 18 eqtrd 
 |-  ( y e. NN0 -> ( 2 ^ ( 2 ^ ( ( y + 1 ) + 1 ) ) ) = ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) )
20 19 oveq1d 
 |-  ( y e. NN0 -> ( ( 2 ^ ( 2 ^ ( ( y + 1 ) + 1 ) ) ) + 1 ) = ( ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) )
21 4 20 eqtrd 
 |-  ( y e. NN0 -> ( FermatNo ` ( ( y + 1 ) + 1 ) ) = ( ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) )
22 21 adantr 
 |-  ( ( y e. NN0 /\ ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) ) -> ( FermatNo ` ( ( y + 1 ) + 1 ) ) = ( ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) )
23 oveq1 
 |-  ( ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) -> ( ( FermatNo ` ( y + 1 ) ) - 1 ) = ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) - 1 ) )
24 23 oveq1d 
 |-  ( ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) -> ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) = ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) )
25 24 oveq1d 
 |-  ( ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) -> ( ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) = ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) )
26 25 adantl 
 |-  ( ( y e. NN0 /\ ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) ) -> ( ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) = ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) )
27 fzfid 
 |-  ( y e. NN0 -> ( 0 ... y ) e. Fin )
28 elfznn0 
 |-  ( n e. ( 0 ... y ) -> n e. NN0 )
29 fmtnonn 
 |-  ( n e. NN0 -> ( FermatNo ` n ) e. NN )
30 29 nncnd 
 |-  ( n e. NN0 -> ( FermatNo ` n ) e. CC )
31 28 30 syl 
 |-  ( n e. ( 0 ... y ) -> ( FermatNo ` n ) e. CC )
32 31 adantl 
 |-  ( ( y e. NN0 /\ n e. ( 0 ... y ) ) -> ( FermatNo ` n ) e. CC )
33 27 32 fprodcl 
 |-  ( y e. NN0 -> prod_ n e. ( 0 ... y ) ( FermatNo ` n ) e. CC )
34 1cnd 
 |-  ( y e. NN0 -> 1 e. CC )
35 33 5 34 addsubassd 
 |-  ( y e. NN0 -> ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) - 1 ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + ( 2 - 1 ) ) )
36 2m1e1 
 |-  ( 2 - 1 ) = 1
37 36 oveq2i 
 |-  ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + ( 2 - 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 1 )
38 35 37 eqtrdi 
 |-  ( y e. NN0 -> ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) - 1 ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 1 ) )
39 38 oveq1d 
 |-  ( y e. NN0 -> ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) = ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) )
40 fmtnonn 
 |-  ( ( y + 1 ) e. NN0 -> ( FermatNo ` ( y + 1 ) ) e. NN )
41 1 40 syl 
 |-  ( y e. NN0 -> ( FermatNo ` ( y + 1 ) ) e. NN )
42 41 nncnd 
 |-  ( y e. NN0 -> ( FermatNo ` ( y + 1 ) ) e. CC )
43 42 34 subcld 
 |-  ( y e. NN0 -> ( ( FermatNo ` ( y + 1 ) ) - 1 ) e. CC )
44 33 42 muls1d 
 |-  ( y e. NN0 -> ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) = ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) )
45 43 mullidd 
 |-  ( y e. NN0 -> ( 1 x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) = ( ( FermatNo ` ( y + 1 ) ) - 1 ) )
46 44 45 oveq12d 
 |-  ( y e. NN0 -> ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + ( 1 x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) ) = ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) )
47 33 43 34 46 joinlmuladdmuld 
 |-  ( y e. NN0 -> ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) = ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) )
48 39 47 eqtrd 
 |-  ( y e. NN0 -> ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) = ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) )
49 48 adantr 
 |-  ( ( y e. NN0 /\ ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) ) -> ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) = ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) )
50 49 oveq1d 
 |-  ( ( y e. NN0 /\ ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) ) -> ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) = ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) )
51 eqcom 
 |-  ( ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) <-> ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) = ( FermatNo ` ( y + 1 ) ) )
52 42 5 33 subadd2d 
 |-  ( y e. NN0 -> ( ( ( FermatNo ` ( y + 1 ) ) - 2 ) = prod_ n e. ( 0 ... y ) ( FermatNo ` n ) <-> ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) = ( FermatNo ` ( y + 1 ) ) ) )
53 51 52 bitr4id 
 |-  ( y e. NN0 -> ( ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) <-> ( ( FermatNo ` ( y + 1 ) ) - 2 ) = prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) )
54 oveq2 
 |-  ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) = ( ( FermatNo ` ( y + 1 ) ) - 2 ) -> ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) = ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) )
55 54 oveq1d 
 |-  ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) = ( ( FermatNo ` ( y + 1 ) ) - 2 ) -> ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) = ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) )
56 55 oveq1d 
 |-  ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) = ( ( FermatNo ` ( y + 1 ) ) - 2 ) -> ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) = ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) )
57 56 eqcoms 
 |-  ( ( ( FermatNo ` ( y + 1 ) ) - 2 ) = prod_ n e. ( 0 ... y ) ( FermatNo ` n ) -> ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) = ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) )
58 33 42 mulcld 
 |-  ( y e. NN0 -> ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) e. CC )
59 42 5 subcld 
 |-  ( y e. NN0 -> ( ( FermatNo ` ( y + 1 ) ) - 2 ) e. CC )
60 58 59 subcld 
 |-  ( y e. NN0 -> ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) e. CC )
61 60 43 34 addassd 
 |-  ( y e. NN0 -> ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) = ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) + ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) + 1 ) ) )
62 elnn0uz 
 |-  ( y e. NN0 <-> y e. ( ZZ>= ` 0 ) )
63 62 biimpi 
 |-  ( y e. NN0 -> y e. ( ZZ>= ` 0 ) )
64 elfznn0 
 |-  ( n e. ( 0 ... ( y + 1 ) ) -> n e. NN0 )
65 64 30 syl 
 |-  ( n e. ( 0 ... ( y + 1 ) ) -> ( FermatNo ` n ) e. CC )
66 65 adantl 
 |-  ( ( y e. NN0 /\ n e. ( 0 ... ( y + 1 ) ) ) -> ( FermatNo ` n ) e. CC )
67 fveq2 
 |-  ( n = ( y + 1 ) -> ( FermatNo ` n ) = ( FermatNo ` ( y + 1 ) ) )
68 63 66 67 fprodp1 
 |-  ( y e. NN0 -> prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) )
69 68 eqcomd 
 |-  ( y e. NN0 -> ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) = prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) )
70 69 oveq1d 
 |-  ( y e. NN0 -> ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) )
71 npcan1 
 |-  ( ( FermatNo ` ( y + 1 ) ) e. CC -> ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) + 1 ) = ( FermatNo ` ( y + 1 ) ) )
72 42 71 syl 
 |-  ( y e. NN0 -> ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) + 1 ) = ( FermatNo ` ( y + 1 ) ) )
73 70 72 oveq12d 
 |-  ( y e. NN0 -> ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) + ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) + 1 ) ) = ( ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) + ( FermatNo ` ( y + 1 ) ) ) )
74 fzfid 
 |-  ( y e. NN0 -> ( 0 ... ( y + 1 ) ) e. Fin )
75 74 66 fprodcl 
 |-  ( y e. NN0 -> prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) e. CC )
76 75 59 42 subadd23d 
 |-  ( y e. NN0 -> ( ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) + ( FermatNo ` ( y + 1 ) ) ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + ( ( FermatNo ` ( y + 1 ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) ) )
77 73 76 eqtrd 
 |-  ( y e. NN0 -> ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) + ( ( ( FermatNo ` ( y + 1 ) ) - 1 ) + 1 ) ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + ( ( FermatNo ` ( y + 1 ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) ) )
78 42 5 nncand 
 |-  ( y e. NN0 -> ( ( FermatNo ` ( y + 1 ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) = 2 )
79 78 oveq2d 
 |-  ( y e. NN0 -> ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + ( ( FermatNo ` ( y + 1 ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) )
80 61 77 79 3eqtrd 
 |-  ( y e. NN0 -> ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - ( ( FermatNo ` ( y + 1 ) ) - 2 ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) )
81 57 80 sylan9eqr 
 |-  ( ( y e. NN0 /\ ( ( FermatNo ` ( y + 1 ) ) - 2 ) = prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) -> ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) )
82 81 ex 
 |-  ( y e. NN0 -> ( ( ( FermatNo ` ( y + 1 ) ) - 2 ) = prod_ n e. ( 0 ... y ) ( FermatNo ` n ) -> ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) ) )
83 53 82 sylbid 
 |-  ( y e. NN0 -> ( ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) -> ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) ) )
84 83 imp 
 |-  ( ( y e. NN0 /\ ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) ) -> ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) x. ( FermatNo ` ( y + 1 ) ) ) - prod_ n e. ( 0 ... y ) ( FermatNo ` n ) ) + ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) )
85 50 84 eqtrd 
 |-  ( ( y e. NN0 /\ ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) ) -> ( ( ( ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) - 1 ) x. ( ( FermatNo ` ( y + 1 ) ) - 1 ) ) + 1 ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) )
86 22 26 85 3eqtrd 
 |-  ( ( y e. NN0 /\ ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) ) -> ( FermatNo ` ( ( y + 1 ) + 1 ) ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) )
87 86 ex 
 |-  ( y e. NN0 -> ( ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) -> ( FermatNo ` ( ( y + 1 ) + 1 ) ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) ) )