Step | Hyp | Ref
| Expression |
1 | | exfzdc.1 |
. . . . 5
   |
2 | | exfzdc.2 |
. . . . 5
   |
3 | | eluz 9540 |
. . . . 5
 
     
   |
4 | 1, 2, 3 | syl2anc 411 |
. . . 4
     
   |
5 | 4 | biimpar 297 |
. . 3
 

      |
6 | | simpl 109 |
. . 3
 

  |
7 | | eluzfz2 10031 |
. . . 4
    
      |
8 | | oveq2 5882 |
. . . . . . . 8
           |
9 | 8 | rexeqdv 2679 |
. . . . . . 7
  
              |
10 | 9 | dcbid 838 |
. . . . . 6
 DECID 
    
DECID          |
11 | 10 | imbi2d 230 |
. . . . 5
  
DECID       
 DECID           |
12 | | oveq2 5882 |
. . . . . . . 8
           |
13 | 12 | rexeqdv 2679 |
. . . . . . 7
  
              |
14 | 13 | dcbid 838 |
. . . . . 6
 DECID 
    
DECID          |
15 | 14 | imbi2d 230 |
. . . . 5
  
DECID       
 DECID           |
16 | | oveq2 5882 |
. . . . . . . 8
               |
17 | 16 | rexeqdv 2679 |
. . . . . . 7
    
                |
18 | 17 | dcbid 838 |
. . . . . 6
   DECID 
    
DECID            |
19 | 18 | imbi2d 230 |
. . . . 5
    
DECID       
 DECID             |
20 | | oveq2 5882 |
. . . . . . . 8
           |
21 | 20 | rexeqdv 2679 |
. . . . . . 7
  
              |
22 | 21 | dcbid 838 |
. . . . . 6
 DECID 
    
DECID          |
23 | 22 | imbi2d 230 |
. . . . 5
  
DECID       
 DECID           |
24 | | eluzfz1 10030 |
. . . . . . . . 9
    
      |
25 | 24 | adantl 277 |
. . . . . . . 8
 
    
      |
26 | | exfzdc.3 |
. . . . . . . . . 10
 
    
DECID   |
27 | 26 | ralrimiva 2550 |
. . . . . . . . 9
      DECID   |
28 | 27 | adantr 276 |
. . . . . . . 8
 
    
     DECID   |
29 | | nfsbc1v 2981 |
. . . . . . . . . 10
  
 ![]. ].](_drbrack.gif)  |
30 | 29 | nfdc 1659 |
. . . . . . . . 9
 DECID   ![]. ].](_drbrack.gif)  |
31 | | sbceq1a 2972 |
. . . . . . . . . 10
    ![]. ].](_drbrack.gif)    |
32 | 31 | dcbid 838 |
. . . . . . . . 9
 DECID DECID   ![]. ].](_drbrack.gif)    |
33 | 30, 32 | rspc 2835 |
. . . . . . . 8
      
    DECID DECID   ![]. ].](_drbrack.gif)    |
34 | 25, 28, 33 | sylc 62 |
. . . . . . 7
 
    
DECID   ![]. ].](_drbrack.gif)   |
35 | 1 | adantr 276 |
. . . . . . . . . . 11
 
    
  |
36 | | fzsn 10065 |
. . . . . . . . . . 11
         |
37 | 35, 36 | syl 14 |
. . . . . . . . . 10
 
    
        |
38 | 37 | rexeqdv 2679 |
. . . . . . . . 9
 
    
 
    
       |
39 | | rexsns 3631 |
. . . . . . . . 9
    
  ![]. ].](_drbrack.gif)   |
40 | 38, 39 | bitrdi 196 |
. . . . . . . 8
 
    
 
    
  ![]. ].](_drbrack.gif)    |
41 | 40 | dcbid 838 |
. . . . . . 7
 
    
DECID
     
DECID   ![]. ].](_drbrack.gif)    |
42 | 34, 41 | mpbird 167 |
. . . . . 6
 
    
DECID         |
43 | 42 | expcom 116 |
. . . . 5
    
 DECID          |
44 | | simpr 110 |
. . . . . . . . . 10
    ..^ 
DECID       
DECID         |
45 | | fzofzp1 10226 |
. . . . . . . . . . . . 13
  ..^
        |
46 | 45 | ad2antrr 488 |
. . . . . . . . . . . 12
    ..^ 
DECID                |
47 | 27 | ad2antlr 489 |
. . . . . . . . . . . 12
    ..^ 
