Proof of Theorem pythagtriplem19
Step | Hyp | Ref
| Expression |
1 | | gcdnncl 11951 |
. . . . 5
 
     |
2 | 1 | 3adant3 1017 |
. . . 4
 
     |
3 | 2 | 3ad2ant1 1018 |
. . 3
  
              
         |
4 | | nnz 9261 |
. . . . . . . . . . 11
   |
5 | | nnz 9261 |
. . . . . . . . . . 11
   |
6 | | gcddvds 11947 |
. . . . . . . . . . 11
 
    
    |
7 | 4, 5, 6 | syl2an 289 |
. . . . . . . . . 10
 
    
    |
8 | 7 | 3adant3 1017 |
. . . . . . . . 9
 
   

    |
9 | 8 | simpld 112 |
. . . . . . . 8
 
     |
10 | 2 | nnzd 9363 |
. . . . . . . . 9
 
     |
11 | 2 | nnne0d 8953 |
. . . . . . . . 9
 
     |
12 | 4 | 3ad2ant1 1018 |
. . . . . . . . 9
 
   |
13 | | dvdsval2 11781 |
. . . . . . . . 9
    
    
       |
14 | 10, 11, 12, 13 | syl3anc 1238 |
. . . . . . . 8
 
   
       |
15 | 9, 14 | mpbid 147 |
. . . . . . 7
 
       |
16 | | nnre 8915 |
. . . . . . . . 9
   |
17 | 16 | 3ad2ant1 1018 |
. . . . . . . 8
 
   |
18 | 2 | nnred 8921 |
. . . . . . . 8
 
     |
19 | | nngt0 8933 |
. . . . . . . . 9
   |
20 | 19 | 3ad2ant1 1018 |
. . . . . . . 8
 
   |
21 | 2 | nngt0d 8952 |
. . . . . . . 8
 
     |
22 | 17, 18, 20, 21 | divgt0d 8881 |
. . . . . . 7
 
       |
23 | | elnnz 9252 |
. . . . . . 7
    
            |
24 | 15, 22, 23 | sylanbrc 417 |
. . . . . 6
 
       |
25 | 24 | 3ad2ant1 1018 |
. . . . 5
  
              
           |
26 | 8 | simprd 114 |
. . . . . . . 8
 
     |
27 | 5 | 3ad2ant2 1019 |
. . . . . . . . 9
 
   |
28 | | dvdsval2 11781 |
. . . . . . . . 9
    
    
       |
29 | 10, 11, 27, 28 | syl3anc 1238 |
. . . . . . . 8
 
   
       |
30 | 26, 29 | mpbid 147 |
. . . . . . 7
 
       |
31 | | nnre 8915 |
. . . . . . . . 9
   |
32 | 31 | 3ad2ant2 1019 |
. . . . . . . 8
 
   |
33 | | nngt0 8933 |
. . . . . . . . 9
   |
34 | 33 | 3ad2ant2 1019 |
. . . . . . . 8
 
   |
35 | 32, 18, 34, 21 | divgt0d 8881 |
. . . . . . 7
 
       |
36 | | elnnz 9252 |
. . . . . . 7
    
            |
37 | 30, 35, 36 | sylanbrc 417 |
. . . . . 6
 
       |
38 | 37 | 3ad2ant1 1018 |
. . . . 5
  
              
           |
39 | | dvdssq 12015 |
. . . . . . . . . . . . . . 15
   
   
             |
40 | 10, 12, 39 | syl2anc 411 |
. . . . . . . . . . . . . 14
 
   
             |
41 | | dvdssq 12015 |
. . . . . . . . . . . . . . 15
   
   
             |
42 | 10, 27, 41 | syl2anc 411 |
. . . . . . . . . . . . . 14
 
   
             |
43 | 40, 42 | anbi12d 473 |
. . . . . . . . . . . . 13
 
     
 
                         |
44 | 8, 43 | mpbid 147 |
. . . . . . . . . . . 12
 
                         |
45 | 2 | nnsqcld 10660 |
. . . . . . . . . . . . . 14
 
         |
46 | 45 | nnzd 9363 |
. . . . . . . . . . . . 13
 
         |
47 | | nnsqcl 10575 |
. . . . . . . . . . . . . . 15
       |
48 | 47 | 3ad2ant1 1018 |
. . . . . . . . . . . . . 14
 
       |
49 | 48 | nnzd 9363 |
. . . . . . . . . . . . 13
 
       |
