Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
subMat1 subMat1 |
2 | | 1smat1.n |
. . . . . 6
|
3 | 2 | adantr 481 |
. . . . 5
|
4 | | 1smat1.i |
. . . . . 6
|
5 | 4 | adantr 481 |
. . . . 5
|
6 | | 1smat1.r |
. . . . . . . 8
|
7 | | fzfi 12771 |
. . . . . . . 8
|
8 | | eqid 2622 |
. . . . . . . . 9
Mat Mat |
9 | | eqid 2622 |
. . . . . . . . 9
Mat Mat |
10 | | 1smat1.1 |
. . . . . . . . 9
Mat |
11 | 8, 9, 10 | mat1bas 20255 |
. . . . . . . 8
Mat |
12 | 6, 7, 11 | sylancl 694 |
. . . . . . 7
Mat |
13 | | eqid 2622 |
. . . . . . . . 9
|
14 | 8, 13 | matbas2 20227 |
. . . . . . . 8
Mat |
15 | 7, 6, 14 | sylancr 695 |
. . . . . . 7
Mat |
16 | 12, 15 | eleqtrrd 2704 |
. . . . . 6
|
17 | 16 | adantr 481 |
. . . . 5
|
18 | | fz1ssnn 12372 |
. . . . . 6
|
19 | | simprl 794 |
. . . . . 6
|
20 | 18, 19 | sseldi 3601 |
. . . . 5
|
21 | | simprr 796 |
. . . . . 6
|
22 | 18, 21 | sseldi 3601 |
. . . . 5
|
23 | | eqidd 2623 |
. . . . 5
|
24 | | eqidd 2623 |
. . . . 5
|
25 | 1, 3, 3, 5, 5, 17,
20, 22, 23, 24 | smatlem 29863 |
. . . 4
subMat1 |
26 | | eqid 2622 |
. . . . 5
|
27 | | eqid 2622 |
. . . . 5
|
28 | 7 | a1i 11 |
. . . . 5
|
29 | 6 | adantr 481 |
. . . . 5
|
30 | | nnuz 11723 |
. . . . . . . . 9
|
31 | 20, 30 | syl6eleq 2711 |
. . . . . . . 8
|
32 | | fznatpl1 12395 |
. . . . . . . . 9
|
33 | 3, 19, 32 | syl2anc 693 |
. . . . . . . 8
|
34 | | peano2fzr 12354 |
. . . . . . . 8
|
35 | 31, 33, 34 | syl2anc 693 |
. . . . . . 7
|
36 | 35, 33 | jca 554 |
. . . . . 6
|
37 | | eleq1 2689 |
. . . . . . 7
|
38 | | eleq1 2689 |
. . . . . . 7
|
39 | 37, 38 | ifboth 4124 |
. . . . . 6
|
40 | 36, 39 | syl 17 |
. . . . 5
|
41 | 22, 30 | syl6eleq 2711 |
. . . . . . . 8
|
42 | | fznatpl1 12395 |
. . . . . . . . 9
|
43 | 3, 21, 42 | syl2anc 693 |
. . . . . . . 8
|
44 | | peano2fzr 12354 |
. . . . . . . 8
|
45 | 41, 43, 44 | syl2anc 693 |
. . . . . . 7
|
46 | 45, 43 | jca 554 |
. . . . . 6
|
47 | | eleq1 2689 |
. . . . . . 7
|
48 | | eleq1 2689 |
. . . . . . 7
|
49 | 47, 48 | ifboth 4124 |
. . . . . 6
|
50 | 46, 49 | syl 17 |
. . . . 5
|
51 | 8, 26, 27, 28, 29, 40, 50, 10 | mat1ov 20254 |
. . . 4
|
52 | | simpr 477 |
. . . . . . . . . 10
|
53 | 52 | iftrued 4094 |
. . . . . . . . 9
|
54 | 53 | eqeq1d 2624 |
. . . . . . . 8
|
55 | | simpr 477 |
. . . . . . . . . . 11
|
56 | 55 | iftrued 4094 |
. . . . . . . . . 10
|
57 | 56 | eqeq2d 2632 |
. . . . . . . . 9
|
58 | | simpr 477 |
. . . . . . . . . . . 12
|
59 | 58 | iffalsed 4097 |
. . . . . . . . . . 11
|
60 | 59 | eqeq2d 2632 |
. . . . . . . . . 10
|
61 | 20 | nnred 11035 |
. . . . . . . . . . . . . 14
|
62 | 61 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
63 | | fz1ssnn 12372 |
. . . . . . . . . . . . . . . . 17
|
64 | 63, 4 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
|
65 | 64 | nnred 11035 |
. . . . . . . . . . . . . . 15
|
66 | 65 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
|
67 | 22 | nnred 11035 |
. . . . . . . . . . . . . . . 16
|
68 | 67 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
69 | | 1red 10055 |
. . . . . . . . . . . . . . 15
|
70 | 68, 69 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
71 | 52 | adantr 481 |
. . . . . . . . . . . . . 14
|
72 | 64 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
|
73 | 72 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
74 | 22 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
|
75 | 74 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
76 | 66, 68, 58 | nltled 10187 |
. . . . . . . . . . . . . . 15
|
77 | | zleltp1 11428 |
. . . . . . . . . . . . . . . 16
|
78 | 77 | biimpa 501 |
. . . . . . . . . . . . . . 15
|
79 | 73, 75, 76, 78 | syl21anc 1325 |
. . . . . . . . . . . . . 14
|
80 | 62, 66, 70, 71, 79 | lttrd 10198 |
. . . . . . . . . . . . 13
|
81 | 62, 80 | ltned 10173 |
. . . . . . . . . . . 12
|
82 | 81 | neneqd 2799 |
. . . . . . . . . . 11
|
83 | 62, 66, 68, 71, 76 | ltletrd 10197 |
. . . . . . . . . . . . 13
|
84 | 62, 83 | ltned 10173 |
. . . . . . . . . . . 12
|
85 | 84 | neneqd 2799 |
. . . . . . . . . . 11
|
86 | 82, 85 | 2falsed 366 |
. . . . . . . . . 10
|
87 | 60, 86 | bitrd 268 |
. . . . . . . . 9
|
88 | 57, 87 | pm2.61dan 832 |
. . . . . . . 8
|
89 | 54, 88 | bitrd 268 |
. . . . . . 7
|
90 | | simpr 477 |
. . . . . . . . . 10
|
91 | 90 | iffalsed 4097 |
. . . . . . . . 9
|
92 | 91 | eqeq1d 2624 |
. . . . . . . 8
|
93 | | simpr 477 |
. . . . . . . . . . . 12
|
94 | 93 | iftrued 4094 |
. . . . . . . . . . 11
|
95 | 94 | eqeq2d 2632 |
. . . . . . . . . 10
|
96 | 67 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
97 | 65 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
98 | 61 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
99 | | 1red 10055 |
. . . . . . . . . . . . . . . 16
|
100 | 98, 99 | readdcld 10069 |
. . . . . . . . . . . . . . 15
|
101 | 72 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
|
102 | 20 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
|
103 | 102 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
104 | 90 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
105 | 97, 98, 104 | nltled 10187 |
. . . . . . . . . . . . . . . 16
|
106 | | zleltp1 11428 |
. . . . . . . . . . . . . . . . 17
|
107 | 106 | biimpa 501 |
. . . . . . . . . . . . . . . 16
|
108 | 101, 103,
105, 107 | syl21anc 1325 |
. . . . . . . . . . . . . . 15
|
109 | 96, 97, 100, 93, 108 | lttrd 10198 |
. . . . . . . . . . . . . 14
|
110 | 96, 109 | ltned 10173 |
. . . . . . . . . . . . 13
|
111 | 110 | necomd 2849 |
. . . . . . . . . . . 12
|
112 | 111 | neneqd 2799 |
. . . . . . . . . . 11
|
113 | 96, 97, 98, 93, 105 | ltletrd 10197 |
. . . . . . . . . . . . . 14
|
114 | 96, 113 | ltned 10173 |
. . . . . . . . . . . . 13
|
115 | 114 | necomd 2849 |
. . . . . . . . . . . 12
|
116 | 115 | neneqd 2799 |
. . . . . . . . . . 11
|
117 | 112, 116 | 2falsed 366 |
. . . . . . . . . 10
|
118 | 95, 117 | bitrd 268 |
. . . . . . . . 9
|
119 | | simpr 477 |
. . . . . . . . . . . 12
|
120 | 119 | iffalsed 4097 |
. . . . . . . . . . 11
|
121 | 120 | eqeq2d 2632 |
. . . . . . . . . 10
|
122 | 20 | nncnd 11036 |
. . . . . . . . . . . . 13
|
123 | 122 | ad3antrrr 766 |
. . . . . . . . . . . 12
|
124 | 22 | nncnd 11036 |
. . . . . . . . . . . . 13
|
125 | 124 | ad3antrrr 766 |
. . . . . . . . . . . 12
|
126 | | 1cnd 10056 |
. . . . . . . . . . . 12
|
127 | | simpr 477 |
. . . . . . . . . . . 12
|
128 | 123, 125,
126, 127 | addcan2ad 10242 |
. . . . . . . . . . 11
|
129 | | simpr 477 |
. . . . . . . . . . . 12
|
130 | 129 | oveq1d 6665 |
. . . . . . . . . . 11
|
131 | 128, 130 | impbida 877 |
. . . . . . . . . 10
|
132 | 121, 131 | bitrd 268 |
. . . . . . . . 9
|
133 | 118, 132 | pm2.61dan 832 |
. . . . . . . 8
|
134 | 92, 133 | bitrd 268 |
. . . . . . 7
|
135 | 89, 134 | pm2.61dan 832 |
. . . . . 6
|
136 | 135 | ifbid 4108 |
. . . . 5
|
137 | | eqid 2622 |
. . . . . 6
Mat
Mat |
138 | | fzfid 12772 |
. . . . . 6
|
139 | | eqid 2622 |
. . . . . 6
Mat Mat |
140 | 137, 26, 27, 138, 29, 19, 21, 139 | mat1ov 20254 |
. . . . 5
Mat |
141 | 136, 140 | eqtr4d 2659 |
. . . 4
Mat |
142 | 25, 51, 141 | 3eqtrd 2660 |
. . 3
subMat1 Mat |
143 | 142 | ralrimivva 2971 |
. 2
subMat1 Mat |
144 | 1, 2, 2, 4, 4, 16 | smatrcl 29862 |
. . . 4
subMat1
|
145 | | elmapfn 7880 |
. . . 4
subMat1
subMat1 |
146 | 144, 145 | syl 17 |
. . 3
subMat1 |
147 | | fzfi 12771 |
. . . . . 6
|
148 | | eqid 2622 |
. . . . . . 7
Mat Mat |
149 | 137, 148,
139 | mat1bas 20255 |
. . . . . 6
Mat Mat |
150 | 6, 147, 149 | sylancl 694 |
. . . . 5
Mat
Mat |
151 | 137, 13 | matbas2 20227 |
. . . . . 6
Mat |
152 | 147, 6, 151 | sylancr 695 |
. . . . 5
Mat |
153 | 150, 152 | eleqtrrd 2704 |
. . . 4
Mat
|
154 | | elmapfn 7880 |
. . . 4
Mat
Mat
|
155 | 153, 154 | syl 17 |
. . 3
Mat
|
156 | | eqfnov2 6767 |
. . 3
subMat1 Mat subMat1 Mat
subMat1
Mat |
157 | 146, 155,
156 | syl2anc 693 |
. 2
subMat1 Mat subMat1 Mat |
158 | 143, 157 | mpbird 247 |
1
subMat1
Mat |