Proof of Theorem fmtno5lem4
Step | Hyp | Ref
| Expression |
1 | | 6nn0 11313 |
. . . . . . . 8
|
2 | | 5nn0 11312 |
. . . . . . . 8
|
3 | 1, 2 | deccl 11512 |
. . . . . . 7
; |
4 | 3, 2 | deccl 11512 |
. . . . . 6
;; |
5 | | 3nn0 11310 |
. . . . . 6
|
6 | 4, 5 | deccl 11512 |
. . . . 5
;;; |
7 | 6, 1 | deccl 11512 |
. . . 4
;;;; |
8 | 7 | nn0cni 11304 |
. . 3
;;;; |
9 | 8 | sqvali 12943 |
. 2
;;;; ;;;; ;;;; |
10 | | fmtno5lem1 41465 |
. . . . . . . . . 10
;;;; ;;;;; |
11 | 10 | eqcomi 2631 |
. . . . . . . . 9
;;;;; ;;;; |
12 | | fmtno5lem2 41466 |
. . . . . . . . . 10
;;;; ;;;;; |
13 | 12 | eqcomi 2631 |
. . . . . . . . 9
;;;;; ;;;; |
14 | 1, 2, 7, 11, 13 | decmul10add 11593 |
. . . . . . . 8
;;;; ; ;;;;;; ;;;;; |
15 | 14 | eqcomi 2631 |
. . . . . . 7
;;;;;; ;;;;; ;;;; ; |
16 | 3, 2, 7, 15, 13 | decmul10add 11593 |
. . . . . 6
;;;; ;; ;;;;;;; ;;;;; ;;;;; |
17 | 16 | eqcomi 2631 |
. . . . 5
;;;;;;; ;;;;; ;;;;; ;;;; ;; |
18 | | fmtno5lem3 41467 |
. . . . . 6
;;;; ;;;;; |
19 | 18 | eqcomi 2631 |
. . . . 5
;;;;; ;;;; |
20 | 4, 5, 7, 17, 19 | decmul10add 11593 |
. . . 4
;;;; ;;; ;;;;;;;; ;;;;; ;;;;; ;;;;; |
21 | 20 | eqcomi 2631 |
. . 3
;;;;;;;; ;;;;; ;;;;; ;;;;; ;;;; ;;; |
22 | 6, 1, 7, 21, 11 | decmul10add 11593 |
. 2
;;;; ;;;; ;;;;;;;;; ;;;;; ;;;;; ;;;;; ;;;;; |
23 | | 4nn0 11311 |
. . . . . . . . . . 11
|
24 | | 2nn0 11309 |
. . . . . . . . . . 11
|
25 | 23, 24 | deccl 11512 |
. . . . . . . . . 10
; |
26 | | 9nn0 11316 |
. . . . . . . . . 10
|
27 | 25, 26 | deccl 11512 |
. . . . . . . . 9
;; |
28 | 27, 23 | deccl 11512 |
. . . . . . . 8
;;; |
29 | 28, 2 | deccl 11512 |
. . . . . . 7
;;;; |
30 | | 7nn0 11314 |
. . . . . . 7
|
31 | 29, 30 | deccl 11512 |
. . . . . 6
;;;;; |
32 | 31, 23 | deccl 11512 |
. . . . 5
;;;;;; |
33 | | 0nn0 11307 |
. . . . 5
|
34 | 32, 33 | deccl 11512 |
. . . 4
;;;;;;; |
35 | | 8nn0 11315 |
. . . 4
|
36 | 34, 35 | deccl 11512 |
. . 3
;;;;;;;; |
37 | 5, 26 | deccl 11512 |
. . . . . 6
; |
38 | 37, 5 | deccl 11512 |
. . . . 5
;; |
39 | 38, 24 | deccl 11512 |
. . . 4
;;; |
40 | | 1nn0 11308 |
. . . 4
|
41 | 39, 40 | deccl 11512 |
. . 3
;;;; |
42 | 27, 24 | deccl 11512 |
. . . . . . . . 9
;;; |
43 | 42, 1 | deccl 11512 |
. . . . . . . 8
;;;; |
44 | 43, 33 | deccl 11512 |
. . . . . . 7
;;;;; |
45 | 44, 35 | deccl 11512 |
. . . . . 6
;;;;;; |
46 | 45, 33 | deccl 11512 |
. . . . 5
;;;;;;; |
47 | 40, 26 | deccl 11512 |
. . . . . . . 8
; |
48 | 47, 1 | deccl 11512 |
. . . . . . 7
;; |
49 | 48, 1 | deccl 11512 |
. . . . . 6
;;; |
50 | 49, 33 | deccl 11512 |
. . . . 5
;;;; |
51 | 25, 2 | deccl 11512 |
. . . . . . . . . . 11
;; |
52 | 51, 26 | deccl 11512 |
. . . . . . . . . 10
;;; |
53 | 52, 35 | deccl 11512 |
. . . . . . . . 9
;;;; |
54 | 53, 23 | deccl 11512 |
. . . . . . . 8
;;;;; |
55 | 54, 33 | deccl 11512 |
. . . . . . 7
;;;;;; |
56 | 5, 24 | deccl 11512 |
. . . . . . . . . 10
; |
57 | 56, 30 | deccl 11512 |
. . . . . . . . 9
;; |
58 | 57, 1 | deccl 11512 |
. . . . . . . 8
;;; |
59 | 58, 35 | deccl 11512 |
. . . . . . 7
;;;; |
60 | 41, 1 | deccl 11512 |
. . . . . . . . 9
;;;;; |
61 | | eqid 2622 |
. . . . . . . . 9
;;;;;; ;;;;;; |
62 | | eqid 2622 |
. . . . . . . . 9
;;;;; ;;;;; |
63 | | eqid 2622 |
. . . . . . . . . 10
;;;;; ;;;;; |
64 | | eqid 2622 |
. . . . . . . . . 10
;;;; ;;;; |
65 | | 7p1e8 11157 |
. . . . . . . . . . 11
|
66 | | eqid 2622 |
. . . . . . . . . . . 12
;;;; ;;;; |
67 | | eqid 2622 |
. . . . . . . . . . . 12
;;; ;;; |
68 | | eqid 2622 |
. . . . . . . . . . . . 13
;;; ;;; |
69 | | eqid 2622 |
. . . . . . . . . . . . 13
;; ;; |
70 | | eqid 2622 |
. . . . . . . . . . . . . 14
;; ;; |
71 | | eqid 2622 |
. . . . . . . . . . . . . 14
; ; |
72 | | eqid 2622 |
. . . . . . . . . . . . . . 15
; ; |
73 | | 3p1e4 11153 |
. . . . . . . . . . . . . . 15
|
74 | | 9p3e12 11621 |
. . . . . . . . . . . . . . 15
; |
75 | 5, 26, 5, 72, 73, 24, 74 | decaddci 11580 |
. . . . . . . . . . . . . 14
; ; |
76 | | 3p2e5 11160 |
. . . . . . . . . . . . . 14
|
77 | 37, 5, 5, 24, 70, 71, 75, 76 | decadd 11570 |
. . . . . . . . . . . . 13
;; ; ;; |
78 | | 7cn 11104 |
. . . . . . . . . . . . . 14
|
79 | | 2cn 11091 |
. . . . . . . . . . . . . 14
|
80 | | 7p2e9 11172 |
. . . . . . . . . . . . . 14
|
81 | 78, 79, 80 | addcomli 10228 |
. . . . . . . . . . . . 13
|
82 | 38, 24, 56, 30, 68, 69, 77, 81 | decadd 11570 |
. . . . . . . . . . . 12
;;; ;; ;;; |
83 | | 6cn 11102 |
. . . . . . . . . . . . 13
|
84 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
|
85 | | 6p1e7 11156 |
. . . . . . . . . . . . 13
|
86 | 83, 84, 85 | addcomli 10228 |
. . . . . . . . . . . 12
|
87 | 39, 40, 57, 1, 66, 67, 82, 86 | decadd 11570 |
. . . . . . . . . . 11
;;;; ;;; ;;;; |
88 | 52, 30, 65, 87 | decsuc 11535 |
. . . . . . . . . 10
;;;; ;;; ;;;; |
89 | | 8cn 11106 |
. . . . . . . . . . 11
|
90 | | 8p6e14 11616 |
. . . . . . . . . . 11
; |
91 | 89, 83, 90 | addcomli 10228 |
. . . . . . . . . 10
; |
92 | 41, 1, 58, 35, 63, 64, 88, 23, 91 | decaddc 11572 |
. . . . . . . . 9
;;;;; ;;;; ;;;;; |
93 | | 00id 10211 |
. . . . . . . . 9
|
94 | 60, 33, 59, 33, 61, 62, 92, 93 | decadd 11570 |
. . . . . . . 8
;;;;;; ;;;;; ;;;;;; |
95 | 94 | deceq1i 11504 |
. . . . . . 7
;;;;;;; ;;;;; ;;;;;;; |
96 | | eqid 2622 |
. . . . . . . 8
;;;;;; ;;;;;; |
97 | | eqid 2622 |
. . . . . . . . 9
;;;;; ;;;;; |
98 | | 5p1e6 11155 |
. . . . . . . . . 10
|
99 | | eqid 2622 |
. . . . . . . . . . 11
;;;; ;;;; |
100 | | 1p1e2 11134 |
. . . . . . . . . . . 12
|
101 | | eqid 2622 |
. . . . . . . . . . . . 13
;;; ;;; |
102 | | 8p1e9 11158 |
. . . . . . . . . . . . . 14
|
103 | | eqid 2622 |
. . . . . . . . . . . . . . 15
;; ;; |
104 | | 5p3e8 11166 |
. . . . . . . . . . . . . . 15
|
105 | 25, 2, 5, 103, 104 | decaddi 11579 |
. . . . . . . . . . . . . 14
;; ;; |
106 | 25, 35, 102, 105 | decsuc 11535 |
. . . . . . . . . . . . 13
;; ;; |
107 | | 9p2e11 11619 |
. . . . . . . . . . . . 13
; |
108 | 51, 26, 5, 24, 101, 71, 106, 40, 107 | decaddc 11572 |
. . . . . . . . . . . 12
;;; ; ;;; |
109 | 27, 40, 100, 108 | decsuc 11535 |
. . . . . . . . . . 11
;;; ; ;;; |
110 | | 8p7e15 11617 |
. . . . . . . . . . 11
; |
111 | 52, 35, 56, 30, 99, 69, 109, 2, 110 | decaddc 11572 |
. . . . . . . . . 10
;;;; ;; ;;;; |
112 | 42, 2, 98, 111 | decsuc 11535 |
. . . . . . . . 9
;;;; ;; ;;;; |
113 | | 4cn 11098 |
. . . . . . . . . 10
|
114 | | 6p4e10 11598 |
. . . . . . . . . 10
; |
115 | 83, 113, 114 | addcomli 10228 |
. . . . . . . . 9
; |
116 | 53, 23, 57, 1, 97, 67, 112, 33, 115 | decaddc 11572 |
. . . . . . . 8
;;;;; ;;; ;;;;; |
117 | 89 | addid2i 10224 |
. . . . . . . 8
|
118 | 54, 33, 58, 35, 96, 64, 116, 117 | decadd 11570 |
. . . . . . 7
;;;;;; ;;;; ;;;;;; |
119 | 55, 33, 59, 33, 95, 62, 118, 93 | decadd 11570 |
. . . . . 6
;;;;;;; ;;;;; ;;;;; ;;;;;;; |
120 | 119 | deceq1i 11504 |
. . . . 5
;;;;;;;; ;;;;; ;;;;; ;;;;;;;; |
121 | | eqid 2622 |
. . . . 5
;;;;; ;;;;; |
122 | 45, 49 | decaddm10 11578 |
. . . . . 6
;;;;;;; ;;;; ;;;;;;; ;;; |
123 | | eqid 2622 |
. . . . . . . 8
;;;;;; ;;;;;; |
124 | | eqid 2622 |
. . . . . . . 8
;;; ;;; |
125 | | eqid 2622 |
. . . . . . . . . 10
;;;;; ;;;;; |
126 | | eqid 2622 |
. . . . . . . . . 10
;; ;; |
127 | | eqid 2622 |
. . . . . . . . . . 11
;;;; ;;;; |
128 | | eqid 2622 |
. . . . . . . . . . 11
; ; |
129 | | 2p1e3 11151 |
. . . . . . . . . . . . 13
|
130 | | eqid 2622 |
. . . . . . . . . . . . 13
;;; ;;; |
131 | 27, 24, 129, 130 | decsuc 11535 |
. . . . . . . . . . . 12
;;; ;;; |
132 | 27, 5, 73, 131 | decsuc 11535 |
. . . . . . . . . . 11
;;; ;;; |
133 | | 9cn 11108 |
. . . . . . . . . . . 12
|
134 | | 9p6e15 11624 |
. . . . . . . . . . . 12
; |
135 | 133, 83, 134 | addcomli 10228 |
. . . . . . . . . . 11
; |
136 | 42, 1, 40, 26, 127, 128, 132, 2, 135 | decaddc 11572 |
. . . . . . . . . 10
;;;; ; ;;;; |
137 | 83 | addid2i 10224 |
. . . . . . . . . 10
|
138 | 43, 33, 47, 1, 125, 126, 136, 137 | decadd 11570 |
. . . . . . . . 9
;;;;; ;; ;;;;; |
139 | 29, 1, 85, 138 | decsuc 11535 |
. . . . . . . 8
;;;;; ;; ;;;;; |
140 | 44, 35, 48, 1, 123, 124, 139, 23, 90 | decaddc 11572 |
. . . . . . 7
;;;;;; ;;; ;;;;;; |
141 | 140 | deceq1i 11504 |
. . . . . 6
;;;;;;; ;;; ;;;;;;; |
142 | 122, 141 | eqtri 2644 |
. . . . 5
;;;;;;; ;;;; ;;;;;;; |
143 | 46, 33, 50, 35, 120, 121, 142, 117 | decadd 11570 |
. . . 4
;;;;;;;; ;;;;; ;;;;; ;;;;; ;;;;;;;; |
144 | 143 | deceq1i 11504 |
. . 3
;;;;;;;;; ;;;;; ;;;;; ;;;;; ;;;;;;;;; |
145 | | eqid 2622 |
. . . 4
;;;;;;;; ;;;;;;;; |
146 | | eqid 2622 |
. . . . 5
;;;;;;; ;;;;;;; |
147 | | eqid 2622 |
. . . . . 6
;;;;;; ;;;;;; |
148 | | eqid 2622 |
. . . . . . 7
;;;;; ;;;;; |
149 | | eqid 2622 |
. . . . . . . . 9
;;;; ;;;; |
150 | 28, 2, 5, 149, 104 | decaddi 11579 |
. . . . . . . 8
;;;; ;;;; |
151 | 28, 35, 102, 150 | decsuc 11535 |
. . . . . . 7
;;;; ;;;; |
152 | | 9p7e16 11625 |
. . . . . . . 8
; |
153 | 133, 78, 152 | addcomli 10228 |
. . . . . . 7
; |
154 | 29, 30, 5, 26, 148, 72, 151, 1, 153 | decaddc 11572 |
. . . . . 6
;;;;; ; ;;;;; |
155 | | 4p3e7 11163 |
. . . . . 6
|
156 | 31, 23, 37, 5, 147, 70, 154, 155 | decadd 11570 |
. . . . 5
;;;;;; ;; ;;;;;; |
157 | 79 | addid2i 10224 |
. . . . 5
|
158 | 32, 33, 38, 24, 146, 68, 156, 157 | decadd 11570 |
. . . 4
;;;;;;; ;;; ;;;;;;; |
159 | 34, 35, 39, 40, 145, 66, 158, 102 | decadd 11570 |
. . 3
;;;;;;;; ;;;; ;;;;;;;; |
160 | 36, 33, 41, 1, 144, 63, 159, 137 | decadd 11570 |
. 2
;;;;;;;;; ;;;;; ;;;;; ;;;;; ;;;;; ;;;;;;;;; |
161 | 9, 22, 160 | 3eqtri 2648 |
1
;;;; ;;;;;;;;; |