Metamath Proof Explorer


Theorem dignn0flhalflem1

Description: Lemma 1 for dignn0flhalf . (Contributed by AV, 7-Jun-2012)

Ref Expression
Assertion dignn0flhalflem1 A A 1 2 N A 2 N 1 < A 1 2 N

Proof

Step Hyp Ref Expression
1 zre A A
2 1 3ad2ant1 A A 1 2 N A
3 2rp 2 +
4 3 a1i N 2 +
5 nnz N N
6 4 5 rpexpcld N 2 N +
7 6 rpred N 2 N
8 7 3ad2ant3 A A 1 2 N 2 N
9 2 8 resubcld A A 1 2 N A 2 N
10 6 3ad2ant3 A A 1 2 N 2 N +
11 9 10 modcld A A 1 2 N A 2 N mod 2 N
12 9 11 resubcld A A 1 2 N A - 2 N - A 2 N mod 2 N
13 peano2zm A A 1
14 13 zred A A 1
15 14 3ad2ant1 A A 1 2 N A 1
16 15 10 modcld A A 1 2 N A 1 mod 2 N
17 15 16 resubcld A A 1 2 N A - 1 - A 1 mod 2 N
18 1red A A 1 2 N 1
19 18 16 readdcld A A 1 2 N 1 + A 1 mod 2 N
20 8 11 readdcld A A 1 2 N 2 N + A 2 N mod 2 N
21 2nn 2
22 21 a1i N 2
23 nnnn0 N N 0
24 22 23 nnexpcld N 2 N
25 24 anim2i A N A 2 N
26 25 3adant2 A A 1 2 N A 2 N
27 m1modmmod A 2 N A 1 mod 2 N A mod 2 N = if A mod 2 N = 0 2 N 1 1
28 26 27 syl A A 1 2 N A 1 mod 2 N A mod 2 N = if A mod 2 N = 0 2 N 1 1
29 nnz A 1 2 A 1 2
30 29 a1i A N A 1 2 A 1 2
31 zcn A A
32 xp1d2m1eqxm1d2 A A + 1 2 1 = A 1 2
33 32 eqcomd A A 1 2 = A + 1 2 1
34 31 33 syl A A 1 2 = A + 1 2 1
35 34 adantr A N A 1 2 = A + 1 2 1
36 35 eleq1d A N A 1 2 A + 1 2 1
37 peano2z A + 1 2 1 A + 1 2 - 1 + 1
38 31 adantr A N A
39 1cnd A N 1
40 38 39 addcld A N A + 1
41 40 halfcld A N A + 1 2
42 41 39 npcand A N A + 1 2 - 1 + 1 = A + 1 2
43 42 eleq1d A N A + 1 2 - 1 + 1 A + 1 2
44 37 43 syl5ib A N A + 1 2 1 A + 1 2
45 36 44 sylbid A N A 1 2 A + 1 2
46 mod0 A 2 N + A mod 2 N = 0 A 2 N
47 1 6 46 syl2an A N A mod 2 N = 0 A 2 N
48 22 nnzd N 2
49 nnm1nn0 N N 1 0
50 zexpcl 2 N 1 0 2 N 1
51 48 49 50 syl2anc N 2 N 1
52 51 adantl A N 2 N 1
53 52 adantr A N A 2 N 2 N 1
54 simpr A N A 2 N A 2 N
55 53 54 zmulcld A N A 2 N 2 N 1 A 2 N
56 55 ex A N A 2 N 2 N 1 A 2 N
57 5 adantl A N N
58 57 zcnd A N N
59 39 negcld A N 1
60 58 39 negsubd A N N + -1 = N 1
61 60 eqcomd A N N 1 = N + -1
62 58 59 61 mvrladdd A N N - 1 - N = 1
63 62 oveq2d A N 2 N - 1 - N = 2 1
64 2cnd A N 2
65 2ne0 2 0
66 65 a1i A N 2 0
67 1zzd N 1
68 5 67 zsubcld N N 1
69 68 5 jca N N 1 N
70 69 adantl A N N 1 N
71 expsub 2 2 0 N 1 N 2 N - 1 - N = 2 N 1 2 N
72 64 66 70 71 syl21anc A N 2 N - 1 - N = 2 N 1 2 N
73 expn1 2 2 1 = 1 2
74 64 73 syl A N 2 1 = 1 2
75 63 72 74 3eqtr3d A N 2 N 1 2 N = 1 2
76 75 oveq2d A N A 2 N 1 2 N = A 1 2
77 2cnd N 2
78 77 49 expcld N 2 N 1
79 78 adantl A N 2 N 1
80 3 a1i A N 2 +
81 80 57 rpexpcld A N 2 N +
82 81 rpcnne0d A N 2 N 2 N 0
83 div12 2 N 1 A 2 N 2 N 0 2 N 1 A 2 N = A 2 N 1 2 N
84 79 38 82 83 syl3anc A N 2 N 1 A 2 N = A 2 N 1 2 N
85 38 64 66 divrecd A N A 2 = A 1 2
86 76 84 85 3eqtr4d A N 2 N 1 A 2 N = A 2
87 86 eleq1d A N 2 N 1 A 2 N A 2
88 56 87 sylibd A N A 2 N A 2
89 47 88 sylbid A N A mod 2 N = 0 A 2
90 zeo2 A A 2 ¬ A + 1 2
91 90 adantr A N A 2 ¬ A + 1 2
92 89 91 sylibd A N A mod 2 N = 0 ¬ A + 1 2
93 92 necon2ad A N A + 1 2 A mod 2 N 0
94 30 45 93 3syld A N A 1 2 A mod 2 N 0
95 94 ex A N A 1 2 A mod 2 N 0
96 95 com23 A A 1 2 N A mod 2 N 0
97 96 3imp A A 1 2 N A mod 2 N 0
98 97 neneqd A A 1 2 N ¬ A mod 2 N = 0
99 98 iffalsed A A 1 2 N if A mod 2 N = 0 2 N 1 1 = 1
100 28 99 eqtrd A A 1 2 N A 1 mod 2 N A mod 2 N = 1
101 neg1lt0 1 < 0
102 2re 2
103 1lt2 1 < 2
104 expgt1 2 N 1 < 2 1 < 2 N
105 102 103 104 mp3an13 N 1 < 2 N
106 1red N 1
107 106 7 posdifd N 1 < 2 N 0 < 2 N 1
108 105 107 mpbid N 0 < 2 N 1
109 106 renegcld N 1
110 0red N 0
111 7 106 resubcld N 2 N 1
112 lttr 1 0 2 N 1 1 < 0 0 < 2 N 1 1 < 2 N 1
113 109 110 111 112 syl3anc N 1 < 0 0 < 2 N 1 1 < 2 N 1
114 108 113 mpan2d N 1 < 0 1 < 2 N 1
115 101 114 mpi N 1 < 2 N 1
116 115 3ad2ant3 A A 1 2 N 1 < 2 N 1
117 100 116 eqbrtrd A A 1 2 N A 1 mod 2 N A mod 2 N < 2 N 1
118 2 10 modcld A A 1 2 N A mod 2 N
119 ltsubadd2b 1 2 N A mod 2 N A 1 mod 2 N A 1 mod 2 N A mod 2 N < 2 N 1 1 + A 1 mod 2 N < 2 N + A mod 2 N
120 18 8 118 16 119 syl22anc A A 1 2 N A 1 mod 2 N A mod 2 N < 2 N 1 1 + A 1 mod 2 N < 2 N + A mod 2 N
121 117 120 mpbid A A 1 2 N 1 + A 1 mod 2 N < 2 N + A mod 2 N
122 modid0 2 N + 2 N mod 2 N = 0
123 10 122 syl A A 1 2 N 2 N mod 2 N = 0
124 123 oveq2d A A 1 2 N A mod 2 N 2 N mod 2 N = A mod 2 N 0
125 118 recnd A A 1 2 N A mod 2 N
126 125 subid1d A A 1 2 N A mod 2 N 0 = A mod 2 N
127 124 126 eqtrd A A 1 2 N A mod 2 N 2 N mod 2 N = A mod 2 N
128 127 oveq1d A A 1 2 N A mod 2 N 2 N mod 2 N mod 2 N = A mod 2 N mod 2 N
129 modsubmodmod A 2 N 2 N + A mod 2 N 2 N mod 2 N mod 2 N = A 2 N mod 2 N
130 2 8 10 129 syl3anc A A 1 2 N A mod 2 N 2 N mod 2 N mod 2 N = A 2 N mod 2 N
131 modabs2 A 2 N + A mod 2 N mod 2 N = A mod 2 N
132 2 10 131 syl2anc A A 1 2 N A mod 2 N mod 2 N = A mod 2 N
133 128 130 132 3eqtr3d A A 1 2 N A 2 N mod 2 N = A mod 2 N
134 133 oveq2d A A 1 2 N 2 N + A 2 N mod 2 N = 2 N + A mod 2 N
135 121 134 breqtrrd A A 1 2 N 1 + A 1 mod 2 N < 2 N + A 2 N mod 2 N
136 19 20 2 135 ltsub2dd A A 1 2 N A 2 N + A 2 N mod 2 N < A 1 + A 1 mod 2 N
137 31 3ad2ant1 A A 1 2 N A
138 8 recnd A A 1 2 N 2 N
139 11 recnd A A 1 2 N A 2 N mod 2 N
140 137 138 139 subsub4d A A 1 2 N A - 2 N - A 2 N mod 2 N = A 2 N + A 2 N mod 2 N
141 1cnd A A 1 2 N 1
142 16 recnd A A 1 2 N A 1 mod 2 N
143 137 141 142 subsub4d A A 1 2 N A - 1 - A 1 mod 2 N = A 1 + A 1 mod 2 N
144 136 140 143 3brtr4d A A 1 2 N A - 2 N - A 2 N mod 2 N < A - 1 - A 1 mod 2 N
145 12 17 10 144 ltdiv1dd A A 1 2 N A - 2 N - A 2 N mod 2 N 2 N < A - 1 - A 1 mod 2 N 2 N
146 7 recnd N 2 N
147 146 3ad2ant3 A A 1 2 N 2 N
148 65 a1i N 2 0
149 77 148 5 expne0d N 2 N 0
150 149 3ad2ant3 A A 1 2 N 2 N 0
151 divsub1dir A 2 N 2 N 0 A 2 N 1 = A 2 N 2 N
152 151 fveq2d A 2 N 2 N 0 A 2 N 1 = A 2 N 2 N
153 137 147 150 152 syl3anc A A 1 2 N A 2 N 1 = A 2 N 2 N
154 fldivmod A 2 N 2 N + A 2 N 2 N = A - 2 N - A 2 N mod 2 N 2 N
155 9 10 154 syl2anc A A 1 2 N A 2 N 2 N = A - 2 N - A 2 N mod 2 N 2 N
156 153 155 eqtrd A A 1 2 N A 2 N 1 = A - 2 N - A 2 N mod 2 N 2 N
157 fldivmod A 1 2 N + A 1 2 N = A - 1 - A 1 mod 2 N 2 N
158 15 10 157 syl2anc A A 1 2 N A 1 2 N = A - 1 - A 1 mod 2 N 2 N
159 145 156 158 3brtr4d A A 1 2 N A 2 N 1 < A 1 2 N