Proof of Theorem gausslemma2dlem3
Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.r |
. . 3
                      |
2 | | oveq1 5917 |
. . . . . . 7
       |
3 | 2 | breq1d 4039 |
. . . . . 6
     
       |
4 | 2 | oveq2d 5926 |
. . . . . 6
 
         |
5 | 3, 2, 4 | ifbieq12d 3583 |
. . . . 5
                                 |
6 | 5 | adantl 277 |
. . . 4
                                           |
7 | | gausslemma2d.p |
. . . . . . . 8
       |
8 | 7 | gausslemma2dlem0a 15107 |
. . . . . . 7
   |
9 | | elfz2 10071 |
. . . . . . . . . 10
      
   
   
    |
10 | | gausslemma2d.m |
. . . . . . . . . . . . . . . . 17
       |
11 | 10 | oveq1i 5920 |
. . . . . . . . . . . . . . . 16
      
    |
12 | 11 | breq1i 4036 |
. . . . . . . . . . . . . . 15
  
          |
13 | | nnz 9326 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
14 | | 4nn 9135 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
15 | | znq 9679 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
16 | 13, 14, 15 | sylancl 413 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
17 | 16 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
18 | | flqlelt 10335 |
. . . . . . . . . . . . . . . . . . . . 21
                  
      |
19 | 17, 18 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
 
     
    

           |
20 | | nnre 8979 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
21 | | 4re 9049 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
22 | 21 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
23 | | 4ap0 9071 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
#  |
24 | 23 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 #   |
25 | 20, 22, 24 | redivclapd 8844 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
26 | 25 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
27 | 16 | flqcld 10336 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
28 | 27 | zred 9429 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
29 | | peano2re 8145 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
30 | 28, 29 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
31 | 30 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     
     |
32 | | zre 9311 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
33 | 32 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
34 | | ltleletr 8091 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
  
         
                 |
35 | 26, 31, 33, 34 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . . . 22
 
         
                 |
36 | 35 | expd 258 |
. . . . . . . . . . . . . . . . . . . . 21
 
                      
    |
37 | 36 | adantld 278 |
. . . . . . . . . . . . . . . . . . . 20
 
          
      
         
  
      |
38 | 19, 37 | mpd 13 |
. . . . . . . . . . . . . . . . . . 19
 
           
   |
39 | 38 | imp 124 |
. . . . . . . . . . . . . . . . . 18
            
    |
40 | 20 | rehalfcld 9219 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
41 | 40 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
42 | | 2re 9042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
43 | 42 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
44 | 32, 43 | remulcld 8040 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
45 | 44 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
46 | | 2pos 9063 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
47 | 42, 46 | pm3.2i 272 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
48 | 47 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
49 | | lediv1 8878 |
. . . . . . . . . . . . . . . . . . . . 21
        
                |
50 | 41, 45, 48, 49 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . 20
 
         
       |
51 | | nncn 8980 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
52 | | 2cnd 9045 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
53 | | 2ap0 9065 |
. . . . . . . . . . . . . . . . . . . . . . . 24
#  |
54 | 53 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . 23
 #   |
55 | 51, 52, 52, 54, 54 | divdivap1d 8831 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
56 | | 2t2e4 9126 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
57 | 56 | oveq2i 5921 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
58 | 55, 57 | eqtrdi 2242 |
. . . . . . . . . . . . . . . . . . . . 21
         |
59 | | zcn 9312 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
60 | | 2cnd 9045 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
61 | 53 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . 22
 #   |
62 | 59, 60, 61 | divcanap4d 8805 |
. . . . . . . . . . . . . . . . . . . . 21
       |
63 | 58, 62 | breqan12rd 4046 |
. . . . . . . . . . . . . . . . . . . 20
 
           
   |
64 | 50, 63 | bitrd 188 |
. . . . . . . . . . . . . . . . . . 19
 
       
   |
65 | 64 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
            
          |
66 | 39, 65 | mpbird 167 |
. . . . . . . . . . . . . . . . 17
            
      |
67 | 66 | exp31 364 |
. . . . . . . . . . . . . . . 16
 
     
  
        |
68 | 67 | com23 78 |
. . . . . . . . . . . . . . 15
      
  
         |
69 | 12, 68 | biimtrid 152 |
. . . . . . . . . . . . . 14
   
         |
70 | 69 | 3ad2ant3 1022 |
. . . . . . . . . . . . 13
   
   
         |
71 | 70 | com12 30 |
. . . . . . . . . . . 12
      
   
      |
72 | 71 | adantr 276 |
. . . . . . . . . . 11
   
      
        |
73 | 72 | impcom 125 |
. . . . . . . . . 10
    
   
 

       |
74 | 9, 73 | sylbi 121 |
. . . . . . . . 9
       
       |
75 | 74 | impcom 125 |
. . . . . . . 8
 
 
           |
76 | | elfzelz 10081 |
. . . . . . . . . . 11
         |
77 | 76 | zred 9429 |
. . . . . . . . . 10
         |
78 | 42 | a1i 9 |
. . . . . . . . . 10
         |
79 | 77, 78 | remulcld 8040 |
. . . . . . . . 9
           |
80 | | lenlt 8085 |
. . . . . . . . 9
           
       |
81 | 40, 79, 80 | syl2an 289 |
. . . . . . . 8
 
 
         
       |
82 | 75, 81 | mpbid 147 |
. . . . . . 7
 
 
    
      |
83 | 8, 82 | sylan 283 |
. . . . . 6
 
             |
84 | 83 | adantr 276 |
. . . . 5
                 |
85 | 84 | iffalsed 3567 |
. . . 4
                                |
86 | 6, 85 | eqtrd 2226 |
. . 3
                                |
87 | 7, 10 | gausslemma2dlem0d 15110 |
. . . . . 6
   |
88 | | nn0p1nn 9269 |
. . . . . . 7

    |
89 | | nnuz 9618 |
. . . . . . 7
     |
90 | 88, 89 | eleqtrdi 2286 |
. . . . . 6

        |
91 | 87, 90 | syl 14 |
. . . . 5
         |
92 | | fzss1 10119 |
. . . . 5
      
 
          |
93 | 91, 92 | syl 14 |
. . . 4
      
      |
94 | 93 | sselda 3179 |
. . 3
 
             |
95 | 8 | nnzd 9428 |
. . . . 5
   |
96 | 95 | adantr 276 |
. . . 4
 
         |
97 | 76 | adantl 277 |
. . . . 5
 
         |
98 | | 2z 9335 |
. . . . . 6
 |
99 | 98 | a1i 9 |
. . . . 5
 
         |
100 | 97, 99 | zmulcld 9435 |
. . . 4
 
           |
101 | 96, 100 | zsubcld 9434 |
. . 3
 
       
     |
102 | 1, 86, 94, 101 | fvmptd2 5631 |
. 2
 
                 |
103 | 102 | ralrimiva 2567 |
1
                   |