Proof of Theorem normpar2i
Step | Hyp | Ref
| Expression |
1 | | normpar2.1 |
. . . . . . 7
|
2 | | normpar2.2 |
. . . . . . 7
|
3 | 1, 2 | hvaddcli 27875 |
. . . . . 6
|
4 | | 2cn 11091 |
. . . . . . 7
|
5 | | normpar2.3 |
. . . . . . 7
|
6 | 4, 5 | hvmulcli 27871 |
. . . . . 6
|
7 | 3, 6 | hvsubcli 27878 |
. . . . 5
|
8 | 7 | normcli 27988 |
. . . 4
|
9 | 8 | resqcli 12949 |
. . 3
|
10 | 9 | recni 10052 |
. 2
|
11 | 1, 2 | hvsubcli 27878 |
. . . . 5
|
12 | 11 | normcli 27988 |
. . . 4
|
13 | 12 | resqcli 12949 |
. . 3
|
14 | 13 | recni 10052 |
. 2
|
15 | | 4cn 11098 |
. . . . 5
|
16 | 1, 5 | hvsubcli 27878 |
. . . . . . . 8
|
17 | 16 | normcli 27988 |
. . . . . . 7
|
18 | 17 | resqcli 12949 |
. . . . . 6
|
19 | 18 | recni 10052 |
. . . . 5
|
20 | 15, 19 | mulcli 10045 |
. . . 4
|
21 | 2, 5 | hvsubcli 27878 |
. . . . . . . 8
|
22 | 21 | normcli 27988 |
. . . . . . 7
|
23 | 22 | resqcli 12949 |
. . . . . 6
|
24 | 23 | recni 10052 |
. . . . 5
|
25 | 15, 24 | mulcli 10045 |
. . . 4
|
26 | | 2ne0 11113 |
. . . 4
|
27 | 20, 25, 4, 26 | divdiri 10782 |
. . 3
|
28 | 20, 25 | addcomi 10227 |
. . . . . . 7
|
29 | | neg1cn 11124 |
. . . . . . . . . . . . . . . 16
|
30 | 29, 6 | hvmulcli 27871 |
. . . . . . . . . . . . . . 15
|
31 | 29, 11 | hvmulcli 27871 |
. . . . . . . . . . . . . . 15
|
32 | 3, 30, 31 | hvadd32i 27911 |
. . . . . . . . . . . . . 14
|
33 | 3, 6 | hvsubvali 27877 |
. . . . . . . . . . . . . . 15
|
34 | 33 | oveq1i 6660 |
. . . . . . . . . . . . . 14
|
35 | 4, 2 | hvmulcli 27871 |
. . . . . . . . . . . . . . . 16
|
36 | 35, 6 | hvsubvali 27877 |
. . . . . . . . . . . . . . 15
|
37 | 1, 2 | hvcomi 27876 |
. . . . . . . . . . . . . . . . . 18
|
38 | 1, 2 | hvnegdii 27919 |
. . . . . . . . . . . . . . . . . 18
|
39 | 37, 38 | oveq12i 6662 |
. . . . . . . . . . . . . . . . 17
|
40 | 2, 1 | hvsubcan2i 27921 |
. . . . . . . . . . . . . . . . 17
|
41 | 39, 40 | eqtri 2644 |
. . . . . . . . . . . . . . . 16
|
42 | 41 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
|
43 | 36, 42 | eqtr4i 2647 |
. . . . . . . . . . . . . 14
|
44 | 32, 34, 43 | 3eqtr4i 2654 |
. . . . . . . . . . . . 13
|
45 | 7, 11 | hvsubvali 27877 |
. . . . . . . . . . . . 13
|
46 | 4, 2, 5 | hvsubdistr1i 27909 |
. . . . . . . . . . . . 13
|
47 | 44, 45, 46 | 3eqtr4i 2654 |
. . . . . . . . . . . 12
|
48 | 47 | fveq2i 6194 |
. . . . . . . . . . 11
|
49 | 4, 21 | norm-iii-i 27996 |
. . . . . . . . . . 11
|
50 | | 0le2 11111 |
. . . . . . . . . . . . 13
|
51 | | 2re 11090 |
. . . . . . . . . . . . . 14
|
52 | 51 | absidi 14117 |
. . . . . . . . . . . . 13
|
53 | 50, 52 | ax-mp 5 |
. . . . . . . . . . . 12
|
54 | 53 | oveq1i 6660 |
. . . . . . . . . . 11
|
55 | 48, 49, 54 | 3eqtri 2648 |
. . . . . . . . . 10
|
56 | 55 | oveq1i 6660 |
. . . . . . . . 9
|
57 | 22 | recni 10052 |
. . . . . . . . . 10
|
58 | 4, 57 | sqmuli 12947 |
. . . . . . . . 9
|
59 | | sq2 12960 |
. . . . . . . . . 10
|
60 | 59 | oveq1i 6660 |
. . . . . . . . 9
|
61 | 56, 58, 60 | 3eqtri 2648 |
. . . . . . . 8
|
62 | 1, 2 | hvsubcan2i 27921 |
. . . . . . . . . . . . . . 15
|
63 | 62 | oveq1i 6660 |
. . . . . . . . . . . . . 14
|
64 | 3, 30, 11 | hvadd32i 27911 |
. . . . . . . . . . . . . 14
|
65 | 4, 1 | hvmulcli 27871 |
. . . . . . . . . . . . . . 15
|
66 | 65, 6 | hvsubvali 27877 |
. . . . . . . . . . . . . 14
|
67 | 63, 64, 66 | 3eqtr4i 2654 |
. . . . . . . . . . . . 13
|
68 | 33 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
69 | 4, 1, 5 | hvsubdistr1i 27909 |
. . . . . . . . . . . . 13
|
70 | 67, 68, 69 | 3eqtr4i 2654 |
. . . . . . . . . . . 12
|
71 | 70 | fveq2i 6194 |
. . . . . . . . . . 11
|
72 | 4, 16 | norm-iii-i 27996 |
. . . . . . . . . . 11
|
73 | 53 | oveq1i 6660 |
. . . . . . . . . . 11
|
74 | 71, 72, 73 | 3eqtri 2648 |
. . . . . . . . . 10
|
75 | 74 | oveq1i 6660 |
. . . . . . . . 9
|
76 | 17 | recni 10052 |
. . . . . . . . . 10
|
77 | 4, 76 | sqmuli 12947 |
. . . . . . . . 9
|
78 | 59 | oveq1i 6660 |
. . . . . . . . 9
|
79 | 75, 77, 78 | 3eqtri 2648 |
. . . . . . . 8
|
80 | 61, 79 | oveq12i 6662 |
. . . . . . 7
|
81 | 28, 80 | eqtr4i 2647 |
. . . . . 6
|
82 | 7, 11 | normpari 28011 |
. . . . . 6
|
83 | 81, 82 | eqtri 2644 |
. . . . 5
|
84 | 83 | oveq1i 6660 |
. . . 4
|
85 | 4, 10 | mulcli 10045 |
. . . . 5
|
86 | 4, 14 | mulcli 10045 |
. . . . 5
|
87 | 85, 86, 4, 26 | divdiri 10782 |
. . . 4
|
88 | 10, 4, 26 | divcan3i 10771 |
. . . . 5
|
89 | 14, 4, 26 | divcan3i 10771 |
. . . . 5
|
90 | 88, 89 | oveq12i 6662 |
. . . 4
|
91 | 84, 87, 90 | 3eqtri 2648 |
. . 3
|
92 | 15, 19, 4, 26 | div23i 10783 |
. . . . 5
|
93 | | 4d2e2 11184 |
. . . . . 6
|
94 | 93 | oveq1i 6660 |
. . . . 5
|
95 | 92, 94 | eqtri 2644 |
. . . 4
|
96 | 15, 24, 4, 26 | div23i 10783 |
. . . . 5
|
97 | 93 | oveq1i 6660 |
. . . . 5
|
98 | 96, 97 | eqtri 2644 |
. . . 4
|
99 | 95, 98 | oveq12i 6662 |
. . 3
|
100 | 27, 91, 99 | 3eqtr3i 2652 |
. 2
|
101 | 10, 14, 100 | mvlladdi 10299 |
1
|