Proof of Theorem quartlem1
Step | Hyp | Ref
| Expression |
1 | | 2cn 10507 |
. . . . . . . . . 10
 |
2 | | quartlem1.p |
. . . . . . . . . 10
   |
3 | | sqmul 12050 |
. . . . . . . . . 10
 
                   |
4 | 1, 2, 3 | sylancr 663 |
. . . . . . . . 9
                   |
5 | | sq2 12083 |
. . . . . . . . . 10
     |
6 | 5 | oveq1i 6213 |
. . . . . . . . 9
                 |
7 | 4, 6 | syl6eq 2511 |
. . . . . . . 8
               |
8 | 7 | oveq1d 6218 |
. . . . . . 7
                               |
9 | | 4cn 10514 |
. . . . . . . . 9
 |
10 | 9 | a1i 11 |
. . . . . . . 8
   |
11 | | 3cn 10511 |
. . . . . . . . 9
 |
12 | 11 | a1i 11 |
. . . . . . . 8
   |
13 | 2 | sqcld 12127 |
. . . . . . . 8
       |
14 | 10, 12, 13 | subdird 9916 |
. . . . . . 7
                         |
15 | 8, 14 | eqtr4d 2498 |
. . . . . 6
                         |
16 | | ax-1cn 9455 |
. . . . . . . . . 10
 |
17 | | 3p1e4 10562 |
. . . . . . . . . 10
   |
18 | 9, 11, 16, 17 | subaddrii 9812 |
. . . . . . . . 9
   |
19 | 18 | oveq1i 6213 |
. . . . . . . 8
               |
20 | | mulid2 9499 |
. . . . . . . 8
                 |
21 | 19, 20 | syl5eq 2507 |
. . . . . . 7
                   |
22 | 13, 21 | syl 16 |
. . . . . 6
               |
23 | 15, 22 | eqtr2d 2496 |
. . . . 5
                     |
24 | 23 | oveq1d 6218 |
. . . 4
      ;                  ;     |
25 | | mulcl 9481 |
. . . . . . 7
 
     |
26 | 1, 2, 25 | sylancr 663 |
. . . . . 6
     |
27 | 26 | sqcld 12127 |
. . . . 5
         |
28 | | mulcl 9481 |
. . . . . 6
               |
29 | 11, 13, 28 | sylancr 663 |
. . . . 5
         |
30 | | 1nn0 10710 |
. . . . . . . 8
 |
31 | | 2nn 10594 |
. . . . . . . 8
 |
32 | 30, 31 | decnncl 10883 |
. . . . . . 7
;  |
33 | 32 | nncni 10447 |
. . . . . 6
;  |
34 | | quartlem1.r |
. . . . . 6
   |
35 | | mulcl 9481 |
. . . . . 6
 ;
 ;    |
36 | 33, 34, 35 | sylancr 663 |
. . . . 5
 ;    |
37 | 27, 29, 36 | subsubd 9862 |
. . . 4
               ;                   ;     |
38 | 24, 37 | eqtr4d 2498 |
. . 3
      ;                 ;      |
39 | | quartlem1.u |
. . 3
      ;     |
40 | | mulcl 9481 |
. . . . . . 7
 
     |
41 | 9, 34, 40 | sylancr 663 |
. . . . . 6
     |
42 | 12, 13, 41 | subdid 9915 |
. . . . 5
                         |
43 | | 4t3e12 10942 |
. . . . . . . . 9
  ;  |
44 | 9, 11, 43 | mulcomli 9508 |
. . . . . . . 8
  ;  |
45 | 44 | oveq1i 6213 |
. . . . . . 7
    ;   |
46 | 12, 10, 34 | mulassd 9524 |
. . . . . . 7
           |
47 | 45, 46 | syl5eqr 2509 |
. . . . . 6
 ;        |
48 | 47 | oveq2d 6219 |
. . . . 5
        ;                 |
49 | 42, 48 | eqtr4d 2498 |
. . . 4
                  ;     |
