Step | Hyp | Ref
| Expression |
1 | | oveq2 5876 |
. . . . . . . 8
           |
2 | 1 | oveq1d 5883 |
. . . . . . 7
     
         |
3 | 2 | eqeq1d 2186 |
. . . . . 6
                 |
4 | 3 | imbi2d 230 |
. . . . 5
             
 
                 |
5 | | oveq2 5876 |
. . . . . . . 8
           |
6 | 5 | oveq1d 5883 |
. . . . . . 7
     
         |
7 | 6 | eqeq1d 2186 |
. . . . . 6
            
    |
8 | 7 | imbi2d 230 |
. . . . 5
             
 
                 |
9 | | oveq2 5876 |
. . . . . . . 8
               |
10 | 9 | oveq1d 5883 |
. . . . . . 7
       
           |
11 | 10 | eqeq1d 2186 |
. . . . . 6
                     |
12 | 11 | imbi2d 230 |
. . . . 5
               
 
                   |
13 | | oveq2 5876 |
. . . . . . . 8
           |
14 | 13 | oveq1d 5883 |
. . . . . . 7
     
         |
15 | 14 | eqeq1d 2186 |
. . . . . 6
            
    |
16 | 15 | imbi2d 230 |
. . . . 5
             
 
                 |
17 | | nncn 8903 |
. . . . . . . . . 10
   |
18 | 17 | exp1d 10621 |
. . . . . . . . 9
       |
19 | 18 | oveq1d 5883 |
. . . . . . . 8
           |
20 | 19 | adantr 276 |
. . . . . . 7
 
           |
21 | 20 | eqeq1d 2186 |
. . . . . 6
 
             |
22 | 21 | biimpar 297 |
. . . . 5
               |
23 | | df-3an 980 |
. . . . . . . . 9
 

 
    |
24 | | simpl1 1000 |
. . . . . . . . . . . . . . . . 17
  
      |
25 | 24 | nncnd 8909 |
. . . . . . . . . . . . . . . 16
  
      |
26 | | simpl3 1002 |
. . . . . . . . . . . . . . . . 17
  
      |
27 | 26 | nnnn0d 9205 |
. . . . . . . . . . . . . . . 16
  
      |
28 | 25, 27 | expp1d 10627 |
. . . . . . . . . . . . . . 15
  
                  |
29 | | simp1 997 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
30 | | nnnn0 9159 |
. . . . . . . . . . . . . . . . . . . . 21
   |
31 | 30 | 3ad2ant3 1020 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
32 | 29, 31 | nnexpcld 10648 |
. . . . . . . . . . . . . . . . . . 19
 
       |
33 | 32 | nnzd 9350 |
. . . . . . . . . . . . . . . . . 18
 
       |
34 | 33 | adantr 276 |
. . . . . . . . . . . . . . . . 17
  
          |
35 | 34 | zcnd 9352 |
. . . . . . . . . . . . . . . 16
  
          |
36 | 35, 25 | mulcomd 7956 |
. . . . . . . . . . . . . . 15
  
                  |
37 | 28, 36 | eqtrd 2210 |
. . . . . . . . . . . . . 14
  
                  |
38 | 37 | oveq2d 5884 |
. . . . . . . . . . . . 13
  
                      |
39 | | simpl2 1001 |
. . . . . . . . . . . . . 14
  
      |
40 | 32 | adantr 276 |
. . . . . . . . . . . . . 14
  
          |
41 | | nnz 9248 |
. . . . . . . . . . . . . . . . . 18
   |
42 | 41 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . 17
 
   |
43 | | nnz 9248 |
. . . . . . . . . . . . . . . . . 18
   |
44 | 43 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . . . 17
 
   |
45 | | gcdcom 11944 |
. . . . . . . . . . . . . . . . 17
 
       |
46 | 42, 44, 45 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
 
       |
47 | 46 | eqeq1d 2186 |
. . . . . . . . . . . . . . 15
 
         |
48 | 47 | biimpa 296 |
. . . . . . . . . . . . . 14
  
        |
49 | | rpmulgcd 11997 |
. . . . . . . . . . . . . 14
        
   
              |
50 | 39, 24, 40, 48, 49 | syl31anc 1241 |
. . . . . . . . . . . . 13
  
     
              |
51 | 38, 50 | eqtrd 2210 |
. . . . . . . . . . . 12
  
                    |
52 | | peano2nn 8907 |
. . . . . . . . . . . . . . . . . 18
     |
53 | 52 | 3ad2ant3 1020 |
. . . . . . . . . . . . . . . . 17
 
     |
54 | 53 | adantr 276 |
. . . . . . . . . . . . . . . 16
  
        |
55 | 54 | nnnn0d 9205 |
. . . . . . . . . . . . . . 15
  
        |
56 | 24, 55 | nnexpcld 10648 |
. . . . . . . . . . . . . 14
  
            |
57 | 56 | nnzd 9350 |
. . . . . . . . . . . . 13
  
            |
58 | 44 | adantr 276 |
. . . . . . . . . . . . 13
  
      |
59 | | gcdcom 11944 |
. . . . . . . . . . . . 13
       
                   |
60 | 57, 58, 59 | syl2anc 411 |
. . . . . . . . . . . 12
  
                      |
61 | | gcdcom 11944 |
. . . . . . . . . . . . 13
     
               |
62 | 34, 58, 61 | syl2anc 411 |
. . . . . . . . . . . 12
  
                  |
63 | 51, 60, 62 | 3eqtr4d 2220 |
. . . . . . . . . . 11
  
                
   |
64 | 63 | eqeq1d 2186 |
. . . . . . . . . 10
  
                      |
65 | 64 | biimprd 158 |
. . . . . . . . 9
  
          
           |
66 | 23, 65 | sylanbr 285 |
. . . . . . . 8
                           |
67 | 66 | an32s 568 |
. . . . . . 7
                           |
68 | 67 | expcom 116 |
. . . . . 6
                           |
69 | 68 | a2d 26 |
. . . . 5
             
                     |
70 | 4, 8, 12, 16, 22, 69 | nnind 8911 |
. . . 4
            
    |
71 | 70 | expd 258 |
. . 3
      
          |
72 | 71 | com12 30 |
. 2
 
               |
73 | 72 | 3impia 1200 |
1
 
             |