50 | | nnsqcl 10575 |
. . . . . . . . . . . . . . 15
       |
51 | 50 | 3ad2ant2 1019 |
. . . . . . . . . . . . . 14
 
       |
52 | 51 | nnzd 9363 |
. . . . . . . . . . . . 13
 
       |
53 | | dvds2add 11816 |
. . . . . . . . . . . . 13
                                                           |
54 | 46, 49, 52, 53 | syl3anc 1238 |
. . . . . . . . . . . 12
 
                                           |
55 | 44, 54 | mpd 13 |
. . . . . . . . . . 11
 
                   |
56 | 55 | adantr 276 |
. . . . . . . . . 10
  
                                  |
57 | | simpr 110 |
. . . . . . . . . 10
  
                                |
58 | 56, 57 | breqtrd 4026 |
. . . . . . . . 9
  
                            |
59 | | nnz 9261 |
. . . . . . . . . . . 12
   |
60 | 59 | 3ad2ant3 1020 |
. . . . . . . . . . 11
 
   |
61 | | dvdssq 12015 |
. . . . . . . . . . 11
   
   
             |
62 | 10, 60, 61 | syl2anc 411 |
. . . . . . . . . 10
 
   
             |
63 | 62 | adantr 276 |
. . . . . . . . 9
  
                                |
64 | 58, 63 | mpbird 167 |
. . . . . . . 8
  
                    |
65 | | dvdsval2 11781 |
. . . . . . . . . 10
    
    
       |
66 | 10, 11, 60, 65 | syl3anc 1238 |
. . . . . . . . 9
 
   
       |
67 | 66 | adantr 276 |
. . . . . . . 8
  
                          |
68 | 64, 67 | mpbid 147 |
. . . . . . 7
  
                      |
69 | | nnre 8915 |
. . . . . . . . . 10
   |
70 | 69 | 3ad2ant3 1020 |
. . . . . . . . 9
 
   |
71 | | nngt0 8933 |
. . . . . . . . . 10
   |
72 | 71 | 3ad2ant3 1020 |
. . . . . . . . 9
 
   |
73 | 70, 18, 72, 21 | divgt0d 8881 |
. . . . . . . 8
 
       |
74 | 73 | adantr 276 |
. . . . . . 7
  
                      |
75 | | elnnz 9252 |
. . . . . . 7
    
            |
76 | 68, 74, 75 | sylanbrc 417 |
. . . . . 6
  
                      |
77 | 76 | 3adant3 1017 |
. . . . 5
  
              
           |
78 | 48 | nncnd 8922 |
. . . . . . . 8
 
       |
79 | 51 | nncnd 8922 |
. . . . . . . 8
 
       |
80 | 45 | nncnd 8922 |
. . . . . . . 8
 
         |
81 | 45 | nnap0d 8954 |
. . . . . . . 8
 
       #   |
82 | 78, 79, 80, 81 | divdirapd 8775 |
. . . . . . 7
 
                                               |
83 | 82 | 3ad2ant1 1018 |
. . . . . 6
  
              
                                                   |
84 | | nncn 8916 |
. . . . . . . . . 10
   |
85 | 84 | 3ad2ant3 1020 |
. . . . . . . . 9
 
   |
86 | 2 | nncnd 8922 |
. . . . . . . . 9
 
     |
87 | 2 | nnap0d 8954 |
. . . . . . . . 9
 
   #   |
88 | 85, 86, 87 | sqdivapd 10652 |
. . . . . . . 8
 
                       |
89 | 88 | 3ad2ant1 1018 |
. . . . . . 7
  
              
                           |
90 | | oveq1 5876 |
. . . . . . . 8
                                               |
91 | 90 | 3ad2ant2 1019 |
. . . . . . 7
  
              
                                     |
92 | 89, 91 | eqtr4d 2213 |
. . . . . 6
  
              
                                 |
93 | | nncn 8916 |
. . . . . . . . . 10
   |
94 | 93 | 3ad2ant1 1018 |
. . . . . . . . 9
 
   |
95 | 94, 86, 87 | sqdivapd 10652 |
. . . . . . . 8
 
                       |
96 | | nncn 8916 |
. . . . . . . . . 10
   |
97 | 96 | 3ad2ant2 1019 |
. . . . . . . . 9
 
   |
98 | 97, 86, 87 | sqdivapd 10652 |
. . . . . . . 8
 
                       |
