Step |
Hyp |
Ref |
Expression |
1 |
|
constrrtlc.s |
|
2 |
|
constrrtlc.a |
|
3 |
|
constrrtlc.b |
|
4 |
|
constrrtlc.c |
|
5 |
|
constrrtlc.e |
|
6 |
|
constrrtlc.f |
|
7 |
|
constrrtlc.t |
|
8 |
|
constrrtlc.1 |
|
9 |
|
constrrtlc.2 |
|
10 |
|
constrrtlc.q |
|
11 |
|
constrrtlc.m |
|
12 |
|
constrrtlc.n |
|
13 |
|
constrrtlc1.1 |
|
14 |
1 2
|
sseldd |
|
15 |
14
|
cjcld |
|
16 |
1 3
|
sseldd |
|
17 |
16
|
cjcld |
|
18 |
17 15
|
subcld |
|
19 |
16 14
|
subcld |
|
20 |
13
|
necomd |
|
21 |
16 14 20
|
subne0d |
|
22 |
18 19 21
|
divcld |
|
23 |
10 22
|
eqeltrid |
|
24 |
14 23
|
mulcld |
|
25 |
15 24
|
subcld |
|
26 |
1 4
|
sseldd |
|
27 |
26
|
cjcld |
|
28 |
25 27
|
subcld |
|
29 |
26 23
|
mulcld |
|
30 |
28 29
|
subcld |
|
31 |
16 14
|
cjsubd |
|
32 |
19 21
|
cjne0d |
|
33 |
31 32
|
eqnetrrd |
|
34 |
18 19 33 21
|
divne0d |
|
35 |
10
|
neeq1i |
|
36 |
34 35
|
sylibr |
|
37 |
30 23 36
|
divcld |
|
38 |
7
|
recnd |
|
39 |
38 19
|
mulcld |
|
40 |
14 39
|
addcld |
|
41 |
8 40
|
eqeltrd |
|
42 |
37 41
|
mulcomd |
|
43 |
11
|
a1i |
|
44 |
43
|
oveq1d |
|
45 |
41 30 23 36
|
divassd |
|
46 |
42 44 45
|
3eqtr4d |
|
47 |
12
|
a1i |
|
48 |
46 47
|
oveq12d |
|
49 |
41 30
|
mulcld |
|
50 |
26 28
|
mulcld |
|
51 |
41
|
sqvald |
|
52 |
51
|
oveq1d |
|
53 |
41 41 23
|
mulassd |
|
54 |
52 53
|
eqtrd |
|
55 |
41 23
|
mulcld |
|
56 |
41 55
|
mulcld |
|
57 |
54 56
|
eqeltrd |
|
58 |
57 49 50
|
addsubd |
|
59 |
54
|
oveq1d |
|
60 |
41 28 29
|
subdid |
|
61 |
59 60
|
oveq12d |
|
62 |
41 28
|
mulcld |
|
63 |
41 29
|
mulcld |
|
64 |
56 62 50 63
|
addsub4d |
|
65 |
41 26 55 28
|
submuladdd |
|
66 |
9
|
oveq1d |
|
67 |
41 26
|
subcld |
|
68 |
67
|
absvalsqd |
|
69 |
1 5
|
sseldd |
|
70 |
1 6
|
sseldd |
|
71 |
69 70
|
subcld |
|
72 |
71
|
absvalsqd |
|
73 |
66 68 72
|
3eqtr3d |
|
74 |
8
|
fvoveq1d |
|
75 |
40 26
|
cjsubd |
|
76 |
14 39
|
cjaddd |
|
77 |
38 19
|
cjmuld |
|
78 |
7
|
cjred |
|
79 |
14 39 8
|
mvrladdd |
|
80 |
79 39
|
eqeltrd |
|
81 |
80 38 19 21
|
divmul3d |
|
82 |
79 81
|
mpbird |
|
83 |
78 82
|
eqtr4d |
|
84 |
83 31
|
oveq12d |
|
85 |
80 19 18 21
|
div32d |
|
86 |
10
|
oveq2i |
|
87 |
85 86
|
eqtr4di |
|
88 |
41 14 23
|
subdird |
|
89 |
84 87 88
|
3eqtrd |
|
90 |
77 89
|
eqtrd |
|
91 |
90
|
oveq2d |
|
92 |
15 55 24
|
addsub12d |
|
93 |
76 91 92
|
3eqtrd |
|
94 |
93
|
oveq1d |
|
95 |
55 25 27
|
addsubassd |
|
96 |
75 94 95
|
3eqtrd |
|
97 |
74 96
|
eqtrd |
|
98 |
97
|
oveq2d |
|
99 |
69 70
|
cjsubd |
|
100 |
99
|
oveq2d |
|
101 |
73 98 100
|
3eqtr3d |
|
102 |
26 41 23
|
mul12d |
|
103 |
102
|
oveq1d |
|
104 |
63 50 103
|
comraddd |
|
105 |
104
|
oveq2d |
|
106 |
65 101 105
|
3eqtr3rd |
|
107 |
61 64 106
|
3eqtr2d |
|
108 |
58 107
|
eqtrd |
|
109 |
57 49
|
addcld |
|
110 |
109 50
|
subcld |
|
111 |
108 110
|
eqeltrrd |
|
112 |
50 111
|
addcld |
|
113 |
112
|
negcld |
|
114 |
49 113 23 36
|
divdird |
|
115 |
48 114
|
eqtr4d |
|
116 |
115
|
oveq2d |
|
117 |
41
|
sqcld |
|
118 |
49 113
|
addcld |
|
119 |
117 23 118 36
|
muldivdid |
|
120 |
57 49 113
|
addassd |
|
121 |
109 112
|
negsubd |
|
122 |
109 50 111
|
subsub4d |
|
123 |
110 108
|
subeq0bd |
|
124 |
121 122 123
|
3eqtr2d |
|
125 |
120 124
|
eqtr3d |
|
126 |
57 118
|
addcld |
|
127 |
126 23 36
|
diveq0ad |
|
128 |
125 127
|
mpbird |
|
129 |
116 119 128
|
3eqtr2d |
|
130 |
129 36
|
jca |
|