Step | Hyp | Ref
| Expression |
1 | | resqrexlemex.seq |
. . . . . . . . . . 11
    
                |
2 | | resqrexlemex.a |
. . . . . . . . . . 11
   |
3 | | resqrexlemex.agt0 |
. . . . . . . . . . 11

  |
4 | 1, 2, 3 | resqrexlemf 11016 |
. . . . . . . . . 10
       |
5 | 4 | adantr 276 |
. . . . . . . . 9
 

      |
6 | | 1nn 8930 |
. . . . . . . . . 10
 |
7 | 6 | a1i 9 |
. . . . . . . . 9
 

  |
8 | 5, 7 | ffvelcdmd 5653 |
. . . . . . . 8
 

      |
9 | | 2z 9281 |
. . . . . . . . 9
 |
10 | 9 | a1i 9 |
. . . . . . . 8
 

  |
11 | 8, 10 | rpexpcld 10678 |
. . . . . . 7
 

          |
12 | | simpr 110 |
. . . . . . 7
 

  |
13 | 11, 12 | rpdivcld 9714 |
. . . . . 6
 

            |
14 | 13 | rpred 9696 |
. . . . 5
 

            |
15 | | 1red 7972 |
. . . . 5
 

  |
16 | 14, 15 | readdcld 7987 |
. . . 4
 

              |
17 | | arch 9173 |
. . . 4
                            |
18 | 16, 17 | syl 14 |
. . 3
 

               |
19 | | simpllr 534 |
. . . . . . . . . 10
     
             
    
  |
20 | | simpr 110 |
. . . . . . . . . 10
     
             
    
      |
21 | | eluznn 9600 |
. . . . . . . . . 10
 
       |
22 | 19, 20, 21 | syl2anc 411 |
. . . . . . . . 9
     
             
    
  |
23 | | simplll 533 |
. . . . . . . . . . . . 13
   

                |
24 | 23 | adantr 276 |
. . . . . . . . . . . 12
     
             
    
  |
25 | 24, 4 | syl 14 |
. . . . . . . . . . 11
     
             
    
      |
26 | 25, 22 | ffvelcdmd 5653 |
. . . . . . . . . 10
     
             
    
      |
27 | 9 | a1i 9 |
. . . . . . . . . 10
     
             
    
  |
28 | 26, 27 | rpexpcld 10678 |
. . . . . . . . 9
     
             
    
          |
29 | | fveq2 5516 |
. . . . . . . . . . 11
           |
30 | 29 | oveq1d 5890 |
. . . . . . . . . 10
                   |
31 | | resqrexlemsqa.g |
. . . . . . . . . 10
           |
32 | 30, 31 | fvmptg 5593 |
. . . . . . . . 9
                         |
33 | 22, 28, 32 | syl2anc 411 |
. . . . . . . 8
     
             
    
              |
34 | 28 | rpred 9696 |
. . . . . . . . . . 11
     
             
    
          |
35 | 24, 2 | syl 14 |
. . . . . . . . . . 11
     
             
    
  |
36 | 34, 35 | resubcld 8338 |
. . . . . . . . . 10
     
             
    
            |
37 | 11 | ad3antrrr 492 |
. . . . . . . . . . . 12
     
             
    
          |
38 | 37 | rpred 9696 |
. . . . . . . . . . 11
     
             
    
          |
39 | | 4re 8996 |
. . . . . . . . . . . . . 14
 |
40 | | 4pos 9016 |
. . . . . . . . . . . . . 14
 |
41 | 39, 40 | elrpii 9656 |
. . . . . . . . . . . . 13
 |
42 | 41 | a1i 9 |
. . . . . . . . . . . 12
     
             
    
  |
43 | | nnm1nn0 9217 |
. . . . . . . . . . . . . 14
     |
44 | 22, 43 | syl 14 |
. . . . . . . . . . . . 13
     
             
    
    |
45 | 44 | nn0zd 9373 |
. . . . . . . . . . . 12
     
             
    
    |
46 | 42, 45 | rpexpcld 10678 |
. . . . . . . . . . 11
     
             
    
        |
47 | 38, 46 | rerpdivcld 9728 |
. . . . . . . . . 10
     
             
    
                  |
48 | 12 | ad3antrrr 492 |
. . . . . . . . . . 11
     
             
    
  |
49 | 48 | rpred 9696 |
. . . . . . . . . 10
     
             
    
  |
