Theorem fmtno5lem4

Description: Lemma 4 for fmtno5 . (Contributed by AV, 30-Jul-2021)

	Ref	Expression
Assertion	fmtno5lem4	$$⊢{65536}^2=4294967296$$

Proof

Step	Hyp	Ref	Expression
1		6nn0	$$⊢6\in {\mathbb{N}}_0$$
2		5nn0	$$⊢5\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢65\in {\mathbb{N}}_0$$
4	3 2	deccl	$$⊢655\in {\mathbb{N}}_0$$
5		3nn0	$$⊢3\in {\mathbb{N}}_0$$
6	4 5	deccl	$$⊢6553\in {\mathbb{N}}_0$$
7	6 1	deccl	$$⊢65536\in {\mathbb{N}}_0$$
8	7	nn0cni	$$⊢65536\in ℂ$$
9	8	sqvali	$$⊢{65536}^2=65536\cdot 65536$$
10		fmtno5lem1	$$⊢65536\cdot 6=393216$$
11	10	eqcomi	$$⊢393216=65536\cdot 6$$
12		fmtno5lem2	$$⊢65536\cdot 5=327680$$
13	12	eqcomi	$$⊢327680=65536\cdot 5$$
14	1 2 7 11 13	decmul10add	$$⊢65536\cdot 65=3932160+327680$$
15	14	eqcomi	$$⊢3932160+327680=65536\cdot 65$$
16	3 2 7 15 13	decmul10add	Could not format ( ; ; ; ; 6 5 5 3 6 x. ; ; 6 5 5 ) = ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) : No typesetting found for |- ( ; ; ; ; 6 5 5 3 6 x. ; ; 6 5 5 ) = ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) with typecode |-
17	16	eqcomi	Could not format ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) = ( ; ; ; ; 6 5 5 3 6 x. ; ; 6 5 5 ) : No typesetting found for |- ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) = ( ; ; ; ; 6 5 5 3 6 x. ; ; 6 5 5 ) with typecode |-
18		fmtno5lem3	$$⊢65536\cdot 3=196608$$
19	18	eqcomi	$$⊢196608=65536\cdot 3$$
20	4 5 7 17 19	decmul10add	Could not format ( ; ; ; ; 6 5 5 3 6 x. ; ; ; 6 5 5 3 ) = ( ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 1 9 6 6 0 8 ) : No typesetting found for |- ( ; ; ; ; 6 5 5 3 6 x. ; ; ; 6 5 5 3 ) = ( ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 1 9 6 6 0 8 ) with typecode |-
21	20	eqcomi	Could not format ( ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 1 9 6 6 0 8 ) = ( ; ; ; ; 6 5 5 3 6 x. ; ; ; 6 5 5 3 ) : No typesetting found for |- ( ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 1 9 6 6 0 8 ) = ( ; ; ; ; 6 5 5 3 6 x. ; ; ; 6 5 5 3 ) with typecode |-
22	6 1 7 21 11	decmul10add	Could not format ( ; ; ; ; 6 5 5 3 6 x. ; ; ; ; 6 5 5 3 6 ) = ( ; ( ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 1 9 6 6 0 8 ) 0 + ; ; ; ; ; 3 9 3 2 1 6 ) : No typesetting found for |- ( ; ; ; ; 6 5 5 3 6 x. ; ; ; ; 6 5 5 3 6 ) = ( ; ( ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 1 9 6 6 0 8 ) 0 + ; ; ; ; ; 3 9 3 2 1 6 ) with typecode |-
23		4nn0	$$⊢4\in {\mathbb{N}}_0$$
24		2nn0	$$⊢2\in {\mathbb{N}}_0$$
25	23 24	deccl	$$⊢42\in {\mathbb{N}}_0$$
26		9nn0	$$⊢9\in {\mathbb{N}}_0$$
27	25 26	deccl	$$⊢429\in {\mathbb{N}}_0$$
28	27 23	deccl	$$⊢4294\in {\mathbb{N}}_0$$
29	28 2	deccl	$$⊢42945\in {\mathbb{N}}_0$$
30		7nn0	$$⊢7\in {\mathbb{N}}_0$$
31	29 30	deccl	$$⊢429457\in {\mathbb{N}}_0$$
32	31 23	deccl	$$⊢4294574\in {\mathbb{N}}_0$$
33		0nn0	$$⊢0\in {\mathbb{N}}_0$$
34	32 33	deccl	$$⊢42945740\in {\mathbb{N}}_0$$
35		8nn0	$$⊢8\in {\mathbb{N}}_0$$
36	34 35	deccl	$$⊢429457408\in {\mathbb{N}}_0$$
37	5 26	deccl	$$⊢39\in {\mathbb{N}}_0$$
38	37 5	deccl	$$⊢393\in {\mathbb{N}}_0$$
39	38 24	deccl	$$⊢3932\in {\mathbb{N}}_0$$
40		1nn0	$$⊢1\in {\mathbb{N}}_0$$
41	39 40	deccl	$$⊢39321\in {\mathbb{N}}_0$$
42	27 24	deccl	$$⊢4292\in {\mathbb{N}}_0$$
43	42 1	deccl	$$⊢42926\in {\mathbb{N}}_0$$
44	43 33	deccl	$$⊢429260\in {\mathbb{N}}_0$$
45	44 35	deccl	$$⊢4292608\in {\mathbb{N}}_0$$
46	45 33	deccl	$$⊢42926080\in {\mathbb{N}}_0$$
47	40 26	deccl	$$⊢19\in {\mathbb{N}}_0$$
48	47 1	deccl	$$⊢196\in {\mathbb{N}}_0$$
49	48 1	deccl	$$⊢1966\in {\mathbb{N}}_0$$
50	49 33	deccl	$$⊢19660\in {\mathbb{N}}_0$$
51	25 2	deccl	$$⊢425\in {\mathbb{N}}_0$$
52	51 26	deccl	$$⊢4259\in {\mathbb{N}}_0$$
53	52 35	deccl	$$⊢42598\in {\mathbb{N}}_0$$
54	53 23	deccl	$$⊢425984\in {\mathbb{N}}_0$$
55	54 33	deccl	$$⊢4259840\in {\mathbb{N}}_0$$
56	5 24	deccl	$$⊢32\in {\mathbb{N}}_0$$
57	56 30	deccl	$$⊢327\in {\mathbb{N}}_0$$
58	57 1	deccl	$$⊢3276\in {\mathbb{N}}_0$$
59	58 35	deccl	$$⊢32768\in {\mathbb{N}}_0$$
60	41 1	deccl	$$⊢393216\in {\mathbb{N}}_0$$
61		eqid	$$⊢3932160=3932160$$
62		eqid	$$⊢327680=327680$$
63		eqid	$$⊢393216=393216$$
64		eqid	$$⊢32768=32768$$
65		7p1e8	$$⊢7+1=8$$
66		eqid	$$⊢39321=39321$$
67		eqid	$$⊢3276=3276$$
68		eqid	$$⊢3932=3932$$
69		eqid	$$⊢327=327$$
70		eqid	$$⊢393=393$$
71		eqid	$$⊢32=32$$
72		eqid	$$⊢39=39$$
73		3p1e4	$$⊢3+1=4$$
74		9p3e12	$$⊢9+3=12$$
75	5 26 5 72 73 24 74	decaddci	$$⊢39+3=42$$
76		3p2e5	$$⊢3+2=5$$
77	37 5 5 24 70 71 75 76	decadd	$$⊢393+32=425$$
78		7cn	$$⊢7\in ℂ$$
79		2cn	$$⊢2\in ℂ$$
80		7p2e9	$$⊢7+2=9$$
81	78 79 80	addcomli	$$⊢2+7=9$$
82	38 24 56 30 68 69 77 81	decadd	$$⊢3932+327=4259$$
83		6cn	$$⊢6\in ℂ$$
84		ax-1cn	$$⊢1\in ℂ$$
85		6p1e7	$$⊢6+1=7$$
86	83 84 85	addcomli	$$⊢1+6=7$$
87	39 40 57 1 66 67 82 86	decadd	$$⊢39321+3276=42597$$
88	52 30 65 87	decsuc	$$⊢39321+3276+1=42598$$
89		8cn	$$⊢8\in ℂ$$
90		8p6e14	$$⊢8+6=14$$
91	89 83 90	addcomli	$$⊢6+8=14$$
92	41 1 58 35 63 64 88 23 91	decaddc	$$⊢393216+32768=425984$$
93		00id	$$⊢0+0=0$$
94	60 33 59 33 61 62 92 93	decadd	$$⊢3932160+327680=4259840$$
95	94	deceq1i	Could not format ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 = ; ; ; ; ; ; ; 4 2 5 9 8 4 0 0 : No typesetting found for |- ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 = ; ; ; ; ; ; ; 4 2 5 9 8 4 0 0 with typecode |-
96		eqid	$$⊢4259840=4259840$$
97		eqid	$$⊢425984=425984$$
98		5p1e6	$$⊢5+1=6$$
99		eqid	$$⊢42598=42598$$
100		1p1e2	$$⊢1+1=2$$
101		eqid	$$⊢4259=4259$$
102		8p1e9	$$⊢8+1=9$$
103		eqid	$$⊢425=425$$
104		5p3e8	$$⊢5+3=8$$
105	25 2 5 103 104	decaddi	$$⊢425+3=428$$
106	25 35 102 105	decsuc	$$⊢425+3+1=429$$
107		9p2e11	$$⊢9+2=11$$
108	51 26 5 24 101 71 106 40 107	decaddc	$$⊢4259+32=4291$$
109	27 40 100 108	decsuc	$$⊢4259+32+1=4292$$
110		8p7e15	$$⊢8+7=15$$
111	52 35 56 30 99 69 109 2 110	decaddc	$$⊢42598+327=42925$$
112	42 2 98 111	decsuc	$$⊢42598+327+1=42926$$
113		4cn	$$⊢4\in ℂ$$
114		6p4e10	$$⊢6+4=10$$
115	83 113 114	addcomli	$$⊢4+6=10$$
116	53 23 57 1 97 67 112 33 115	decaddc	$$⊢425984+3276=429260$$
117	89	addid2i	$$⊢0+8=8$$
118	54 33 58 35 96 64 116 117	decadd	$$⊢4259840+32768=4292608$$
119	55 33 59 33 95 62 118 93	decadd	Could not format ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) = ; ; ; ; ; ; ; 4 2 9 2 6 0 8 0 : No typesetting found for |- ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) = ; ; ; ; ; ; ; 4 2 9 2 6 0 8 0 with typecode |-
120	119	deceq1i	Could not format ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 = ; ; ; ; ; ; ; ; 4 2 9 2 6 0 8 0 0 : No typesetting found for |- ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 = ; ; ; ; ; ; ; ; 4 2 9 2 6 0 8 0 0 with typecode |-
121		eqid	$$⊢196608=196608$$
122	45 49	decaddm10	Could not format ( ; ; ; ; ; ; ; 4 2 9 2 6 0 8 0 + ; ; ; ; 1 9 6 6 0 ) = ; ( ; ; ; ; ; ; 4 2 9 2 6 0 8 + ; ; ; 1 9 6 6 ) 0 : No typesetting found for |- ( ; ; ; ; ; ; ; 4 2 9 2 6 0 8 0 + ; ; ; ; 1 9 6 6 0 ) = ; ( ; ; ; ; ; ; 4 2 9 2 6 0 8 + ; ; ; 1 9 6 6 ) 0 with typecode |-
123		eqid	$$⊢4292608=4292608$$
124		eqid	$$⊢1966=1966$$
125		eqid	$$⊢429260=429260$$
126		eqid	$$⊢196=196$$
127		eqid	$$⊢42926=42926$$
128		eqid	$$⊢19=19$$
129		2p1e3	$$⊢2+1=3$$
130		eqid	$$⊢4292=4292$$
131	27 24 129 130	decsuc	$$⊢4292+1=4293$$
132	27 5 73 131	decsuc	$$⊢4292+1+1=4294$$
133		9cn	$$⊢9\in ℂ$$
134		9p6e15	$$⊢9+6=15$$
135	133 83 134	addcomli	$$⊢6+9=15$$
136	42 1 40 26 127 128 132 2 135	decaddc	$$⊢42926+19=42945$$
137	83	addid2i	$$⊢0+6=6$$
138	43 33 47 1 125 126 136 137	decadd	$$⊢429260+196=429456$$
139	29 1 85 138	decsuc	$$⊢429260+196+1=429457$$
140	44 35 48 1 123 124 139 23 90	decaddc	$$⊢4292608+1966=4294574$$
141	140	deceq1i	Could not format ; ( ; ; ; ; ; ; 4 2 9 2 6 0 8 + ; ; ; 1 9 6 6 ) 0 = ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 : No typesetting found for |- ; ( ; ; ; ; ; ; 4 2 9 2 6 0 8 + ; ; ; 1 9 6 6 ) 0 = ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 with typecode |-
142	122 141	eqtri	$$⊢42926080+19660=42945740$$
143	46 33 50 35 120 121 142 117	decadd	Could not format ( ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 1 9 6 6 0 8 ) = ; ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 8 : No typesetting found for |- ( ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 1 9 6 6 0 8 ) = ; ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 8 with typecode |-
144	143	deceq1i	Could not format ; ( ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 1 9 6 6 0 8 ) 0 = ; ; ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 8 0 : No typesetting found for |- ; ( ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 1 9 6 6 0 8 ) 0 = ; ; ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 8 0 with typecode |-
145		eqid	$$⊢429457408=429457408$$
146		eqid	$$⊢42945740=42945740$$
147		eqid	$$⊢4294574=4294574$$
148		eqid	$$⊢429457=429457$$
149		eqid	$$⊢42945=42945$$
150	28 2 5 149 104	decaddi	$$⊢42945+3=42948$$
151	28 35 102 150	decsuc	$$⊢42945+3+1=42949$$
152		9p7e16	$$⊢9+7=16$$
153	133 78 152	addcomli	$$⊢7+9=16$$
154	29 30 5 26 148 72 151 1 153	decaddc	$$⊢429457+39=429496$$
155		4p3e7	$$⊢4+3=7$$
156	31 23 37 5 147 70 154 155	decadd	$$⊢4294574+393=4294967$$
157	79	addid2i	$$⊢0+2=2$$
158	32 33 38 24 146 68 156 157	decadd	$$⊢42945740+3932=42949672$$
159	34 35 39 40 145 66 158 102	decadd	$$⊢429457408+39321=429496729$$
160	36 33 41 1 144 63 159 137	decadd	Could not format ( ; ( ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 1 9 6 6 0 8 ) 0 + ; ; ; ; ; 3 9 3 2 1 6 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 6 : No typesetting found for |- ( ; ( ; ( ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 + ; ; ; ; ; 1 9 6 6 0 8 ) 0 + ; ; ; ; ; 3 9 3 2 1 6 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 6 with typecode |-
161	9 22 160	3eqtri	$$⊢{65536}^2=4294967296$$