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 ∈ ℕ0
2 5nn0 ⊢ 5 ∈ ℕ0
3 1 2 deccl ⊢ 6 5 ∈ ℕ0
4 3 2 deccl ⊢ 6 5 5 ∈ ℕ0
5 3nn0 ⊢ 3 ∈ ℕ0
6 4 5 deccl ⊢ 6 5 5 3 ∈ ℕ0
7 6 1 deccl ⊢ 6 5 5 3 6 ∈ ℕ0
8 7 nn0cni ⊢ 6 5 5 3 6 ∈ ℂ
9 8 sqvali ⊢ ( 6 5 5 3 6 ↑ 2 ) = ( 6 5 5 3 6 · 6 5 5 3 6 )
10 fmtno5lem1 ⊢ ( 6 5 5 3 6 · 6 ) = 3 9 3 2 1 6
11 10 eqcomi ⊢ 3 9 3 2 1 6 = ( 6 5 5 3 6 · 6 )
12 fmtno5lem2 ⊢ ( 6 5 5 3 6 · 5 ) = 3 2 7 6 8 0
13 12 eqcomi ⊢ 3 2 7 6 8 0 = ( 6 5 5 3 6 · 5 )
14 1 2 7 11 13 decmul10add ⊢ ( 6 5 5 3 6 · 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 · 6 5 )
16 3 2 7 15 13 decmul10add ⊢ ( 6 5 5 3 6 · 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 · 6 5 5 )
18 fmtno5lem3 ⊢ ( 6 5 5 3 6 · 3 ) = 1 9 6 6 0 8
19 18 eqcomi ⊢ 1 9 6 6 0 8 = ( 6 5 5 3 6 · 3 )
20 4 5 7 17 19 decmul10add ⊢ ( 6 5 5 3 6 · 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 · 6 5 5 3 )
22 6 1 7 21 11 decmul10add ⊢ ( 6 5 5 3 6 · 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 ∈ ℕ0
24 2nn0 ⊢ 2 ∈ ℕ0
25 23 24 deccl ⊢ 4 2 ∈ ℕ0
26 9nn0 ⊢ 9 ∈ ℕ0
27 25 26 deccl ⊢ 4 2 9 ∈ ℕ0
28 27 23 deccl ⊢ 4 2 9 4 ∈ ℕ0
29 28 2 deccl ⊢ 4 2 9 4 5 ∈ ℕ0
30 7nn0 ⊢ 7 ∈ ℕ0
31 29 30 deccl ⊢ 4 2 9 4 5 7 ∈ ℕ0
32 31 23 deccl ⊢ 4 2 9 4 5 7 4 ∈ ℕ0
33 0nn0 ⊢ 0 ∈ ℕ0
34 32 33 deccl ⊢ 4 2 9 4 5 7 4 0 ∈ ℕ0
35 8nn0 ⊢ 8 ∈ ℕ0
36 34 35 deccl ⊢ 4 2 9 4 5 7 4 0 8 ∈ ℕ0
37 5 26 deccl ⊢ 3 9 ∈ ℕ0
38 37 5 deccl ⊢ 3 9 3 ∈ ℕ0
39 38 24 deccl ⊢ 3 9 3 2 ∈ ℕ0
40 1nn0 ⊢ 1 ∈ ℕ0
41 39 40 deccl ⊢ 3 9 3 2 1 ∈ ℕ0
42 27 24 deccl ⊢ 4 2 9 2 ∈ ℕ0
43 42 1 deccl ⊢ 4 2 9 2 6 ∈ ℕ0
44 43 33 deccl ⊢ 4 2 9 2 6 0 ∈ ℕ0
45 44 35 deccl ⊢ 4 2 9 2 6 0 8 ∈ ℕ0
46 45 33 deccl ⊢ 4 2 9 2 6 0 8 0 ∈ ℕ0
47 40 26 deccl ⊢ 1 9 ∈ ℕ0
48 47 1 deccl ⊢ 1 9 6 ∈ ℕ0
49 48 1 deccl ⊢ 1 9 6 6 ∈ ℕ0
50 49 33 deccl ⊢ 1 9 6 6 0 ∈ ℕ0
51 25 2 deccl ⊢ 4 2 5 ∈ ℕ0
52 51 26 deccl ⊢ 4 2 5 9 ∈ ℕ0
53 52 35 deccl ⊢ 4 2 5 9 8 ∈ ℕ0
54 53 23 deccl ⊢ 4 2 5 9 8 4 ∈ ℕ0
55 54 33 deccl ⊢ 4 2 5 9 8 4 0 ∈ ℕ0
56 5 24 deccl ⊢ 3 2 ∈ ℕ0
57 56 30 deccl ⊢ 3 2 7 ∈ ℕ0
58 57 1 deccl ⊢ 3 2 7 6 ∈ ℕ0
59 58 35 deccl ⊢ 3 2 7 6 8 ∈ ℕ0
60 41 1 deccl ⊢ 3 9 3 2 1 6 ∈ ℕ0
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 ∈ ℂ
79 2cn ⊢ 2 ∈ ℂ
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 ∈ ℂ
84 ax-1cn ⊢ 1 ∈ ℂ
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 ∈ ℂ
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 ∈ ℂ
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 ∈ ℂ
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