Step | Hyp | Ref
| Expression |
1 | | gruina.1 |
. . . . . 6
   |
2 | | inss1 3652 |
. . . . . 6
   |
3 | 1, 2 | eqsstri 3462 |
. . . . 5
 |
4 | | sseq2 3454 |
. . . . 5


   |
5 | 3, 4 | mpbii 215 |
. . . 4

  |
6 | | ss0 3765 |
. . . 4

  |
7 | | fveq2 5865 |
. . . . . 6

          |
8 | | r10 8239 |
. . . . . 6
     |
9 | 7, 8 | syl6eq 2501 |
. . . . 5

      |
10 | | 0ss 3763 |
. . . . 5
 |
11 | 9, 10 | syl6eqss 3482 |
. . . 4

      |
12 | 5, 6, 11 | 3syl 18 |
. . 3

      |
13 | 12 | a1i 11 |
. 2


       |
14 | 1 | gruina 9243 |
. . . . 5
     |
15 | | inawina 9115 |
. . . . 5

   |
16 | | winaon 9113 |
. . . . . 6
    |
17 | | winalim 9120 |
. . . . . 6
    |
18 | | r1lim 8243 |
. . . . . 6
              |
19 | 16, 17, 18 | syl2anc 667 |
. . . . 5
             |
20 | 14, 15, 19 | 3syl 18 |
. . . 4
              |
21 | | inss2 3653 |
. . . . . . . . . . . 12
   |
22 | 1, 21 | eqsstri 3462 |
. . . . . . . . . . 11
 |
23 | 22 | sseli 3428 |
. . . . . . . . . 10
   |
24 | | eleq1 2517 |
. . . . . . . . . . . . 13


   |
25 | | fveq2 5865 |
. . . . . . . . . . . . . . 15

          |
26 | 25, 8 | syl6eq 2501 |
. . . . . . . . . . . . . 14

      |
27 | 26 | eleq1d 2513 |
. . . . . . . . . . . . 13

    
   |
28 | 24, 27 | imbi12d 322 |
. . . . . . . . . . . 12

            |
29 | | eleq1 2517 |
. . . . . . . . . . . . 13
 
   |
30 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
31 | 30 | eleq1d 2513 |
. . . . . . . . . . . . 13
     
       |
32 | 29, 31 | imbi12d 322 |
. . . . . . . . . . . 12
                 |
33 | | eleq1 2517 |
. . . . . . . . . . . . 13
     |
34 | | fveq2 5865 |
. . . . . . . . . . . . . 14
       
   |
35 | 34 | eleq1d 2513 |
. . . . . . . . . . . . 13
             |
36 | 33, 35 | imbi12d 322 |
. . . . . . . . . . . 12
  
     
  
     |
37 | 3 | sseli 3428 |
. . . . . . . . . . . . 13

  |
38 | 37 | a1i 11 |
. . . . . . . . . . . 12


   |
39 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
   |
40 | | elelsuc 5495 |
. . . . . . . . . . . . . . . . . 18

  |
41 | 3 | sseli 3428 |
. . . . . . . . . . . . . . . . . . . . 21

  |
42 | | ne0i 3737 |
. . . . . . . . . . . . . . . . . . . . 21
   |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   |
44 | 14, 15, 16 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
     |
45 | 43, 44 | sylan2 477 |
. . . . . . . . . . . . . . . . . . 19
 
   |
46 | | eloni 5433 |
. . . . . . . . . . . . . . . . . . 19
   |
47 | | ordsucelsuc 6649 |
. . . . . . . . . . . . . . . . . . 19


   |
48 | 45, 46, 47 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
 
     |
49 | 40, 48 | syl5ibr 225 |
. . . . . . . . . . . . . . . . 17
 
 
   |
50 | 39, 49 | mpd 15 |
. . . . . . . . . . . . . . . 16
 
   |
51 | | grupw 9220 |
. . . . . . . . . . . . . . . . . . 19
              |
52 | 51 | ex 436 |
. . . . . . . . . . . . . . . . . 18

             |