DECID             DECID   |
48 | | nfsbc1v 2981 |
. . . . . . . . . . . . . 14
      ![]. ].](_drbrack.gif)  |
49 | 48 | nfdc 1659 |
. . . . . . . . . . . . 13
 DECID     ![]. ].](_drbrack.gif)  |
50 | | sbceq1a 2972 |
. . . . . . . . . . . . . 14
        ![]. ].](_drbrack.gif)    |
51 | 50 | dcbid 838 |
. . . . . . . . . . . . 13
   DECID DECID     ![]. ].](_drbrack.gif)    |
52 | 49, 51 | rspc 2835 |
. . . . . . . . . . . 12
        
    DECID DECID     ![]. ].](_drbrack.gif)    |
53 | 46, 47, 52 | sylc 62 |
. . . . . . . . . . 11
    ..^ 
DECID       
DECID     ![]. ].](_drbrack.gif)   |
54 | | rexsns 3631 |
. . . . . . . . . . . 12
      
    ![]. ].](_drbrack.gif)   |
55 | 54 | dcbii 840 |
. . . . . . . . . . 11
DECID       DECID     ![]. ].](_drbrack.gif)   |
56 | 53, 55 | sylibr 134 |
. . . . . . . . . 10
    ..^ 
DECID       
DECID         |
57 | | dcor 935 |
. . . . . . . . . 10
DECID       DECID 
    
DECID        
         |
58 | 44, 56, 57 | sylc 62 |
. . . . . . . . 9
    ..^ 
DECID       
DECID        
        |
59 | | rexun 3315 |
. . . . . . . . . 10
            
 
              |
60 | 59 | dcbii 840 |
. . . . . . . . 9
DECID             DECID                 |
61 | 58, 60 | sylibr 134 |
. . . . . . . 8
    ..^ 
DECID       
DECID               |
62 | | elfzouz 10150 |
. . . . . . . . . . . 12
  ..^
      |
63 | 62 | ad2antrr 488 |
. . . . . . . . . . 11
    ..^ 
DECID              |
64 | | fzsuc 10068 |
. . . . . . . . . . 11
    
                  |
65 | 63, 64 | syl 14 |
. . . . . . . . . 10
    ..^ 
DECID                          |
66 | 65 | rexeqdv 2679 |
. . . . . . . . 9
    ..^ 
DECID         
                      |
67 | 66 | dcbid 838 |
. . . . . . . 8
    ..^ 
DECID        DECID 
      
DECID                |
68 | 61, 67 | mpbird 167 |
. . . . . . 7
    ..^ 
DECID       
DECID           |
69 | 68 | exp31 364 |
. . . . . 6
  ..^
 DECID      
DECID             |
70 | 69 | a2d 26 |
. . . . 5
  ..^
  DECID 
     
 DECID             |
71 | 11, 15, 19, 23, 43, 70 | fzind2 10238 |
. . . 4
      DECID 
        |
72 | 7, 71 | syl 14 |
. . 3
    
 DECID          |
73 | 5, 6, 72 | sylc 62 |
. 2
 

DECID         |
74 | | rex0 3440 |
. . . . 5

 |
75 | | zltnle 9298 |
. . . . . . . . 9
 
 
   |
76 | 2, 1, 75 | syl2anc 411 |
. . . . . . . 8
 
   |
77 | 76 | biimpar 297 |
. . . . . . 7
 
   |
78 | | fzn 10041 |
. . . . . . . . 9
 
         |
79 | 1, 2, 78 | syl2anc 411 |
. . . . . . . 8
         |
80 | 79 | adantr 276 |
. . . . . . 7
 
 
       |
81 | 77, 80 | mpbid 147 |
. . . . . 6
 
       |
82 | 81 | rexeqdv 2679 |
. . . . 5
 
  
         |
83 | 74, 82 | mtbiri 675 |
. . . 4
 
         |
84 | 83 | olcd 734 |
. . 3
 
  
              |
85 | | df-dc 835 |
. . 3
DECID      
 
              |
86 | 84, 85 | sylibr 134 |
. 2
 

DECID         |
87 | | zdcle 9328 |
. . . 4
 
 DECID   |
88 | | exmiddc 836 |
. . . 4
DECID 
   |
89 | 87, 88 | syl 14 |
. . 3
 
     |
90 | 1, 2, 89 | syl2anc 411 |
. 2
     |
91 | 73, 86, 90 | mpjaodan 798 |
1
 DECID         |