Proof of Theorem fzind
Step | Hyp | Ref
| Expression |
1 | | breq1 4003 |
. . . . . . . . . . 11
 
   |
2 | 1 | anbi2d 464 |
. . . . . . . . . 10
  
      |
3 | | fzind.1 |
. . . . . . . . . 10
     |
4 | 2, 3 | imbi12d 234 |
. . . . . . . . 9
       
     |
5 | | breq1 4003 |
. . . . . . . . . . 11
 
   |
6 | 5 | anbi2d 464 |
. . . . . . . . . 10
  
      |
7 | | fzind.2 |
. . . . . . . . . 10
     |
8 | 6, 7 | imbi12d 234 |
. . . . . . . . 9
       
     |
9 | | breq1 4003 |
. . . . . . . . . . 11
   
     |
10 | 9 | anbi2d 464 |
. . . . . . . . . 10
    
   
    |
11 | | fzind.3 |
. . . . . . . . . 10
       |
12 | 10, 11 | imbi12d 234 |
. . . . . . . . 9
           
     |
13 | | breq1 4003 |
. . . . . . . . . . 11
 
   |
14 | 13 | anbi2d 464 |
. . . . . . . . . 10
  
      |
15 | | fzind.4 |
. . . . . . . . . 10
     |
16 | 14, 15 | imbi12d 234 |
. . . . . . . . 9
       
     |
17 | | fzind.5 |
. . . . . . . . . 10
 
   |
18 | 17 | 3expib 1206 |
. . . . . . . . 9
  
    |
19 | | zre 9246 |
. . . . . . . . . . . . . 14
   |
20 | | zre 9246 |
. . . . . . . . . . . . . 14
   |
21 | | p1le 8795 |
. . . . . . . . . . . . . . 15
 
  
  |
22 | 21 | 3expia 1205 |
. . . . . . . . . . . . . 14
 
   
   |
23 | 19, 20, 22 | syl2an 289 |
. . . . . . . . . . . . 13
 
   
   |
24 | 23 | imdistanda 448 |
. . . . . . . . . . . 12
    
 
    |
25 | 24 | imim1d 75 |
. . . . . . . . . . 11
               |
26 | 25 | 3ad2ant2 1019 |
. . . . . . . . . 10
 
               |
27 | | zltp1le 9296 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
28 | 27 | adantlr 477 |
. . . . . . . . . . . . . . . . . . . . 21
  

       |
29 | 28 | expcom 116 |
. . . . . . . . . . . . . . . . . . . 20
  
        |
30 | 29 | pm5.32d 450 |
. . . . . . . . . . . . . . . . . . 19
     
    
    |
31 | 30 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
 
     
    
    |
32 | | fzind.6 |
. . . . . . . . . . . . . . . . . . . . 21
    
      |
33 | 32 | expcom 116 |
. . . . . . . . . . . . . . . . . . . 20
           |
34 | 33 | 3expa 1203 |
. . . . . . . . . . . . . . . . . . 19
  

         |
35 | 34 | com12 30 |
. . . . . . . . . . . . . . . . . 18
 
           |
36 | 31, 35 | sylbird 170 |
. . . . . . . . . . . . . . . . 17
 
             |
37 | 36 | ex 115 |
. . . . . . . . . . . . . . . 16
 
             |
38 | 37 | com23 78 |
. . . . . . . . . . . . . . 15
               |
39 | 38 | expd 258 |
. . . . . . . . . . . . . 14
  
            |
40 | 39 | 3impib 1201 |
. . . . . . . . . . . . 13
 
   
 
     |
41 | 40 | com23 78 |
. . . . . . . . . . . 12
 
 
  

     |
42 | 41 | impd 254 |
. . . . . . . . . . 11
 
    
      |
43 | 42 | a2d 26 |
. . . . . . . . . 10
 
                 |
44 | 26, 43 | syld 45 |
. . . . . . . . 9
 
               |
45 | 4, 8, 12, 16, 18, 44 | uzind 9353 |
. . . . . . . 8
 
  
    |
46 | 45 | expcomd 1441 |
. . . . . . 7
 
  
    |
47 | 46 | 3expb 1204 |
. . . . . 6
  
 


    |
48 | 47 | expcom 116 |
. . . . 5
           |
49 | 48 | com23 78 |
. . . 4
           |
50 | 49 | 3impia 1200 |
. . 3
   
     |
51 | 50 | impd 254 |
. 2
         |
52 | 51 | impcom 125 |
1
         |