Step | Hyp | Ref
| Expression |
1 | | 2sqlem4.3 |
. . . . . . . 8
   |
2 | | 2sqlem4.4 |
. . . . . . . 8
   |
3 | | gzreim 12360 |
. . . . . . . 8
 
        ![] ]](rbrack.gif)  |
4 | 1, 2, 3 | syl2anc 411 |
. . . . . . 7
        ![] ]](rbrack.gif)  |
5 | | 2sqlem4.5 |
. . . . . . . 8
   |
6 | | 2sqlem4.6 |
. . . . . . . 8
   |
7 | | gzreim 12360 |
. . . . . . . 8
 
        ![] ]](rbrack.gif)  |
8 | 5, 6, 7 | syl2anc 411 |
. . . . . . 7
        ![] ]](rbrack.gif)  |
9 | | gzmulcl 12359 |
. . . . . . 7
        

      ![] ]](rbrack.gif)
 
           ![] ]](rbrack.gif)  |
10 | 4, 8, 9 | syl2anc 411 |
. . . . . 6
   
  
       ![] ]](rbrack.gif)  |
11 | | gzcn 12353 |
. . . . . 6
             
 
          |
12 | 10, 11 | syl 14 |
. . . . 5
   
  
      |
13 | | 2sqlem5.2 |
. . . . . . 7
   |
14 | | prmnn 12093 |
. . . . . . 7

  |
15 | 13, 14 | syl 14 |
. . . . . 6
   |
16 | 15 | nncnd 8922 |
. . . . 5
   |
17 | 15 | nnap0d 8954 |
. . . . 5
 #   |
18 | 12, 16, 17 | divclapd 8736 |
. . . 4
               |
19 | 15 | nnred 8921 |
. . . . . 6
   |
20 | 19, 12, 17 | redivapd 10967 |
. . . . 5
       
  
                        |
21 | | prmz 12094 |
. . . . . . . . . . . 12

  |
22 | 13, 21 | syl 14 |
. . . . . . . . . . 11
   |
23 | | zsqcl 10576 |
. . . . . . . . . . . 12
       |
24 | 22, 23 | syl 14 |
. . . . . . . . . . 11
       |
25 | | 2sqlem5.1 |
. . . . . . . . . . . . 13
   |
26 | 25 | nnzd 9363 |
. . . . . . . . . . . 12
   |
27 | 26, 24 | zmulcld 9370 |
. . . . . . . . . . 11
         |
28 | | dvdsmul2 11805 |
. . . . . . . . . . . . 13
 
     |
29 | 22, 22, 28 | syl2anc 411 |
. . . . . . . . . . . 12
     |
30 | 16 | sqvald 10636 |
. . . . . . . . . . . 12
         |
31 | 29, 30 | breqtrrd 4028 |
. . . . . . . . . . 11
       |
32 | | dvdsmul2 11805 |
. . . . . . . . . . . 12
                   |
33 | 26, 24, 32 | syl2anc 411 |
. . . . . . . . . . 11
             |
34 | 22, 24, 27, 31, 33 | dvdstrd 11821 |
. . . . . . . . . 10
         |
35 | | gzcn 12353 |
. . . . . . . . . . . . . . . 16
       
      |
36 | 4, 35 | syl 14 |
. . . . . . . . . . . . . . 15
       |
37 | 36 | abscld 11174 |
. . . . . . . . . . . . . 14
    
      |
38 | 37 | recnd 7976 |
. . . . . . . . . . . . 13
    
      |
39 | | gzcn 12353 |
. . . . . . . . . . . . . . . 16
       
      |
40 | 8, 39 | syl 14 |
. . . . . . . . . . . . . . 15
       |
41 | 40 | abscld 11174 |
. . . . . . . . . . . . . 14
    
      |
42 | 41 | recnd 7976 |
. . . . . . . . . . . . 13
    
      |
43 | 38, 42 | sqmuld 10651 |
. . . . . . . . . . . 12
               
                                   |
44 | 1 | zred 9364 |
. . . . . . . . . . . . . . . . 17
   |
45 | 2 | zred 9364 |
. . . . . . . . . . . . . . . . 17
   |
46 | 44, 45 | crred 10969 |
. . . . . . . . . . . . . . . 16
    
      |
47 | 46 | oveq1d 5884 |
. . . . . . . . . . . . . . 15
     

            |
48 | 44, 45 | crimd 10970 |
. . . . . . . . . . . . . . . 16
    
      |
49 | 48 | oveq1d 5884 |
. . . . . . . . . . . . . . 15
     

            |
50 | 47, 49 | oveq12d 5887 |
. . . . . . . . . . . . . 14
       
          
                    |
51 | 36 | absvalsq2d 11176 |
. . . . . . . . . . . . . 14
     
             
          
          |
