Step | Hyp | Ref
| Expression |
1 | | 2sqlem6.1 |
. 2
   |
2 | | 2sqlem6.2 |
. . 3
   |
3 | | 2sqlem6.3 |
. . 3
  
   |
4 | | breq2 4004 |
. . . . . . 7
 
   |
5 | 4 | imbi1d 231 |
. . . . . 6
         |
6 | 5 | ralbidv 2477 |
. . . . 5
  

  
    |
7 | | oveq2 5877 |
. . . . . . . 8
       |
8 | 7 | eleq1d 2246 |
. . . . . . 7
   
     |
9 | 8 | imbi1d 231 |
. . . . . 6
             |
10 | 9 | ralbidv 2477 |
. . . . 5
  
    
       |
11 | 6, 10 | imbi12d 234 |
. . . 4
               
   
     |
12 | | breq2 4004 |
. . . . . . 7
 
   |
13 | 12 | imbi1d 231 |
. . . . . 6
         |
14 | 13 | ralbidv 2477 |
. . . . 5
  

  
    |
15 | | oveq2 5877 |
. . . . . . . 8
       |
16 | 15 | eleq1d 2246 |
. . . . . . 7
   
     |
17 | 16 | imbi1d 231 |
. . . . . 6
             |
18 | 17 | ralbidv 2477 |
. . . . 5
  
    
       |
19 | 14, 18 | imbi12d 234 |
. . . 4
               
   
     |
20 | | breq2 4004 |
. . . . . . 7
 
   |
21 | 20 | imbi1d 231 |
. . . . . 6
         |
22 | 21 | ralbidv 2477 |
. . . . 5
  

  
    |
23 | | oveq2 5877 |
. . . . . . . 8
       |
24 | 23 | eleq1d 2246 |
. . . . . . 7
   
     |
25 | 24 | imbi1d 231 |
. . . . . 6
             |
26 | 25 | ralbidv 2477 |
. . . . 5
  
    
       |
27 | 22, 26 | imbi12d 234 |
. . . 4
               
   
     |
28 | | breq2 4004 |
. . . . . . 7
   
     |
29 | 28 | imbi1d 231 |
. . . . . 6
             |
30 | 29 | ralbidv 2477 |
. . . . 5
    

  
      |
31 | | oveq2 5877 |
. . . . . . . 8
           |
32 | 31 | eleq1d 2246 |
. . . . . . 7
     
       |
33 | 32 | imbi1d 231 |
. . . . . 6
                 |
34 | 33 | ralbidv 2477 |
. . . . 5
    
    
         |
35 | 30, 34 | imbi12d 234 |
. . . 4
                  
      
     |
36 | | breq2 4004 |
. . . . . . 7
 
   |
37 | 36 | imbi1d 231 |
. . . . . 6
         |
38 | 37 | ralbidv 2477 |
. . . . 5
  

  
    |
39 | | oveq2 5877 |
. . . . . . . 8
       |
40 | 39 | eleq1d 2246 |
. . . . . . 7
   
     |
41 | 40 | imbi1d 231 |
. . . . . 6
             |
42 | 41 | ralbidv 2477 |
. . . . 5
  
    
       |
43 | 38, 42 | imbi12d 234 |
. . . 4
               
   
     |
44 | | nncn 8916 |
. . . . . . . . 9
   |
45 | 44 | mulid1d 7965 |
. . . . . . . 8
     |
46 | 45 | eleq1d 2246 |
. . . . . . 7
   
   |
47 | 46 | biimpd 144 |
. . . . . 6
   
   |
48 | 47 | rgen 2530 |
. . . . 5
   
  |
49 | 48 | a1i 9 |
. . . 4
 
     
   |
50 | | breq1 4003 |
. . . . . . 7
 
   |
51 | | eleq1 2240 |
. . . . . . 7
 
   |
52 | 50, 51 | imbi12d 234 |
. . . . . 6
         |
53 | 52 | rspcv 2837 |
. . . . 5

 
  
    |
54 | | prmz 12094 |
. . . . . . 7

  |
55 | | iddvds 11795 |
. . . . . . 7
   |
56 | 54, 55 | syl 14 |
. . . . . 6

  |
57 | | 2sq.1 |
. . . . . . . . . 10
              |
58 | | simprl 529 |
. . . . . . . . . 10
        
  |
59 | | simpll 527 |
. . . . . . . . . 10
        
  |
60 | | simprr 531 |
. . . . . . . . . 10
             |
61 | | simplr 528 |
. . . . . . . . . 10
        
  |
62 | 57, 58, 59, 60, 61 | 2sqlem5 14122 |
. . . . . . . . 9
        
  |
63 | 62 | expr 375 |
. . . . . . . 8
       
   |
64 | 63 | ralrimiva 2550 |
. . . . . . 7
      
   |
65 | 64 | ex 115 |
. . . . . 6

    
    |
66 | 56, 65 | embantd 56 |
. . . . 5

 
         |
67 | 53, 66 | syld 45 |
. . . 4

 
     
    |
68 | | anim12 344 |
. . . . 5
             
     
     
  
       
 
  
     |
69 | | simpr 110 |
. . . . . . . . . . . . . 14
      
    

  |
70 | | eluzelz 9526 |
. . . . . . . . . . . . . . 15
    
  |
71 | 70 | ad2antrr 488 |
. . . . . . . . . . . . . 14
      
    
   |
72 | | eluzelz 9526 |
. . . . . . . . . . . . . . 15
    
  |
73 | 72 | ad2antlr 489 |
. . . . . . . . . . . . . 14
      
    
   |
