Proof of Theorem dvdssq
Step | Hyp | Ref
| Expression |
1 | | 0z 8963 |
. . . 4
 |
2 | | zdceq 9024 |
. . . 4
 
 DECID   |
3 | 1, 2 | mpan2 419 |
. . 3

DECID
  |
4 | | exmiddc 804 |
. . 3
DECID

   |
5 | | 0dvds 11355 |
. . . . . . . 8
 
   |
6 | | zcn 8957 |
. . . . . . . . 9
   |
7 | | sqeq0 10243 |
. . . . . . . . 9
         |
8 | 6, 7 | syl 14 |
. . . . . . . 8
         |
9 | 5, 8 | bitr4d 190 |
. . . . . . 7
 
       |
10 | | zsqcl 10250 |
. . . . . . . 8
       |
11 | | 0dvds 11355 |
. . . . . . . 8
     
   
       |
12 | 10, 11 | syl 14 |
. . . . . . 7
 
   
       |
13 | 9, 12 | bitr4d 190 |
. . . . . 6
 
       |
14 | 13 | adantl 273 |
. . . . 5
 
         |
15 | | breq1 3896 |
. . . . . 6
 
   |
16 | | sq0i 10271 |
. . . . . . 7
       |
17 | 16 | breq1d 3903 |
. . . . . 6
         
       |
18 | 15, 17 | bibi12d 234 |
. . . . 5
           

        |
19 | 14, 18 | syl5ibr 155 |
. . . 4
                 |
20 | | df-ne 2281 |
. . . . 5

  |
21 | | nnabscl 10758 |
. . . . . . . . 9
         |
22 | | zdceq 9024 |
. . . . . . . . . . . 12
 
 DECID   |
23 | 1, 22 | mpan2 419 |
. . . . . . . . . . 11

DECID
  |
24 | | exmiddc 804 |
. . . . . . . . . . 11
DECID

   |
25 | | nnz 8971 |
. . . . . . . . . . . . . . 15
           |
26 | | dvds0 11350 |
. . . . . . . . . . . . . . . 16
           |
27 | | zsqcl 10250 |
. . . . . . . . . . . . . . . . 17
               |
28 | | dvds0 11350 |
. . . . . . . . . . . . . . . . 17
                   |
29 | 27, 28 | syl 14 |
. . . . . . . . . . . . . . . 16
               |
30 | 26, 29 | 2thd 174 |
. . . . . . . . . . . . . . 15
         
           |
31 | 25, 30 | syl 14 |
. . . . . . . . . . . . . 14
         
           |
32 | 31 | adantr 272 |
. . . . . . . . . . . . 13
     
     
           |
33 | | breq2 3897 |
. . . . . . . . . . . . . 14
     
       |
34 | | sq0i 10271 |
. . . . . . . . . . . . . . 15
       |
35 | 34 | breq2d 3905 |
. . . . . . . . . . . . . 14
             
           |
36 | 33, 35 | bibi12d 234 |
. . . . . . . . . . . . 13
      
                 
            |
37 | 32, 36 | syl5ibr 155 |
. . . . . . . . . . . 12
      
     
                |
38 | | df-ne 2281 |
. . . . . . . . . . . . 13

  |
39 | | nnabscl 10758 |
. . . . . . . . . . . . . . . . 17
         |
40 | | dvdssqlem 11558 |
. . . . . . . . . . . . . . . . 17
               
   
                   |
41 | 39, 40 | sylan2 282 |
. . . . . . . . . . . . . . . 16
      
 
                            |
42 | | simpl 108 |
. . . . . . . . . . . . . . . . 17
  
  |
43 | | dvdsabsb 11354 |
. . . . . . . . . . . . . . . . 17
     
     
           |
44 | 25, 42, 43 | syl2an 285 |
. . . . . . . . . . . . . . . 16
      
 
        
       |
45 | | nnsqcl 10249 |
. . . . . . . . . . . . . . . . . . 19
               |
46 | 45 | nnzd 9070 |
. . . . . . . . . . . . . . . . . 18
               |
47 | 10 | adantr 272 |
. . . . . . . . . . . . . . . . . 18
         |
48 | | dvdsabsb 11354 |
. . . . . . . . . . . . . . . . . 18
                           
                   |
49 | 46, 47, 48 | syl2an 285 |
. . . . . . . . . . . . . . . . 17
      
 
            
                   |
50 | 6 | adantr 272 |
. . . . . . . . . . . . . . . . . . . 20
  
  |
51 | | abssq 10739 |
. . . . . . . . . . . . . . . . . . . 20
                   |
52 | 50, 51 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
                     |
53 | 52 | breq2d 3905 |
. . . . . . . . . . . . . . . . . 18
                   
                   |
54 | 53 | adantl 273 |
. . . . . . . . . . . . . . . . 17
      
 
                                    |
55 | 49, 54 | bitr4d 190 |
. . . . . . . . . . . . . . . 16
      
 
            
                   |
56 | 41, 44, 55 | 3bitr4d 219 |
. . . . . . . . . . . . . . 15
      
 
                    |
57 | 56 | anassrs 395 |
. . . . . . . . . . . . . 14
      


                    |
58 | 57 | expcom 115 |
. . . . . . . . . . . . 13
      
     
                |
59 | 38, 58 | sylbir 134 |
. . . . . . . . . . . 12
                             |
60 | 37, 59 | jaoi 688 |
. . . . . . . . . . 11
  
     
     
                |
61 | 23, 24, 60 | 3syl 17 |
. . . . . . . . . 10
      
     
                |
62 | 61 | anabsi7 553 |
. . . . . . . . 9
     
     
               |
63 | 21, 62 | sylan 279 |
. . . . . . . 8
                         |
64 | | absdvdsb 11353 |
. . . . . . . . 9
 
         |
65 | 64 | adantlr 466 |
. . . . . . . 8
         
   |
66 | | zsqcl 10250 |
. . . . . . . . . . 11
       |
67 | 66 | adantr 272 |
. . . . . . . . . 10
         |
68 | | absdvdsb 11353 |
. . . . . . . . . 10
                   
               |
69 | 67, 10, 68 | syl2an 285 |
. . . . . . . . 9
                             |
70 | | zcn 8957 |
. . . . . . . . . . . . . 14
   |
71 | | abssq 10739 |
. . . . . . . . . . . . . 14
                   |
72 | 70, 71 | syl 14 |
. . . . . . . . . . . . 13
                   |
73 | 72 | eqcomd 2118 |
. . . . . . . . . . . 12
                   |
74 | 73 | adantr 272 |
. . . . . . . . . . 11
                     |
75 | 74 | breq1d 3903 |
. . . . . . . . . 10
               
               |
76 | 75 | adantr 272 |
. . . . . . . . 9
                 
               |
77 | 69, 76 | bitrd 187 |
. . . . . . . 8
                             |
78 | 63, 65, 77 | 3bitr4d 219 |
. . . . . . 7
                 |
79 | 78 | an32s 540 |
. . . . . 6
    
            |
80 | 79 | expcom 115 |
. . . . 5
                 |
81 | 20, 80 | sylbir 134 |
. . . 4
    
            |
82 | 19, 81 | jaoi 688 |
. . 3
  
 
 
            |
83 | 3, 4, 82 | 3syl 17 |
. 2
                 |
84 | 83 | anabsi5 551 |
1
 
             |