Step | Hyp | Ref
| Expression |
1 | | smueq.a |
. . . . . . . 8
|
2 | 1 | adantr 481 |
. . . . . . 7
..^ |
3 | | smueq.b |
. . . . . . . 8
|
4 | 3 | adantr 481 |
. . . . . . 7
..^ |
5 | | smueq.p |
. . . . . . 7
sadd
|
6 | | elfzouz 12474 |
. . . . . . . . 9
..^
|
7 | 6 | adantl 482 |
. . . . . . . 8
..^ |
8 | | nn0uz 11722 |
. . . . . . . 8
|
9 | 7, 8 | syl6eleqr 2712 |
. . . . . . 7
..^ |
10 | 9 | nn0zd 11480 |
. . . . . . . . 9
..^ |
11 | 10 | peano2zd 11485 |
. . . . . . . 8
..^ |
12 | | smueq.n |
. . . . . . . . . 10
|
13 | 12 | adantr 481 |
. . . . . . . . 9
..^ |
14 | 13 | nn0zd 11480 |
. . . . . . . 8
..^ |
15 | | elfzolt2 12479 |
. . . . . . . . . 10
..^
|
16 | 15 | adantl 482 |
. . . . . . . . 9
..^ |
17 | | nn0ltp1le 11435 |
. . . . . . . . . 10
|
18 | 9, 13, 17 | syl2anc 693 |
. . . . . . . . 9
..^ |
19 | 16, 18 | mpbid 222 |
. . . . . . . 8
..^ |
20 | | eluz2 11693 |
. . . . . . . 8
|
21 | 11, 14, 19, 20 | syl3anbrc 1246 |
. . . . . . 7
..^ |
22 | 2, 4, 5, 9, 21 | smuval2 15204 |
. . . . . 6
..^ smul |
23 | 12, 8 | syl6eleq 2711 |
. . . . . . . . . . 11
|
24 | | eluzfz2b 12350 |
. . . . . . . . . . 11
|
25 | 23, 24 | sylib 208 |
. . . . . . . . . 10
|
26 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
27 | 26 | ineq1d 3813 |
. . . . . . . . . . . . 13
..^ ..^ |
28 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
29 | 28 | ineq1d 3813 |
. . . . . . . . . . . . 13
..^ ..^ |
30 | 27, 29 | eqeq12d 2637 |
. . . . . . . . . . . 12
..^ ..^ ..^ ..^ |
31 | 30 | imbi2d 330 |
. . . . . . . . . . 11
..^
..^
..^
..^ |
32 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
33 | 32 | ineq1d 3813 |
. . . . . . . . . . . . 13
..^ ..^ |
34 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
35 | 34 | ineq1d 3813 |
. . . . . . . . . . . . 13
..^ ..^ |
36 | 33, 35 | eqeq12d 2637 |
. . . . . . . . . . . 12
..^ ..^ ..^ ..^ |
37 | 36 | imbi2d 330 |
. . . . . . . . . . 11
..^
..^
..^
..^ |
38 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
39 | 38 | ineq1d 3813 |
. . . . . . . . . . . . 13
..^ ..^ |
40 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
41 | 40 | ineq1d 3813 |
. . . . . . . . . . . . 13
..^ ..^ |
42 | 39, 41 | eqeq12d 2637 |
. . . . . . . . . . . 12
..^ ..^ ..^ ..^ |
43 | 42 | imbi2d 330 |
. . . . . . . . . . 11
..^
..^
..^ ..^ |
44 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
45 | 44 | ineq1d 3813 |
. . . . . . . . . . . . 13
..^ ..^ |
46 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
47 | 46 | ineq1d 3813 |
. . . . . . . . . . . . 13
..^ ..^ |
48 | 45, 47 | eqeq12d 2637 |
. . . . . . . . . . . 12
..^ ..^ ..^ ..^ |
49 | 48 | imbi2d 330 |
. . . . . . . . . . 11
..^
..^
..^
..^ |
50 | 1, 3, 5 | smup0 15201 |
. . . . . . . . . . . . . 14
|
51 | | inss1 3833 |
. . . . . . . . . . . . . . . 16
..^ |
52 | 51, 3 | syl5ss 3614 |
. . . . . . . . . . . . . . 15
..^ |
53 | | smueq.q |
. . . . . . . . . . . . . . 15
sadd
..^ |
54 | 1, 52, 53 | smup0 15201 |
. . . . . . . . . . . . . 14
|
55 | 50, 54 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
56 | 55 | ineq1d 3813 |
. . . . . . . . . . . 12
..^ ..^ |
57 | 56 | a1i 11 |
. . . . . . . . . . 11
..^ ..^ |
58 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
..^ ..^ ..^ sadd ..^ ..^ sadd ..^ |
59 | 58 | ineq1d 3813 |
. . . . . . . . . . . . . 14
..^ ..^
..^ sadd
..^ ..^ ..^ sadd ..^ ..^ |
60 | 1 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
..^ |
61 | 3 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
..^ |
62 | | elfzonn0 12512 |
. . . . . . . . . . . . . . . . . . 19
..^
|
63 | 62 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
..^ |
64 | 60, 61, 5, 63 | smupp1 15202 |
. . . . . . . . . . . . . . . . 17
..^ sadd |
65 | 64 | ineq1d 3813 |
. . . . . . . . . . . . . . . 16
..^ ..^ sadd ..^ |
66 | 1, 3, 5 | smupf 15200 |
. . . . . . . . . . . . . . . . . . 19
|
67 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . 19
|
68 | 66, 62, 67 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
..^ |
69 | 68 | elpwid 4170 |
. . . . . . . . . . . . . . . . 17
..^ |
70 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . 18
|
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . . 17
..^
|
72 | 12 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^ |
73 | 69, 71, 72 | sadeq 15194 |
. . . . . . . . . . . . . . . 16
..^ sadd
..^
..^ sadd
..^ ..^ |
74 | 65, 73 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
..^ ..^ ..^ sadd
..^ ..^ |
75 | 52 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
76 | 60, 75, 53, 63 | smupp1 15202 |
. . . . . . . . . . . . . . . . 17
..^ sadd ..^ |
77 | 76 | ineq1d 3813 |
. . . . . . . . . . . . . . . 16
..^ ..^ sadd ..^ ..^ |
78 | 1, 52, 53 | smupf 15200 |
. . . . . . . . . . . . . . . . . . 19
|
79 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . 19
|
80 | 78, 62, 79 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
..^ |
81 | 80 | elpwid 4170 |
. . . . . . . . . . . . . . . . 17
..^ |
82 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . 18
..^ |
83 | 82 | a1i 11 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
84 | 81, 83, 72 | sadeq 15194 |
. . . . . . . . . . . . . . . 16
..^ sadd
..^ ..^ ..^ sadd ..^ ..^ ..^ |
85 | | inss2 3834 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^ |
86 | 85 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
87 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^ ..^
|
88 | 87 | sseld 3602 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^ ..^
|
89 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^
|
90 | 89 | simp2bi 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^
|
91 | 90 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^ ..^
|
92 | | elfzonn0 12512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
..^
|
93 | 92 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
..^ ..^
|
94 | 93 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^ ..^
|
95 | 63 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
..^ ..^
|
96 | 95 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^ ..^
|
97 | 94, 96 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^ ..^
|
98 | 91 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^ ..^
|
99 | 95 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^ ..^
|
100 | 94, 96 | subge02d 10619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^ ..^
|
101 | 99, 100 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^ ..^
|
102 | | elfzolt2 12479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^
|
103 | 102 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^ ..^
|
104 | 97, 94, 98, 101, 103 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^ ..^
|
105 | 91, 104 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^ ..^
|
106 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^
|
107 | | 3anass 1042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
108 | 106, 107 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^
|
109 | 108 | baib 944 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^ |
110 | 105, 109 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^ ..^
..^ |
111 | 88, 110 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ ..^
..^ |
112 | 111 | pm4.71rd 667 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ ..^
..^ |
113 | | ancom 466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
..^ |
114 | | elin 3796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ ..^ |
115 | 113, 114 | bitr4i 267 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
..^ |
116 | 112, 115 | syl6rbb 277 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^
..^ |
117 | 116 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^
..^
|
118 | 86, 117 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^
..^
|
119 | 118 | rabbidva 3188 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ ..^ ..^
|
120 | | inrab2 3900 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ ..^
..^ |
121 | | inrab2 3900 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
122 | 119, 120,
121 | 3eqtr4g 2681 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ ..^ ..^ |
123 | 122 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
..^ ..^ sadd ..^ ..^ ..^ sadd ..^ |
124 | 123 | ineq1d 3813 |
. . . . . . . . . . . . . . . 16
..^
..^ sadd
..^ ..^ ..^ ..^ sadd
..^ ..^ |
125 | 77, 84, 124 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
..^ ..^ ..^ sadd
..^ ..^ |
126 | 74, 125 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
..^ ..^ ..^
..^ sadd
..^ ..^ ..^ sadd
..^ ..^ |
127 | 59, 126 | syl5ibr 236 |
. . . . . . . . . . . . 13
..^ ..^
..^ ..^ ..^ |
128 | 127 | expcom 451 |
. . . . . . . . . . . 12
..^
..^ ..^ ..^ ..^ |
129 | 128 | a2d 29 |
. . . . . . . . . . 11
..^
..^ ..^
..^ ..^ |
130 | 31, 37, 43, 49, 57, 129 | fzind2 12586 |
. . . . . . . . . 10
..^ ..^ |
131 | 25, 130 | mpcom 38 |
. . . . . . . . 9
..^ ..^ |
132 | 131 | adantr 481 |
. . . . . . . 8
..^ ..^ ..^ |
133 | 132 | eleq2d 2687 |
. . . . . . 7
..^ ..^ ..^ |
134 | | elin 3796 |
. . . . . . . . 9
..^
..^ |
135 | 134 | rbaib 947 |
. . . . . . . 8
..^
..^ |
136 | 135 | adantl 482 |
. . . . . . 7
..^ ..^ |
137 | | elin 3796 |
. . . . . . . . 9
..^
..^ |
138 | 137 | rbaib 947 |
. . . . . . . 8
..^
..^ |
139 | 138 | adantl 482 |
. . . . . . 7
..^ ..^ |
140 | 133, 136,
139 | 3bitr3d 298 |
. . . . . 6
..^ |
141 | 52 | adantr 481 |
. . . . . . . 8
..^ ..^ |
142 | 2, 141, 53, 13 | smupval 15210 |
. . . . . . 7
..^ ..^ smul ..^ |
143 | 142 | eleq2d 2687 |
. . . . . 6
..^ ..^ smul ..^ |
144 | 22, 140, 143 | 3bitrd 294 |
. . . . 5
..^ smul ..^ smul ..^ |
145 | 144 | ex 450 |
. . . 4
..^ smul
..^ smul ..^ |
146 | 145 | pm5.32rd 672 |
. . 3
smul ..^ ..^ smul ..^ ..^ |
147 | | elin 3796 |
. . 3
smul ..^ smul
..^ |
148 | | elin 3796 |
. . 3
..^ smul ..^ ..^ ..^ smul ..^ ..^ |
149 | 146, 147,
148 | 3bitr4g 303 |
. 2
smul ..^
..^ smul ..^ ..^ |
150 | 149 | eqrdv 2620 |
1
smul
..^ ..^ smul ..^ ..^ |