Proof of Theorem gausslemma2dlem4
Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.p |
. . 3
|
2 | | gausslemma2d.h |
. . 3
|
3 | | gausslemma2d.r |
. . 3
|
4 | 1, 2, 3 | gausslemma2dlem1 25091 |
. 2
|
5 | | eldif 3584 |
. . . 4
|
6 | | prm23ge5 15520 |
. . . . . 6
|
7 | | eleq1 2689 |
. . . . . . . . 9
|
8 | 7 | notbid 308 |
. . . . . . . 8
|
9 | | 2ex 11092 |
. . . . . . . . . . . 12
|
10 | 9 | snid 4208 |
. . . . . . . . . . 11
|
11 | 10 | 2a1i 12 |
. . . . . . . . . 10
|
12 | 11 | necon1bd 2812 |
. . . . . . . . 9
|
13 | 12 | a1dd 50 |
. . . . . . . 8
|
14 | 8, 13 | sylbid 230 |
. . . . . . 7
|
15 | | gausslemma2d.m |
. . . . . . . . . 10
|
16 | | 3lt4 11197 |
. . . . . . . . . . . 12
|
17 | | breq1 4656 |
. . . . . . . . . . . 12
|
18 | 16, 17 | mpbiri 248 |
. . . . . . . . . . 11
|
19 | | 3nn0 11310 |
. . . . . . . . . . . . 13
|
20 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
21 | 19, 20 | mpbiri 248 |
. . . . . . . . . . . 12
|
22 | | 4nn 11187 |
. . . . . . . . . . . 12
|
23 | | divfl0 12625 |
. . . . . . . . . . . 12
|
24 | 21, 22, 23 | sylancl 694 |
. . . . . . . . . . 11
|
25 | 18, 24 | mpbid 222 |
. . . . . . . . . 10
|
26 | 15, 25 | syl5eq 2668 |
. . . . . . . . 9
|
27 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
|
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . 15
|
29 | | fz10 12362 |
. . . . . . . . . . . . . . 15
|
30 | 28, 29 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
31 | 30 | prodeq1d 14651 |
. . . . . . . . . . . . 13
|
32 | | prod0 14673 |
. . . . . . . . . . . . 13
|
33 | 31, 32 | syl6eq 2672 |
. . . . . . . . . . . 12
|
34 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . 15
|
36 | | 0p1e1 11132 |
. . . . . . . . . . . . . . 15
|
37 | 35, 36 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
38 | 37 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
39 | 38 | prodeq1d 14651 |
. . . . . . . . . . . 12
|
40 | 33, 39 | oveq12d 6668 |
. . . . . . . . . . 11
|
41 | | fzfid 12772 |
. . . . . . . . . . . . 13
|
42 | 3 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
43 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
|
44 | 43 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
|
45 | 43 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
|
46 | 44, 43, 45 | ifbieq12d 4113 |
. . . . . . . . . . . . . . . . 17
|
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
48 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
49 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . 20
|
50 | 49 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
|
51 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 50, 51 | mulcld 10060 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
54 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . 21
|
56 | 55 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | 1, 54, 56 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
|
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
59 | 58, 53 | subcld 10392 |
. . . . . . . . . . . . . . . . 17
|
60 | 53, 59 | ifcld 4131 |
. . . . . . . . . . . . . . . 16
|
61 | 42, 47, 48, 60 | fvmptd 6288 |
. . . . . . . . . . . . . . 15
|
62 | 61, 60 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
|
63 | 62 | adantll 750 |
. . . . . . . . . . . . 13
|
64 | 41, 63 | fprodcl 14682 |
. . . . . . . . . . . 12
|
65 | 64 | mulid2d 10058 |
. . . . . . . . . . 11
|
66 | 40, 65 | eqtr2d 2657 |
. . . . . . . . . 10
|
67 | 66 | ex 450 |
. . . . . . . . 9
|
68 | 26, 67 | syl 17 |
. . . . . . . 8
|
69 | 68 | a1d 25 |
. . . . . . 7
|
70 | 1, 15 | gausslemma2dlem0d 25084 |
. . . . . . . . . . . . . 14
|
71 | 70 | nn0red 11352 |
. . . . . . . . . . . . 13
|
72 | 71 | ltp1d 10954 |
. . . . . . . . . . . 12
|
73 | | fzdisj 12368 |
. . . . . . . . . . . 12
|
74 | 72, 73 | syl 17 |
. . . . . . . . . . 11
|
75 | 74 | adantl 482 |
. . . . . . . . . 10
|
76 | | eluzelre 11698 |
. . . . . . . . . . . . . . . . . . . 20
|
77 | | 4re 11097 |
. . . . . . . . . . . . . . . . . . . . 21
|
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | | 4ne0 11117 |
. . . . . . . . . . . . . . . . . . . . 21
|
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
81 | 76, 78, 80 | redivcld 10853 |
. . . . . . . . . . . . . . . . . . 19
|
82 | 81 | flcld 12599 |
. . . . . . . . . . . . . . . . . 18
|
83 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . . . . 21
|
84 | 22, 83 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
85 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . 21
|
86 | | 4lt5 11200 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
87 | | 5re 11099 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
89 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
90 | 89 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
91 | | ltleletr 10130 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
92 | 77, 88, 90, 91 | mp3an2i 1429 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
93 | 86, 92 | mpani 712 |
. . . . . . . . . . . . . . . . . . . . . 22
|
94 | 93 | 3impia 1261 |
. . . . . . . . . . . . . . . . . . . . 21
|
95 | 85, 94 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . 20
|
96 | | divge1 11898 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | 84, 76, 95, 96 | mp3an2i 1429 |
. . . . . . . . . . . . . . . . . . 19
|
98 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . . 20
|
99 | | flge 12606 |
. . . . . . . . . . . . . . . . . . . 20
|
100 | 81, 98, 99 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
101 | 97, 100 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
102 | | elnnz1 11403 |
. . . . . . . . . . . . . . . . . 18
|
103 | 82, 101, 102 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
|
104 | 103 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
105 | | oddprm 15515 |
. . . . . . . . . . . . . . . . 17
|
106 | 105 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
107 | | prmuz2 15408 |
. . . . . . . . . . . . . . . . . . 19
|
108 | 54, 107 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
110 | | fldiv4lem1div2uz2 12637 |
. . . . . . . . . . . . . . . . 17
|
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
|
112 | 104, 106,
111 | 3jca 1242 |
. . . . . . . . . . . . . . 15
|
113 | 112 | ex 450 |
. . . . . . . . . . . . . 14
|
114 | 1, 113 | syl 17 |
. . . . . . . . . . . . 13
|
115 | 114 | impcom 446 |
. . . . . . . . . . . 12
|
116 | 2 | oveq2i 6661 |
. . . . . . . . . . . . . 14
|
117 | 15, 116 | eleq12i 2694 |
. . . . . . . . . . . . 13
|
118 | | elfz1b 12409 |
. . . . . . . . . . . . 13
|
119 | 117, 118 | bitri 264 |
. . . . . . . . . . . 12
|
120 | 115, 119 | sylibr 224 |
. . . . . . . . . . 11
|
121 | | fzsplit 12367 |
. . . . . . . . . . 11
|
122 | 120, 121 | syl 17 |
. . . . . . . . . 10
|
123 | | fzfid 12772 |
. . . . . . . . . 10
|
124 | 62 | adantll 750 |
. . . . . . . . . 10
|
125 | 75, 122, 123, 124 | fprodsplit 14696 |
. . . . . . . . 9
|
126 | 125 | ex 450 |
. . . . . . . 8
|
127 | 126 | a1d 25 |
. . . . . . 7
|
128 | 14, 69, 127 | 3jaoi 1391 |
. . . . . 6
|
129 | 6, 128 | syl 17 |
. . . . 5
|
130 | 129 | imp 445 |
. . . 4
|
131 | 5, 130 | sylbi 207 |
. . 3
|
132 | 1, 131 | mpcom 38 |
. 2
|
133 | 4, 132 | eqtrd 2656 |
1
|