99 | 95, 98 | oveq12d 5887 |
. . . . . . 7
 
                                               |
100 | 99 | 3ad2ant1 1018 |
. . . . . 6
  
              
                                                   |
101 | 83, 92, 100 | 3eqtr4rd 2221 |
. . . . 5
  
              
                                 |
102 | | gcddiv 12003 |
. . . . . . . 8
   
     
                     |
103 | 12, 27, 2, 8, 102 | syl31anc 1241 |
. . . . . . 7
 
                   |
104 | 86, 87 | dividapd 8732 |
. . . . . . 7
 
         |
105 | 103, 104 | eqtr3d 2212 |
. . . . . 6
 
             |
106 | 105 | 3ad2ant1 1018 |
. . . . 5
  
              
                 |
107 | | simp3 999 |
. . . . 5
  
              
    
      |
108 | | pythagtriplem18 12264 |
. . . . 5
                                                                                                     |
109 | 25, 38, 77, 101, 106, 107, 108 | syl312anc 1259 |
. . . 4
  
              
     
                                         |
110 | 94, 86, 87 | divcanap2d 8738 |
. . . . . . . . . 10
 
           |
111 | 110 | eqcomd 2183 |
. . . . . . . . 9
 
           |
112 | 97, 86, 87 | divcanap2d 8738 |
. . . . . . . . . 10
 
           |
113 | 112 | eqcomd 2183 |
. . . . . . . . 9
 
           |
114 | 85, 86, 87 | divcanap2d 8738 |
. . . . . . . . . 10
 
           |
115 | 114 | eqcomd 2183 |
. . . . . . . . 9
 
           |
116 | 111, 113,
115 | 3jca 1177 |
. . . . . . . 8
 
 
               
           |
117 | 116 | 3ad2ant1 1018 |
. . . . . . 7
  
              
             
                   |
118 | | oveq2 5877 |
. . . . . . . . . 10
                                       |
119 | 118 | eqeq2d 2189 |
. . . . . . . . 9
               
       
                 |
120 | 119 | 3ad2ant1 1018 |
. . . . . . . 8
                                      
        
                 |
121 | | oveq2 5877 |
. . . . . . . . . 10
                           |
122 | 121 | eqeq2d 2189 |
. . . . . . . . 9
         
       
           |
123 | 122 | 3ad2ant2 1019 |
. . . . . . . 8
                                      
        
           |
124 | | oveq2 5877 |
. . . . . . . . . 10
                                       |
125 | 124 | eqeq2d 2189 |
. . . . . . . . 9
               
       
                 |
126 | 125 | 3ad2ant3 1020 |
. . . . . . . 8
                                      
        
                 |
127 | 120, 123,
126 | 3anbi123d 1312 |
. . . . . . 7
                                      
 
               
        
                                         |
128 | 117, 127 | syl5ibcom 155 |
. . . . . 6
  
              
                                           
                                         |
129 | 128 | reximdv 2578 |
. . . . 5
  
              
                                            
                                          |
130 | 129 | reximdv 2578 |
. . . 4
  
              
                                             
                                           |
131 | 109, 130 | mpd 13 |
. . 3
  
              
     
 
                                       |
132 | | oveq1 5876 |
. . . . . . 7
  
                            |
133 | 132 | eqeq2d 2189 |
. . . . . 6
  
            
                 |
134 | | oveq1 5876 |
. . . . . . 7
  
                |
135 | 134 | eqeq2d 2189 |
. . . . . 6
  
      
           |
136 | | oveq1 5876 |
. . . . . . 7
  
                            |
137 | 136 | eqeq2d 2189 |
. . . . . 6
  
            
                 |
138 | 133, 135,
137 | 3anbi123d 1312 |
. . . . 5
  
 
                              
                                         |
139 | 138 | 2rexbidv 2502 |
. . . 4
  
 
                                
                                           |
140 | 139 | rspcev 2841 |
. . 3
     

                                        

                                 |
141 | 3, 131, 140 | syl2anc 411 |
. 2
  
              
     
 

                                 |
142 | | rexcom 2641 |
. . 3
  
                                
                                     |
143 | | rexcom 2641 |
. . . 4
  

                              
                                    |
144 | 143 | rexbii 2484 |
. . 3
  
                                
                                     |
145 | 142, 144 | bitri 184 |
. 2
  
                                
                                     |
146 | 141, 145 | sylib 122 |
1
  
              
     
 

                                 |