Proof of Theorem fmtno5lem4
Step | Hyp | Ref
| Expression |
1 | | 6nn0 12254 |
. . . . . . . 8
⊢ 6 ∈
ℕ0 |
2 | | 5nn0 12253 |
. . . . . . . 8
⊢ 5 ∈
ℕ0 |
3 | 1, 2 | deccl 12452 |
. . . . . . 7
⊢ ;65 ∈
ℕ0 |
4 | 3, 2 | deccl 12452 |
. . . . . 6
⊢ ;;655 ∈ ℕ0 |
5 | | 3nn0 12251 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
6 | 4, 5 | deccl 12452 |
. . . . 5
⊢ ;;;6553
∈ ℕ0 |
7 | 6, 1 | deccl 12452 |
. . . 4
⊢ ;;;;65536 ∈
ℕ0 |
8 | 7 | nn0cni 12245 |
. . 3
⊢ ;;;;65536 ∈ ℂ |
9 | 8 | sqvali 13897 |
. 2
⊢ (;;;;65536↑2) = (;;;;65536 · ;;;;65536) |
10 | | fmtno5lem1 45005 |
. . . . . . . . . 10
⊢ (;;;;65536 · 6) = ;;;;;393216 |
11 | 10 | eqcomi 2747 |
. . . . . . . . 9
⊢ ;;;;;393216 = (;;;;65536 · 6) |
12 | | fmtno5lem2 45006 |
. . . . . . . . . 10
⊢ (;;;;65536 · 5) = ;;;;;327680 |
13 | 12 | eqcomi 2747 |
. . . . . . . . 9
⊢ ;;;;;327680 = (;;;;65536 · 5) |
14 | 1, 2, 7, 11, 13 | decmul10add 12506 |
. . . . . . . 8
⊢ (;;;;65536 · ;65) = (;;;;;;3932160 + ;;;;;327680) |
15 | 14 | eqcomi 2747 |
. . . . . . 7
⊢ (;;;;;;3932160 + ;;;;;327680) = (;;;;65536 · ;65) |
16 | 3, 2, 7, 15, 13 | decmul10add 12506 |
. . . . . 6
⊢ (;;;;65536 · ;;655) =
(;(;;;;;;3932160 + ;;;;;327680)0 + ;;;;;327680) |
17 | 16 | eqcomi 2747 |
. . . . 5
⊢ (;(;;;;;;3932160 + ;;;;;327680)0 + ;;;;;327680) = (;;;;65536 · ;;655) |
18 | | fmtno5lem3 45007 |
. . . . . 6
⊢ (;;;;65536 · 3) = ;;;;;196608 |
19 | 18 | eqcomi 2747 |
. . . . 5
⊢ ;;;;;196608 = (;;;;65536 · 3) |
20 | 4, 5, 7, 17, 19 | decmul10add 12506 |
. . . 4
⊢ (;;;;65536 · ;;;6553) = (;(;(;;;;;;3932160 + ;;;;;327680)0 + ;;;;;327680)0 + ;;;;;196608) |
21 | 20 | eqcomi 2747 |
. . 3
⊢ (;(;(;;;;;;3932160 + ;;;;;327680)0 + ;;;;;327680)0 + ;;;;;196608) = (;;;;65536 · ;;;6553) |
22 | 6, 1, 7, 21, 11 | decmul10add 12506 |
. 2
⊢ (;;;;65536 · ;;;;65536) = (;(;(;(;;;;;;3932160 + ;;;;;327680)0 + ;;;;;327680)0 + ;;;;;196608)0 + ;;;;;393216) |
23 | | 4nn0 12252 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ0 |
24 | | 2nn0 12250 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
25 | 23, 24 | deccl 12452 |
. . . . . . . . . 10
⊢ ;42 ∈
ℕ0 |
26 | | 9nn0 12257 |
. . . . . . . . . 10
⊢ 9 ∈
ℕ0 |
27 | 25, 26 | deccl 12452 |
. . . . . . . . 9
⊢ ;;429 ∈ ℕ0 |
28 | 27, 23 | deccl 12452 |
. . . . . . . 8
⊢ ;;;4294
∈ ℕ0 |
29 | 28, 2 | deccl 12452 |
. . . . . . 7
⊢ ;;;;42945 ∈
ℕ0 |
30 | | 7nn0 12255 |
. . . . . . 7
⊢ 7 ∈
ℕ0 |
31 | 29, 30 | deccl 12452 |
. . . . . 6
⊢ ;;;;;429457 ∈ ℕ0 |
32 | 31, 23 | deccl 12452 |
. . . . 5
⊢ ;;;;;;4294574 ∈ ℕ0 |
33 | | 0nn0 12248 |
. . . . 5
⊢ 0 ∈
ℕ0 |
34 | 32, 33 | deccl 12452 |
. . . 4
⊢ ;;;;;;;42945740 ∈
ℕ0 |
35 | | 8nn0 12256 |
. . . 4
⊢ 8 ∈
ℕ0 |
36 | 34, 35 | deccl 12452 |
. . 3
⊢ ;;;;;;;;429457408 ∈
ℕ0 |
37 | 5, 26 | deccl 12452 |
. . . . . 6
⊢ ;39 ∈
ℕ0 |
38 | 37, 5 | deccl 12452 |
. . . . 5
⊢ ;;393 ∈ ℕ0 |
39 | 38, 24 | deccl 12452 |
. . . 4
⊢ ;;;3932
∈ ℕ0 |
40 | | 1nn0 12249 |
. . . 4
⊢ 1 ∈
ℕ0 |
41 | 39, 40 | deccl 12452 |
. . 3
⊢ ;;;;39321 ∈
ℕ0 |
42 | 27, 24 | deccl 12452 |
. . . . . . . . 9
⊢ ;;;4292
∈ ℕ0 |
43 | 42, 1 | deccl 12452 |
. . . . . . . 8
⊢ ;;;;42926 ∈
ℕ0 |
44 | 43, 33 | deccl 12452 |
. . . . . . 7
⊢ ;;;;;429260 ∈ ℕ0 |
45 | 44, 35 | deccl 12452 |
. . . . . 6
⊢ ;;;;;;4292608 ∈ ℕ0 |
46 | 45, 33 | deccl 12452 |
. . . . 5
⊢ ;;;;;;;42926080 ∈
ℕ0 |
47 | 40, 26 | deccl 12452 |
. . . . . . . 8
⊢ ;19 ∈
ℕ0 |
48 | 47, 1 | deccl 12452 |
. . . . . . 7
⊢ ;;196 ∈ ℕ0 |
49 | 48, 1 | deccl 12452 |
. . . . . 6
⊢ ;;;1966
∈ ℕ0 |
50 | 49, 33 | deccl 12452 |
. . . . 5
⊢ ;;;;19660 ∈
ℕ0 |
51 | 25, 2 | deccl 12452 |
. . . . . . . . . . 11
⊢ ;;425 ∈ ℕ0 |
52 | 51, 26 | deccl 12452 |
. . . . . . . . . 10
⊢ ;;;4259
∈ ℕ0 |
53 | 52, 35 | deccl 12452 |
. . . . . . . . 9
⊢ ;;;;42598 ∈
ℕ0 |
54 | 53, 23 | deccl 12452 |
. . . . . . . 8
⊢ ;;;;;425984 ∈ ℕ0 |
55 | 54, 33 | deccl 12452 |
. . . . . . 7
⊢ ;;;;;;4259840 ∈ ℕ0 |
56 | 5, 24 | deccl 12452 |
. . . . . . . . . 10
⊢ ;32 ∈
ℕ0 |
57 | 56, 30 | deccl 12452 |
. . . . . . . . 9
⊢ ;;327 ∈ ℕ0 |
58 | 57, 1 | deccl 12452 |
. . . . . . . 8
⊢ ;;;3276
∈ ℕ0 |
59 | 58, 35 | deccl 12452 |
. . . . . . 7
⊢ ;;;;32768 ∈
ℕ0 |
60 | 41, 1 | deccl 12452 |
. . . . . . . . 9
⊢ ;;;;;393216 ∈ ℕ0 |
61 | | eqid 2738 |
. . . . . . . . 9
⊢ ;;;;;;3932160 = ;;;;;;3932160 |
62 | | eqid 2738 |
. . . . . . . . 9
⊢ ;;;;;327680 = ;;;;;327680 |
63 | | eqid 2738 |
. . . . . . . . . 10
⊢ ;;;;;393216 = ;;;;;393216 |
64 | | eqid 2738 |
. . . . . . . . . 10
⊢ ;;;;32768 = ;;;;32768 |
65 | | 7p1e8 12122 |
. . . . . . . . . . 11
⊢ (7 + 1) =
8 |
66 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ ;;;;39321 = ;;;;39321 |
67 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ ;;;3276 =
;;;3276 |
68 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ ;;;3932 =
;;;3932 |
69 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ ;;327 = ;;327 |
70 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ ;;393 = ;;393 |
71 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ ;32 = ;32 |
72 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ ;39 = ;39 |
73 | | 3p1e4 12118 |
. . . . . . . . . . . . . . 15
⊢ (3 + 1) =
4 |
74 | | 9p3e12 12525 |
. . . . . . . . . . . . . . 15
⊢ (9 + 3) =
;12 |
75 | 5, 26, 5, 72, 73, 24, 74 | decaddci 12498 |
. . . . . . . . . . . . . 14
⊢ (;39 + 3) = ;42 |
76 | | 3p2e5 12124 |
. . . . . . . . . . . . . 14
⊢ (3 + 2) =
5 |
77 | 37, 5, 5, 24, 70, 71, 75, 76 | decadd 12491 |
. . . . . . . . . . . . 13
⊢ (;;393 + ;32) = ;;425 |
78 | | 7cn 12067 |
. . . . . . . . . . . . . 14
⊢ 7 ∈
ℂ |
79 | | 2cn 12048 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
80 | | 7p2e9 12134 |
. . . . . . . . . . . . . 14
⊢ (7 + 2) =
9 |
81 | 78, 79, 80 | addcomli 11167 |
. . . . . . . . . . . . 13
⊢ (2 + 7) =
9 |
82 | 38, 24, 56, 30, 68, 69, 77, 81 | decadd 12491 |
. . . . . . . . . . . 12
⊢ (;;;3932 +
;;327) = ;;;4259 |
83 | | 6cn 12064 |
. . . . . . . . . . . . 13
⊢ 6 ∈
ℂ |
84 | | ax-1cn 10929 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
85 | | 6p1e7 12121 |
. . . . . . . . . . . . 13
⊢ (6 + 1) =
7 |
86 | 83, 84, 85 | addcomli 11167 |
. . . . . . . . . . . 12
⊢ (1 + 6) =
7 |
87 | 39, 40, 57, 1, 66, 67, 82, 86 | decadd 12491 |
. . . . . . . . . . 11
⊢ (;;;;39321 + ;;;3276) = ;;;;42597 |
88 | 52, 30, 65, 87 | decsuc 12468 |
. . . . . . . . . 10
⊢ ((;;;;39321 + ;;;3276) + 1) = ;;;;42598 |
89 | | 8cn 12070 |
. . . . . . . . . . 11
⊢ 8 ∈
ℂ |
90 | | 8p6e14 12521 |
. . . . . . . . . . 11
⊢ (8 + 6) =
;14 |
91 | 89, 83, 90 | addcomli 11167 |
. . . . . . . . . 10
⊢ (6 + 8) =
;14 |
92 | 41, 1, 58, 35, 63, 64, 88, 23, 91 | decaddc 12492 |
. . . . . . . . 9
⊢ (;;;;;393216 + ;;;;32768) = ;;;;;425984 |
93 | | 00id 11150 |
. . . . . . . . 9
⊢ (0 + 0) =
0 |
94 | 60, 33, 59, 33, 61, 62, 92, 93 | decadd 12491 |
. . . . . . . 8
⊢ (;;;;;;3932160 + ;;;;;327680) = ;;;;;;4259840 |
95 | 94 | deceq1i 12444 |
. . . . . . 7
⊢ ;(;;;;;;3932160 + ;;;;;327680)0 = ;;;;;;;42598400 |
96 | | eqid 2738 |
. . . . . . . 8
⊢ ;;;;;;4259840 = ;;;;;;4259840 |
97 | | eqid 2738 |
. . . . . . . . 9
⊢ ;;;;;425984 = ;;;;;425984 |
98 | | 5p1e6 12120 |
. . . . . . . . . 10
⊢ (5 + 1) =
6 |
99 | | eqid 2738 |
. . . . . . . . . . 11
⊢ ;;;;42598 = ;;;;42598 |
100 | | 1p1e2 12098 |
. . . . . . . . . . . 12
⊢ (1 + 1) =
2 |
101 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ ;;;4259 =
;;;4259 |
102 | | 8p1e9 12123 |
. . . . . . . . . . . . . 14
⊢ (8 + 1) =
9 |
103 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ ;;425 = ;;425 |
104 | | 5p3e8 12130 |
. . . . . . . . . . . . . . 15
⊢ (5 + 3) =
8 |
105 | 25, 2, 5, 103, 104 | decaddi 12497 |
. . . . . . . . . . . . . 14
⊢ (;;425 + 3) = ;;428 |
106 | 25, 35, 102, 105 | decsuc 12468 |
. . . . . . . . . . . . 13
⊢ ((;;425 + 3) + 1) = ;;429 |
107 | | 9p2e11 12524 |
. . . . . . . . . . . . 13
⊢ (9 + 2) =
;11 |
108 | 51, 26, 5, 24, 101, 71, 106, 40, 107 | decaddc 12492 |
. . . . . . . . . . . 12
⊢ (;;;4259 +
;32) = ;;;4291 |
109 | 27, 40, 100, 108 | decsuc 12468 |
. . . . . . . . . . 11
⊢ ((;;;4259 +
;32) + 1) = ;;;4292 |
110 | | 8p7e15 12522 |
. . . . . . . . . . 11
⊢ (8 + 7) =
;15 |
111 | 52, 35, 56, 30, 99, 69, 109, 2, 110 | decaddc 12492 |
. . . . . . . . . 10
⊢ (;;;;42598 + ;;327) =
;;;;42925 |
112 | 42, 2, 98, 111 | decsuc 12468 |
. . . . . . . . 9
⊢ ((;;;;42598 + ;;327) +
1) = ;;;;42926 |
113 | | 4cn 12058 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
114 | | 6p4e10 12509 |
. . . . . . . . . 10
⊢ (6 + 4) =
;10 |
115 | 83, 113, 114 | addcomli 11167 |
. . . . . . . . 9
⊢ (4 + 6) =
;10 |
116 | 53, 23, 57, 1, 97, 67, 112, 33, 115 | decaddc 12492 |
. . . . . . . 8
⊢ (;;;;;425984 + ;;;3276) = ;;;;;429260 |
117 | 89 | addid2i 11163 |
. . . . . . . 8
⊢ (0 + 8) =
8 |
118 | 54, 33, 58, 35, 96, 64, 116, 117 | decadd 12491 |
. . . . . . 7
⊢ (;;;;;;4259840 + ;;;;32768) = ;;;;;;4292608 |
119 | 55, 33, 59, 33, 95, 62, 118, 93 | decadd 12491 |
. . . . . 6
⊢ (;(;;;;;;3932160 + ;;;;;327680)0 + ;;;;;327680) = ;;;;;;;42926080 |
120 | 119 | deceq1i 12444 |
. . . . 5
⊢ ;(;(;;;;;;3932160 + ;;;;;327680)0 + ;;;;;327680)0 = ;;;;;;;;429260800 |
121 | | eqid 2738 |
. . . . 5
⊢ ;;;;;196608 = ;;;;;196608 |
122 | 45, 49 | decaddm10 12496 |
. . . . . 6
⊢ (;;;;;;;42926080 + ;;;;19660) = ;(;;;;;;4292608 + ;;;1966)0 |
123 | | eqid 2738 |
. . . . . . . 8
⊢ ;;;;;;4292608 = ;;;;;;4292608 |
124 | | eqid 2738 |
. . . . . . . 8
⊢ ;;;1966 =
;;;1966 |
125 | | eqid 2738 |
. . . . . . . . . 10
⊢ ;;;;;429260 = ;;;;;429260 |
126 | | eqid 2738 |
. . . . . . . . . 10
⊢ ;;196 = ;;196 |
127 | | eqid 2738 |
. . . . . . . . . . 11
⊢ ;;;;42926 = ;;;;42926 |
128 | | eqid 2738 |
. . . . . . . . . . 11
⊢ ;19 = ;19 |
129 | | 2p1e3 12115 |
. . . . . . . . . . . . 13
⊢ (2 + 1) =
3 |
130 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ ;;;4292 =
;;;4292 |
131 | 27, 24, 129, 130 | decsuc 12468 |
. . . . . . . . . . . 12
⊢ (;;;4292 +
1) = ;;;4293 |
132 | 27, 5, 73, 131 | decsuc 12468 |
. . . . . . . . . . 11
⊢ ((;;;4292 +
1) + 1) = ;;;4294 |
133 | | 9cn 12073 |
. . . . . . . . . . . 12
⊢ 9 ∈
ℂ |
134 | | 9p6e15 12528 |
. . . . . . . . . . . 12
⊢ (9 + 6) =
;15 |
135 | 133, 83, 134 | addcomli 11167 |
. . . . . . . . . . 11
⊢ (6 + 9) =
;15 |
136 | 42, 1, 40, 26, 127, 128, 132, 2, 135 | decaddc 12492 |
. . . . . . . . . 10
⊢ (;;;;42926 + ;19) = ;;;;42945 |
137 | 83 | addid2i 11163 |
. . . . . . . . . 10
⊢ (0 + 6) =
6 |
138 | 43, 33, 47, 1, 125, 126, 136, 137 | decadd 12491 |
. . . . . . . . 9
⊢ (;;;;;429260 + ;;196) =
;;;;;429456 |
139 | 29, 1, 85, 138 | decsuc 12468 |
. . . . . . . 8
⊢ ((;;;;;429260 + ;;196) +
1) = ;;;;;429457 |
140 | 44, 35, 48, 1, 123, 124, 139, 23, 90 | decaddc 12492 |
. . . . . . 7
⊢ (;;;;;;4292608 + ;;;1966) = ;;;;;;4294574 |
141 | 140 | deceq1i 12444 |
. . . . . 6
⊢ ;(;;;;;;4292608 + ;;;1966)0 = ;;;;;;;42945740 |
142 | 122, 141 | eqtri 2766 |
. . . . 5
⊢ (;;;;;;;42926080 + ;;;;19660) = ;;;;;;;42945740 |
143 | 46, 33, 50, 35, 120, 121, 142, 117 | decadd 12491 |
. . . 4
⊢ (;(;(;;;;;;3932160 + ;;;;;327680)0 + ;;;;;327680)0 + ;;;;;196608) = ;;;;;;;;429457408 |
144 | 143 | deceq1i 12444 |
. . 3
⊢ ;(;(;(;;;;;;3932160 + ;;;;;327680)0 + ;;;;;327680)0 + ;;;;;196608)0 = ;;;;;;;;;4294574080 |
145 | | eqid 2738 |
. . . 4
⊢ ;;;;;;;;429457408 = ;;;;;;;;429457408 |
146 | | eqid 2738 |
. . . . 5
⊢ ;;;;;;;42945740 = ;;;;;;;42945740 |
147 | | eqid 2738 |
. . . . . 6
⊢ ;;;;;;4294574 = ;;;;;;4294574 |
148 | | eqid 2738 |
. . . . . . 7
⊢ ;;;;;429457 = ;;;;;429457 |
149 | | eqid 2738 |
. . . . . . . . 9
⊢ ;;;;42945 = ;;;;42945 |
150 | 28, 2, 5, 149, 104 | decaddi 12497 |
. . . . . . . 8
⊢ (;;;;42945 + 3) = ;;;;42948 |
151 | 28, 35, 102, 150 | decsuc 12468 |
. . . . . . 7
⊢ ((;;;;42945 + 3) + 1) = ;;;;42949 |
152 | | 9p7e16 12529 |
. . . . . . . 8
⊢ (9 + 7) =
;16 |
153 | 133, 78, 152 | addcomli 11167 |
. . . . . . 7
⊢ (7 + 9) =
;16 |
154 | 29, 30, 5, 26, 148, 72, 151, 1, 153 | decaddc 12492 |
. . . . . 6
⊢ (;;;;;429457 + ;39) = ;;;;;429496 |
155 | | 4p3e7 12127 |
. . . . . 6
⊢ (4 + 3) =
7 |
156 | 31, 23, 37, 5, 147, 70, 154, 155 | decadd 12491 |
. . . . 5
⊢ (;;;;;;4294574 + ;;393) =
;;;;;;4294967 |
157 | 79 | addid2i 11163 |
. . . . 5
⊢ (0 + 2) =
2 |
158 | 32, 33, 38, 24, 146, 68, 156, 157 | decadd 12491 |
. . . 4
⊢ (;;;;;;;42945740 + ;;;3932) = ;;;;;;;42949672 |
159 | 34, 35, 39, 40, 145, 66, 158, 102 | decadd 12491 |
. . 3
⊢ (;;;;;;;;429457408 + ;;;;39321) = ;;;;;;;;429496729 |
160 | 36, 33, 41, 1, 144, 63, 159, 137 | decadd 12491 |
. 2
⊢ (;(;(;(;;;;;;3932160 + ;;;;;327680)0 + ;;;;;327680)0 + ;;;;;196608)0 + ;;;;;393216) = ;;;;;;;;;4294967296 |
161 | 9, 22, 160 | 3eqtri 2770 |
1
⊢ (;;;;65536↑2) = ;;;;;;;;;4294967296 |