Proof of Theorem 4sqlem10
Step | Hyp | Ref
| Expression |
1 | | 4sqlem5.3 |
. . . . . 6
   |
2 | 1 | adantr 276 |
. . . . 5
 
   |
3 | 2 | nnzd 9363 |
. . . 4
 
   |
4 | | zsqcl 10576 |
. . . 4
       |
5 | 3, 4 | syl 14 |
. . 3
 
       |
6 | | 4sqlem5.2 |
. . . . . 6
   |
7 | 6 | adantr 276 |
. . . . 5
 
   |
8 | 2 | nnred 8921 |
. . . . . . . . 9
 
   |
9 | 8 | rehalfcld 9154 |
. . . . . . . 8
 
     |
10 | 9 | recnd 7976 |
. . . . . . 7
 
     |
11 | 10 | negnegd 8249 |
. . . . . 6
 
         |
12 | | 4sqlem5.4 |
. . . . . . . . . . . . . . 15
           |
13 | 6, 1, 12 | 4sqlem5 12363 |
. . . . . . . . . . . . . 14
         |
14 | 13 | adantr 276 |
. . . . . . . . . . . . 13
 
         |
15 | 14 | simpld 112 |
. . . . . . . . . . . 12
 
   |
16 | 15 | zred 9364 |
. . . . . . . . . . 11
 
   |
17 | 6, 1, 12 | 4sqlem6 12364 |
. . . . . . . . . . . . 13
          |
18 | 17 | adantr 276 |
. . . . . . . . . . . 12
 
          |
19 | 18 | simprd 114 |
. . . . . . . . . . 11
 
     |
20 | 16, 19 | ltned 8061 |
. . . . . . . . . 10
 
     |
21 | 20 | neneqd 2368 |
. . . . . . . . 9
 
     |
22 | | 2cnd 8981 |
. . . . . . . . . . . . . . 15
 
   |
23 | 22 | sqvald 10636 |
. . . . . . . . . . . . . 14
 
         |
24 | 23 | oveq2d 5885 |
. . . . . . . . . . . . 13
 
                     |
25 | 2 | nncnd 8922 |
. . . . . . . . . . . . . 14
 
   |
26 | | 2ap0 9001 |
. . . . . . . . . . . . . . 15
#  |
27 | 26 | a1i 9 |
. . . . . . . . . . . . . 14
 
 #   |
28 | 25, 22, 27 | sqdivapd 10652 |
. . . . . . . . . . . . 13
 
                   |
29 | 25 | sqcld 10637 |
. . . . . . . . . . . . . 14
 
       |
30 | 29, 22, 22, 27, 27 | divdivap1d 8768 |
. . . . . . . . . . . . 13
 
                   |
31 | 24, 28, 30 | 3eqtr4d 2220 |
. . . . . . . . . . . 12
 
                 |
32 | 29 | halfcld 9152 |
. . . . . . . . . . . . . 14
 
         |
33 | 32 | halfcld 9152 |
. . . . . . . . . . . . 13
 
           |
34 | 15 | zcnd 9365 |
. . . . . . . . . . . . . 14
 
   |
35 | 34 | sqcld 10637 |
. . . . . . . . . . . . 13
 
       |
36 | | 4sqlem10.5 |
. . . . . . . . . . . . 13
 
                 |
37 | 33, 35, 36 | subeq0d 8266 |
. . . . . . . . . . . 12
 
               |
38 | 31, 37 | eqtr2d 2211 |
. . . . . . . . . . 11
 
             |
39 | | zq 9615 |
. . . . . . . . . . . . 13
   |
40 | 15, 39 | syl 14 |
. . . . . . . . . . . 12
 
   |
41 | | 2nn 9069 |
. . . . . . . . . . . . . 14
 |
42 | 41 | a1i 9 |
. . . . . . . . . . . . 13
 
   |
43 | | znq 9613 |
. . . . . . . . . . . . 13
 
     |
44 | 3, 42, 43 | syl2anc 411 |
. . . . . . . . . . . 12
 
     |
45 | | qsqeqor 10616 |
. . . . . . . . . . . 12
  
                       |
46 | 40, 44, 45 | syl2anc 411 |
. . . . . . . . . . 11
 
                
     |
47 | 38, 46 | mpbid 147 |
. . . . . . . . . 10
 
     
    |
