Proof of Theorem 83prm
Step | Hyp | Ref
| Expression |
1 | | 8nn0 10920 |
. . 3
 |
2 | | 3nn 10796 |
. . 3
 |
3 | 1, 2 | decnncl 11092 |
. 2
;  |
4 | | 4nn0 10916 |
. . . 4
 |
5 | 1, 4 | deccl 11093 |
. . 3
;  |
6 | | 3nn0 10915 |
. . 3
 |
7 | | 1nn0 10913 |
. . 3
 |
8 | | 3lt10 10846 |
. . 3
 |
9 | | 8nn 10801 |
. . . 4
 |
10 | | 8lt10 10841 |
. . . 4
 |
11 | 9, 4, 1, 10 | declti 11104 |
. . 3
;  |
12 | 1, 5, 6, 7, 8, 11 | decltc 11101 |
. 2
; ;;   |
13 | | 1lt10 10848 |
. . 3
 |
14 | 9, 6, 7, 13 | declti 11104 |
. 2
;  |
15 | | 2cn 10707 |
. . . 4
 |
16 | 15 | mulid2i 9671 |
. . 3
   |
17 | | df-3 10696 |
. . 3
   |
18 | 1, 7, 16, 17 | dec2dvds 15083 |
. 2
;  |
19 | | 2nn0 10914 |
. . . 4
 |
20 | | 7nn0 10919 |
. . . 4
 |
21 | 19, 20 | deccl 11093 |
. . 3
;  |
22 | | 2nn 10795 |
. . 3
 |
23 | | 0nn0 10912 |
. . . 4
 |
24 | | eqid 2461 |
. . . 4
; ;  |
25 | 19 | dec0h 11095 |
. . . 4
;  |
26 | | 3t2e6 10789 |
. . . . . 6
   |
27 | 15 | addid2i 9846 |
. . . . . 6
   |
28 | 26, 27 | oveq12i 6326 |
. . . . 5
         |
29 | | 6p2e8 10779 |
. . . . 5
   |
30 | 28, 29 | eqtri 2483 |
. . . 4
       |
31 | 20 | nn0cni 10909 |
. . . . . 6
 |
32 | | 3cn 10711 |
. . . . . 6
 |
33 | | 7t3e21 11162 |
. . . . . 6
  ;  |
34 | 31, 32, 33 | mulcomli 9675 |
. . . . 5
  ;  |
35 | | 1p2e3 10762 |
. . . . 5
   |
36 | 19, 7, 19, 34, 35 | decaddi 11123 |
. . . 4
    ;  |
37 | 19, 20, 23, 19, 24, 25, 6, 6, 19, 30, 36 | decma2c 11119 |
. . 3
  ;   ;  |
38 | | 2lt3 10805 |
. . 3
 |
39 | 2, 21, 22, 37, 38 | ndvdsi 14439 |
. 2
;  |
40 | | 3lt5 10811 |
. . 3
 |
41 | 1, 2, 40 | dec5dvds 15084 |
. 2
;  |
42 | | 7nn 10800 |
. . 3
 |
43 | 7, 7 | deccl 11093 |
. . 3
;  |
44 | | 6nn 10799 |
. . 3
 |
45 | 44 | nnnn0i 10905 |
. . . 4
 |
46 | | eqid 2461 |
. . . 4
; ;  |
47 | 45 | dec0h 11095 |
. . . 4
;  |
48 | 31 | mulid1i 9670 |
. . . . . 6
   |
49 | | ax-1cn 9622 |
. . . . . . 7
 |
50 | 49 | addid2i 9846 |
. . . . . 6
   |
51 | 48, 50 | oveq12i 6326 |
. . . . 5
         |
52 | | 7p1e8 10767 |
. . . . 5
   |
53 | 51, 52 | eqtri 2483 |
. . . 4
       |
54 | 48 | oveq1i 6324 |
. . . . 5
       |
55 | | 7p6e13 11133 |
. . . . 5
  ;  |
56 | 54, 55 | eqtri 2483 |
. . . 4
    ;  |
57 | 7, 7, 23, 45, 46, 47, 20, 6, 7, 53, 56 | decma2c 11119 |
. . 3
  ;   ;  |
58 | | 6lt7 10819 |
. . 3
 |
59 | 42, 43, 44, 57, 58 | ndvdsi 14439 |
. 2
;  |
60 | | 1nn 10647 |
. . . 4
 |
61 | 7, 60 | decnncl 11092 |
. . 3
;  |
62 | 61 | nncni 10646 |
. . . . . 6
;  |
63 | 62, 31 | mulcomi 9674 |
. . . . 5
;   ;   |
64 | 63 | oveq1i 6324 |
. . . 4
 ;     ;    |
65 | 64, 57 | eqtri 2483 |
. . 3
 ;   ;  |
66 | | 6lt10 10843 |
. . . 4
 |
67 | 60, 7, 45, 66 | declti 11104 |
. . 3
;  |
68 | 61, 20, 44, 65, 67 | ndvdsi 14439 |
. 2
; ;  |
69 | 7, 2 | decnncl 11092 |
. . 3
;  |
70 | | 5nn 10798 |
. . 3
 |
71 | 70 | nnnn0i 10905 |
. . . 4
 |
