Step | Hyp | Ref
| Expression |
1 | | prmlem2.n |
. 2
 |
2 | | prmlem2.gt |
. 2
 |
3 | | prmlem2.2 |
. 2
 |
4 | | prmlem2.3 |
. 2
 |
5 | | eluzelre 11197 |
. . . . . . . . . . . . . . . . . . . 20
   ; 
  |
6 | 5 | resqcld 12473 |
. . . . . . . . . . . . . . . . . . 19
   ;        |
7 | | eluzle 11199 |
. . . . . . . . . . . . . . . . . . . 20
   ;  ;   |
8 | | 2nn0 10914 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
9 | | 9nn0 10921 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
10 | 8, 9 | deccl 11093 |
. . . . . . . . . . . . . . . . . . . . . 22
;  |
11 | 10 | nn0rei 10908 |
. . . . . . . . . . . . . . . . . . . . 21
;  |
12 | 10 | nn0ge0i 10925 |
. . . . . . . . . . . . . . . . . . . . 21
;  |
13 | | le2sq2 12381 |
. . . . . . . . . . . . . . . . . . . . 21
  ;
;  
;
 
;   
      |
14 | 11, 12, 13 | mpanl12 693 |
. . . . . . . . . . . . . . . . . . . 20
  ;  ;   
      |
15 | 5, 7, 14 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . 19
   ;  ;   
      |
16 | 1 | nnrei 10645 |
. . . . . . . . . . . . . . . . . . . 20
 |
17 | 11 | resqcli 12391 |
. . . . . . . . . . . . . . . . . . . 20
;     |
18 | | prmlem2.lt |
. . . . . . . . . . . . . . . . . . . . . 22
;;   |
19 | 10 | nn0cni 10909 |
. . . . . . . . . . . . . . . . . . . . . . . 24
;  |
20 | 19 | sqvali 12385 |
. . . . . . . . . . . . . . . . . . . . . . 23
;    ; ;   |
21 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . . . 24
; ;  |
22 | | 1nn0 10913 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
23 | | 6nn0 10918 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
24 | 8, 23 | deccl 11093 |
. . . . . . . . . . . . . . . . . . . . . . . 24
;  |
25 | | 5nn0 10917 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
26 | | 8nn0 10920 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
27 | 19 | 2timesi 10758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 ;  ; ;   |
28 | | 2p2e4 10755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
29 | 28 | oveq1i 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
30 | | 4p1e5 10764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
31 | 29, 30 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
32 | | 9p9e18 11148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  ;  |
33 | 8, 9, 8, 9, 21, 21, 31, 26, 32 | decaddc 11121 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
; ;  ;  |
34 | 27, 33 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 ;  ;  |
35 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
; ;  |
36 | | 5p2e7 10775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
37 | 36 | oveq1i 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
38 | | 7p1e8 10767 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
39 | 37, 38 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
40 | | 4nn0 10916 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
41 | | 8p6e14 11138 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  ;  |
42 | 25, 26, 8, 23, 34, 35, 39, 40, 41 | decaddc 11121 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  ;  ;  ;  |
43 | | 9t2e18 11174 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  ;  |
44 | | 1p1e2 10750 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
45 | | 8p8e16 11140 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  ;  |
46 | 22, 26, 26, 43, 44, 23, 45 | decaddci 11124 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ;  |
47 | | 9t9e81 11181 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  ;  |
48 | 9, 8, 9, 21, 22, 26, 46, 47 | decmul2c 11127 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 ;  ;;   |
49 | 10, 8, 9, 21, 22, 24, 42, 48 | decmul1c 11126 |
. . . . . . . . . . . . . . . . . . . . . . 23
; ;  ;;   |
50 | 20, 49 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . . . 22
;    ;;   |
51 | 18, 50 | breqtrri 4441 |
. . . . . . . . . . . . . . . . . . . . 21
;     |
52 | | ltletr 9750 |
. . . . . . . . . . . . . . . . . . . . 21
  ;           ;    ;   
            |