52 | | 2sqlem4.7 |
. . . . . . . . . . . . . 14
               |
53 | 50, 51, 52 | 3eqtr4d 2220 |
. . . . . . . . . . . . 13
     
           |
54 | 5 | zred 9364 |
. . . . . . . . . . . . . . . . 17
   |
55 | 6 | zred 9364 |
. . . . . . . . . . . . . . . . 17
   |
56 | 54, 55 | crred 10969 |
. . . . . . . . . . . . . . . 16
    
      |
57 | 56 | oveq1d 5884 |
. . . . . . . . . . . . . . 15
     

            |
58 | 54, 55 | crimd 10970 |
. . . . . . . . . . . . . . . 16
    
      |
59 | 58 | oveq1d 5884 |
. . . . . . . . . . . . . . 15
     

            |
60 | 57, 59 | oveq12d 5887 |
. . . . . . . . . . . . . 14
       
          
                    |
61 | 40 | absvalsq2d 11176 |
. . . . . . . . . . . . . 14
     
             
          
          |
62 | | 2sqlem4.8 |
. . . . . . . . . . . . . 14
             |
63 | 60, 61, 62 | 3eqtr4d 2220 |
. . . . . . . . . . . . 13
     
         |
64 | 53, 63 | oveq12d 5887 |
. . . . . . . . . . . 12
                                 |
65 | 25 | nncnd 8922 |
. . . . . . . . . . . . 13
   |
66 | 65, 16, 16 | mulassd 7971 |
. . . . . . . . . . . 12
           |
67 | 43, 64, 66 | 3eqtrd 2214 |
. . . . . . . . . . 11
               
        
    |
68 | 36, 40 | absmuld 11187 |
. . . . . . . . . . . 12
                           
       |
69 | 68 | oveq1d 5884 |
. . . . . . . . . . 11
                                
          |
70 | 30 | oveq2d 5885 |
. . . . . . . . . . 11
        
    |
71 | 67, 69, 70 | 3eqtr4d 2220 |
. . . . . . . . . 10
                           |
72 | 34, 71 | breqtrrd 4028 |
. . . . . . . . 9
           
         |
73 | 12 | absvalsq2d 11176 |
. . . . . . . . . 10
                              
             
  
           |
74 | | elgz 12352 |
. . . . . . . . . . . . . . 15
                     
                                  |
75 | 74 | simp2bi 1013 |
. . . . . . . . . . . . . 14
             
     
  
       |
76 | 10, 75 | syl 14 |
. . . . . . . . . . . . 13
                 |
77 | | zsqcl 10576 |
. . . . . . . . . . . . 13
          
                        |
78 | 76, 77 | syl 14 |
. . . . . . . . . . . 12
       
  
          |
79 | 78 | zcnd 9365 |
. . . . . . . . . . 11
       
  
          |
80 | 74 | simp3bi 1014 |
. . . . . . . . . . . . . 14
             
     
  
       |
81 | 10, 80 | syl 14 |
. . . . . . . . . . . . 13
                 |
82 | | zsqcl 10576 |
. . . . . . . . . . . . 13
          
                        |
83 | 81, 82 | syl 14 |
. . . . . . . . . . . 12
       
  
          |
84 | 83 | zcnd 9365 |
. . . . . . . . . . 11
       
  
          |
85 | 79, 84 | addcomd 8098 |
. . . . . . . . . 10
                                                                               |
86 | 73, 85 | eqtrd 2210 |
. . . . . . . . 9
                              
             
  
           |
87 | 72, 86 | breqtrd 4026 |
. . . . . . . 8
                                         |
88 | | 2sqlem4.9 |
. . . . . . . . . . . 12
         |
89 | 5 | zcnd 9365 |
. . . . . . . . . . . . . . 15
   |
90 | 2 | zcnd 9365 |
. . . . . . . . . . . . . . 15
   |
91 | 89, 90 | mulcld 7968 |
. . . . . . . . . . . . . 14
     |
92 | 1 | zcnd 9365 |
. . . . . . . . . . . . . . 15
   |
93 | 6 | zcnd 9365 |
. . . . . . . . . . . . . . 15
   |
94 | 92, 93 | mulcld 7968 |
. . . . . . . . . . . . . 14
     |
95 | 91, 94 | addcomd 8098 |
. . . . . . . . . . . . 13
               |
96 | 89, 90 | mulcomd 7969 |
. . . . . . . . . . . . . 14
       |
97 | 96 | oveq2d 5885 |
. . . . . . . . . . . . 13
               |
98 | 95, 97 | eqtrd 2210 |
. . . . . . . . . . . 12
               |
99 | 88, 98 | breqtrd 4026 |
. . . . . . . . . . 11
         |
