Proof of Theorem stoweidlem13
Step | Hyp | Ref
| Expression |
1 | | stoweidlem13.3 |
. . . 4
|
2 | | stoweidlem13.2 |
. . . 4
|
3 | 1, 2 | resubcld 10458 |
. . 3
|
4 | | 2re 11090 |
. . . 4
|
5 | | stoweidlem13.1 |
. . . . 5
|
6 | 5 | rpred 11872 |
. . . 4
|
7 | | remulcl 10021 |
. . . 4
|
8 | 4, 6, 7 | sylancr 695 |
. . 3
|
9 | 1 | recnd 10068 |
. . . . 5
|
10 | 2 | recnd 10068 |
. . . . 5
|
11 | 9, 10 | negsubdi2d 10408 |
. . . 4
|
12 | 2, 1 | resubcld 10458 |
. . . . 5
|
13 | | 1red 10055 |
. . . . . 6
|
14 | 13, 6 | remulcld 10070 |
. . . . 5
|
15 | | stoweidlem13.4 |
. . . . . . . . . . 11
|
16 | | 3re 11094 |
. . . . . . . . . . . . 13
|
17 | | 3ne0 11115 |
. . . . . . . . . . . . 13
|
18 | 16, 17 | rereccli 10790 |
. . . . . . . . . . . 12
|
19 | 18 | a1i 11 |
. . . . . . . . . . 11
|
20 | 15, 19 | resubcld 10458 |
. . . . . . . . . 10
|
21 | 20, 6 | remulcld 10070 |
. . . . . . . . 9
|
22 | 21, 1 | resubcld 10458 |
. . . . . . . 8
|
23 | | 4re 11097 |
. . . . . . . . . . . . 13
|
24 | 23, 16, 17 | 3pm3.2i 1239 |
. . . . . . . . . . . 12
|
25 | | redivcl 10744 |
. . . . . . . . . . . 12
|
26 | 24, 25 | mp1i 13 |
. . . . . . . . . . 11
|
27 | 15, 26 | resubcld 10458 |
. . . . . . . . . 10
|
28 | 27, 6 | remulcld 10070 |
. . . . . . . . 9
|
29 | 21, 28 | resubcld 10458 |
. . . . . . . 8
|
30 | | stoweidlem13.6 |
. . . . . . . . 9
|
31 | 2, 21, 1, 30 | lesub1dd 10643 |
. . . . . . . 8
|
32 | | stoweidlem13.7 |
. . . . . . . . 9
|
33 | 28, 1, 21, 32 | ltsub2dd 10640 |
. . . . . . . 8
|
34 | 12, 22, 29, 31, 33 | lelttrd 10195 |
. . . . . . 7
|
35 | 15 | recnd 10068 |
. . . . . . . . . 10
|
36 | 19 | recnd 10068 |
. . . . . . . . . 10
|
37 | 35, 36 | subcld 10392 |
. . . . . . . . 9
|
38 | 26 | recnd 10068 |
. . . . . . . . . 10
|
39 | 35, 38 | subcld 10392 |
. . . . . . . . 9
|
40 | 6 | recnd 10068 |
. . . . . . . . 9
|
41 | 37, 39, 40 | subdird 10487 |
. . . . . . . 8
|
42 | 35, 36, 35, 38 | sub4d 10441 |
. . . . . . . . . 10
|
43 | 35, 35 | subcld 10392 |
. . . . . . . . . . 11
|
44 | 43, 36, 38 | subsub2d 10421 |
. . . . . . . . . 10
|
45 | 42, 44 | eqtrd 2656 |
. . . . . . . . 9
|
46 | 45 | oveq1d 6665 |
. . . . . . . 8
|
47 | 41, 46 | eqtr3d 2658 |
. . . . . . 7
|
48 | 34, 47 | breqtrd 4679 |
. . . . . 6
|
49 | 35 | subidd 10380 |
. . . . . . . . 9
|
50 | 49 | oveq1d 6665 |
. . . . . . . 8
|
51 | | 4cn 11098 |
. . . . . . . . . . . 12
|
52 | | 3cn 11095 |
. . . . . . . . . . . 12
|
53 | 51, 52, 17 | divcli 10767 |
. . . . . . . . . . 11
|
54 | | ax-1cn 9994 |
. . . . . . . . . . . 12
|
55 | 54, 52, 17 | divcli 10767 |
. . . . . . . . . . 11
|
56 | | 1div1e1 10717 |
. . . . . . . . . . . . . 14
|
57 | 56 | oveq2i 6661 |
. . . . . . . . . . . . 13
|
58 | | ax-1ne0 10005 |
. . . . . . . . . . . . . 14
|
59 | 54, 52, 54, 54, 17, 58 | divadddivi 10787 |
. . . . . . . . . . . . 13
|
60 | 57, 59 | eqtr3i 2646 |
. . . . . . . . . . . 12
|
61 | 52, 54 | addcomi 10227 |
. . . . . . . . . . . . . 14
|
62 | | df-4 11081 |
. . . . . . . . . . . . . 14
|
63 | | 1t1e1 11175 |
. . . . . . . . . . . . . . 15
|
64 | 52 | mulid2i 10043 |
. . . . . . . . . . . . . . 15
|
65 | 63, 64 | oveq12i 6662 |
. . . . . . . . . . . . . 14
|
66 | 61, 62, 65 | 3eqtr4ri 2655 |
. . . . . . . . . . . . 13
|
67 | 66 | oveq1i 6660 |
. . . . . . . . . . . 12
|
68 | | 3t1e3 11178 |
. . . . . . . . . . . . 13
|
69 | 68 | oveq2i 6661 |
. . . . . . . . . . . 12
|
70 | 60, 67, 69 | 3eqtri 2648 |
. . . . . . . . . . 11
|
71 | 53, 55, 54, 70 | subaddrii 10370 |
. . . . . . . . . 10
|
72 | 71 | oveq2i 6661 |
. . . . . . . . 9
|
73 | | 1e0p1 11552 |
. . . . . . . . 9
|
74 | 72, 73 | eqtr4i 2647 |
. . . . . . . 8
|
75 | 50, 74 | syl6eq 2672 |
. . . . . . 7
|
76 | 75 | oveq1d 6665 |
. . . . . 6
|
77 | 48, 76 | breqtrd 4679 |
. . . . 5
|
78 | | 1lt2 11194 |
. . . . . 6
|
79 | 4 | a1i 11 |
. . . . . . 7
|
80 | 13, 79, 5 | ltmul1d 11913 |
. . . . . 6
|
81 | 78, 80 | mpbii 223 |
. . . . 5
|
82 | 12, 14, 8, 77, 81 | lttrd 10198 |
. . . 4
|
83 | 11, 82 | eqbrtrd 4675 |
. . 3
|
84 | 3, 8, 83 | ltnegcon1d 10607 |
. 2
|
85 | | 5re 11099 |
. . . . . 6
|
86 | 85 | a1i 11 |
. . . . 5
|
87 | 16 | a1i 11 |
. . . . 5
|
88 | 17 | a1i 11 |
. . . . 5
|
89 | 86, 87, 88 | redivcld 10853 |
. . . 4
|
90 | 89, 6 | remulcld 10070 |
. . 3
|
91 | 2 | renegcld 10457 |
. . . . 5
|
92 | 15, 19 | readdcld 10069 |
. . . . . 6
|
93 | 92, 6 | remulcld 10070 |
. . . . 5
|
94 | 28 | renegcld 10457 |
. . . . 5
|
95 | | stoweidlem13.8 |
. . . . 5
|
96 | | stoweidlem13.5 |
. . . . . 6
|
97 | 28, 2 | ltnegd 10605 |
. . . . . 6
|
98 | 96, 97 | mpbid 222 |
. . . . 5
|
99 | 1, 91, 93, 94, 95, 98 | lt2addd 10650 |
. . . 4
|
100 | 9, 10 | negsubd 10398 |
. . . 4
|
101 | 35, 36, 40 | adddird 10065 |
. . . . . 6
|
102 | 35, 38 | negsubd 10398 |
. . . . . . . . . . 11
|
103 | 102 | eqcomd 2628 |
. . . . . . . . . 10
|
104 | 103 | oveq1d 6665 |
. . . . . . . . 9
|
105 | 38 | negcld 10379 |
. . . . . . . . . 10
|
106 | 35, 105, 40 | adddird 10065 |
. . . . . . . . 9
|
107 | 38, 40 | mulneg1d 10483 |
. . . . . . . . . 10
|
108 | 107 | oveq2d 6666 |
. . . . . . . . 9
|
109 | 104, 106,
108 | 3eqtrd 2660 |
. . . . . . . 8
|
110 | 109 | negeqd 10275 |
. . . . . . 7
|
111 | 35, 40 | mulcld 10060 |
. . . . . . . 8
|
112 | 38, 40 | mulcld 10060 |
. . . . . . . . 9
|
113 | 112 | negcld 10379 |
. . . . . . . 8
|
114 | 111, 113 | negdid 10405 |
. . . . . . 7
|
115 | 112 | negnegd 10383 |
. . . . . . . 8
|
116 | 115 | oveq2d 6666 |
. . . . . . 7
|
117 | 110, 114,
116 | 3eqtrd 2660 |
. . . . . 6
|
118 | 101, 117 | oveq12d 6668 |
. . . . 5
|
119 | 36, 40 | mulcld 10060 |
. . . . . . . 8
|
120 | 111 | negcld 10379 |
. . . . . . . 8
|
121 | 111, 119,
120, 112 | add4d 10264 |
. . . . . . 7
|
122 | 111 | negidd 10382 |
. . . . . . . 8
|
123 | 122 | oveq1d 6665 |
. . . . . . 7
|
124 | 119, 112 | addcld 10059 |
. . . . . . . 8
|
125 | 124 | addid2d 10237 |
. . . . . . 7
|
126 | 121, 123,
125 | 3eqtrd 2660 |
. . . . . 6
|
127 | 36, 38, 40 | adddird 10065 |
. . . . . 6
|
128 | 87 | recnd 10068 |
. . . . . . . 8
|
129 | 36, 38 | addcld 10059 |
. . . . . . . 8
|
130 | 128, 36, 38 | adddid 10064 |
. . . . . . . . 9
|
131 | 54, 51 | addcomi 10227 |
. . . . . . . . . 10
|
132 | 54, 52, 17 | divcan2i 10768 |
. . . . . . . . . . 11
|
133 | 51, 52, 17 | divcan2i 10768 |
. . . . . . . . . . 11
|
134 | 132, 133 | oveq12i 6662 |
. . . . . . . . . 10
|
135 | | df-5 11082 |
. . . . . . . . . 10
|
136 | 131, 134,
135 | 3eqtr4i 2654 |
. . . . . . . . 9
|
137 | 130, 136 | syl6eq 2672 |
. . . . . . . 8
|
138 | 128, 129,
88, 137 | mvllmuld 10857 |
. . . . . . 7
|
139 | 138 | oveq1d 6665 |
. . . . . 6
|
140 | 126, 127,
139 | 3eqtr2d 2662 |
. . . . 5
|
141 | 118, 140 | eqtrd 2656 |
. . . 4
|
142 | 99, 100, 141 | 3brtr3d 4684 |
. . 3
|
143 | | 5lt6 11204 |
. . . . . . 7
|
144 | | 3t2e6 11179 |
. . . . . . 7
|
145 | 143, 144 | breqtrri 4680 |
. . . . . 6
|
146 | | 3pos 11114 |
. . . . . . . 8
|
147 | 16, 146 | pm3.2i 471 |
. . . . . . 7
|
148 | | ltdivmul 10898 |
. . . . . . 7
|
149 | 85, 4, 147, 148 | mp3an 1424 |
. . . . . 6
|
150 | 145, 149 | mpbir 221 |
. . . . 5
|
151 | 150 | a1i 11 |
. . . 4
|
152 | 89, 79, 5, 151 | ltmul1dd 11927 |
. . 3
|
153 | 3, 90, 8, 142, 152 | lttrd 10198 |
. 2
|
154 | 3, 8 | absltd 14168 |
. 2
|
155 | 84, 153, 154 | mpbir2and 957 |
1
|