53 | 51, 52 | mpani 687 |
. . . . . . . . . . . . . . . . . . . 20
  ;          ;   
           |
54 | 16, 17, 53 | mp3an12 1363 |
. . . . . . . . . . . . . . . . . . 19
      ;   
           |
55 | 6, 15, 54 | sylc 62 |
. . . . . . . . . . . . . . . . . 18
   ;        |
56 | | ltnle 9738 |
. . . . . . . . . . . . . . . . . . 19
           
       |
57 | 16, 6, 56 | sylancr 674 |
. . . . . . . . . . . . . . . . . 18
   ;          
   |
58 | 55, 57 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
   ;     
  |
59 | 58 | pm2.21d 110 |
. . . . . . . . . . . . . . . 16
   ;          |
60 | 59 | adantld 473 |
. . . . . . . . . . . . . . 15
   ;    
       
   |
61 | 60 | adantl 472 |
. . . . . . . . . . . . . 14
  ;   ;            
    |
62 | | 9nn 10802 |
. . . . . . . . . . . . . . . 16
 |
63 | | 3nn 10796 |
. . . . . . . . . . . . . . . 16
 |
64 | | 1lt9 10839 |
. . . . . . . . . . . . . . . 16
 |
65 | | 1lt3 10806 |
. . . . . . . . . . . . . . . 16
 |
66 | | 9t3e27 11175 |
. . . . . . . . . . . . . . . 16
  ;  |
67 | 62, 63, 64, 65, 66 | nprmi 14687 |
. . . . . . . . . . . . . . 15
;  |
68 | 67 | pm2.21i 136 |
. . . . . . . . . . . . . 14
; ;   |
69 | | 7nn0 10919 |
. . . . . . . . . . . . . . 15
 |
70 | | eqid 2461 |
. . . . . . . . . . . . . . 15
; ;  |
71 | | 7p2e9 10782 |
. . . . . . . . . . . . . . 15
   |
72 | 8, 69, 8, 70, 71 | decaddi 11123 |
. . . . . . . . . . . . . 14
;  ;  |
73 | 61, 68, 72 | prmlem0 15125 |
. . . . . . . . . . . . 13
  ;   ;            
    |
74 | | 5nn 10798 |
. . . . . . . . . . . . . . 15
 |
75 | | 1lt5 10813 |
. . . . . . . . . . . . . . 15
 |
76 | | 5t5e25 11155 |
. . . . . . . . . . . . . . 15
  ;  |
77 | 74, 74, 75, 75, 76 | nprmi 14687 |
. . . . . . . . . . . . . 14
;  |
78 | 77 | pm2.21i 136 |
. . . . . . . . . . . . 13
; ;   |
79 | | eqid 2461 |
. . . . . . . . . . . . . 14
; ;  |
80 | 8, 25, 8, 79, 36 | decaddi 11123 |
. . . . . . . . . . . . 13
;  ;  |
81 | 73, 78, 80 | prmlem0 15125 |
. . . . . . . . . . . 12
  ;   ;            
    |
82 | | prmlem2.23 |
. . . . . . . . . . . . 13
;  |
83 | 82 | a1i 11 |
. . . . . . . . . . . 12
; ;   |
84 | | 3nn0 10915 |
. . . . . . . . . . . . 13
 |
85 | | eqid 2461 |
. . . . . . . . . . . . 13
; ;  |
86 | | 3p2e5 10770 |
. . . . . . . . . . . . 13
   |
87 | 8, 84, 8, 85, 86 | decaddi 11123 |
. . . . . . . . . . . 12
;  ;  |
88 | 81, 83, 87 | prmlem0 15125 |
. . . . . . . . . . 11
  ;   ;            
    |
89 | | 7nn 10800 |
. . . . . . . . . . . . 13
 |
90 | | 1lt7 10824 |
. . . . . . . . . . . . 13
 |
