Proof of Theorem ax5seglem3
Step | Hyp | Ref
| Expression |
1 | | 1re 9660 |
. . . . . . . . . 10
 |
2 | | 0re 9661 |
. . . . . . . . . . . 12
 |
3 | 2, 1 | elicc2i 11725 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif) 
    |
4 | 3 | simp1bi 1045 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
5 | | resubcl 9958 |
. . . . . . . . . 10
 
     |
6 | 1, 4, 5 | sylancr 676 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)      |
7 | 6 | ad2antrr 740 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               |
8 | 7 | 3ad2ant2 1052 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
    |
9 | | fzfid 12224 |
. . . . . . . . . 10
  
   
         
       
            |
10 | | ax5seglem3a 25039 |
. . . . . . . . . . . 12
                         
                                   |
11 | 10 | simpld 466 |
. . . . . . . . . . 11
                         
                       |
12 | 11 | resqcld 12480 |
. . . . . . . . . 10
                         
                           |
13 | 9, 12 | fsumrecl 13877 |
. . . . . . . . 9
  
   
         
       
                            |
14 | 11 | sqge0d 12481 |
. . . . . . . . . 10
                         
                           |
15 | 9, 12, 14 | fsumge0 13932 |
. . . . . . . . 9
  
   
         
       
                            |
16 | 13, 15 | resqrtcld 13556 |
. . . . . . . 8
  
   
         
       
                                |
17 | 16 | 3ad2ant1 1051 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                          |
18 | 8, 17 | remulcld 9689 |
. . . . . 6
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
      
                       |
19 | 2, 1 | elicc2i 11725 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif) 
    |
20 | 19 | simp1bi 1045 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
21 | | resubcl 9958 |
. . . . . . . . . 10
 
     |
22 | 1, 20, 21 | sylancr 676 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)      |
23 | 22 | ad2antlr 741 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               |
24 | 23 | 3ad2ant2 1052 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
    |
25 | 10 | simprd 470 |
. . . . . . . . . . 11
                         
                       |
26 | 25 | resqcld 12480 |
. . . . . . . . . 10
                         
                           |
27 | 9, 26 | fsumrecl 13877 |
. . . . . . . . 9
  
   
         
       
                            |
28 | 25 | sqge0d 12481 |
. . . . . . . . . 10
                         
                           |
29 | 9, 26, 28 | fsumge0 13932 |
. . . . . . . . 9
  
   
         
       
                            |
30 | 27, 29 | resqrtcld 13556 |
. . . . . . . 8
  
   
         
       
                                |
31 | 30 | 3ad2ant1 1051 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                          |
32 | 24, 31 | remulcld 9689 |
. . . . . 6
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
      
                       |
33 | 3 | simp3bi 1047 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
34 | | subge0 10148 |
. . . . . . . . . . 11
 
   
   |
35 | 1, 4, 34 | sylancr 676 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)  
 
   |
36 | 33, 35 | mpbird 240 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)      |
37 | 36 | ad2antrr 740 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               |
38 | 37 | 3ad2ant2 1052 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
    |
39 | 13, 15 | sqrtge0d 13559 |
. . . . . . . 8
  
   
         
       
         
                      |
40 | 39 | 3ad2ant1 1051 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                          |
41 | 8, 17, 38, 40 | mulge0d 10211 |
. . . . . 6
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                              |
42 | 19 | simp3bi 1047 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
43 | | subge0 10148 |
. . . . . . . . . . 11
 
   
   |
44 | 1, 20, 43 | sylancr 676 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)  
 
   |
45 | 42, 44 | mpbird 240 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)      |
46 | 45 | ad2antlr 741 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               |
47 | 46 | 3ad2ant2 1052 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
    |
48 | 27, 29 | sqrtge0d 13559 |
. . . . . . . 8
  
   
         
       
         
                      |
49 | 48 | 3ad2ant1 1051 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                          |
50 | 24, 31, 47, 49 | mulge0d 10211 |
. . . . . 6
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                              |
51 | | resqrtth 13396 |
. . . . . . . . . 10
                                          
                                                  |
52 | 13, 15, 51 | syl2anc 673 |
. . . . . . . . 9
  
   
         
       
          
                                             |
53 | 52 | 3ad2ant1 1051 |
. . . . . . . 8
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                                                  |
54 | 53 | oveq2d 6324 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                                                                  |
55 | | ax-1cn 9615 |
. . . . . . . . 9
 |
56 | 4 | recnd 9687 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
57 | 56 | ad2antrr 740 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                             |
58 | 57 | 3ad2ant2 1052 |
. . . . . . . . 9
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
  |
59 | | subcl 9894 |
. . . . . . . . 9
 
     |
60 | 55, 58, 59 | sylancr 676 |
. . . . . . . 8
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
    |
61 | 16 | recnd 9687 |
. . . . . . . . 9
  
   
         
       
                                |
62 | 61 | 3ad2ant1 1051 |
. . . . . . . 8
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                          |
63 | 60, 62 | sqmuld 12466 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                                                                      |
64 | | resqrtth 13396 |
. . . . . . . . . . 11
                                          
                                                  |
