Proof of Theorem modsumfzodifsn
Step | Hyp | Ref
| Expression |
1 | | elfzoelz 9157 |
. . . . . . . 8
..^
|
2 | 1 | adantl 271 |
. . . . . . 7
..^ ..^
|
3 | | zq 8711 |
. . . . . . 7
|
4 | 2, 3 | syl 14 |
. . . . . 6
..^ ..^
|
5 | | elfzo0 9191 |
. . . . . . . . . . 11
..^
|
6 | 5 | biimpi 118 |
. . . . . . . . . 10
..^
|
7 | 6 | adantr 270 |
. . . . . . . . 9
..^ ..^
|
8 | 7 | simp1d 950 |
. . . . . . . 8
..^ ..^
|
9 | 8 | nn0zd 8467 |
. . . . . . 7
..^ ..^
|
10 | | zq 8711 |
. . . . . . 7
|
11 | 9, 10 | syl 14 |
. . . . . 6
..^ ..^
|
12 | | qaddcl 8720 |
. . . . . 6
|
13 | 4, 11, 12 | syl2anc 403 |
. . . . 5
..^ ..^
|
14 | 13 | adantr 270 |
. . . 4
..^
..^
|
15 | 7 | simp2d 951 |
. . . . . 6
..^ ..^
|
16 | | nnq 8718 |
. . . . . 6
|
17 | 15, 16 | syl 14 |
. . . . 5
..^ ..^
|
18 | 17 | adantr 270 |
. . . 4
..^
..^
|
19 | | elfzo1 9199 |
. . . . . . . . . . 11
..^ |
20 | 19 | biimpi 118 |
. . . . . . . . . 10
..^
|
21 | 20 | adantl 271 |
. . . . . . . . 9
..^ ..^
|
22 | 21 | simp1d 950 |
. . . . . . . 8
..^ ..^
|
23 | 22 | nnnn0d 8341 |
. . . . . . 7
..^ ..^
|
24 | 23, 8 | nn0addcld 8345 |
. . . . . 6
..^ ..^
|
25 | 24 | nn0ge0d 8344 |
. . . . 5
..^ ..^
|
26 | 25 | adantr 270 |
. . . 4
..^
..^
|
27 | | simpr 108 |
. . . 4
..^
..^
|
28 | | modqid 9351 |
. . . 4
|
29 | 14, 18, 26, 27, 28 | syl22anc 1170 |
. . 3
..^
..^
|
30 | 24 | adantr 270 |
. . . . 5
..^
..^
|
31 | 15 | adantr 270 |
. . . . 5
..^
..^
|
32 | | elfzo0 9191 |
. . . . 5
..^
|
33 | 30, 31, 27, 32 | syl3anbrc 1122 |
. . . 4
..^
..^
..^ |
34 | 2 | zcnd 8470 |
. . . . . . 7
..^ ..^
|
35 | | 0cnd 7112 |
. . . . . . 7
..^ ..^
|
36 | 8 | nn0cnd 8343 |
. . . . . . 7
..^ ..^
|
37 | 22 | nnne0d 8083 |
. . . . . . 7
..^ ..^
|
38 | 34, 35, 36, 37 | addneintr2d 7297 |
. . . . . 6
..^ ..^
|
39 | 36 | addid2d 7258 |
. . . . . 6
..^ ..^
|
40 | 38, 39 | neeqtrd 2273 |
. . . . 5
..^ ..^
|
41 | 40 | adantr 270 |
. . . 4
..^
..^
|
42 | | eldifsn 3517 |
. . . 4
..^
..^ |
43 | 33, 41, 42 | sylanbrc 408 |
. . 3
..^
..^
..^ |
44 | 29, 43 | eqeltrd 2155 |
. 2
..^
..^
..^ |
45 | 15 | nncnd 8053 |
. . . . . . . . 9
..^ ..^
|
46 | 45 | adantr 270 |
. . . . . . . 8
..^
..^
|
47 | 46 | mulm1d 7514 |
. . . . . . 7
..^
..^
|
48 | 47 | oveq2d 5548 |
. . . . . 6
..^
..^
|
49 | 34, 36 | addcld 7138 |
. . . . . . . 8
..^ ..^
|
50 | 49, 45 | negsubd 7425 |
. . . . . . 7
..^ ..^
|
51 | 50 | adantr 270 |
. . . . . 6
..^
..^
|
52 | 48, 51 | eqtrd 2113 |
. . . . 5
..^
..^
|
53 | 52 | oveq1d 5547 |
. . . 4
..^
..^
|
54 | 13 | adantr 270 |
. . . . 5
..^
..^
|
55 | | neg1z 8383 |
. . . . . 6
|
56 | 55 | a1i 9 |
. . . . 5
..^
..^
|
57 | 17 | adantr 270 |
. . . . 5
..^
..^
|
58 | 15 | nngt0d 8082 |
. . . . . 6
..^ ..^
|
59 | 58 | adantr 270 |
. . . . 5
..^
..^
|
60 | | modqcyc 9361 |
. . . . 5
|
61 | 54, 56, 57, 59, 60 | syl22anc 1170 |
. . . 4
..^
..^
|
62 | | qsubcl 8723 |
. . . . . . 7
|
63 | 13, 17, 62 | syl2anc 403 |
. . . . . 6
..^ ..^
|
64 | 63 | adantr 270 |
. . . . 5
..^
..^
|
65 | | simpr 108 |
. . . . . . 7
..^
..^
|
66 | 15 | nnred 8052 |
. . . . . . . . 9
..^ ..^
|
67 | 66 | adantr 270 |
. . . . . . . 8
..^
..^
|
68 | 24 | nn0red 8342 |
. . . . . . . . 9
..^ ..^
|
69 | 68 | adantr 270 |
. . . . . . . 8
..^
..^
|
70 | 67, 69 | lenltd 7227 |
. . . . . . 7
..^
..^
|
71 | 65, 70 | mpbird 165 |
. . . . . 6
..^
..^
|
72 | 69, 67 | subge0d 7635 |
. . . . . 6
..^
..^
|
73 | 71, 72 | mpbird 165 |
. . . . 5
..^
..^
|
74 | 2 | zred 8469 |
. . . . . . . 8
..^ ..^
|
75 | 8 | nn0red 8342 |
. . . . . . . 8
..^ ..^
|
76 | 21 | simp3d 952 |
. . . . . . . 8
..^ ..^
|
77 | 7 | simp3d 952 |
. . . . . . . 8
..^ ..^
|
78 | 74, 75, 66, 66, 76, 77 | lt2addd 7667 |
. . . . . . 7
..^ ..^
|
79 | 68, 66, 66 | ltsubaddd 7641 |
. . . . . . 7
..^ ..^
|
80 | 78, 79 | mpbird 165 |
. . . . . 6
..^ ..^
|
81 | 80 | adantr 270 |
. . . . 5
..^
..^
|
82 | | modqid 9351 |
. . . . 5
|
83 | 64, 57, 73, 81, 82 | syl22anc 1170 |
. . . 4
..^
..^
|
84 | 53, 61, 83 | 3eqtr3d 2121 |
. . 3
..^
..^
|
85 | 24 | nn0zd 8467 |
. . . . . . . 8
..^ ..^
|
86 | 15 | nnzd 8468 |
. . . . . . . 8
..^ ..^
|
87 | 85, 86 | zsubcld 8474 |
. . . . . . 7
..^ ..^
|
88 | 87 | adantr 270 |
. . . . . 6
..^
..^
|
89 | | elnn0z 8364 |
. . . . . 6
|
90 | 88, 73, 89 | sylanbrc 408 |
. . . . 5
..^
..^
|
91 | 15 | adantr 270 |
. . . . 5
..^
..^
|
92 | | elfzo0 9191 |
. . . . 5
..^
|
93 | 90, 91, 81, 92 | syl3anbrc 1122 |
. . . 4
..^
..^
..^ |
94 | 34, 45 | subcld 7419 |
. . . . . . 7
..^ ..^
|
95 | 74, 76 | ltned 7224 |
. . . . . . . 8
..^ ..^
|
96 | 34, 45, 95 | subne0d 7428 |
. . . . . . 7
..^ ..^
|
97 | 94, 35, 36, 96 | addneintr2d 7297 |
. . . . . 6
..^ ..^
|
98 | 34, 36, 45 | addsubd 7440 |
. . . . . 6
..^ ..^
|
99 | 39 | eqcomd 2086 |
. . . . . 6
..^ ..^
|
100 | 97, 98, 99 | 3netr4d 2278 |
. . . . 5
..^ ..^
|
101 | 100 | adantr 270 |
. . . 4
..^
..^
|
102 | | eldifsn 3517 |
. . . 4
..^
..^ |
103 | 93, 101, 102 | sylanbrc 408 |
. . 3
..^
..^
..^ |
104 | 84, 103 | eqeltrd 2155 |
. 2
..^
..^
..^ |
105 | | zdclt 8425 |
. . . 4
DECID |
106 | | exmiddc 777 |
. . . 4
DECID
|
107 | 105, 106 | syl 14 |
. . 3
|
108 | 85, 86, 107 | syl2anc 403 |
. 2
..^ ..^
|
109 | 44, 104, 108 | mpjaodan 744 |
1
..^ ..^
..^ |