50 | 1, 2, 3 | resqrexlemcalc3 11025 |
. . . . . . . . . . 11
 

                            |
51 | 24, 22, 50 | syl2anc 411 |
. . . . . . . . . 10
     
             
    
                            |
52 | 14 | ad3antrrr 492 |
. . . . . . . . . . . 12
     
             
    
            |
53 | 22 | nnred 8932 |
. . . . . . . . . . . . 13
     
             
    
  |
54 | | 1red 7972 |
. . . . . . . . . . . . 13
     
             
    
  |
55 | 53, 54 | resubcld 8338 |
. . . . . . . . . . . 12
     
             
    
    |
56 | 39 | a1i 9 |
. . . . . . . . . . . . 13
     
             
    
  |
57 | 56, 44 | reexpcld 10671 |
. . . . . . . . . . . 12
     
             
    
        |
58 | 16 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
     
             
    
              |
59 | 19 | nnred 8932 |
. . . . . . . . . . . . . 14
     
             
    
  |
60 | | simplr 528 |
. . . . . . . . . . . . . 14
     
             
    
              |
61 | | eluzle 9540 |
. . . . . . . . . . . . . . 15
    
  |
62 | 61 | adantl 277 |
. . . . . . . . . . . . . 14
     
             
    
  |
63 | 58, 59, 53, 60, 62 | ltletrd 8380 |
. . . . . . . . . . . . 13
     
             
    
              |
64 | 52, 54, 53 | ltaddsubd 8502 |
. . . . . . . . . . . . 13
     
             
    
            
               |
65 | 63, 64 | mpbid 147 |
. . . . . . . . . . . 12
     
             
    
              |
66 | | 4z 9283 |
. . . . . . . . . . . . . 14
 |
67 | | 2re 8989 |
. . . . . . . . . . . . . . 15
 |
68 | | 2lt4 9092 |
. . . . . . . . . . . . . . 15
 |
69 | 67, 39, 68 | ltleii 8060 |
. . . . . . . . . . . . . 14
 |
70 | | eluz2 9534 |
. . . . . . . . . . . . . 14
         |
71 | 9, 66, 69, 70 | mpbir3an 1179 |
. . . . . . . . . . . . 13
     |
72 | | bernneq3 10643 |
. . . . . . . . . . . . 13
                   |
73 | 71, 44, 72 | sylancr 414 |
. . . . . . . . . . . 12
     
             
    
          |
74 | 52, 55, 57, 65, 73 | lttrd 8083 |
. . . . . . . . . . 11
     
             
    
                  |
75 | 38, 48, 46, 74 | ltdiv23d 9757 |
. . . . . . . . . 10
     
             
    
                  |
76 | 36, 47, 49, 51, 75 | lelttrd 8082 |
. . . . . . . . 9
     
             
    
            |
77 | 34, 35, 49 | ltsubadd2d 8500 |
. . . . . . . . 9
     
             
    
          
             |
78 | 76, 77 | mpbid 147 |
. . . . . . . 8
     
             
    
            |
79 | 33, 78 | eqbrtrd 4026 |
. . . . . . 7
     
             
    
    
   |
80 | 33, 28 | eqeltrd 2254 |
. . . . . . . . 9
     
             
    
      |
81 | 80 | rpred 9696 |
. . . . . . . 8
     
             
    
      |
82 | 81, 49 | readdcld 7987 |
. . . . . . . 8
     
             
    
        |
83 | 1, 2, 3 | resqrexlemover 11019 |
. . . . . . . . . 10
 

          |
84 | 24, 22, 83 | syl2anc 411 |
. . . . . . . . 9
     
             
    
          |
85 | 84, 33 | breqtrrd 4032 |
. . . . . . . 8
     
             
    
      |
86 | 81, 48 | ltaddrpd 9730 |
. . . . . . . 8
     
             
    
            |
87 | 35, 81, 82, 85, 86 | lttrd 8083 |
. . . . . . 7
     
             
    
        |
88 | 79, 87 | jca 306 |
. . . . . 6
     
             
    
                |
89 | 88 | ralrimiva 2550 |
. . . . 5
   

                        
           |
90 | 89 | ex 115 |
. . . 4
                  
         
            |
91 | 90 | reximdva 2579 |
. . 3
 

 
                        

          |
92 | 18, 91 | mpd 13 |
. 2
 

            

         |
93 | 92 | ralrimiva 2550 |
1
   
                     |