Step | Hyp | Ref
| Expression |
1 | | elnn0 10895 |
. . . 4

    |
2 | | eleq1 2537 |
. . . . . 6
 
   |
3 | | eleq1 2537 |
. . . . . 6
 
   |
4 | | eleq1 2537 |
. . . . . 6
 
   |
5 | | eleq1 2537 |
. . . . . 6
   
     |
6 | | eleq1 2537 |
. . . . . 6
 
   |
7 | | abs1 13437 |
. . . . . . . . . . 11
     |
8 | 7 | oveq1i 6318 |
. . . . . . . . . 10
             |
9 | | sq1 12407 |
. . . . . . . . . 10
     |
10 | 8, 9 | eqtri 2493 |
. . . . . . . . 9
         |
11 | | abs0 13425 |
. . . . . . . . . . 11
     |
12 | 11 | oveq1i 6318 |
. . . . . . . . . 10
             |
13 | | sq0 12404 |
. . . . . . . . . 10
     |
14 | 12, 13 | eqtri 2493 |
. . . . . . . . 9
         |
15 | 10, 14 | oveq12i 6320 |
. . . . . . . 8
                     |
16 | | 1p0e1 10744 |
. . . . . . . 8
   |
17 | 15, 16 | eqtri 2493 |
. . . . . . 7
                   |
18 | | 1z 10991 |
. . . . . . . . 9
 |
19 | | zgz 14956 |
. . . . . . . . 9
    ![] ]](rbrack.gif)  |
20 | 18, 19 | ax-mp 5 |
. . . . . . . 8
   ![] ]](rbrack.gif) |
21 | | 0z 10972 |
. . . . . . . . 9
 |
22 | | zgz 14956 |
. . . . . . . . 9
    ![] ]](rbrack.gif)  |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
   ![] ]](rbrack.gif) |
24 | | 4sq.1 |
. . . . . . . . 9
 
                           |
25 | 24 | 4sqlem4a 14974 |
. . . . . . . 8
    
   ![] ]](rbrack.gif)
                    |
26 | 20, 23, 25 | mp2an 686 |
. . . . . . 7
                   |
27 | 17, 26 | eqeltrri 2546 |
. . . . . 6
 |
28 | | eleq1 2537 |
. . . . . . 7
 
   |
29 | | eldifsn 4088 |
. . . . . . . . 9
    

   |
30 | | oddprm 14844 |
. . . . . . . . . . 11
           |
31 | 30 | adantr 472 |
. . . . . . . . . 10
              
      |
32 | | eldifi 3544 |
. . . . . . . . . . . . . . . 16
       |
33 | 32 | adantr 472 |
. . . . . . . . . . . . . . 15
              
  |
34 | | prmnn 14704 |
. . . . . . . . . . . . . . 15

  |
35 | | nncn 10639 |
. . . . . . . . . . . . . . 15
   |
36 | 33, 34, 35 | 3syl 18 |
. . . . . . . . . . . . . 14
              
  |
37 | | ax-1cn 9615 |
. . . . . . . . . . . . . 14
 |
38 | | subcl 9894 |
. . . . . . . . . . . . . 14
 
     |
39 | 36, 37, 38 | sylancl 675 |
. . . . . . . . . . . . 13
              
    |
40 | | 2cnd 10704 |
. . . . . . . . . . . . 13
              
  |
41 | | 2ne0 10724 |
. . . . . . . . . . . . . 14
 |
42 | 41 | a1i 11 |
. . . . . . . . . . . . 13
              
  |
43 | 39, 40, 42 | divcan2d 10407 |
. . . . . . . . . . . 12
              
          |
44 | 43 | oveq1d 6323 |
. . . . . . . . . . 11
              
              |
45 | | npcan 9904 |
. . . . . . . . . . . 12
 
       |
46 | 36, 37, 45 | sylancl 675 |
. . . . . . . . . . 11
              
      |
47 | 44, 46 | eqtr2d 2506 |
. . . . . . . . . 10
              
          |
48 | 43 | oveq2d 6324 |
. . . . . . . . . . . 12
              
                  |
49 | | nnm1nn0 10935 |
. . . . . . . . . . . . . . 15
     |
50 | 33, 34, 49 | 3syl 18 |
. . . . . . . . . . . . . 14
              
    |
51 | | elnn0uz 11220 |
. . . . . . . . . . . . . 14
  
        |
52 | 50, 51 | sylib 201 |
. . . . . . . . . . . . 13
              
        |