53 | 52 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
              |
54 | | r1suc 8241 |
. . . . . . . . . . . . . . . . . . 19
            |
55 | 54 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . 18
              |
56 | 55 | biimprcd 229 |
. . . . . . . . . . . . . . . . 17
              |
57 | 53, 56 | syl6 34 |
. . . . . . . . . . . . . . . 16
 
               |
58 | 50, 57 | embantd 56 |
. . . . . . . . . . . . . . 15
 
  
    

        |
59 | 58 | ex 436 |
. . . . . . . . . . . . . 14

  
    

         |
60 | 59 | com23 81 |
. . . . . . . . . . . . 13

       
          |
61 | 60 | com4r 89 |
. . . . . . . . . . . 12
 
       
  
      |
62 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
     |
63 | 3 | sseli 3428 |
. . . . . . . . . . . . . . . . . . . . 21
   |
64 | | ne0i 3737 |
. . . . . . . . . . . . . . . . . . . . 21
   |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   |
66 | 65, 44 | sylan2 477 |
. . . . . . . . . . . . . . . . . . 19
     |
67 | | ontr1 5469 |
. . . . . . . . . . . . . . . . . . . . . 22
  

   |
68 | | pm2.27 40 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
69 | 67, 68 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . 21
  

               |
70 | 69 | expd 438 |
. . . . . . . . . . . . . . . . . . . 20
    
    
         |
71 | 70 | com3r 82 |
. . . . . . . . . . . . . . . . . . 19
 
  
    
         |
72 | 62, 66, 71 | sylc 62 |
. . . . . . . . . . . . . . . . . 18
     
    
        |
73 | 72 | imp 431 |
. . . . . . . . . . . . . . . . 17
    
              |
74 | 73 | ralimdva 2796 |
. . . . . . . . . . . . . . . 16
    
              |
75 | | gruiun 9224 |
. . . . . . . . . . . . . . . . . 18
 

    
       |
76 | 75 | 3expia 1210 |
. . . . . . . . . . . . . . . . 17
    
    
       |
77 | 63, 76 | sylan2 477 |
. . . . . . . . . . . . . . . 16
    
    
       |
78 | 74, 77 | syld 45 |
. . . . . . . . . . . . . . 15
    
              |
79 | | vex 3048 |
. . . . . . . . . . . . . . . . . 18
 |
80 | | r1lim 8243 |
. . . . . . . . . . . . . . . . . 18
              |
81 | 79, 80 | mpan 676 |
. . . . . . . . . . . . . . . . 17

    
      |
82 | 81 | eleq1d 2513 |
. . . . . . . . . . . . . . . 16

             |
83 | 82 | biimprd 227 |
. . . . . . . . . . . . . . 15

 
   
       |
84 | 78, 83 | sylan9r 664 |
. . . . . . . . . . . . . 14
  
    
    
       |
85 | 84 | exp32 610 |
. . . . . . . . . . . . 13



 
               |
86 | 85 | com34 86 |
. . . . . . . . . . . 12


 
      
         |
87 | 28, 32, 36, 38, 61, 86 | tfinds2 6690 |
. . . . . . . . . . 11
 
         |
88 | 87 | com3r 82 |
. . . . . . . . . 10
           |
89 | 23, 88 | mpd 15 |
. . . . . . . . 9
 
       |
90 | 89 | impcom 432 |
. . . . . . . 8
         |
91 | | gruelss 9219 |
. . . . . . . 8
             |
92 | 90, 91 | syldan 473 |
. . . . . . 7
         |
93 | 92 | ralrimiva 2802 |
. . . . . 6


      |
94 | | iunss 4319 |
. . . . . 6
 
           |
95 | 93, 94 | sylibr 216 |
. . . . 5


      |
96 | 95 | adantr 467 |
. . . 4
   
      |
97 | 20, 96 | eqsstrd 3466 |
. . 3
         |
98 | 97 | ex 436 |
. 2


       |
99 | 13, 98 | pm2.61dne 2710 |
1

      |