Metamath Proof Explorer

Theorem fmtno5lem4

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

Ref Expression
Assertion fmtno5lem4 
|- ( ; ; ; ; 6 5 5 3 6 ^ 2 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 6

Proof

Step Hyp Ref Expression
1 6nn0 
 |-  6 e. NN0
2 5nn0 
 |-  5 e. NN0
3 1 2 deccl 
 |-  ; 6 5 e. NN0
4 3 2 deccl 
 |-  ; ; 6 5 5 e. NN0
5 3nn0 
 |-  3 e. NN0
6 4 5 deccl 
 |-  ; ; ; 6 5 5 3 e. NN0
7 6 1 deccl 
 |-  ; ; ; ; 6 5 5 3 6 e. NN0
8 7 nn0cni 
 |-  ; ; ; ; 6 5 5 3 6 e. CC
9 8 sqvali 
 |-  ( ; ; ; ; 6 5 5 3 6 ^ 2 ) = ( ; ; ; ; 6 5 5 3 6 x. ; ; ; ; 6 5 5 3 6 )
10 fmtno5lem1 
 |-  ( ; ; ; ; 6 5 5 3 6 x. 6 ) = ; ; ; ; ; 3 9 3 2 1 6
11 10 eqcomi 
 |-  ; ; ; ; ; 3 9 3 2 1 6 = ( ; ; ; ; 6 5 5 3 6 x. 6 )
12 fmtno5lem2 
 |-  ( ; ; ; ; 6 5 5 3 6 x. 5 ) = ; ; ; ; ; 3 2 7 6 8 0
13 12 eqcomi 
 |-  ; ; ; ; ; 3 2 7 6 8 0 = ( ; ; ; ; 6 5 5 3 6 x. 5 )
14 1 2 7 11 13 decmul10add 
 |-  ( ; ; ; ; 6 5 5 3 6 x. ; 6 5 ) = ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 )
15 14 eqcomi 
 |-  ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) = ( ; ; ; ; 6 5 5 3 6 x. ; 6 5 )
16 3 2 7 15 13 decmul10add 
 |-  ( ; ; ; ; 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 )
