Step | Hyp | Ref
| Expression |
1 | | nmopcoadj.1 |
. . . . . . 7
|
2 | | adjbdlnb 28943 |
. . . . . . 7
|
3 | 1, 2 | mpbi 220 |
. . . . . 6
|
4 | | bdopf 28721 |
. . . . . 6
|
5 | 3, 4 | ax-mp 5 |
. . . . 5
|
6 | | bdopf 28721 |
. . . . . 6
|
7 | 1, 6 | ax-mp 5 |
. . . . 5
|
8 | 5, 7 | hocofi 28625 |
. . . 4
|
9 | | nmopre 28729 |
. . . . . . 7
|
10 | 1, 9 | ax-mp 5 |
. . . . . 6
|
11 | 10 | resqcli 12949 |
. . . . 5
|
12 | | rexr 10085 |
. . . . 5
|
13 | 11, 12 | ax-mp 5 |
. . . 4
|
14 | | nmopub 28767 |
. . . 4
|
15 | 8, 13, 14 | mp2an 708 |
. . 3
|
16 | 5, 7 | hocoi 28623 |
. . . . . . . 8
|
17 | 16 | fveq2d 6195 |
. . . . . . 7
|
18 | 17 | adantr 481 |
. . . . . 6
|
19 | 7 | ffvelrni 6358 |
. . . . . . . . 9
|
20 | 5 | ffvelrni 6358 |
. . . . . . . . 9
|
21 | | normcl 27982 |
. . . . . . . . 9
|
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . 8
|
23 | 22 | adantr 481 |
. . . . . . 7
|
24 | | nmopre 28729 |
. . . . . . . . . 10
|
25 | 3, 24 | ax-mp 5 |
. . . . . . . . 9
|
26 | | normcl 27982 |
. . . . . . . . . 10
|
27 | 19, 26 | syl 17 |
. . . . . . . . 9
|
28 | | remulcl 10021 |
. . . . . . . . 9
|
29 | 25, 27, 28 | sylancr 695 |
. . . . . . . 8
|
30 | 29 | adantr 481 |
. . . . . . 7
|
31 | 25, 10 | remulcli 10054 |
. . . . . . . 8
|
32 | 31 | a1i 11 |
. . . . . . 7
|
33 | 3 | nmbdoplbi 28883 |
. . . . . . . . 9
|
34 | 19, 33 | syl 17 |
. . . . . . . 8
|
35 | 34 | adantr 481 |
. . . . . . 7
|
36 | 27 | adantr 481 |
. . . . . . . 8
|
37 | 10 | a1i 11 |
. . . . . . . 8
|
38 | | normcl 27982 |
. . . . . . . . . . 11
|
39 | | remulcl 10021 |
. . . . . . . . . . 11
|
40 | 10, 38, 39 | sylancr 695 |
. . . . . . . . . 10
|
41 | 40 | adantr 481 |
. . . . . . . . 9
|
42 | 1 | nmbdoplbi 28883 |
. . . . . . . . . 10
|
43 | 42 | adantr 481 |
. . . . . . . . 9
|
44 | | 1re 10039 |
. . . . . . . . . . . 12
|
45 | | nmopge0 28770 |
. . . . . . . . . . . . . . 15
|
46 | 1, 6, 45 | mp2b 10 |
. . . . . . . . . . . . . 14
|
47 | 10, 46 | pm3.2i 471 |
. . . . . . . . . . . . 13
|
48 | | lemul2a 10878 |
. . . . . . . . . . . . 13
|
49 | 47, 48 | mp3anl3 1420 |
. . . . . . . . . . . 12
|
50 | 44, 49 | mpanl2 717 |
. . . . . . . . . . 11
|
51 | 38, 50 | sylan 488 |
. . . . . . . . . 10
|
52 | 10 | recni 10052 |
. . . . . . . . . . 11
|
53 | 52 | mulid1i 10042 |
. . . . . . . . . 10
|
54 | 51, 53 | syl6breq 4694 |
. . . . . . . . 9
|
55 | 36, 41, 37, 43, 54 | letrd 10194 |
. . . . . . . 8
|
56 | | nmopge0 28770 |
. . . . . . . . . . 11
|
57 | 3, 4, 56 | mp2b 10 |
. . . . . . . . . 10
|
58 | 25, 57 | pm3.2i 471 |
. . . . . . . . 9
|
59 | | lemul2a 10878 |
. . . . . . . . 9
|
60 | 58, 59 | mp3anl3 1420 |
. . . . . . . 8
|
61 | 36, 37, 55, 60 | syl21anc 1325 |
. . . . . . 7
|
62 | 23, 30, 32, 35, 61 | letrd 10194 |
. . . . . 6
|
63 | 18, 62 | eqbrtrd 4675 |
. . . . 5
|
64 | 1 | nmopadji 28949 |
. . . . . . 7
|
65 | 64 | oveq1i 6660 |
. . . . . 6
|
66 | 52 | sqvali 12943 |
. . . . . 6
|
67 | 65, 66 | eqtr4i 2647 |
. . . . 5
|
68 | 63, 67 | syl6breq 4694 |
. . . 4
|
69 | 68 | ex 450 |
. . 3
|
70 | 15, 69 | mprgbir 2927 |
. 2
|
71 | | nmopge0 28770 |
. . . . . . . 8
|
72 | 8, 71 | ax-mp 5 |
. . . . . . 7
|
73 | 3, 1 | bdopcoi 28957 |
. . . . . . . . 9
|
74 | | nmopre 28729 |
. . . . . . . . 9
|
75 | 73, 74 | ax-mp 5 |
. . . . . . . 8
|
76 | 75 | sqrtcli 14111 |
. . . . . . 7
|
77 | | rexr 10085 |
. . . . . . 7
|
78 | 72, 76, 77 | mp2b 10 |
. . . . . 6
|
79 | | nmopub 28767 |
. . . . . 6
|
80 | 7, 78, 79 | mp2an 708 |
. . . . 5
|
81 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
|
82 | | hicl 27937 |
. . . . . . . . . . . 12
|
83 | 81, 82 | mpancom 703 |
. . . . . . . . . . 11
|
84 | 83 | abscld 14175 |
. . . . . . . . . 10
|
85 | 84 | adantr 481 |
. . . . . . . . 9
|
86 | 22, 38 | remulcld 10070 |
. . . . . . . . . 10
|
87 | 86 | adantr 481 |
. . . . . . . . 9
|
88 | 75 | a1i 11 |
. . . . . . . . 9
|
89 | | bcs 28038 |
. . . . . . . . . . 11
|
90 | 81, 89 | mpancom 703 |
. . . . . . . . . 10
|
91 | 90 | adantr 481 |
. . . . . . . . 9
|
92 | 5, 7 | hococli 28624 |
. . . . . . . . . . . 12
|
93 | | normcl 27982 |
. . . . . . . . . . . 12
|
94 | 92, 93 | syl 17 |
. . . . . . . . . . 11
|
95 | 94 | adantr 481 |
. . . . . . . . . 10
|
96 | 38 | adantr 481 |
. . . . . . . . . . . 12
|
97 | | normge0 27983 |
. . . . . . . . . . . . . . 15
|
98 | 19, 20, 97 | 3syl 18 |
. . . . . . . . . . . . . 14
|
99 | 22, 98 | jca 554 |
. . . . . . . . . . . . 13
|
100 | 99 | adantr 481 |
. . . . . . . . . . . 12
|
101 | | simpr 477 |
. . . . . . . . . . . 12
|
102 | | lemul2a 10878 |
. . . . . . . . . . . . 13
|
103 | 44, 102 | mp3anl2 1419 |
. . . . . . . . . . . 12
|
104 | 96, 100, 101, 103 | syl21anc 1325 |
. . . . . . . . . . 11
|
105 | 22 | recnd 10068 |
. . . . . . . . . . . . . 14
|
106 | 105 | mulid1d 10057 |
. . . . . . . . . . . . 13
|
107 | 106, 17 | eqtr4d 2659 |
. . . . . . . . . . . 12
|
108 | 107 | adantr 481 |
. . . . . . . . . . 11
|
109 | 104, 108 | breqtrd 4679 |
. . . . . . . . . 10
|
110 | | remulcl 10021 |
. . . . . . . . . . . . 13
|
111 | 75, 38, 110 | sylancr 695 |
. . . . . . . . . . . 12
|
112 | 111 | adantr 481 |
. . . . . . . . . . 11
|
113 | 73 | nmbdoplbi 28883 |
. . . . . . . . . . . 12
|
114 | 113 | adantr 481 |
. . . . . . . . . . 11
|
115 | 75, 72 | pm3.2i 471 |
. . . . . . . . . . . . . . 15
|
116 | | lemul2a 10878 |
. . . . . . . . . . . . . . 15
|
117 | 115, 116 | mp3anl3 1420 |
. . . . . . . . . . . . . 14
|
118 | 44, 117 | mpanl2 717 |
. . . . . . . . . . . . 13
|
119 | 38, 118 | sylan 488 |
. . . . . . . . . . . 12
|
120 | 75 | recni 10052 |
. . . . . . . . . . . . 13
|
121 | 120 | mulid1i 10042 |
. . . . . . . . . . . 12
|
122 | 119, 121 | syl6breq 4694 |
. . . . . . . . . . 11
|
123 | 95, 112, 88, 114, 122 | letrd 10194 |
. . . . . . . . . 10
|
124 | 87, 95, 88, 109, 123 | letrd 10194 |
. . . . . . . . 9
|
125 | 85, 87, 88, 91, 124 | letrd 10194 |
. . . . . . . 8
|
126 | | resqcl 12931 |
. . . . . . . . . . . 12
|
127 | | sqge0 12940 |
. . . . . . . . . . . 12
|
128 | 126, 127 | absidd 14161 |
. . . . . . . . . . 11
|
129 | 19, 26, 128 | 3syl 18 |
. . . . . . . . . 10
|
130 | | normsq 27991 |
. . . . . . . . . . . . 13
|
131 | 19, 130 | syl 17 |
. . . . . . . . . . . 12
|
132 | | bdopadj 28941 |
. . . . . . . . . . . . . . . 16
|
133 | 3, 132 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
134 | | adj2 28793 |
. . . . . . . . . . . . . . 15
|
135 | 133, 134 | mp3an1 1411 |
. . . . . . . . . . . . . 14
|
136 | 19, 135 | mpancom 703 |
. . . . . . . . . . . . 13
|
137 | | bdopadj 28941 |
. . . . . . . . . . . . . . . 16
|
138 | | adjadj 28795 |
. . . . . . . . . . . . . . . 16
|
139 | 1, 137, 138 | mp2b 10 |
. . . . . . . . . . . . . . 15
|
140 | 139 | fveq1i 6192 |
. . . . . . . . . . . . . 14
|
141 | 140 | oveq2i 6661 |
. . . . . . . . . . . . 13
|
142 | 136, 141 | syl6req 2673 |
. . . . . . . . . . . 12
|
143 | 131, 142 | eqtrd 2656 |
. . . . . . . . . . 11
|
144 | 143 | fveq2d 6195 |
. . . . . . . . . 10
|
145 | 129, 144 | eqtr3d 2658 |
. . . . . . . . 9
|
146 | 145 | adantr 481 |
. . . . . . . 8
|
147 | 75 | sqsqrti 14115 |
. . . . . . . . . 10
|
148 | 8, 71, 147 | mp2b 10 |
. . . . . . . . 9
|
149 | 148 | a1i 11 |
. . . . . . . 8
|
150 | 125, 146,
149 | 3brtr4d 4685 |
. . . . . . 7
|
151 | | normge0 27983 |
. . . . . . . . . 10
|
152 | 19, 151 | syl 17 |
. . . . . . . . 9
|
153 | 8, 71, 76 | mp2b 10 |
. . . . . . . . . 10
|
154 | 75 | sqrtge0i 14116 |
. . . . . . . . . . 11
|
155 | 8, 71, 154 | mp2b 10 |
. . . . . . . . . 10
|
156 | | le2sq 12938 |
. . . . . . . . . 10
|
157 | 153, 155,
156 | mpanr12 721 |
. . . . . . . . 9
|
158 | 27, 152, 157 | syl2anc 693 |
. . . . . . . 8
|
159 | 158 | adantr 481 |
. . . . . . 7
|
160 | 150, 159 | mpbird 247 |
. . . . . 6
|
161 | 160 | ex 450 |
. . . . 5
|
162 | 80, 161 | mprgbir 2927 |
. . . 4
|
163 | 10, 153 | le2sqi 12953 |
. . . . 5
|
164 | 46, 155, 163 | mp2an 708 |
. . . 4
|
165 | 162, 164 | mpbi 220 |
. . 3
|
166 | 165, 148 | breqtri 4678 |
. 2
|
167 | 75, 11 | letri3i 10153 |
. 2
|
168 | 70, 166, 167 | mpbir2an 955 |
1
|