74 | | euclemma 12129 |
. . . . . . . . . . . . . 14
   
 
     |
75 | 69, 71, 73, 74 | syl3anc 1238 |
. . . . . . . . . . . . 13
      
    
    
    |
76 | 75 | imbi1d 231 |
. . . . . . . . . . . 12
      
    
    

 

    |
77 | | jaob 710 |
. . . . . . . . . . . 12
  
     
    |
78 | 76, 77 | bitrdi 196 |
. . . . . . . . . . 11
      
    
    

 
 
     |
79 | 78 | ralbidva 2473 |
. . . . . . . . . 10
          
 
   
    
     |
80 | | r19.26 2603 |
. . . . . . . . . 10
 
 
       
      |
81 | 79, 80 | bitrdi 196 |
. . . . . . . . 9
          
 
   
 
  
      |
82 | 81 | biimpa 296 |
. . . . . . . 8
      
      
              |
83 | | oveq1 5876 |
. . . . . . . . . . . . 13
       |
84 | 83 | eleq1d 2246 |
. . . . . . . . . . . 12
   
     |
85 | | eleq1 2240 |
. . . . . . . . . . . 12
 
   |
86 | 84, 85 | imbi12d 234 |
. . . . . . . . . . 11
             |
87 | 86 | cbvralvw 2707 |
. . . . . . . . . 10
 
  
    
   |
88 | 44 | adantl 277 |
. . . . . . . . . . . . . . 15
        
    
   
     
 

  |
89 | | uzssz 9536 |
. . . . . . . . . . . . . . . . 17
     |
90 | | zsscn 9250 |
. . . . . . . . . . . . . . . . 17
 |
91 | 89, 90 | sstri 3164 |
. . . . . . . . . . . . . . . 16
     |
92 | | simpll 527 |
. . . . . . . . . . . . . . . . 17
      
      
          |
93 | 92 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
        
    
   
     
 

      |
94 | 91, 93 | sselid 3153 |
. . . . . . . . . . . . . . 15
        
    
   
     
 

  |
95 | | simplr 528 |
. . . . . . . . . . . . . . . . 17
      
      
          |
96 | 95 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
        
    
   
     
 

      |
97 | 91, 96 | sselid 3153 |
. . . . . . . . . . . . . . 15
        
    
   
     
 

  |
98 | | mul32 8077 |
. . . . . . . . . . . . . . . 16
 
           |
99 | | mulass 7933 |
. . . . . . . . . . . . . . . 16
 
           |
100 | 98, 99 | eqtr3d 2212 |
. . . . . . . . . . . . . . 15
 
           |
101 | 88, 94, 97, 100 | syl3anc 1238 |
. . . . . . . . . . . . . 14
        
    
   
     
 

          |
102 | 101 | eleq1d 2246 |
. . . . . . . . . . . . 13
        
    
   
     
 

    
       |
103 | | simpr 110 |
. . . . . . . . . . . . . . 15
        
    
   
     
 

  |
104 | | eluz2nn 9555 |
. . . . . . . . . . . . . . . 16
    
  |
105 | 96, 104 | syl 14 |
. . . . . . . . . . . . . . 15
        
    
   
     
 

  |
106 | 103, 105 | nnmulcld 8957 |
. . . . . . . . . . . . . 14
        
    
   
     
 

    |
107 | | simplr 528 |
. . . . . . . . . . . . . 14
        
    
   
     
 

   
   |
108 | | oveq1 5876 |
. . . . . . . . . . . . . . . . 17
           |
109 | 108 | eleq1d 2246 |
. . . . . . . . . . . . . . . 16
     
       |
110 | | eleq1 2240 |
. . . . . . . . . . . . . . . 16
   
     |
111 | 109, 110 | imbi12d 234 |
. . . . . . . . . . . . . . 15
                   |
112 | 111 | rspcv 2837 |
. . . . . . . . . . . . . 14
    
        
      |
113 | 106, 107,
112 | sylc 62 |
. . . . . . . . . . . . 13
        
    
   
     
 

          |
114 | 102, 113 | sylbird 170 |
. . . . . . . . . . . 12
        
    
   
     
 

          |
115 | 114 | imim1d 75 |
. . . . . . . . . . 11
        
    
   
     
 

   
          |
116 | 115 | ralimdva 2544 |
. . . . . . . . . 10
       
           
  
 
 
  
           |
117 | 87, 116 | sylan2b 287 |
. . . . . . . . 9
       
           
  
 
 
  
           |
118 | 117 | expimpd 363 |
. . . . . . . 8
      
      
         
 
  
 
     
    |
119 | 82, 118 | embantd 56 |
. . . . . . 7
      
      
       
  
       
 
  
        
    |
120 | 119 | ex 115 |
. . . . . 6
          
 
         
     
       
              |
121 | 120 | com23 78 |
. . . . 5
          
         
 
  
         
  
            |
122 | 68, 121 | syl5 32 |
. . . 4
          
             
     
       
      
     |
123 | 11, 19, 27, 35, 43, 49, 67, 122 | prmind 12104 |
. . 3
  

         |
124 | 2, 3, 123 | sylc 62 |
. 2
        |
125 | | 2sqlem6.4 |
. 2
     |
126 | | oveq1 5876 |
. . . . 5
       |
127 | 126 | eleq1d 2246 |
. . . 4
   
     |
128 | | eleq1 2240 |
. . . 4
 
   |
129 | 127, 128 | imbi12d 234 |
. . 3
             |
130 | 129 | rspcv 2837 |
. 2
  
      
    |
131 | 1, 124, 125, 130 | syl3c 63 |
1
   |