100 | 36, 40 | immuld 10957 |
. . . . . . . . . . . 12
                    
       

        

               |
101 | 46, 58 | oveq12d 5887 |
. . . . . . . . . . . . 13
     

                |
102 | 48, 56 | oveq12d 5887 |
. . . . . . . . . . . . 13
     

                |
103 | 101, 102 | oveq12d 5887 |
. . . . . . . . . . . 12
       
      
                 

             |
104 | 100, 103 | eqtrd 2210 |
. . . . . . . . . . 11
                       |
105 | 99, 104 | breqtrrd 4028 |
. . . . . . . . . 10
                 |
106 | | 2nn 9069 |
. . . . . . . . . . . 12
 |
107 | 106 | a1i 9 |
. . . . . . . . . . 11
   |
108 | | prmdvdsexp 12131 |
. . . . . . . . . . 11
      
                            
    
            |
109 | 13, 81, 107, 108 | syl3anc 1238 |
. . . . . . . . . 10
                   
     
  
        |
110 | 105, 109 | mpbird 167 |
. . . . . . . . 9
           
         |
111 | | dvdsadd2b 11831 |
. . . . . . . . 9
        
  
               
  
              
  
                            
       
  
                              |
112 | 22, 78, 83, 110, 111 | syl112anc 1242 |
. . . . . . . 8
                   
                                         |
113 | 87, 112 | mpbird 167 |
. . . . . . 7
           
         |
114 | | prmdvdsexp 12131 |
. . . . . . . 8
      
                            
    
            |
115 | 13, 76, 107, 114 | syl3anc 1238 |
. . . . . . 7
                   
     
  
        |
116 | 113, 115 | mpbid 147 |
. . . . . 6
                 |
117 | 15 | nnne0d 8953 |
. . . . . . 7
   |
118 | | dvdsval2 11781 |
. . . . . . 7
      
                
  
                        |
119 | 22, 117, 76, 118 | syl3anc 1238 |
. . . . . 6
      
        
     
             |
120 | 116, 119 | mpbid 147 |
. . . . 5
       
  
        |
121 | 20, 120 | eqeltrd 2254 |
. . . 4
       
  
        |
122 | 19, 12, 17 | imdivapd 10968 |
. . . . 5
       
  
                        |
123 | | dvdsval2 11781 |
. . . . . . 7
      
                
  
                        |
124 | 22, 117, 81, 123 | syl3anc 1238 |
. . . . . 6
      
        
     
             |
125 | 105, 124 | mpbid 147 |
. . . . 5
       
  
        |
126 | 122, 125 | eqeltrd 2254 |
. . . 4
       
  
        |
127 | | elgz 12352 |
. . . 4
    
  
                                                        |
128 | 18, 121, 126, 127 | syl3anbrc 1181 |
. . 3
                ![] ]](rbrack.gif)  |
129 | 12, 16, 17 | absdivapd 11188 |
. . . . . 6
       
  
            
  
            |
130 | 15 | nnnn0d 9218 |
. . . . . . . . 9
   |
131 | 130 | nn0ge0d 9221 |
. . . . . . . 8

  |
132 | 19, 131 | absidd 11160 |
. . . . . . 7
       |
133 | 132 | oveq2d 5885 |
. . . . . 6
                                       |
134 | 129, 133 | eqtrd 2210 |
. . . . 5
       
  
            
  
        |
135 | 134 | oveq1d 5884 |
. . . 4
        
  
                
  
           |
136 | 12 | abscld 11174 |
. . . . . 6
                 |
137 | 136 | recnd 7976 |
. . . . 5
                 |
138 | 137, 16, 17 | sqdivapd 10652 |
. . . 4
        
  
                
  
               |
139 | 71 | oveq1d 5884 |
. . . . 5
        
  
                           |
140 | 15 | nnsqcld 10660 |
. . . . . . 7
       |
141 | 140 | nncnd 8922 |
. . . . . 6
       |
142 | 140 | nnap0d 8954 |
. . . . . 6
     #   |
143 | 65, 141, 142 | divcanap4d 8742 |
. . . . 5
               |
144 | 139, 143 | eqtrd 2210 |
. . . 4
        
  
               |
145 | 135, 138,
144 | 3eqtrrd 2215 |
. . 3
                       |
146 | | fveq2 5511 |
. . . . 5
        
              
  
        |
147 | 146 | oveq1d 5884 |
. . . 4
        
                                  |
148 | 147 | rspceeqv 2859 |
. . 3
                
       
  
                        |
149 | 128, 145,
148 | syl2anc 411 |
. 2
               |
150 | | 2sq.1 |
. . 3
              |
151 | 150 | 2sqlem1 14117 |
. 2

   
          |
152 | 149, 151 | sylibr 134 |
1
   |