72 | | eqid 2461 |
. . . 4
; ;  |
73 | 71 | dec0h 11095 |
. . . 4
;  |
74 | | 6cn 10718 |
. . . . . . 7
 |
75 | 74 | mulid2i 9671 |
. . . . . 6
   |
76 | 75, 27 | oveq12i 6326 |
. . . . 5
         |
77 | 76, 29 | eqtri 2483 |
. . . 4
       |
78 | | 6t3e18 11157 |
. . . . . 6
  ;  |
79 | 74, 32, 78 | mulcomli 9675 |
. . . . 5
  ;  |
80 | | 1p1e2 10750 |
. . . . 5
   |
81 | | 8p5e13 11137 |
. . . . 5
  ;  |
82 | 7, 1, 71, 79, 80, 6, 81 | decaddci 11124 |
. . . 4
    ;  |
83 | 7, 6, 23, 71, 72, 73, 45, 6, 19, 77, 82 | decmac 11118 |
. . 3
 ;   ;  |
84 | | 5lt10 10844 |
. . . 4
 |
85 | 60, 6, 71, 84 | declti 11104 |
. . 3
;  |
86 | 69, 45, 70, 83, 85 | ndvdsi 14439 |
. 2
; ;  |
87 | 7, 42 | decnncl 11092 |
. . 3
;  |
88 | 7, 70 | decnncl 11092 |
. . 3
;  |
89 | | eqid 2461 |
. . . 4
; ;  |
90 | | eqid 2461 |
. . . 4
; ;  |
91 | 4 | nn0cni 10909 |
. . . . . . 7
 |
92 | 91 | mulid2i 9671 |
. . . . . 6
   |
93 | | 3p1e4 10763 |
. . . . . . 7
   |
94 | 32, 49, 93 | addcomli 9850 |
. . . . . 6
   |
95 | 92, 94 | oveq12i 6326 |
. . . . 5
         |
96 | | 4p4e8 10774 |
. . . . 5
   |
97 | 95, 96 | eqtri 2483 |
. . . 4
       |
98 | | 7t4e28 11163 |
. . . . 5
  ;  |
99 | | 2p1e3 10761 |
. . . . 5
   |
100 | 19, 1, 71, 98, 99, 6, 81 | decaddci 11124 |
. . . 4
    ;  |
101 | 7, 20, 7, 71, 89, 90, 4, 6, 6,
97, 100 | decmac 11118 |
. . 3
 ;  ;  ;  |
102 | | 5lt7 10820 |
. . . 4
 |
103 | 7, 71, 42, 102 | declt 11100 |
. . 3
; ;  |
104 | 87, 4, 88, 101, 103 | ndvdsi 14439 |
. 2
; ;  |
105 | | 9nn 10802 |
. . . 4
 |
106 | 7, 105 | decnncl 11092 |
. . 3
;  |
107 | | 9nn0 10921 |
. . . 4
 |
108 | | eqid 2461 |
. . . 4
; ;  |
109 | 20 | dec0h 11095 |
. . . 4
;  |
110 | 91 | addid2i 9846 |
. . . . . 6
   |
111 | 92, 110 | oveq12i 6326 |
. . . . 5
         |
112 | 111, 96 | eqtri 2483 |
. . . 4
       |
113 | | 9t4e36 11176 |
. . . . 5
  ;  |
114 | 31, 74, 55 | addcomli 9850 |
. . . . 5
  ;  |
115 | 6, 45, 20, 113, 93, 6, 114 | decaddci 11124 |
. . . 4
    ;  |
116 | 7, 107, 23, 20, 108, 109, 4, 6, 4, 112, 115 | decmac 11118 |
. . 3
 ;   ;  |
117 | | 7lt10 10842 |
. . . 4
 |
118 | 60, 107, 20, 117 | declti 11104 |
. . 3
;  |
119 | 106, 4, 42, 116, 118 | ndvdsi 14439 |
. 2
; ;  |
120 | 19, 2 | decnncl 11092 |
. . 3
;  |
121 | | 4nn 10797 |
. . . 4
 |
122 | 7, 121 | decnncl 11092 |
. . 3
;  |
123 | | eqid 2461 |
. . . 4
; ;  |
124 | | eqid 2461 |
. . . 4
; ;  |
125 | 32, 15, 26 | mulcomli 9675 |
. . . . . 6
   |
126 | 125, 80 | oveq12i 6326 |
. . . . 5
         |
127 | 126, 29 | eqtri 2483 |
. . . 4
       |
128 | | 3t3e9 10790 |
. . . . . 6
   |
129 | 128 | oveq1i 6324 |
. . . . 5
       |
130 | | 9p4e13 11143 |
. . . . 5
  ;  |
131 | 129, 130 | eqtri 2483 |
. . . 4
    ;  |
132 | 19, 6, 7, 4, 123, 124, 6, 6, 7, 127, 131 | decmac 11118 |
. . 3
 ;  ;  ;  |
133 | | 4lt10 10845 |
. . . 4
 |
134 | | 1lt2 10804 |
. . . 4
 |
135 | 7, 19, 4, 6, 133, 134 | decltc 11101 |
. . 3
; ;  |
136 | 120, 6, 122, 132, 135 | ndvdsi 14439 |
. 2
; ;  |
137 | 3, 12, 14, 18, 39, 41, 59, 68, 86, 104, 119, 136 | prmlem2 15139 |
1
;  |