Step | Hyp | Ref
| Expression |
1 | | 0exp 10538 |
. . . . . 6
       |
2 | 1 | oveq1d 5884 |
. . . . 5
     
     |
3 | 2 | eqeq1d 2186 |
. . . 4
        
    |
4 | | oveq1 5876 |
. . . . . . 7
           |
5 | | oveq12 5878 |
. . . . . . 7
         
           
   |
6 | 4, 5 | sylan 283 |
. . . . . 6
             
   |
7 | 6 | eqeq1d 2186 |
. . . . 5
                   |
8 | | oveq12 5878 |
. . . . . 6
         |
9 | 8 | eqeq1d 2186 |
. . . . 5
           |
10 | 7, 9 | bibi12d 235 |
. . . 4
         

                |
11 | 3, 10 | syl5ibrcom 157 |
. . 3
   
     

      |
12 | 11 | 3ad2ant3 1020 |
. 2
 
   
     

      |
13 | | exprmfct 12118 |
. . . . . . 7
     
              |
14 | | simpl1 1000 |
. . . . . . . . . . . . . . . . 17
  
   
  |
15 | | simpl3 1002 |
. . . . . . . . . . . . . . . . . 18
  
   
  |
16 | 15 | nnnn0d 9215 |
. . . . . . . . . . . . . . . . 17
  
   
  |
17 | | zexpcl 10518 |
. . . . . . . . . . . . . . . . 17
 
       |
18 | 14, 16, 17 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
  
          |
19 | 18 | adantr 276 |
. . . . . . . . . . . . . . 15
     
         |
20 | | simpl2 1001 |
. . . . . . . . . . . . . . . 16
  
   
  |
21 | 20 | adantr 276 |
. . . . . . . . . . . . . . 15
     
     |
22 | | gcddvds 11944 |
. . . . . . . . . . . . . . 15
     
                 
   |
23 | 19, 21, 22 | syl2anc 411 |
. . . . . . . . . . . . . 14
     
         
        
    |
24 | 23 | simpld 112 |
. . . . . . . . . . . . 13
     
       
       |
25 | | prmz 12091 |
. . . . . . . . . . . . . . 15

  |
26 | 25 | adantl 277 |
. . . . . . . . . . . . . 14
     
     |
27 | | simpr 110 |
. . . . . . . . . . . . . . . . . 18
  
        |
28 | 14 | zcnd 9362 |
. . . . . . . . . . . . . . . . . . . 20
  
   
  |
29 | | expeq0 10534 |
. . . . . . . . . . . . . . . . . . . 20
 
         |
30 | 28, 15, 29 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
  
            |
31 | 30 | anbi1d 465 |
. . . . . . . . . . . . . . . . . 18
  
          
     |
32 | 27, 31 | mtbird 673 |
. . . . . . . . . . . . . . . . 17
  
            |
33 | | gcdn0cl 11943 |
. . . . . . . . . . . . . . . . 17
                       |
34 | 18, 20, 32, 33 | syl21anc 1237 |
. . . . . . . . . . . . . . . 16
  
            |
35 | 34 | nnzd 9360 |
. . . . . . . . . . . . . . 15
  
            |
36 | 35 | adantr 276 |
. . . . . . . . . . . . . 14
     
       
   |
37 | | dvdstr 11816 |
. . . . . . . . . . . . . 14
                    
                  |
38 | 26, 36, 19, 37 | syl3anc 1238 |
. . . . . . . . . . . . 13
     
         
      
            |
39 | 24, 38 | mpan2d 428 |
. . . . . . . . . . . 12
     
   
             |
40 | | simpr 110 |
. . . . . . . . . . . . 13
     
     |
41 | | simpll1 1036 |
. . . . . . . . . . . . 13
     
     |
42 | 15 | adantr 276 |
. . . . . . . . . . . . 13
     
     |
43 | | prmdvdsexp 12128 |
. . . . . . . . . . . . 13
   
   
   |
44 | 40, 41, 42, 43 | syl3anc 1238 |
. . . . . . . . . . . 12
     
   
   
   |
45 | 39, 44 | sylibd 149 |
. . . . . . . . . . 11
     
   
         |
46 | 23 | simprd 114 |
. . . . . . . . . . . 12
     
       
   |
47 | | dvdstr 11816 |
. . . . . . . . . . . . 13
       
        
      
   |
48 | 26, 36, 21, 47 | syl3anc 1238 |
. . . . . . . . . . . 12
     
         
      
    |
49 | 46, 48 | mpan2d 428 |
. . . . . . . . . . 11
     
   
         |
50 | 45, 49 | jcad 307 |
. . . . . . . . . 10
     
   
      
    |
51 | | dvdsgcd 11993 |
. . . . . . . . . . 11
 
  
      |
52 | 26, 41, 21, 51 | syl3anc 1238 |
. . . . . . . . . 10
     
    
      |
53 | | nprmdvds1 12120 |
. . . . . . . . . . . . 13

  |
54 | | breq2 4004 |
. . . . . . . . . . . . . 14
   
 
   |
55 | 54 | notbid 667 |
. . . . . . . . . . . . 13
   
 
   |
56 | 53, 55 | syl5ibrcom 157 |
. . . . . . . . . . . 12

        |
57 | 56 | necon2ad 2404 |
. . . . . . . . . . 11

  
     |
58 | 57 | adantl 277 |
. . . . . . . . . 10
     
   
       |
59 | 50, 52, 58 | 3syld 57 |
. . . . . . . . 9
     
   
           |
60 | 59 | rexlimdva 2594 |
. . . . . . . 8
  
     
           |
61 | | gcdn0cl 11943 |
. . . . . . . . . 10
           |
62 | 61 | 3adantl3 1155 |
. . . . . . . . 9
  
        |