17 16 eqcomi 
 |-  ( ; ( ; ; ; ; ; ; 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 )
18 fmtno5lem3 
 |-  ( ; ; ; ; 6 5 5 3 6 x. 3 ) = ; ; ; ; ; 1 9 6 6 0 8
19 18 eqcomi 
 |-  ; ; ; ; ; 1 9 6 6 0 8 = ( ; ; ; ; 6 5 5 3 6 x. 3 )
20 4 5 7 17 19 decmul10add 
 |-  ( ; ; ; ; 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 )
21 20 eqcomi 
 |-  ( ; ( ; ( ; ; ; ; ; ; 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 )
22 6 1 7 21 11 decmul10add 
 |-  ( ; ; ; ; 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 )
23 4nn0 
 |-  4 e. NN0
24 2nn0 
 |-  2 e. NN0
25 23 24 deccl 
 |-  ; 4 2 e. NN0
26 9nn0 
 |-  9 e. NN0
27 25 26 deccl 
 |-  ; ; 4 2 9 e. NN0
28 27 23 deccl 
 |-  ; ; ; 4 2 9 4 e. NN0
29 28 2 deccl 
 |-  ; ; ; ; 4 2 9 4 5 e. NN0
30 7nn0 
 |-  7 e. NN0
31 29 30 deccl 
 |-  ; ; ; ; ; 4 2 9 4 5 7 e. NN0
32 31 23 deccl 
 |-  ; ; ; ; ; ; 4 2 9 4 5 7 4 e. NN0
33 0nn0 
 |-  0 e. NN0
34 32 33 deccl 
 |-  ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 e. NN0
35 8nn0 
 |-  8 e. NN0
36 34 35 deccl 
 |-  ; ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 8 e. NN0
37 5 26 deccl 
 |-  ; 3 9 e. NN0
38 37 5 deccl 
 |-  ; ; 3 9 3 e. NN0
39 38 24 deccl 
 |-  ; ; ; 3 9 3 2 e. NN0
40 1nn0 
 |-  1 e. NN0
41 39 40 deccl 
 |-  ; ; ; ; 3 9 3 2 1 e. NN0
42 27 24 deccl 
 |-  ; ; ; 4 2 9 2 e. NN0
43 42 1 deccl 
 |-  ; ; ; ; 4 2 9 2 6 e. NN0
44 43 33 deccl 
 |-  ; ; ; ; ; 4 2 9 2 6 0 e. NN0
45 44 35 deccl 
 |-  ; ; ; ; ; ; 4 2 9 2 6 0 8 e. NN0
46 45 33 deccl 
 |-  ; ; ; ; ; ; ; 4 2 9 2 6 0 8 0 e. NN0
47 40 26 deccl 
 |-  ; 1 9 e. NN0
48 47 1 deccl 
 |-  ; ; 1 9 6 e. NN0
49 48 1 deccl 
 |-  ; ; ; 1 9 6 6 e. NN0
50 49 33 deccl 
 |-  ; ; ; ; 1 9 6 6 0 e. NN0
51 25 2 deccl 
 |-  ; ; 4 2 5 e. NN0
52 51 26 deccl 
 |-  ; ; ; 4 2 5 9 e. NN0
53 52 35 deccl 
 |-  ; ; ; ; 4 2 5 9 8 e. NN0
54 53 23 deccl 
 |-  ; ; ; ; ; 4 2 5 9 8 4 e. NN0
55 54 33 deccl 
 |-  ; ; ; ; ; ; 4 2 5 9 8 4 0 e. NN0
56 5 24 deccl 
 |-  ; 3 2 e. NN0
57 56 30 deccl 
 |-  ; ; 3 2 7 e. NN0
58 57 1 deccl 
 |-  ; ; ; 3 2 7 6 e. NN0
59 58 35 deccl 
 |-  ; ; ; ; 3 2 7 6 8 e. NN0
60 41 1 deccl 
 |-  ; ; ; ; ; 3 9 3 2 1 6 e. NN0
61 eqid 
 |-  ; ; ; ; ; ; 3 9 3 2 1 6 0 = ; ; ; ; ; ; 3 9 3 2 1 6 0
62 eqid 
 |-  ; ; ; ; ; 3 2 7 6 8 0 = ; ; ; ; ; 3 2 7 6 8 0
63 eqid 
 |-  ; ; ; ; ; 3 9 3 2 1 6 = ; ; ; ; ; 3 9 3 2 1 6
64 eqid 
 |-  ; ; ; ; 3 2 7 6 8 = ; ; ; ; 3 2 7 6 8
65 7p1e8 
 |-  ( 7 + 1 ) = 8
66 eqid 
 |-  ; ; ; ; 3 9 3 2 1 = ; ; ; ; 3 9 3 2 1
67 eqid 
 |-  ; ; ; 3 2 7 6 = ; ; ; 3 2 7 6
68 eqid 
 |-  ; ; ; 3 9 3 2 = ; ; ; 3 9 3 2
69 eqid 
 |-  ; ; 3 2 7 = ; ; 3 2 7
70 eqid 
 |-  ; ; 3 9 3 = ; ; 3 9 3
71 eqid 
 |-  ; 3 2 = ; 3 2
72 eqid 
 |-  ; 3 9 = ; 3 9
73 3p1e4 
 |-  ( 3 + 1 ) = 4
74 9p3e12 
 |-  ( 9 + 3 ) = ; 1 2
75 5 26 5 72 73 24 74 decaddci 
 |-  ( ; 3 9 + 3 ) = ; 4 2
76 3p2e5 
 |-  ( 3 + 2 ) = 5
77 37 5 5 24 70 71 75 76 decadd 
 |-  ( ; ; 3 9 3 + ; 3 2 ) = ; ; 4 2 5
78 7cn 
 |-  7 e. CC
79 2cn 
 |-  2 e. CC
80 7p2e9 
 |-  ( 7 + 2 ) = 9
81 78 79 80 addcomli 
 |-  ( 2 + 7 ) = 9
82 38 24 56 30 68 69 77 81 decadd 
 |-  ( ; ; ; 3 9 3 2 + ; ; 3 2 7 ) = ; ; ; 4 2 5 9
83 6cn 
 |-  6 e. CC
84 ax-1cn 
 |-  1 e. CC
85 6p1e7 
 |-  ( 6 + 1 ) = 7
86 83 84 85 addcomli 
 |-  ( 1 + 6 ) = 7
87 39 40 57 1 66 67 82 86 decadd 
 |-  ( ; ; ; ; 3 9 3 2 1 + ; ; ; 3 2 7 6 ) = ; ; ; ; 4 2 5 9 7
88 52 30 65 87 decsuc 
 |-  ( ( ; ; ; ; 3 9 3 2 1 + ; ; ; 3 2 7 6 ) + 1 ) = ; ; ; ; 4 2 5 9 8
89 8cn 
 |-  8 e. CC
90 8p6e14 
 |-  ( 8 + 6 ) = ; 1 4
91 89 83 90 addcomli 
 |-  ( 6 + 8 ) = ; 1 4
92 41 1 58 35 63 64 88 23 91 decaddc 
 |-  ( ; ; ; ; ; 3 9 3 2 1 6 + ; ; ; ; 3 2 7 6 8 ) = ; ; ; ; ; 4 2 5 9 8 4
93 00id 
 |-  ( 0 + 0 ) = 0
94 60 33 59 33 61 62 92 93 decadd 
 |-  ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) = ; ; ; ; ; ; 4 2 5 9 8 4 0
95 94 deceq1i 
 |-  ; ( ; ; ; ; ; ; 3 9 3 2 1 6 0 + ; ; ; ; ; 3 2 7 6 8 0 ) 0 = ; ; ; ; ; ; ; 4 2 5 9 8 4 0 0
96 eqid 
 |-  ; ; ; ; ; ; 4 2 5 9 8 4 0 = ; ; ; ; ; ; 4 2 5 9 8 4 0
97 eqid 
 |-  ; ; ; ; ; 4 2 5 9 8 4 = ; ; ; ; ; 4 2 5 9 8 4
98 5p1e6 
 |-  ( 5 + 1 ) = 6
99 eqid 
 |-  ; ; ; ; 4 2 5 9 8 = ; ; ; ; 4 2 5 9 8
100 1p1e2 
 |-  ( 1 + 1 ) = 2
101 eqid 
 |-  ; ; ; 4 2 5 9 = ; ; ; 4 2 5 9
102 8p1e9 
 |-  ( 8 + 1 ) = 9
103 eqid 
 |-  ; ; 4 2 5 = ; ; 4 2 5
104 5p3e8 
 |-  ( 5 + 3 ) = 8
105 25 2 5 103 104 decaddi 
 |-  ( ; ; 4 2 5 + 3 ) = ; ; 4 2 8
106 25 35 102 105 decsuc 
 |-  ( ( ; ; 4 2 5 + 3 ) + 1 ) = ; ; 4 2 9
107 9p2e11 
 |-  ( 9 + 2 ) = ; 1 1
108 51 26 5 24 101 71 106 40 107 decaddc 
 |-  ( ; ; ; 4 2 5 9 + ; 3 2 ) = ; ; ; 4 2 9 1
109 27 40 100 108 decsuc 
 |-  ( ( ; ; ; 4 2 5 9 + ; 3 2 ) + 1 ) = ; ; ; 4 2 9 2
110 8p7e15 
 |-  ( 8 + 7 ) = ; 1 5
111 52 35 56 30 99 69 109 2 110 decaddc 
 |-  ( ; ; ; ; 4 2 5 9 8 + ; ; 3 2 7 ) = ; ; ; ; 4 2 9 2 5
112 42 2 98 111 decsuc 
 |-  ( ( ; ; ; ; 4 2 5 9 8 + ; ; 3 2 7 ) + 1 ) = ; ; ; ; 4 2 9 2 6
113 4cn 
 |-  4 e. CC
114 6p4e10 
 |-  ( 6 + 4 ) = ; 1 0
115 83 113 114 addcomli 
 |-  ( 4 + 6 ) = ; 1 0
116 53 23 57 1 97 67 112 33 115 decaddc 
 |-  ( ; ; ; ; ; 4 2 5 9 8 4 + ; ; ; 3 2 7 6 ) = ; ; ; ; ; 4 2 9 2 6 0
117 89 addlidi 
 |-  ( 0 + 8 ) = 8
118 54 33 58 35 96 64 116 117 decadd 
 |-  ( ; ; ; ; ; ; 4 2 5 9 8 4 0 + ; ; ; ; 3 2 7 6 8 ) = ; ; ; ; ; ; 4 2 9 2 6 0 8
119 55 33 59 33 95 62 118 93 decadd 
 |-  ( ; ( ; ; ; ; ; ; 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
120 119 deceq1i 
 |-  ; ( ; ( ; ; ; ; ; ; 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
121 eqid 
 |-  ; ; ; ; ; 1 9 6 6 0 8 = ; ; ; ; ; 1 9 6 6 0 8
122 45 49 decaddm10 
 |-  ( ; ; ; ; ; ; ; 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
123 eqid 
 |-  ; ; ; ; ; ; 4 2 9 2 6 0 8 = ; ; ; ; ; ; 4 2 9 2 6 0 8
124 eqid 
 |-  ; ; ; 1 9 6 6 = ; ; ; 1 9 6 6
125 eqid 
 |-  ; ; ; ; ; 4 2 9 2 6 0 = ; ; ; ; ; 4 2 9 2 6 0
126 eqid 
 |-  ; ; 1 9 6 = ; ; 1 9 6
127 eqid 
 |-  ; ; ; ; 4 2 9 2 6 = ; ; ; ; 4 2 9 2 6
128 eqid 
 |-  ; 1 9 = ; 1 9
129 2p1e3 
 |-  ( 2 + 1 ) = 3
130 eqid 
 |-  ; ; ; 4 2 9 2 = ; ; ; 4 2 9 2
131 27 24 129 130 decsuc 
 |-  ( ; ; ; 4 2 9 2 + 1 ) = ; ; ; 4 2 9 3
132 27 5 73 131 decsuc 
 |-  ( ( ; ; ; 4 2 9 2 + 1 ) + 1 ) = ; ; ; 4 2 9 4
133 9cn 
 |-  9 e. CC
134 9p6e15 
 |-  ( 9 + 6 ) = ; 1 5
135 133 83 134 addcomli 
 |-  ( 6 + 9 ) = ; 1 5
136 42 1 40 26 127 128 132 2 135 decaddc 
 |-  ( ; ; ; ; 4 2 9 2 6 + ; 1 9 ) = ; ; ; ; 4 2 9 4 5
137 83 addlidi 
 |-  ( 0 + 6 ) = 6
138 43 33 47 1 125 126 136 137 decadd 
 |-  ( ; ; ; ; ; 4 2 9 2 6 0 + ; ; 1 9 6 ) = ; ; ; ; ; 4 2 9 4 5 6
139 29 1 85 138 decsuc 
 |-  ( ( ; ; ; ; ; 4 2 9 2 6 0 + ; ; 1 9 6 ) + 1 ) = ; ; ; ; ; 4 2 9 4 5 7
140 44 35 48 1 123 124 139 23 90 decaddc 
 |-  ( ; ; ; ; ; ; 4 2 9 2 6 0 8 + ; ; ; 1 9 6 6 ) = ; ; ; ; ; ; 4 2 9 4 5 7 4
141 140 deceq1i 
 |-  ; ( ; ; ; ; ; ; 4 2 9 2 6 0 8 + ; ; ; 1 9 6 6 ) 0 = ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0
142 122 141 eqtri 
 |-  ( ; ; ; ; ; ; ; 4 2 9 2 6 0 8 0 + ; ; ; ; 1 9 6 6 0 ) = ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0
143 46 33 50 35 120 121 142 117 decadd 
 |-  ( ; ( ; ( ; ; ; ; ; ; 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
144 143 deceq1i 
 |-  ; ( ; ( ; ( ; ; ; ; ; ; 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
145 eqid 
 |-  ; ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 8 = ; ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 8
146 eqid 
 |-  ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 = ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0
147 eqid 
 |-  ; ; ; ; ; ; 4 2 9 4 5 7 4 = ; ; ; ; ; ; 4 2 9 4 5 7 4
148 eqid 
 |-  ; ; ; ; ; 4 2 9 4 5 7 = ; ; ; ; ; 4 2 9 4 5 7
149 eqid 
 |-  ; ; ; ; 4 2 9 4 5 = ; ; ; ; 4 2 9 4 5
150 28 2 5 149 104 decaddi 
 |-  ( ; ; ; ; 4 2 9 4 5 + 3 ) = ; ; ; ; 4 2 9 4 8
151 28 35 102 150 decsuc 
 |-  ( ( ; ; ; ; 4 2 9 4 5 + 3 ) + 1 ) = ; ; ; ; 4 2 9 4 9
152 9p7e16 
 |-  ( 9 + 7 ) = ; 1 6
153 133 78 152 addcomli 
 |-  ( 7 + 9 ) = ; 1 6
154 29 30 5 26 148 72 151 1 153 decaddc 
 |-  ( ; ; ; ; ; 4 2 9 4 5 7 + ; 3 9 ) = ; ; ; ; ; 4 2 9 4 9 6
155 4p3e7 
 |-  ( 4 + 3 ) = 7
156 31 23 37 5 147 70 154 155 decadd 
 |-  ( ; ; ; ; ; ; 4 2 9 4 5 7 4 + ; ; 3 9 3 ) = ; ; ; ; ; ; 4 2 9 4 9 6 7
157 79 addlidi 
 |-  ( 0 + 2 ) = 2
158 32 33 38 24 146 68 156 157 decadd 
 |-  ( ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 + ; ; ; 3 9 3 2 ) = ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2
159 34 35 39 40 145 66 158 102 decadd 
 |-  ( ; ; ; ; ; ; ; ; 4 2 9 4 5 7 4 0 8 + ; ; ; ; 3 9 3 2 1 ) = ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9
160 36 33 41 1 144 63 159 137 decadd 
 |-  ( ; ( ; ( ; ( ; ; ; ; ; ; 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
161 9 22 160 3eqtri 
 |-  ( ; ; ; ; 6 5 5 3 6 ^ 2 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 6