Proof of Theorem fldivp1
Step | Hyp | Ref
| Expression |
1 | | nnz 9218 |
. . . . . . . . 9
|
2 | | nnne0 8893 |
. . . . . . . . 9
|
3 | | peano2z 9235 |
. . . . . . . . . 10
|
4 | 3 | adantr 274 |
. . . . . . . . 9
|
5 | | dvdsval2 11739 |
. . . . . . . . 9
|
6 | 1, 2, 4, 5 | syl2an23an 1294 |
. . . . . . . 8
|
7 | 6 | biimpa 294 |
. . . . . . 7
|
8 | | flid 10227 |
. . . . . . 7
|
9 | 7, 8 | syl 14 |
. . . . . 6
|
10 | | nnm1nn0 9163 |
. . . . . . . . . 10
|
11 | 10 | nn0red 9176 |
. . . . . . . . 9
|
12 | 10 | nn0ge0d 9178 |
. . . . . . . . 9
|
13 | | nnre 8872 |
. . . . . . . . 9
|
14 | | nngt0 8890 |
. . . . . . . . 9
|
15 | | divge0 8776 |
. . . . . . . . 9
|
16 | 11, 12, 13, 14, 15 | syl22anc 1234 |
. . . . . . . 8
|
17 | 16 | ad2antlr 486 |
. . . . . . 7
|
18 | 13 | ltm1d 8835 |
. . . . . . . . . 10
|
19 | | nncn 8873 |
. . . . . . . . . . 11
|
20 | 19 | mulid1d 7924 |
. . . . . . . . . 10
|
21 | 18, 20 | breqtrrd 4015 |
. . . . . . . . 9
|
22 | | 1red 7922 |
. . . . . . . . . 10
|
23 | | ltdivmul 8779 |
. . . . . . . . . 10
|
24 | 11, 22, 13, 14, 23 | syl112anc 1237 |
. . . . . . . . 9
|
25 | 21, 24 | mpbird 166 |
. . . . . . . 8
|
26 | 25 | ad2antlr 486 |
. . . . . . 7
|
27 | 10 | nn0zd 9319 |
. . . . . . . . . 10
|
28 | | znq 9570 |
. . . . . . . . . 10
|
29 | 27, 28 | mpancom 420 |
. . . . . . . . 9
|
30 | 29 | ad2antlr 486 |
. . . . . . . 8
|
31 | | flqbi2 10234 |
. . . . . . . 8
|
32 | 7, 30, 31 | syl2anc 409 |
. . . . . . 7
|
33 | 17, 26, 32 | mpbir2and 939 |
. . . . . 6
|
34 | 9, 33 | eqtr4d 2206 |
. . . . 5
|
35 | | zcn 9204 |
. . . . . . . . . 10
|
36 | 35 | adantr 274 |
. . . . . . . . 9
|
37 | 19 | adantl 275 |
. . . . . . . . 9
|
38 | | nnap0 8894 |
. . . . . . . . . 10
# |
39 | 38 | adantl 275 |
. . . . . . . . 9
# |
40 | 36, 37, 37, 39 | divdirapd 8733 |
. . . . . . . 8
|
41 | | ax-1cn 7854 |
. . . . . . . . . . . 12
|
42 | 41 | a1i 9 |
. . . . . . . . . . 11
|
43 | 36, 42, 37 | ppncand 8257 |
. . . . . . . . . 10
|
44 | 43 | oveq1d 5865 |
. . . . . . . . 9
|
45 | 4 | zcnd 9322 |
. . . . . . . . . 10
|
46 | | subcl 8105 |
. . . . . . . . . . . 12
|
47 | 19, 41, 46 | sylancl 411 |
. . . . . . . . . . 11
|
48 | 47 | adantl 275 |
. . . . . . . . . 10
|
49 | 45, 48, 37, 39 | divdirapd 8733 |
. . . . . . . . 9
|
50 | 44, 49 | eqtr3d 2205 |
. . . . . . . 8
|
51 | 37, 39 | dividapd 8690 |
. . . . . . . . 9
|
52 | 51 | oveq2d 5866 |
. . . . . . . 8
|
53 | 40, 50, 52 | 3eqtr3d 2211 |
. . . . . . 7
|
54 | 53 | fveq2d 5498 |
. . . . . 6
|
55 | 54 | adantr 274 |
. . . . 5
|
56 | | znq 9570 |
. . . . . . 7
|
57 | | 1z 9225 |
. . . . . . 7
|
58 | | flqaddz 10240 |
. . . . . . 7
|
59 | 56, 57, 58 | sylancl 411 |
. . . . . 6
|
60 | 59 | adantr 274 |
. . . . 5
|
61 | 34, 55, 60 | 3eqtrrd 2208 |
. . . 4
|
62 | | znq 9570 |
. . . . . . . . 9
|
63 | 3, 62 | sylan 281 |
. . . . . . . 8
|
64 | 63 | flqcld 10220 |
. . . . . . 7
|
65 | 64 | zcnd 9322 |
. . . . . 6
|
66 | 56 | flqcld 10220 |
. . . . . . 7
|
67 | 66 | zcnd 9322 |
. . . . . 6
|
68 | 65, 67, 42 | subaddd 8235 |
. . . . 5
|
69 | 68 | adantr 274 |
. . . 4
|
70 | 61, 69 | mpbird 166 |
. . 3
|
71 | | iftrue 3530 |
. . . 4
|
72 | 71 | adantl 275 |
. . 3
|
73 | 70, 72 | eqtr4d 2206 |
. 2
|
74 | | zmodcl 10287 |
. . . . . . . . . . 11
|
75 | 3, 74 | sylan 281 |
. . . . . . . . . 10
|
76 | 75 | nn0red 9176 |
. . . . . . . . 9
|
77 | | 1re 7906 |
. . . . . . . . 9
|
78 | | resubcl 8170 |
. . . . . . . . 9
|
79 | 76, 77, 78 | sylancl 411 |
. . . . . . . 8
|
80 | 79 | adantr 274 |
. . . . . . 7
|
81 | 75 | nn0zd 9319 |
. . . . . . . . . . . 12
|
82 | | elnndc 9558 |
. . . . . . . . . . . 12
DECID |
83 | 81, 82 | syl 14 |
. . . . . . . . . . 11
DECID |
84 | | elnn0 9124 |
. . . . . . . . . . . . . 14
|
85 | 75, 84 | sylib 121 |
. . . . . . . . . . . . 13
|
86 | 85 | ord 719 |
. . . . . . . . . . . 12
|
87 | | id 19 |
. . . . . . . . . . . . 13
|
88 | | dvdsval3 11740 |
. . . . . . . . . . . . 13
|
89 | 87, 3, 88 | syl2anr 288 |
. . . . . . . . . . . 12
|
90 | 86, 89 | sylibrd 168 |
. . . . . . . . . . 11
|
91 | | con1dc 851 |
. . . . . . . . . . 11
DECID
|
92 | 83, 90, 91 | sylc 62 |
. . . . . . . . . 10
|
93 | 92 | imp 123 |
. . . . . . . . 9
|
94 | | nnm1nn0 9163 |
. . . . . . . . 9
|
95 | 93, 94 | syl 14 |
. . . . . . . 8
|
96 | 95 | nn0ge0d 9178 |
. . . . . . 7
|
97 | 13, 14 | jca 304 |
. . . . . . . 8
|
98 | 97 | ad2antlr 486 |
. . . . . . 7
|
99 | | divge0 8776 |
. . . . . . 7
|
100 | 80, 96, 98, 99 | syl21anc 1232 |
. . . . . 6
|
101 | 13 | adantl 275 |
. . . . . . . . . 10
|
102 | 76 | ltm1d 8835 |
. . . . . . . . . 10
|
103 | | zq 9572 |
. . . . . . . . . . . . 13
|
104 | 3, 103 | syl 14 |
. . . . . . . . . . . 12
|
105 | 104 | adantr 274 |
. . . . . . . . . . 11
|
106 | | nnq 9579 |
. . . . . . . . . . . 12
|
107 | 106 | adantl 275 |
. . . . . . . . . . 11
|
108 | 14 | adantl 275 |
. . . . . . . . . . 11
|
109 | | modqlt 10276 |
. . . . . . . . . . 11
|
110 | 105, 107,
108, 109 | syl3anc 1233 |
. . . . . . . . . 10
|
111 | 79, 76, 101, 102, 110 | lttrd 8032 |
. . . . . . . . 9
|
112 | 37 | mulid1d 7924 |
. . . . . . . . 9
|
113 | 111, 112 | breqtrrd 4015 |
. . . . . . . 8
|
114 | | 1red 7922 |
. . . . . . . . 9
|
115 | | ltdivmul 8779 |
. . . . . . . . 9
|
116 | 79, 114, 101, 108, 115 | syl112anc 1237 |
. . . . . . . 8
|
117 | 113, 116 | mpbird 166 |
. . . . . . 7
|
118 | 117 | adantr 274 |
. . . . . 6
|
119 | | peano2zm 9237 |
. . . . . . . . . 10
|
120 | 81, 119 | syl 14 |
. . . . . . . . 9
|
121 | | znq 9570 |
. . . . . . . . 9
|
122 | 120, 121 | sylancom 418 |
. . . . . . . 8
|
123 | | flqbi2 10234 |
. . . . . . . 8
|
124 | 64, 122, 123 | syl2anc 409 |
. . . . . . 7
|
125 | 124 | adantr 274 |
. . . . . 6
|
126 | 100, 118,
125 | mpbir2and 939 |
. . . . 5
|
127 | | modqval 10267 |
. . . . . . . . . . . . 13
|
128 | 105, 107,
108, 127 | syl3anc 1233 |
. . . . . . . . . . . 12
|
129 | 128 | oveq1d 5865 |
. . . . . . . . . . 11
|
130 | 37, 65 | mulcld 7927 |
. . . . . . . . . . . 12
|
131 | 45, 42, 130 | sub32d 8249 |
. . . . . . . . . . 11
|
132 | | pncan 8112 |
. . . . . . . . . . . . 13
|
133 | 36, 41, 132 | sylancl 411 |
. . . . . . . . . . . 12
|
134 | 133 | oveq1d 5865 |
. . . . . . . . . . 11
|
135 | 129, 131,
134 | 3eqtr2d 2209 |
. . . . . . . . . 10
|
136 | 135 | oveq1d 5865 |
. . . . . . . . 9
|
137 | 36, 130, 37, 39 | divsubdirapd 8734 |
. . . . . . . . 9
|
138 | 65, 37, 39 | divcanap3d 8699 |
. . . . . . . . . 10
|
139 | 138 | oveq2d 5866 |
. . . . . . . . 9
|
140 | 136, 137,
139 | 3eqtrrd 2208 |
. . . . . . . 8
|
141 | | zre 9203 |
. . . . . . . . . . 11
|
142 | | nndivre 8901 |
. . . . . . . . . . 11
|
143 | 141, 142 | sylan 281 |
. . . . . . . . . 10
|
144 | 143 | recnd 7935 |
. . . . . . . . 9
|
145 | | nndivre 8901 |
. . . . . . . . . . 11
|
146 | 79, 145 | sylancom 418 |
. . . . . . . . . 10
|
147 | 146 | recnd 7935 |
. . . . . . . . 9
|
148 | 144, 65, 147 | subaddd 8235 |
. . . . . . . 8
|
149 | 140, 148 | mpbid 146 |
. . . . . . 7
|
150 | 149 | adantr 274 |
. . . . . 6
|
151 | 150 | fveq2d 5498 |
. . . . 5
|
152 | 126, 151 | eqtr3d 2205 |
. . . 4
|
153 | 65, 67 | subeq0ad 8227 |
. . . . 5
|
154 | 153 | adantr 274 |
. . . 4
|
155 | 152, 154 | mpbird 166 |
. . 3
|
156 | | iffalse 3533 |
. . . 4
|
157 | 156 | adantl 275 |
. . 3
|
158 | 155, 157 | eqtr4d 2206 |
. 2
|
159 | | simpr 109 |
. . . 4
|
160 | | dvdsdc 11747 |
. . . 4
DECID
|
161 | 159, 4, 160 | syl2anc 409 |
. . 3
DECID |
162 | | exmiddc 831 |
. . 3
DECID
|
163 | 161, 162 | syl 14 |
. 2
|
164 | 73, 158, 163 | mpjaodan 793 |
1
|