65 | 27, 29, 64 | syl2anc 673 |
. . . . . . . . . 10
  
   
         
       
          
                                             |
66 | 65 | 3ad2ant1 1051 |
. . . . . . . . 9
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                                                  |
67 | 66 | oveq2d 6324 |
. . . . . . . 8
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                                                                  |
68 | 20 | recnd 9687 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)    |
69 | 68 | ad2antlr 741 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                             |
70 | 69 | 3ad2ant2 1052 |
. . . . . . . . . 10
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
  |
71 | | subcl 9894 |
. . . . . . . . . 10
 
     |
72 | 55, 70, 71 | sylancr 676 |
. . . . . . . . 9
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
    |
73 | 30 | recnd 9687 |
. . . . . . . . . 10
  
   
         
       
                                |
74 | 73 | 3ad2ant1 1051 |
. . . . . . . . 9
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                          |
75 | 72, 74 | sqmuld 12466 |
. . . . . . . 8
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                                                                      |
76 | | simp3r 1059 |
. . . . . . . . . 10
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
   Cgr     |
77 | | simp122 1163 |
. . . . . . . . . . 11
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
      |
78 | | simp123 1164 |
. . . . . . . . . . 11
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
      |
79 | | simp132 1166 |
. . . . . . . . . . 11
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
      |
80 | | simp133 1167 |
. . . . . . . . . . 11
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
      |
81 | | brcgr 25009 |
. . . . . . . . . . 11
                           Cgr   
                                          |
82 | 77, 78, 79, 80, 81 | syl22anc 1293 |
. . . . . . . . . 10
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
    Cgr                                              |
83 | 76, 82 | mpbid 215 |
. . . . . . . . 9
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                    
                     |
84 | | simp11 1060 |
. . . . . . . . . 10
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
  |
85 | | simp121 1162 |
. . . . . . . . . 10
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
      |
86 | | simp2ll 1097 |
. . . . . . . . . 10
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
  ![[,] [,]](_icc.gif)    |
87 | | simp2rl 1099 |
. . . . . . . . . 10
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                            |
88 | | ax5seglem2 25038 |
. . . . . . . . . 10
  
   
     
  ![[,] [,]](_icc.gif)                                                                                |
89 | 84, 85, 78, 86, 87, 88 | syl122anc 1301 |
. . . . . . . . 9
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                                                  |
90 | | simp131 1165 |
. . . . . . . . . 10
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
      |
91 | | simp2lr 1098 |
. . . . . . . . . 10
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
  ![[,] [,]](_icc.gif)    |
92 | | simp2rr 1100 |
. . . . . . . . . 10
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                            |
93 | | ax5seglem2 25038 |
. . . . . . . . . 10
  
   
     
  ![[,] [,]](_icc.gif)                                                                                |
94 | 84, 90, 80, 91, 92, 93 | syl122anc 1301 |
. . . . . . . . 9
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                                                  |
95 | 83, 89, 94 | 3eqtr3d 2513 |
. . . . . . . 8
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                                                          |
96 | 67, 75, 95 | 3eqtr4d 2515 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                                                              |
97 | 54, 63, 96 | 3eqtr4d 2515 |
. . . . . 6
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                                                                  |
98 | 18, 32, 41, 50, 97 | sq11d 12490 |
. . . . 5
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
      
                                                   |
99 | 4 | ad2antrr 740 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                             |
100 | 99 | 3ad2ant2 1052 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
  |
101 | 100, 17 | remulcld 9689 |
. . . . . 6
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
    
                       |
102 | 20 | ad2antlr 741 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                             |
103 | 102 | 3ad2ant2 1052 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
  |
104 | 103, 31 | remulcld 9689 |
. . . . . 6
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
    
                       |
105 | 3 | simp2bi 1046 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)    |
106 | 105 | ad2antrr 740 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                             |
107 | 106 | 3ad2ant2 1052 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
  |
108 | 100, 17, 107, 40 | mulge0d 10211 |
. . . . . 6
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                            |
109 | 19 | simp2bi 1046 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)    |
110 | 109 | ad2antlr 741 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                             |
111 | 110 | 3ad2ant2 1052 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
  |
112 | 103, 31, 111, 49 | mulge0d 10211 |
. . . . . 6
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
                            |
113 | 52 | oveq2d 6324 |
. . . . . . . 8
  
   
         
       
                                             
                      |
114 | 113 | 3ad2ant1 1051 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
         
                                                    |
115 | 58, 62 | sqmuld 12466 |
. . . . . . 7
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
 
                                                                |
116 | 66 | oveq2d 6324 |
. . . . . . . 8
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
         
                                                    |
117 | 70, 74 | sqmuld 12466 |
. . . . . . . 8
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
 
                                                                |
118 | | simp3l 1058 |
. . . . . . . . . 10
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
                         
                               Cgr      Cgr    
   Cgr     |
119 | | brcgr 25009 |
. . . . . . . . . . 11
                           Cgr   
                                          |
120 | 85, 77, 90, 79, 119 | syl22anc 1293 |
. . . . . . . . . 10
                         
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)    
            |