91 | | 7t3e21 11162 |
. . . . . . . . . . . . 13
  ;  |
92 | 89, 63, 90, 65, 91 | nprmi 14687 |
. . . . . . . . . . . 12
;  |
93 | 92 | pm2.21i 136 |
. . . . . . . . . . 11
; ;   |
94 | | eqid 2461 |
. . . . . . . . . . . 12
; ;  |
95 | | 1p2e3 10762 |
. . . . . . . . . . . 12
   |
96 | 8, 22, 8, 94, 95 | decaddi 11123 |
. . . . . . . . . . 11
;  ;  |
97 | 88, 93, 96 | prmlem0 15125 |
. . . . . . . . . 10
  ;   ;            
    |
98 | | prmlem2.19 |
. . . . . . . . . . 11
;  |
99 | 98 | a1i 11 |
. . . . . . . . . 10
; ;   |
100 | | eqid 2461 |
. . . . . . . . . . 11
; ;  |
101 | | 9p2e11 11141 |
. . . . . . . . . . 11
  ;  |
102 | 22, 9, 8, 100, 44, 22, 101 | decaddci 11124 |
. . . . . . . . . 10
;  ;  |
103 | 97, 99, 102 | prmlem0 15125 |
. . . . . . . . 9
  ;   ;            
    |
104 | | prmlem2.17 |
. . . . . . . . . 10
;  |
105 | 104 | a1i 11 |
. . . . . . . . 9
; ;   |
106 | | eqid 2461 |
. . . . . . . . . 10
; ;  |
107 | 22, 69, 8, 106, 71 | decaddi 11123 |
. . . . . . . . 9
;  ;  |
108 | 103, 105,
107 | prmlem0 15125 |
. . . . . . . 8
  ;   ;            
    |
109 | | 5t3e15 11153 |
. . . . . . . . . 10
  ;  |
110 | 74, 63, 75, 65, 109 | nprmi 14687 |
. . . . . . . . 9
;  |
111 | 110 | pm2.21i 136 |
. . . . . . . 8
; ;   |
112 | | eqid 2461 |
. . . . . . . . 9
; ;  |
113 | 22, 25, 8, 112, 36 | decaddi 11123 |
. . . . . . . 8
;  ;  |
114 | 108, 111,
113 | prmlem0 15125 |
. . . . . . 7
  ;   ;            
    |
115 | | prmlem2.13 |
. . . . . . . 8
;  |
116 | 115 | a1i 11 |
. . . . . . 7
; ;   |
117 | | eqid 2461 |
. . . . . . . 8
; ;  |
118 | 22, 84, 8, 117, 86 | decaddi 11123 |
. . . . . . 7
;  ;  |
119 | 114, 116,
118 | prmlem0 15125 |
. . . . . 6
  ;   ;            
    |
120 | | prmlem2.11 |
. . . . . . 7
;  |
121 | 120 | a1i 11 |
. . . . . 6
; ;   |
122 | | eqid 2461 |
. . . . . . 7
; ;  |
123 | 22, 22, 8, 122, 95 | decaddi 11123 |
. . . . . 6
;  ;  |
124 | 119, 121,
123 | prmlem0 15125 |
. . . . 5
  ;   ;            
    |
125 | | 9nprm 15132 |
. . . . . 6
 |
126 | 125 | pm2.21i 136 |
. . . . 5

  |
127 | 124, 126,
101 | prmlem0 15125 |
. . . 4
 
              
    |
128 | | prmlem2.7 |
. . . . 5
 |
129 | 128 | a1i 11 |
. . . 4

  |
130 | 127, 129,
71 | prmlem0 15125 |
. . 3
 
              
    |
131 | | prmlem2.5 |
. . . 4
 |
132 | 131 | a1i 11 |
. . 3

  |
133 | 130, 132,
36 | prmlem0 15125 |
. 2
 
              
    |
134 | 1, 2, 3, 4, 133 | prmlem1a 15126 |
1
 |