63 | | eluz2b3 9590 |
. . . . . . . . . 10
               |
64 | 63 | baib 919 |
. . . . . . . . 9
         
     |
65 | 62, 64 | syl 14 |
. . . . . . . 8
  
          
     |
66 | 60, 65 | sylibrd 169 |
. . . . . . 7
  
     
               |
67 | 13, 66 | syl5 32 |
. . . . . 6
  
                        |
68 | | exprmfct 12118 |
. . . . . . 7
      
     |
69 | | gcddvds 11944 |
. . . . . . . . . . . . . . 15
 
    
    |
70 | 41, 21, 69 | syl2anc 411 |
. . . . . . . . . . . . . 14
     
     

    |
71 | 70 | simpld 112 |
. . . . . . . . . . . . 13
     
       |
72 | | iddvdsexp 11803 |
. . . . . . . . . . . . . 14
 
       |
73 | 41, 42, 72 | syl2anc 411 |
. . . . . . . . . . . . 13
     
         |
74 | 62 | nnzd 9360 |
. . . . . . . . . . . . . . 15
  
        |
75 | 74 | adantr 276 |
. . . . . . . . . . . . . 14
     
       |
76 | | dvdstr 11816 |
. . . . . . . . . . . . . 14
   
               
       |
77 | 75, 41, 19, 76 | syl3anc 1238 |
. . . . . . . . . . . . 13
     
             
       |
78 | 71, 73, 77 | mp2and 433 |
. . . . . . . . . . . 12
     
           |
79 | | dvdstr 11816 |
. . . . . . . . . . . . 13
  
          
             |
80 | 26, 75, 19, 79 | syl3anc 1238 |
. . . . . . . . . . . 12
     
       
             |
81 | 78, 80 | mpan2d 428 |
. . . . . . . . . . 11
     
   
         |
82 | 70 | simprd 114 |
. . . . . . . . . . . 12
     
       |
83 | | dvdstr 11816 |
. . . . . . . . . . . . 13
  
      
     |
84 | 26, 75, 21, 83 | syl3anc 1238 |
. . . . . . . . . . . 12
     
       
     |
85 | 82, 84 | mpan2d 428 |
. . . . . . . . . . 11
     
   
     |
86 | 81, 85 | jcad 307 |
. . . . . . . . . 10
     
   
  
        |
87 | | dvdsgcd 11993 |
. . . . . . . . . . 11
                       |
88 | 26, 19, 21, 87 | syl3anc 1238 |
. . . . . . . . . 10
     
                   |
89 | | breq2 4004 |
. . . . . . . . . . . . . 14
     
 
     
   |
90 | 89 | notbid 667 |
. . . . . . . . . . . . 13
     
 
     
   |
91 | 53, 90 | syl5ibrcom 157 |
. . . . . . . . . . . 12

     
          |
92 | 91 | necon2ad 2404 |
. . . . . . . . . . 11

           
    |
93 | 92 | adantl 277 |
. . . . . . . . . 10
     
   
          
    |
94 | 86, 88, 93 | 3syld 57 |
. . . . . . . . 9
     
   
      
    |
95 | 94 | rexlimdva 2594 |
. . . . . . . 8
  
     
           |
96 | | eluz2b3 9590 |
. . . . . . . . . 10
     
                     |
97 | 96 | baib 919 |
. . . . . . . . 9
     

     
         
    |
98 | 34, 97 | syl 14 |
. . . . . . . 8
  
              
         |
99 | 95, 98 | sylibrd 169 |
. . . . . . 7
  
     
               |
100 | 68, 99 | syl5 32 |
. . . . . 6
  
               
        |
101 | 67, 100 | impbid 129 |
. . . . 5
  
              
         |
102 | 101, 98, 65 | 3bitr3d 218 |
. . . 4
  
                |
103 | | simp1 997 |
. . . . . . . . . 10
 
   |
104 | | simp3 999 |
. . . . . . . . . . 11
 
   |
105 | 104 | nnnn0d 9215 |
. . . . . . . . . 10
 
   |
106 | 103, 105,
17 | syl2anc 411 |
. . . . . . . . 9
 
       |
107 | | simp2 998 |
. . . . . . . . 9
 
   |
108 | 106, 107 | gcdcld 11949 |
. . . . . . . 8
 
     
   |
109 | 108 | nn0zd 9359 |
. . . . . . 7
 
     
   |
110 | | 1zzd 9266 |
. . . . . . 7
 
   |
111 | | zdceq 9314 |
. . . . . . 7
       
 DECID     
   |
112 | 109, 110,
111 | syl2anc 411 |
. . . . . 6
 

DECID         |
113 | 103, 107 | gcdcld 11949 |
. . . . . . . 8
 
     |
114 | 113 | nn0zd 9359 |
. . . . . . 7
 
     |
115 | | zdceq 9314 |
. . . . . . 7
   
 DECID     |
116 | 114, 110,
115 | syl2anc 411 |
. . . . . 6
 

DECID     |
117 | | nebidc 2427 |
. . . . . 6
DECID      
DECID
        

                 |
118 | 112, 116,
117 | sylc 62 |
. . . . 5
 
                         |
119 | 118 | adantr 276 |
. . . 4
  
                            |
120 | 102, 119 | mpbird 167 |
. . 3
  
                |
121 | 120 | ex 115 |
. 2
 
   
     

      |
122 | | gcdmndc 11925 |
. . . 4
 
 DECID     |
123 | | exmiddc 836 |
. . . 4
DECID      
    |
124 | 122, 123 | syl 14 |
. . 3
 
    
    |
125 | 124 | 3adant3 1017 |
. 2
 
    
    |
126 | 12, 121, 125 | mpjaod 718 |
1
 
             |