48 | 47 | ord 724 |
. . . . . . . . 9
 
   
      |
49 | 21, 48 | mpd 13 |
. . . . . . . 8
 
      |
50 | 49, 15 | eqeltrrd 2255 |
. . . . . . 7
 
      |
51 | 50 | znegcld 9366 |
. . . . . 6
 
       |
52 | 11, 51 | eqeltrrd 2255 |
. . . . 5
 
     |
53 | 7, 52 | zaddcld 9368 |
. . . 4
 
       |
54 | | zsqcl 10576 |
. . . 4
               |
55 | 53, 54 | syl 14 |
. . 3
 
   
       |
56 | 53, 3 | zmulcld 9370 |
. . 3
 
   
     |
57 | | zq 9615 |
. . . . . . . . . 10
   |
58 | 7, 57 | syl 14 |
. . . . . . . . 9
 
   |
59 | | qaddcl 9624 |
. . . . . . . . 9
  
   
    |
60 | 58, 44, 59 | syl2anc 411 |
. . . . . . . 8
 
       |
61 | | nnq 9622 |
. . . . . . . . 9
   |
62 | 2, 61 | syl 14 |
. . . . . . . 8
 
   |
63 | 2 | nngt0d 8952 |
. . . . . . . 8
 
   |
64 | 60, 62, 63 | modqcld 10314 |
. . . . . . 7
 
   
     |
65 | | qcn 9623 |
. . . . . . 7
               |
66 | 64, 65 | syl 14 |
. . . . . 6
 
   
     |
67 | | 0cnd 7941 |
. . . . . 6
 
   |
68 | | df-neg 8121 |
. . . . . . 7
        |
69 | 49, 12, 68 | 3eqtr3g 2233 |
. . . . . 6
 
                 |
70 | 66, 67, 10, 69 | subcan2d 8300 |
. . . . 5
 
   
     |
71 | | dvdsval3 11782 |
. . . . . 6
  
     
     
      |
72 | 2, 53, 71 | syl2anc 411 |
. . . . 5
 
  
     
      |
73 | 70, 72 | mpbird 167 |
. . . 4
 
       |
74 | | dvdssq 12015 |
. . . . 5
  
     
                  |
75 | 3, 53, 74 | syl2anc 411 |
. . . 4
 
  
                  |
76 | 73, 75 | mpbid 147 |
. . 3
 
               |
77 | 25 | sqvald 10636 |
. . . 4
 
         |
78 | 2 | nnne0d 8953 |
. . . . . 6
 
   |
79 | | dvdsmulcr 11812 |
. . . . . 6
  
   
          
       |
80 | 3, 53, 3, 78, 79 | syl112anc 1242 |
. . . . 5
 
         
       |
81 | 73, 80 | mpbird 167 |
. . . 4
 
  
 
      |
82 | 77, 81 | eqbrtrd 4022 |
. . 3
 
             |
83 | 5, 55, 56, 76, 82 | dvds2subd 11818 |
. 2
 
                       |
84 | 53 | zcnd 9365 |
. . . . 5
 
       |
85 | 84 | sqvald 10636 |
. . . 4
 
   
           
     |
86 | 85 | oveq1d 5884 |
. . 3
 
                                     |
87 | 84, 84, 25 | subdid 8361 |
. . 3
 
   
                             |
88 | 25 | 2halvesd 9153 |
. . . . . . 7
 
         |
89 | 88 | oveq2d 5885 |
. . . . . 6
 
   
                 |
90 | 7 | zcnd 9365 |
. . . . . . 7
 
   |
91 | 90, 10, 10 | pnpcan2d 8296 |
. . . . . 6
 
   
               |
92 | 89, 91 | eqtr3d 2212 |
. . . . 5
 
   
         |
93 | 92 | oveq2d 5885 |
. . . 4
 
   
               
     |
94 | | subsq 10612 |
. . . . 5
  
                          |
95 | 90, 10, 94 | syl2anc 411 |
. . . 4
 
                   
     |
96 | 31 | oveq2d 5885 |
. . . 4
 
                             |
97 | 93, 95, 96 | 3eqtr2d 2216 |
. . 3
 
   
                         |
98 | 86, 87, 97 | 3eqtr2d 2216 |
. 2
 
                                 |
99 | 83, 98 | breqtrd 4026 |
1
 
                     |