53 | | eluzfz1 11832 |
. . . . . . . . . . . . 13
      
        |
54 | | fzsplit 11851 |
. . . . . . . . . . . . 13
                             |
55 | 52, 53, 54 | 3syl 18 |
. . . . . . . . . . . 12
              
                      |
56 | 48, 55 | eqtrd 2505 |
. . . . . . . . . . 11
              
                          |
57 | | fzsn 11866 |
. . . . . . . . . . . . . . 15
         |
58 | 21, 57 | ax-mp 5 |
. . . . . . . . . . . . . 14
       |
59 | 14, 14 | oveq12i 6320 |
. . . . . . . . . . . . . . . . 17
                     |
60 | | 00id 9826 |
. . . . . . . . . . . . . . . . 17
   |
61 | 59, 60 | eqtri 2493 |
. . . . . . . . . . . . . . . 16
                   |
62 | 24 | 4sqlem4a 14974 |
. . . . . . . . . . . . . . . . 17
    
   ![] ]](rbrack.gif)
                    |
63 | 23, 23, 62 | mp2an 686 |
. . . . . . . . . . . . . . . 16
                   |
64 | 61, 63 | eqeltrri 2546 |
. . . . . . . . . . . . . . 15
 |
65 | | snssi 4107 |
. . . . . . . . . . . . . . 15
  
  |
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . . 14
 
 |
67 | 58, 66 | eqsstri 3448 |
. . . . . . . . . . . . 13
     |
68 | 67 | a1i 11 |
. . . . . . . . . . . 12
              
      |
69 | | 0p1e1 10743 |
. . . . . . . . . . . . . 14
   |
70 | 69 | oveq1i 6318 |
. . . . . . . . . . . . 13
               |
71 | | simpr 468 |
. . . . . . . . . . . . . 14
              
          |
72 | | dfss3 3408 |
. . . . . . . . . . . . . 14
      
          |
73 | 71, 72 | sylibr 217 |
. . . . . . . . . . . . 13
              
        |
74 | 70, 73 | syl5eqss 3462 |
. . . . . . . . . . . 12
              
          |
75 | 68, 74 | unssd 3601 |
. . . . . . . . . . 11
              
                |
76 | 56, 75 | eqsstrd 3452 |
. . . . . . . . . 10
              
            |
77 | | oveq1 6315 |
. . . . . . . . . . . 12
       |
78 | 77 | eleq1d 2533 |
. . . . . . . . . . 11
   
     |
79 | 78 | cbvrabv 3030 |
. . . . . . . . . 10
         |
80 | | eqid 2471 |
. . . . . . . . . 10
inf       inf        |
81 | 24, 31, 47, 33, 76, 79, 80 | 4sqlem18 14991 |
. . . . . . . . 9
              
  |
82 | 29, 81 | sylanbr 481 |
. . . . . . . 8
            
  |
83 | 82 | an32s 821 |
. . . . . . 7
            
  |
84 | 10, 10 | oveq12i 6320 |
. . . . . . . . . 10
                     |
85 | | df-2 10690 |
. . . . . . . . . 10
   |
86 | 84, 85 | eqtr4i 2496 |
. . . . . . . . 9
                   |
87 | 24 | 4sqlem4a 14974 |
. . . . . . . . . 10
    
   ![] ]](rbrack.gif)
                    |
88 | 20, 20, 87 | mp2an 686 |
. . . . . . . . 9
                   |
89 | 86, 88 | eqeltrri 2546 |
. . . . . . . 8
 |
90 | 89 | a1i 11 |
. . . . . . 7
  
          |
91 | 28, 83, 90 | pm2.61ne 2728 |
. . . . . 6
  
          |
92 | 24 | mul4sq 14977 |
. . . . . . 7
 
     |
93 | 92 | a1i 11 |
. . . . . 6
          
 
      |
94 | 2, 3, 4, 5, 6, 27,
91, 93 | prmind2 14714 |
. . . . 5
   |
95 | | id 22 |
. . . . . 6
   |
96 | 95, 64 | syl6eqel 2557 |
. . . . 5
   |
97 | 94, 96 | jaoi 386 |
. . . 4
 
   |
98 | 1, 97 | sylbi 200 |
. . 3

  |
99 | 98 | ssriv 3422 |
. 2
 |
100 | 24 | 4sqlem1 14971 |
. 2
 |
101 | 99, 100 | eqssi 3434 |
1
 |