50 | 49 | oveq2d 6219 |
. . 3
                                 ;      |
51 | 38, 39, 50 | 3eqtr4d 2505 |
. 2
                     |
52 | 1 | a1i 11 |
. . . . . . . . . 10
   |
53 | | 3nn0 10712 |
. . . . . . . . . . 11
 |
54 | 53 | a1i 11 |
. . . . . . . . . 10
   |
55 | 52, 2, 54 | mulexpd 12144 |
. . . . . . . . 9
                   |
56 | | cu2 12085 |
. . . . . . . . . 10
     |
57 | 56 | oveq1i 6213 |
. . . . . . . . 9
                 |
58 | 55, 57 | syl6eq 2511 |
. . . . . . . 8
               |
59 | 58 | oveq2d 6219 |
. . . . . . 7
                   |
60 | | 8cn 10522 |
. . . . . . . . 9
 |
61 | 60 | a1i 11 |
. . . . . . . 8
   |
62 | | expcl 12004 |
. . . . . . . . 9
 
       |
63 | 2, 53, 62 | sylancl 662 |
. . . . . . . 8
       |
64 | 52, 61, 63 | mul12d 9693 |
. . . . . . 7
                   |
65 | 59, 64 | eqtrd 2495 |
. . . . . 6
                   |
66 | | 9cn 10524 |
. . . . . . . . 9
 |
67 | 66 | a1i 11 |
. . . . . . . 8
   |
68 | | mulcl 9481 |
. . . . . . . . 9
               |
69 | 1, 63, 68 | sylancr 663 |
. . . . . . . 8
         |
70 | 2, 34 | mulcld 9521 |
. . . . . . . . 9
     |
71 | | mulcl 9481 |
. . . . . . . . 9
  
        |
72 | 60, 70, 71 | sylancr 663 |
. . . . . . . 8
  
    |
73 | 67, 69, 72 | subdid 9915 |
. . . . . . 7
                                 |
74 | 26, 13, 41 | subdid 9915 |
. . . . . . . . 9
                               |
75 | 52, 2, 13 | mulassd 9524 |
. . . . . . . . . . 11
                   |
76 | 2, 13 | mulcomd 9522 |
. . . . . . . . . . . . 13
               |
77 | | df-3 10496 |
. . . . . . . . . . . . . . 15
   |
78 | 77 | oveq2i 6214 |
. . . . . . . . . . . . . 14
           |
79 | | 2nn0 10711 |
. . . . . . . . . . . . . . 15
 |
80 | | expp1 11993 |
. . . . . . . . . . . . . . 15
 
               |
81 | 2, 79, 80 | sylancl 662 |
. . . . . . . . . . . . . 14
               |
82 | 78, 81 | syl5eq 2507 |
. . . . . . . . . . . . 13
             |
83 | 76, 82 | eqtr4d 2498 |
. . . . . . . . . . . 12
             |
84 | 83 | oveq2d 6219 |
. . . . . . . . . . 11
  
              |
85 | 75, 84 | eqtrd 2495 |
. . . . . . . . . 10
                 |
86 | 52, 2, 10, 34 | mul4d 9696 |
. . . . . . . . . . 11
               |
87 | | 4t2e8 10590 |
. . . . . . . . . . . . 13
   |
88 | 9, 1, 87 | mulcomli 9508 |
. . . . . . . . . . . 12
   |
89 | 88 | oveq1i 6213 |
. . . . . . . . . . 11
       
   |
90 | 86, 89 | syl6eq 2511 |
. . . . . . . . . 10
             |
91 | 85, 90 | oveq12d 6221 |
. . . . . . . . 9
                               |
92 | 74, 91 | eqtrd 2495 |
. . . . . . . 8
                           |
93 | 92 | oveq2d 6219 |
. . . . . . 7
                        
      |
94 | | 9t8e72 10971 |
. . . . . . . . . 10
  ;  |
95 | 94 | oveq1i 6213 |
. . . . . . . . 9
      ; 
   |
