Proof of Theorem jm2.27a
Step | Hyp | Ref
| Expression |
1 | | jm2.27a23 |
. 2
Yrm |
2 | | 2z 11409 |
. . . . . 6
|
3 | | jm2.27a3 |
. . . . . . 7
|
4 | 3 | nnzd 11481 |
. . . . . 6
|
5 | | zmulcl 11426 |
. . . . . 6
|
6 | 2, 4, 5 | sylancr 695 |
. . . . 5
|
7 | | jm2.27a2 |
. . . . . 6
|
8 | 7 | nnzd 11481 |
. . . . 5
|
9 | | jm2.27a27 |
. . . . 5
|
10 | | jm2.27a21 |
. . . . 5
|
11 | | jm2.27a8 |
. . . . . . . 8
|
12 | 11 | nn0zd 11480 |
. . . . . . 7
|
13 | | jm2.27a19 |
. . . . . . . 8
|
14 | | congsym 37535 |
. . . . . . . 8
|
15 | 6, 12, 8, 13, 14 | syl22anc 1327 |
. . . . . . 7
|
16 | | jm2.27a17 |
. . . . . . . 8
|
17 | | jm2.27a13 |
. . . . . . . . . 10
|
18 | 11 | nn0ge0d 11354 |
. . . . . . . . . . . . 13
|
19 | | rmy0 37494 |
. . . . . . . . . . . . . 14
Yrm |
20 | 17, 19 | syl 17 |
. . . . . . . . . . . . 13
Yrm |
21 | | jm2.27a29 |
. . . . . . . . . . . . . 14
Yrm |
22 | 21 | eqcomd 2628 |
. . . . . . . . . . . . 13
Yrm |
23 | 18, 20, 22 | 3brtr4d 4685 |
. . . . . . . . . . . 12
Yrm
Yrm |
24 | | 0zd 11389 |
. . . . . . . . . . . . 13
|
25 | | lermy 37522 |
. . . . . . . . . . . . 13
Yrm
Yrm |
26 | 17, 24, 9, 25 | syl3anc 1326 |
. . . . . . . . . . . 12
Yrm Yrm |
27 | 23, 26 | mpbird 247 |
. . . . . . . . . . 11
|
28 | | elnn0z 11390 |
. . . . . . . . . . 11
|
29 | 9, 27, 28 | sylanbrc 698 |
. . . . . . . . . 10
|
30 | | jm2.16nn0 37571 |
. . . . . . . . . 10
Yrm |
31 | 17, 29, 30 | syl2anc 693 |
. . . . . . . . 9
Yrm |
32 | 21 | oveq1d 6665 |
. . . . . . . . 9
Yrm |
33 | 31, 32 | breqtrrd 4681 |
. . . . . . . 8
|
34 | | jm2.27a7 |
. . . . . . . . . . 11
|
35 | 34 | nn0zd 11480 |
. . . . . . . . . 10
|
36 | | peano2zm 11420 |
. . . . . . . . . 10
|
37 | 35, 36 | syl 17 |
. . . . . . . . 9
|
38 | 12, 9 | zsubcld 11487 |
. . . . . . . . 9
|
39 | | dvdstr 15018 |
. . . . . . . . 9
|
40 | 6, 37, 38, 39 | syl3anc 1326 |
. . . . . . . 8
|
41 | 16, 33, 40 | mp2and 715 |
. . . . . . 7
|
42 | | congtr 37532 |
. . . . . . 7
|
43 | 6, 8, 12, 9, 15, 41, 42 | syl222anc 1342 |
. . . . . 6
|
44 | 43 | orcd 407 |
. . . . 5
|
45 | | jm2.27a24 |
. . . . . . 7
|
46 | | zmulcl 11426 |
. . . . . . 7
|
47 | 2, 45, 46 | sylancr 695 |
. . . . . 6
|
48 | | zsqcl 12934 |
. . . . . . . . . . . . . 14
|
49 | 4, 48 | syl 17 |
. . . . . . . . . . . . 13
|
50 | | dvdsmul2 15004 |
. . . . . . . . . . . . 13
|
51 | 2, 49, 50 | sylancr 695 |
. . . . . . . . . . . 12
|
52 | | jm2.27a10 |
. . . . . . . . . . . . . . 15
|
53 | 52 | nn0zd 11480 |
. . . . . . . . . . . . . 14
|
54 | 53 | peano2zd 11485 |
. . . . . . . . . . . . 13
|
55 | | zmulcl 11426 |
. . . . . . . . . . . . . 14
|
56 | 2, 49, 55 | sylancr 695 |
. . . . . . . . . . . . 13
|
57 | | dvdsmultr2 15021 |
. . . . . . . . . . . . 13
|
58 | 49, 54, 56, 57 | syl3anc 1326 |
. . . . . . . . . . . 12
|
59 | 51, 58 | mpd 15 |
. . . . . . . . . . 11
|
60 | 1 | oveq1d 6665 |
. . . . . . . . . . 11
Yrm |
61 | | jm2.27a15 |
. . . . . . . . . . . 12
|
62 | | jm2.27a26 |
. . . . . . . . . . . 12
Yrm |
63 | 61, 62 | eqtr3d 2658 |
. . . . . . . . . . 11
Yrm |
64 | 59, 60, 63 | 3brtr3d 4684 |
. . . . . . . . . 10
Yrm
Yrm |
65 | | jm2.27a1 |
. . . . . . . . . . 11
|
66 | 54 | zred 11482 |
. . . . . . . . . . . . . . . 16
|
67 | 56 | zred 11482 |
. . . . . . . . . . . . . . . 16
|
68 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . . 18
|
69 | 52, 68 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
70 | 69 | nngt0d 11064 |
. . . . . . . . . . . . . . . 16
|
71 | | 2nn 11185 |
. . . . . . . . . . . . . . . . . 18
|
72 | 3 | nnsqcld 13029 |
. . . . . . . . . . . . . . . . . 18
|
73 | | nnmulcl 11043 |
. . . . . . . . . . . . . . . . . 18
|
74 | 71, 72, 73 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
|
75 | 74 | nngt0d 11064 |
. . . . . . . . . . . . . . . 16
|
76 | 66, 67, 70, 75 | mulgt0d 10192 |
. . . . . . . . . . . . . . 15
|
77 | 76, 61 | breqtrrd 4681 |
. . . . . . . . . . . . . 14
|
78 | | rmy0 37494 |
. . . . . . . . . . . . . . 15
Yrm |
79 | 65, 78 | syl 17 |
. . . . . . . . . . . . . 14
Yrm |
80 | 62 | eqcomd 2628 |
. . . . . . . . . . . . . 14
Yrm |
81 | 77, 79, 80 | 3brtr4d 4685 |
. . . . . . . . . . . . 13
Yrm
Yrm |
82 | | ltrmy 37519 |
. . . . . . . . . . . . . 14
Yrm Yrm |
83 | 65, 24, 45, 82 | syl3anc 1326 |
. . . . . . . . . . . . 13
Yrm Yrm |
84 | 81, 83 | mpbird 247 |
. . . . . . . . . . . 12
|
85 | | elnnz 11387 |
. . . . . . . . . . . 12
|
86 | 45, 84, 85 | sylanbrc 698 |
. . . . . . . . . . 11
|
87 | 3 | nngt0d 11064 |
. . . . . . . . . . . . . 14
|
88 | 1 | eqcomd 2628 |
. . . . . . . . . . . . . 14
Yrm |
89 | 87, 79, 88 | 3brtr4d 4685 |
. . . . . . . . . . . . 13
Yrm
Yrm |
90 | | ltrmy 37519 |
. . . . . . . . . . . . . 14
Yrm Yrm |
91 | 65, 24, 10, 90 | syl3anc 1326 |
. . . . . . . . . . . . 13
Yrm Yrm |
92 | 89, 91 | mpbird 247 |
. . . . . . . . . . . 12
|
93 | | elnnz 11387 |
. . . . . . . . . . . 12
|
94 | 10, 92, 93 | sylanbrc 698 |
. . . . . . . . . . 11
|
95 | | jm2.20nn 37564 |
. . . . . . . . . . 11
Yrm
Yrm
Yrm |
96 | 65, 86, 94, 95 | syl3anc 1326 |
. . . . . . . . . 10
Yrm Yrm Yrm |
97 | 64, 96 | mpbid 222 |
. . . . . . . . 9
Yrm |
98 | 1, 4 | eqeltrrd 2702 |
. . . . . . . . . 10
Yrm |
99 | | muldvds2 15007 |
. . . . . . . . . 10
Yrm Yrm Yrm |
100 | 10, 98, 45, 99 | syl3anc 1326 |
. . . . . . . . 9
Yrm Yrm |
101 | 97, 100 | mpd 15 |
. . . . . . . 8
Yrm |
102 | 1, 101 | eqbrtrd 4675 |
. . . . . . 7
|
103 | 2 | a1i 11 |
. . . . . . . 8
|
104 | | dvdscmul 15008 |
. . . . . . . 8
|
105 | 4, 45, 103, 104 | syl3anc 1326 |
. . . . . . 7
|
106 | 102, 105 | mpd 15 |
. . . . . 6
|
107 | | jm2.27a25 |
. . . . . . . . . 10
Xrm |
108 | | jm2.27a6 |
. . . . . . . . . . 11
|
109 | 108 | nn0zd 11480 |
. . . . . . . . . 10
|
110 | 107, 109 | eqeltrrd 2702 |
. . . . . . . . 9
Xrm |
111 | | frmy 37479 |
. . . . . . . . . . 11
Yrm
|
112 | 111 | fovcl 6765 |
. . . . . . . . . 10
Yrm |
113 | 65, 9, 112 | syl2anc 693 |
. . . . . . . . 9
Yrm |
114 | 21, 12 | eqeltrrd 2702 |
. . . . . . . . 9
Yrm |
115 | | eluzelz 11697 |
. . . . . . . . . . . . 13
|
116 | 65, 115 | syl 17 |
. . . . . . . . . . . 12
|
117 | | jm2.27a16 |
. . . . . . . . . . . 12
|
118 | | congsym 37535 |
. . . . . . . . . . . 12
|
119 | 109, 35, 116, 117, 118 | syl22anc 1327 |
. . . . . . . . . . 11
|
120 | 107, 119 | eqbrtrrd 4677 |
. . . . . . . . . 10
Xrm
|
121 | | jm2.15nn0 37570 |
. . . . . . . . . . 11
Yrm
Yrm |
122 | 65, 17, 29, 121 | syl3anc 1326 |
. . . . . . . . . 10
Yrm Yrm |
123 | 116, 35 | zsubcld 11487 |
. . . . . . . . . . 11
|
124 | 113, 114 | zsubcld 11487 |
. . . . . . . . . . 11
Yrm Yrm |
125 | | dvdstr 15018 |
. . . . . . . . . . 11
Xrm Yrm Yrm Xrm
Yrm Yrm Xrm
Yrm
Yrm |
126 | 110, 123,
124, 125 | syl3anc 1326 |
. . . . . . . . . 10
Xrm
Yrm Yrm Xrm Yrm Yrm |
127 | 120, 122,
126 | mp2and 715 |
. . . . . . . . 9
Xrm Yrm Yrm |
128 | | jm2.27a18 |
. . . . . . . . . 10
|
129 | 21, 1 | oveq12d 6668 |
. . . . . . . . . 10
Yrm Yrm |
130 | 128, 107,
129 | 3brtr3d 4684 |
. . . . . . . . 9
Xrm Yrm Yrm |
131 | | congtr 37532 |
. . . . . . . . 9
Xrm Yrm Yrm
Yrm
Xrm Yrm Yrm Xrm Yrm Yrm
Xrm
Yrm Yrm |
132 | 110, 113,
114, 98, 127, 130, 131 | syl222anc 1342 |
. . . . . . . 8
Xrm Yrm Yrm |
133 | 132 | orcd 407 |
. . . . . . 7
Xrm Yrm Yrm Xrm
Yrm
Yrm |
134 | | jm2.26 37569 |
. . . . . . . 8
Xrm Yrm Yrm Xrm Yrm Yrm
|
135 | 65, 86, 9, 10, 134 | syl22anc 1327 |
. . . . . . 7
Xrm Yrm Yrm
Xrm Yrm Yrm
|
136 | 133, 135 | mpbid 222 |
. . . . . 6
|
137 | | dvdsacongtr 37551 |
. . . . . 6
|
138 | 47, 9, 10, 6, 106, 136, 137 | syl222anc 1342 |
. . . . 5
|
139 | | acongtr 37545 |
. . . . 5
|
140 | 6, 8, 9, 10, 44, 138, 139 | syl222anc 1342 |
. . . 4
|
141 | 7 | nnnn0d 11351 |
. . . . . 6
|
142 | 3 | nnnn0d 11351 |
. . . . . 6
|
143 | | jm2.27a20 |
. . . . . 6
|
144 | | elfz2nn0 12431 |
. . . . . 6
|
145 | 141, 142,
143, 144 | syl3anbrc 1246 |
. . . . 5
|
146 | 94 | nnnn0d 11351 |
. . . . . 6
|
147 | | rmygeid 37531 |
. . . . . . . 8
Yrm |
148 | 65, 146, 147 | syl2anc 693 |
. . . . . . 7
Yrm |
149 | 148, 1 | breqtrrd 4681 |
. . . . . 6
|
150 | | elfz2nn0 12431 |
. . . . . 6
|
151 | 146, 142,
149, 150 | syl3anbrc 1246 |
. . . . 5
|
152 | | acongeq 37550 |
. . . . 5
|
153 | 3, 145, 151, 152 | syl3anc 1326 |
. . . 4
|
154 | 140, 153 | mpbird 247 |
. . 3
|
155 | 154 | oveq2d 6666 |
. 2
Yrm
Yrm |
156 | 1, 155 | eqtr4d 2659 |
1
Yrm |