Proof of Theorem ax5seglem3
Step | Hyp | Ref
| Expression |
1 | | 1re 10039 |
. . . . . . . . . 10
|
2 | | 0re 10040 |
. . . . . . . . . . . 12
|
3 | 2, 1 | elicc2i 12239 |
. . . . . . . . . . 11
|
4 | 3 | simp1bi 1076 |
. . . . . . . . . 10
|
5 | | resubcl 10345 |
. . . . . . . . . 10
|
6 | 1, 4, 5 | sylancr 695 |
. . . . . . . . 9
|
7 | 6 | ad2antrr 762 |
. . . . . . . 8
|
8 | 7 | 3ad2ant2 1083 |
. . . . . . 7
Cgr Cgr
|
9 | | fzfid 12772 |
. . . . . . . . . 10
|
10 | | ax5seglem3a 25810 |
. . . . . . . . . . . 12
|
11 | 10 | simpld 475 |
. . . . . . . . . . 11
|
12 | 11 | resqcld 13035 |
. . . . . . . . . 10
|
13 | 9, 12 | fsumrecl 14465 |
. . . . . . . . 9
|
14 | 11 | sqge0d 13036 |
. . . . . . . . . 10
|
15 | 9, 12, 14 | fsumge0 14527 |
. . . . . . . . 9
|
16 | 13, 15 | resqrtcld 14156 |
. . . . . . . 8
|
17 | 16 | 3ad2ant1 1082 |
. . . . . . 7
Cgr Cgr
|
18 | 8, 17 | remulcld 10070 |
. . . . . 6
Cgr Cgr
|
19 | 2, 1 | elicc2i 12239 |
. . . . . . . . . . 11
|
20 | 19 | simp1bi 1076 |
. . . . . . . . . 10
|
21 | | resubcl 10345 |
. . . . . . . . . 10
|
22 | 1, 20, 21 | sylancr 695 |
. . . . . . . . 9
|
23 | 22 | ad2antlr 763 |
. . . . . . . 8
|
24 | 23 | 3ad2ant2 1083 |
. . . . . . 7
Cgr Cgr
|
25 | 10 | simprd 479 |
. . . . . . . . . . 11
|
26 | 25 | resqcld 13035 |
. . . . . . . . . 10
|
27 | 9, 26 | fsumrecl 14465 |
. . . . . . . . 9
|
28 | 25 | sqge0d 13036 |
. . . . . . . . . 10
|
29 | 9, 26, 28 | fsumge0 14527 |
. . . . . . . . 9
|
30 | 27, 29 | resqrtcld 14156 |
. . . . . . . 8
|
31 | 30 | 3ad2ant1 1082 |
. . . . . . 7
Cgr Cgr
|
32 | 24, 31 | remulcld 10070 |
. . . . . 6
Cgr Cgr
|
33 | 3 | simp3bi 1078 |
. . . . . . . . . 10
|
34 | | subge0 10541 |
. . . . . . . . . . 11
|
35 | 1, 4, 34 | sylancr 695 |
. . . . . . . . . 10
|
36 | 33, 35 | mpbird 247 |
. . . . . . . . 9
|
37 | 36 | ad2antrr 762 |
. . . . . . . 8
|
38 | 37 | 3ad2ant2 1083 |
. . . . . . 7
Cgr Cgr
|
39 | 13, 15 | sqrtge0d 14159 |
. . . . . . . 8
|
40 | 39 | 3ad2ant1 1082 |
. . . . . . 7
Cgr Cgr
|
41 | 8, 17, 38, 40 | mulge0d 10604 |
. . . . . 6
Cgr Cgr
|
42 | 19 | simp3bi 1078 |
. . . . . . . . . 10
|
43 | | subge0 10541 |
. . . . . . . . . . 11
|
44 | 1, 20, 43 | sylancr 695 |
. . . . . . . . . 10
|
45 | 42, 44 | mpbird 247 |
. . . . . . . . 9
|
46 | 45 | ad2antlr 763 |
. . . . . . . 8
|
47 | 46 | 3ad2ant2 1083 |
. . . . . . 7
Cgr Cgr
|
48 | 27, 29 | sqrtge0d 14159 |
. . . . . . . 8
|
49 | 48 | 3ad2ant1 1082 |
. . . . . . 7
Cgr Cgr
|
50 | 24, 31, 47, 49 | mulge0d 10604 |
. . . . . 6
Cgr Cgr
|
51 | | resqrtth 13996 |
. . . . . . . . . 10
|
52 | 13, 15, 51 | syl2anc 693 |
. . . . . . . . 9
|
53 | 52 | 3ad2ant1 1082 |
. . . . . . . 8
Cgr Cgr
|
54 | 53 | oveq2d 6666 |
. . . . . . 7
Cgr Cgr
|
55 | | ax-1cn 9994 |
. . . . . . . . 9
|
56 | 4 | recnd 10068 |
. . . . . . . . . . 11
|
57 | 56 | ad2antrr 762 |
. . . . . . . . . 10
|
58 | 57 | 3ad2ant2 1083 |
. . . . . . . . 9
Cgr Cgr
|
59 | | subcl 10280 |
. . . . . . . . 9
|
60 | 55, 58, 59 | sylancr 695 |
. . . . . . . 8
Cgr Cgr
|
61 | 16 | recnd 10068 |
. . . . . . . . 9
|
62 | 61 | 3ad2ant1 1082 |
. . . . . . . 8
Cgr Cgr
|
63 | 60, 62 | sqmuld 13020 |
. . . . . . 7
Cgr Cgr
|
64 | | resqrtth 13996 |
. . . . . . . . . . 11
|
65 | 27, 29, 64 | syl2anc 693 |
. . . . . . . . . 10
|
66 | 65 | 3ad2ant1 1082 |
. . . . . . . . 9
Cgr Cgr
|
67 | 66 | oveq2d 6666 |
. . . . . . . 8
Cgr Cgr
|
68 | 20 | recnd 10068 |
. . . . . . . . . . . 12
|
69 | 68 | ad2antlr 763 |
. . . . . . . . . . 11
|
70 | 69 | 3ad2ant2 1083 |
. . . . . . . . . 10
Cgr Cgr
|
71 | | subcl 10280 |
. . . . . . . . . 10
|
72 | 55, 70, 71 | sylancr 695 |
. . . . . . . . 9
Cgr Cgr
|
73 | 30 | recnd 10068 |
. . . . . . . . . 10
|
74 | 73 | 3ad2ant1 1082 |
. . . . . . . . 9
Cgr Cgr
|
75 | 72, 74 | sqmuld 13020 |
. . . . . . . 8
Cgr Cgr
|
76 | | simp3r 1090 |
. . . . . . . . . 10
Cgr Cgr
Cgr |
77 | | simp122 1194 |
. . . . . . . . . . 11
Cgr Cgr
|
78 | | simp123 1195 |
. . . . . . . . . . 11
Cgr Cgr
|
79 | | simp132 1197 |
. . . . . . . . . . 11
Cgr Cgr
|
80 | | simp133 1198 |
. . . . . . . . . . 11
Cgr Cgr
|
81 | | brcgr 25780 |
. . . . . . . . . . 11
Cgr
|
82 | 77, 78, 79, 80, 81 | syl22anc 1327 |
. . . . . . . . . 10
Cgr Cgr
Cgr |
83 | 76, 82 | mpbid 222 |
. . . . . . . . 9
Cgr Cgr
|
84 | | simp11 1091 |
. . . . . . . . . 10
Cgr Cgr
|
85 | | simp121 1193 |
. . . . . . . . . 10
Cgr Cgr
|
86 | | simp2ll 1128 |
. . . . . . . . . 10
Cgr Cgr
|
87 | | simp2rl 1130 |
. . . . . . . . . 10
Cgr Cgr
|
88 | | ax5seglem2 25809 |
. . . . . . . . . 10
|
89 | 84, 85, 78, 86, 87, 88 | syl122anc 1335 |
. . . . . . . . 9
Cgr Cgr
|
90 | | simp131 1196 |
. . . . . . . . . 10
Cgr Cgr
|
91 | | simp2lr 1129 |
. . . . . . . . . 10
Cgr Cgr
|
92 | | simp2rr 1131 |
. . . . . . . . . 10
Cgr Cgr
|
93 | | ax5seglem2 25809 |
. . . . . . . . . 10
|
94 | 84, 90, 80, 91, 92, 93 | syl122anc 1335 |
. . . . . . . . 9
Cgr Cgr
|
95 | 83, 89, 94 | 3eqtr3d 2664 |
. . . . . . . 8
Cgr Cgr
|
96 | 67, 75, 95 | 3eqtr4d 2666 |
. . . . . . 7
Cgr Cgr
|
97 | 54, 63, 96 | 3eqtr4d 2666 |
. . . . . 6
Cgr Cgr
|
98 | 18, 32, 41, 50, 97 | sq11d 13045 |
. . . . 5
Cgr Cgr
|
99 | 4 | ad2antrr 762 |
. . . . . . . 8
|
100 | 99 | 3ad2ant2 1083 |
. . . . . . 7
Cgr Cgr
|
101 | 100, 17 | remulcld 10070 |
. . . . . 6
Cgr Cgr
|
102 | 20 | ad2antlr 763 |
. . . . . . . 8
|
103 | 102 | 3ad2ant2 1083 |
. . . . . . 7
Cgr Cgr
|
104 | 103, 31 | remulcld 10070 |
. . . . . 6
Cgr Cgr
|
105 | 3 | simp2bi 1077 |
. . . . . . . . 9
|
106 | 105 | ad2antrr 762 |
. . . . . . . 8
|
107 | 106 | 3ad2ant2 1083 |
. . . . . . 7
Cgr Cgr
|
108 | 100, 17, 107, 40 | mulge0d 10604 |
. . . . . 6
Cgr Cgr
|
109 | 19 | simp2bi 1077 |
. . . . . . . . 9
|
110 | 109 | ad2antlr 763 |
. . . . . . . 8
|
111 | 110 | 3ad2ant2 1083 |
. . . . . . 7
Cgr Cgr
|
112 | 103, 31, 111, 49 | mulge0d 10604 |
. . . . . 6
Cgr Cgr
|
113 | 52 | oveq2d 6666 |
. . . . . . . 8
|
114 | 113 | 3ad2ant1 1082 |
. . . . . . 7
Cgr Cgr
|
115 | 58, 62 | sqmuld 13020 |
. . . . . . 7
Cgr Cgr
|
116 | 66 | oveq2d 6666 |
. . . . . . . 8
Cgr Cgr
|
117 | 70, 74 | sqmuld 13020 |
. . . . . . . 8
Cgr Cgr
|
118 | | simp3l 1089 |
. . . . . . . . . 10
Cgr Cgr
Cgr |
119 | | brcgr 25780 |
. . . . . . . . . . 11
Cgr
|
120 | 85, 77, 90, 79, 119 | syl22anc 1327 |
. . . . . . . . . 10
Cgr Cgr
Cgr |
121 | 118, 120 | mpbid 222 |
. . . . . . . . 9
Cgr Cgr
|
122 | | ax5seglem1 25808 |
. . . . . . . . . 10
|
123 | 84, 85, 78, 86, 87, 122 | syl122anc 1335 |
. . . . . . . . 9
Cgr Cgr
|
124 | | ax5seglem1 25808 |
. . . . . . . . . 10
|
125 | 84, 90, 80, 91, 92, 124 | syl122anc 1335 |
. . . . . . . . 9
Cgr Cgr
|
126 | 121, 123,
125 | 3eqtr3d 2664 |
. . . . . . . 8
Cgr Cgr
|
127 | 116, 117,
126 | 3eqtr4d 2666 |
. . . . . . 7
Cgr Cgr
|
128 | 114, 115,
127 | 3eqtr4d 2666 |
. . . . . 6
Cgr Cgr
|
129 | 101, 104,
108, 112, 128 | sq11d 13045 |
. . . . 5
Cgr Cgr
|
130 | 98, 129 | oveq12d 6668 |
. . . 4
Cgr Cgr
|
131 | 60, 58, 62 | adddird 10065 |
. . . 4
Cgr Cgr
|
132 | 72, 70, 74 | adddird 10065 |
. . . 4
Cgr Cgr
|
133 | 130, 131,
132 | 3eqtr4d 2666 |
. . 3
Cgr Cgr
|
134 | | npcan 10290 |
. . . . . . . . 9
|
135 | 55, 56, 134 | sylancr 695 |
. . . . . . . 8
|
136 | 135 | adantr 481 |
. . . . . . 7
|
137 | 136 | oveq1d 6665 |
. . . . . 6
|
138 | 137 | adantr 481 |
. . . . 5
|
139 | 138 | 3ad2ant2 1083 |
. . . 4
Cgr Cgr
|
140 | 61 | mulid2d 10058 |
. . . . 5
|
141 | 140 | 3ad2ant1 1082 |
. . . 4
Cgr Cgr
|
142 | 139, 141 | eqtrd 2656 |
. . 3
Cgr Cgr
|
143 | | npcan 10290 |
. . . . . . . 8
|
144 | 55, 68, 143 | sylancr 695 |
. . . . . . 7
|
145 | 144 | oveq1d 6665 |
. . . . . 6
|
146 | 145 | ad2antlr 763 |
. . . . 5
|
147 | 146 | 3ad2ant2 1083 |
. . . 4
Cgr Cgr
|
148 | 73 | mulid2d 10058 |
. . . . 5
|
149 | 148 | 3ad2ant1 1082 |
. . . 4
Cgr Cgr
|
150 | 147, 149 | eqtrd 2656 |
. . 3
Cgr Cgr
|
151 | 133, 142,
150 | 3eqtr3d 2664 |
. 2
Cgr Cgr
|
152 | | sqrt11 14003 |
. . . 4
|
153 | 13, 15, 27, 29, 152 | syl22anc 1327 |
. . 3
|
154 | 153 | 3ad2ant1 1082 |
. 2
Cgr Cgr
|
155 | 151, 154 | mpbid 222 |
1
Cgr Cgr
|