96 | 67, 61, 70 | mulassd 9524 |
. . . . . . . . 9
    
          |
97 | 95, 96 | syl5eqr 2509 |
. . . . . . . 8
 ; 
          |
98 | 97 | oveq2d 6219 |
. . . . . . 7
          ; 
                     |
99 | 73, 93, 98 | 3eqtr4d 2505 |
. . . . . 6
                        ; 
     |
100 | 65, 99 | oveq12d 6221 |
. . . . 5
                                           ;        |
101 | | mulcl 9481 |
. . . . . . 7
                   |
102 | 60, 69, 101 | sylancr 663 |
. . . . . 6
           |
103 | | mulcl 9481 |
. . . . . . 7
                   |
104 | 66, 69, 103 | sylancr 663 |
. . . . . 6
           |
105 | | 7nn0 10716 |
. . . . . . . . 9
 |
106 | 105, 31 | decnncl 10883 |
. . . . . . . 8
;  |
107 | 106 | nncni 10447 |
. . . . . . 7
;  |
108 | | mulcl 9481 |
. . . . . . 7
 ; 
  ; 
    |
109 | 107, 70, 108 | sylancr 663 |
. . . . . 6
 ; 
    |
110 | 102, 104,
109 | subsubd 9862 |
. . . . 5
                   ; 
                       ;       |
111 | 104, 102 | negsubdi2d 9850 |
. . . . . . 7
                                        |
112 | 67, 61, 69 | subdird 9916 |
. . . . . . . . 9
                               |
113 | | 8p1e9 10567 |
. . . . . . . . . . . 12
   |
114 | 66, 60, 16, 113 | subaddrii 9812 |
. . . . . . . . . . 11
   |
115 | 114 | oveq1i 6213 |
. . . . . . . . . 10
                   |
116 | 69 | mulid2d 9519 |
. . . . . . . . . 10
                 |
117 | 115, 116 | syl5eq 2507 |
. . . . . . . . 9
                   |
118 | 112, 117 | eqtr3d 2497 |
. . . . . . . 8
                           |
119 | 118 | negeqd 9719 |
. . . . . . 7
                             |
120 | 111, 119 | eqtr3d 2497 |
. . . . . 6
                            |
121 | 120 | oveq1d 6218 |
. . . . 5
                    ;             ; 
     |
122 | 100, 110,
121 | 3eqtrd 2499 |
. . . 4
                                 ; 
     |
123 | | 7nn 10599 |
. . . . . . 7
 |
124 | 79, 123 | decnncl 10883 |
. . . . . 6
;  |
125 | 124 | nncni 10447 |
. . . . 5
;  |
126 | | quartlem1.q |
. . . . . 6
   |
127 | 126 | sqcld 12127 |
. . . . 5
       |
128 | | mulneg2 9897 |
. . . . 5
 ;      ;        ;        |
129 | 125, 127,
128 | sylancr 663 |
. . . 4
 ;        ;        |
130 | 122, 129 | oveq12d 6221 |
. . 3
                          ;                 ;      ;         |
131 | 69 | negcld 9821 |
. . . . 5
          |
132 | | mulcl 9481 |
. . . . . 6
 ;      ;        |
133 | 125, 127,
132 | sylancr 663 |
. . . . 5
 ;        |
134 | 131, 109,
133 | addsubd 9855 |
. . . 4
          ; 
   ;                ;       ; 
     |
135 | 131, 109 | addcld 9520 |
. . . . 5
         ; 
     |
136 | 135, 133 | negsubd 9840 |
. . . 4
          ; 
    ;                ;     ;         |
137 | | quartlem1.v |
. . . 4
          ;       ; 
     |
138 | 134, 136,
137 | 3eqtr4d 2505 |
. . 3
          ; 
    ;         |
139 | 130, 138 | eqtr2d 2496 |
. 2
                          ;          |
140 | 51, 139 | jca 532 |
1
                                             ;           |