Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dignn0flhalflem1 Structured version   Visualization version   GIF version

Theorem dignn0flhalflem1 41731
Description: Lemma 1 for dignn0flhalf 41734. (Contributed by AV, 7-Jun-2012.)
Assertion
Ref Expression
dignn0flhalflem1 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝐴 / (2↑𝑁)) − 1)) < (⌊‘((𝐴 − 1) / (2↑𝑁))))

Proof of Theorem dignn0flhalflem1
StepHypRef Expression
1 zre 11341 . . . . . 6 (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
213ad2ant1 1080 . . . . 5 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝐴 ∈ ℝ)
3 2rp 11797 . . . . . . . . 9 2 ∈ ℝ+
43a1i 11 . . . . . . . 8 (𝑁 ∈ ℕ → 2 ∈ ℝ+)
5 nnz 11359 . . . . . . . 8 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
64, 5rpexpcld 12988 . . . . . . 7 (𝑁 ∈ ℕ → (2↑𝑁) ∈ ℝ+)
76rpred 11832 . . . . . 6 (𝑁 ∈ ℕ → (2↑𝑁) ∈ ℝ)
873ad2ant3 1082 . . . . 5 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2↑𝑁) ∈ ℝ)
92, 8resubcld 10418 . . . 4 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 − (2↑𝑁)) ∈ ℝ)
1063ad2ant3 1082 . . . . 5 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2↑𝑁) ∈ ℝ+)
119, 10modcld 12630 . . . 4 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (2↑𝑁)) mod (2↑𝑁)) ∈ ℝ)
129, 11resubcld 10418 . . 3 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (2↑𝑁)) − ((𝐴 − (2↑𝑁)) mod (2↑𝑁))) ∈ ℝ)
13 peano2zm 11380 . . . . . 6 (𝐴 ∈ ℤ → (𝐴 − 1) ∈ ℤ)
1413zred 11442 . . . . 5 (𝐴 ∈ ℤ → (𝐴 − 1) ∈ ℝ)
15143ad2ant1 1080 . . . 4 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 − 1) ∈ ℝ)
1615, 10modcld 12630 . . . 4 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 − 1) mod (2↑𝑁)) ∈ ℝ)
1715, 16resubcld 10418 . . 3 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 − 1) − ((𝐴 − 1) mod (2↑𝑁))) ∈ ℝ)
18 1red 10015 . . . . . 6 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℝ)
1918, 16readdcld 10029 . . . . 5 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (1 + ((𝐴 − 1) mod (2↑𝑁))) ∈ ℝ)
208, 11readdcld 10029 . . . . 5 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) + ((𝐴 − (2↑𝑁)) mod (2↑𝑁))) ∈ ℝ)
21 2nn 11145 . . . . . . . . . . . . . 14 2 ∈ ℕ
2221a1i 11 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 2 ∈ ℕ)
23 nnnn0 11259 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
2422, 23nnexpcld 12986 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (2↑𝑁) ∈ ℕ)
2524anim2i 592 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 ∈ ℤ ∧ (2↑𝑁) ∈ ℕ))
26253adant2 1078 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 ∈ ℤ ∧ (2↑𝑁) ∈ ℕ))
27 m1modmmod 41634 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (2↑𝑁) ∈ ℕ) → (((𝐴 − 1) mod (2↑𝑁)) − (𝐴 mod (2↑𝑁))) = if((𝐴 mod (2↑𝑁)) = 0, ((2↑𝑁) − 1), -1))
2826, 27syl 17 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) mod (2↑𝑁)) − (𝐴 mod (2↑𝑁))) = if((𝐴 mod (2↑𝑁)) = 0, ((2↑𝑁) − 1), -1))
29 nnz 11359 . . . . . . . . . . . . . . . 16 (((𝐴 − 1) / 2) ∈ ℕ → ((𝐴 − 1) / 2) ∈ ℤ)
3029a1i 11 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) / 2) ∈ ℕ → ((𝐴 − 1) / 2) ∈ ℤ))
31 zcn 11342 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℤ → 𝐴 ∈ ℂ)
32 xp1d2m1eqxm1d2 11246 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℂ → (((𝐴 + 1) / 2) − 1) = ((𝐴 − 1) / 2))
3332eqcomd 2627 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℂ → ((𝐴 − 1) / 2) = (((𝐴 + 1) / 2) − 1))
3431, 33syl 17 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℤ → ((𝐴 − 1) / 2) = (((𝐴 + 1) / 2) − 1))
3534adantr 481 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 − 1) / 2) = (((𝐴 + 1) / 2) − 1))
3635eleq1d 2683 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) / 2) ∈ ℤ ↔ (((𝐴 + 1) / 2) − 1) ∈ ℤ))
37 peano2z 11378 . . . . . . . . . . . . . . . . 17 ((((𝐴 + 1) / 2) − 1) ∈ ℤ → ((((𝐴 + 1) / 2) − 1) + 1) ∈ ℤ)
3831adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐴 ∈ ℂ)
39 1cnd 10016 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℂ)
4038, 39addcld 10019 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 + 1) ∈ ℂ)
4140halfcld 11237 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 + 1) / 2) ∈ ℂ)
4241, 39npcand 10356 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝐴 + 1) / 2) − 1) + 1) = ((𝐴 + 1) / 2))
4342eleq1d 2683 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((((𝐴 + 1) / 2) − 1) + 1) ∈ ℤ ↔ ((𝐴 + 1) / 2) ∈ ℤ))
4437, 43syl5ib 234 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝐴 + 1) / 2) − 1) ∈ ℤ → ((𝐴 + 1) / 2) ∈ ℤ))
4536, 44sylbid 230 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) / 2) ∈ ℤ → ((𝐴 + 1) / 2) ∈ ℤ))
46 mod0 12631 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+) → ((𝐴 mod (2↑𝑁)) = 0 ↔ (𝐴 / (2↑𝑁)) ∈ ℤ))
471, 6, 46syl2an 494 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod (2↑𝑁)) = 0 ↔ (𝐴 / (2↑𝑁)) ∈ ℤ))
4822nnzd 11441 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 2 ∈ ℤ)
49 nnm1nn0 11294 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
50 zexpcl 12831 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ0) → (2↑(𝑁 − 1)) ∈ ℤ)
5148, 49, 50syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → (2↑(𝑁 − 1)) ∈ ℤ)
5251adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (2↑(𝑁 − 1)) ∈ ℤ)
5352adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝐴 / (2↑𝑁)) ∈ ℤ) → (2↑(𝑁 − 1)) ∈ ℤ)
54 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝐴 / (2↑𝑁)) ∈ ℤ) → (𝐴 / (2↑𝑁)) ∈ ℤ)
5553, 54zmulcld 11448 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝐴 / (2↑𝑁)) ∈ ℤ) → ((2↑(𝑁 − 1)) · (𝐴 / (2↑𝑁))) ∈ ℤ)
5655ex 450 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 / (2↑𝑁)) ∈ ℤ → ((2↑(𝑁 − 1)) · (𝐴 / (2↑𝑁))) ∈ ℤ))
575adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℤ)
5857zcnd 11443 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℂ)
5958, 39negsubd 10358 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 + -1) = (𝑁 − 1))
6059eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) = (𝑁 + -1))
6160oveq1d 6630 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 1) − 𝑁) = ((𝑁 + -1) − 𝑁))
6239negcld 10339 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → -1 ∈ ℂ)
6358, 62pncan2d 10354 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 + -1) − 𝑁) = -1)
6461, 63eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 1) − 𝑁) = -1)
6564oveq2d 6631 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (2↑((𝑁 − 1) − 𝑁)) = (2↑-1))
66 2cnd 11053 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 2 ∈ ℂ)
67 2ne0 11073 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ≠ 0
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 2 ≠ 0)
69 1zzd 11368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → 1 ∈ ℤ)
705, 69zsubcld 11447 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℤ)
7170, 5jca 554 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ))
7271adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ))
73 expsub 12864 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((𝑁 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (2↑((𝑁 − 1) − 𝑁)) = ((2↑(𝑁 − 1)) / (2↑𝑁)))
7466, 68, 72, 73syl21anc 1322 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (2↑((𝑁 − 1) − 𝑁)) = ((2↑(𝑁 − 1)) / (2↑𝑁)))
75 expn1 12826 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 ∈ ℂ → (2↑-1) = (1 / 2))
7666, 75syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (2↑-1) = (1 / 2))
7765, 74, 763eqtr3d 2663 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((2↑(𝑁 − 1)) / (2↑𝑁)) = (1 / 2))
7877oveq2d 6631 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 · ((2↑(𝑁 − 1)) / (2↑𝑁))) = (𝐴 · (1 / 2)))
79 2cnd 11053 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 2 ∈ ℂ)
8079, 49expcld 12964 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → (2↑(𝑁 − 1)) ∈ ℂ)
8180adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (2↑(𝑁 − 1)) ∈ ℂ)
823a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 2 ∈ ℝ+)
8382, 57rpexpcld 12988 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (2↑𝑁) ∈ ℝ+)
8483rpcnne0d 11841 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) ∈ ℂ ∧ (2↑𝑁) ≠ 0))
85 div12 10667 . . . . . . . . . . . . . . . . . . . . . 22 (((2↑(𝑁 − 1)) ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ((2↑𝑁) ∈ ℂ ∧ (2↑𝑁) ≠ 0)) → ((2↑(𝑁 − 1)) · (𝐴 / (2↑𝑁))) = (𝐴 · ((2↑(𝑁 − 1)) / (2↑𝑁))))
8681, 38, 84, 85syl3anc 1323 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((2↑(𝑁 − 1)) · (𝐴 / (2↑𝑁))) = (𝐴 · ((2↑(𝑁 − 1)) / (2↑𝑁))))
8738, 66, 68divrecd 10764 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 / 2) = (𝐴 · (1 / 2)))
8878, 86, 873eqtr4d 2665 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((2↑(𝑁 − 1)) · (𝐴 / (2↑𝑁))) = (𝐴 / 2))
8988eleq1d 2683 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((2↑(𝑁 − 1)) · (𝐴 / (2↑𝑁))) ∈ ℤ ↔ (𝐴 / 2) ∈ ℤ))
9056, 89sylibd 229 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 / (2↑𝑁)) ∈ ℤ → (𝐴 / 2) ∈ ℤ))
9147, 90sylbid 230 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod (2↑𝑁)) = 0 → (𝐴 / 2) ∈ ℤ))
92 zeo2 11424 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℤ → ((𝐴 / 2) ∈ ℤ ↔ ¬ ((𝐴 + 1) / 2) ∈ ℤ))
9392adantr 481 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 / 2) ∈ ℤ ↔ ¬ ((𝐴 + 1) / 2) ∈ ℤ))
9491, 93sylibd 229 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod (2↑𝑁)) = 0 → ¬ ((𝐴 + 1) / 2) ∈ ℤ))
9594necon2ad 2805 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 + 1) / 2) ∈ ℤ → (𝐴 mod (2↑𝑁)) ≠ 0))
9630, 45, 953syld 60 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) / 2) ∈ ℕ → (𝐴 mod (2↑𝑁)) ≠ 0))
9796ex 450 . . . . . . . . . . . . 13 (𝐴 ∈ ℤ → (𝑁 ∈ ℕ → (((𝐴 − 1) / 2) ∈ ℕ → (𝐴 mod (2↑𝑁)) ≠ 0)))
9897com23 86 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → (((𝐴 − 1) / 2) ∈ ℕ → (𝑁 ∈ ℕ → (𝐴 mod (2↑𝑁)) ≠ 0)))
99983imp 1254 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 mod (2↑𝑁)) ≠ 0)
10099neneqd 2795 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ¬ (𝐴 mod (2↑𝑁)) = 0)
101100iffalsed 4075 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → if((𝐴 mod (2↑𝑁)) = 0, ((2↑𝑁) − 1), -1) = -1)
10228, 101eqtrd 2655 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) mod (2↑𝑁)) − (𝐴 mod (2↑𝑁))) = -1)
103 neg1lt0 11087 . . . . . . . . . 10 -1 < 0
104 2re 11050 . . . . . . . . . . . . 13 2 ∈ ℝ
105 1lt2 11154 . . . . . . . . . . . . 13 1 < 2
106 expgt1 12854 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ 𝑁 ∈ ℕ ∧ 1 < 2) → 1 < (2↑𝑁))
107104, 105, 106mp3an13 1412 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 1 < (2↑𝑁))
108 1red 10015 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 1 ∈ ℝ)
109108, 7posdifd 10574 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 < (2↑𝑁) ↔ 0 < ((2↑𝑁) − 1)))
110107, 109mpbid 222 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 0 < ((2↑𝑁) − 1))
111108renegcld 10417 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → -1 ∈ ℝ)
112 0red 10001 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 0 ∈ ℝ)
1137, 108resubcld 10418 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((2↑𝑁) − 1) ∈ ℝ)
114 lttr 10074 . . . . . . . . . . . 12 ((-1 ∈ ℝ ∧ 0 ∈ ℝ ∧ ((2↑𝑁) − 1) ∈ ℝ) → ((-1 < 0 ∧ 0 < ((2↑𝑁) − 1)) → -1 < ((2↑𝑁) − 1)))
115111, 112, 113, 114syl3anc 1323 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((-1 < 0 ∧ 0 < ((2↑𝑁) − 1)) → -1 < ((2↑𝑁) − 1)))
116110, 115mpan2d 709 . . . . . . . . . 10 (𝑁 ∈ ℕ → (-1 < 0 → -1 < ((2↑𝑁) − 1)))
117103, 116mpi 20 . . . . . . . . 9 (𝑁 ∈ ℕ → -1 < ((2↑𝑁) − 1))
1181173ad2ant3 1082 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → -1 < ((2↑𝑁) − 1))
119102, 118eqbrtrd 4645 . . . . . . 7 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) mod (2↑𝑁)) − (𝐴 mod (2↑𝑁))) < ((2↑𝑁) − 1))
1202, 10modcld 12630 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 mod (2↑𝑁)) ∈ ℝ)
121 ltsubadd2b 41624 . . . . . . . 8 (((1 ∈ ℝ ∧ (2↑𝑁) ∈ ℝ) ∧ ((𝐴 mod (2↑𝑁)) ∈ ℝ ∧ ((𝐴 − 1) mod (2↑𝑁)) ∈ ℝ)) → ((((𝐴 − 1) mod (2↑𝑁)) − (𝐴 mod (2↑𝑁))) < ((2↑𝑁) − 1) ↔ (1 + ((𝐴 − 1) mod (2↑𝑁))) < ((2↑𝑁) + (𝐴 mod (2↑𝑁)))))
12218, 8, 120, 16, 121syl22anc 1324 . . . . . . 7 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((𝐴 − 1) mod (2↑𝑁)) − (𝐴 mod (2↑𝑁))) < ((2↑𝑁) − 1) ↔ (1 + ((𝐴 − 1) mod (2↑𝑁))) < ((2↑𝑁) + (𝐴 mod (2↑𝑁)))))
123119, 122mpbid 222 . . . . . 6 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (1 + ((𝐴 − 1) mod (2↑𝑁))) < ((2↑𝑁) + (𝐴 mod (2↑𝑁))))
124 modid0 12652 . . . . . . . . . . . 12 ((2↑𝑁) ∈ ℝ+ → ((2↑𝑁) mod (2↑𝑁)) = 0)
12510, 124syl 17 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) mod (2↑𝑁)) = 0)
126125oveq2d 6631 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod (2↑𝑁)) − ((2↑𝑁) mod (2↑𝑁))) = ((𝐴 mod (2↑𝑁)) − 0))
127120recnd 10028 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 mod (2↑𝑁)) ∈ ℂ)
128127subid1d 10341 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod (2↑𝑁)) − 0) = (𝐴 mod (2↑𝑁)))
129126, 128eqtrd 2655 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod (2↑𝑁)) − ((2↑𝑁) mod (2↑𝑁))) = (𝐴 mod (2↑𝑁)))
130129oveq1d 6630 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 mod (2↑𝑁)) − ((2↑𝑁) mod (2↑𝑁))) mod (2↑𝑁)) = ((𝐴 mod (2↑𝑁)) mod (2↑𝑁)))
131 modsubmodmod 12685 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ (2↑𝑁) ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+) → (((𝐴 mod (2↑𝑁)) − ((2↑𝑁) mod (2↑𝑁))) mod (2↑𝑁)) = ((𝐴 − (2↑𝑁)) mod (2↑𝑁)))
1322, 8, 10, 131syl3anc 1323 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 mod (2↑𝑁)) − ((2↑𝑁) mod (2↑𝑁))) mod (2↑𝑁)) = ((𝐴 − (2↑𝑁)) mod (2↑𝑁)))
133 modabs2 12660 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+) → ((𝐴 mod (2↑𝑁)) mod (2↑𝑁)) = (𝐴 mod (2↑𝑁)))
1342, 10, 133syl2anc 692 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod (2↑𝑁)) mod (2↑𝑁)) = (𝐴 mod (2↑𝑁)))
135130, 132, 1343eqtr3d 2663 . . . . . . 7 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (2↑𝑁)) mod (2↑𝑁)) = (𝐴 mod (2↑𝑁)))
136135oveq2d 6631 . . . . . 6 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) + ((𝐴 − (2↑𝑁)) mod (2↑𝑁))) = ((2↑𝑁) + (𝐴 mod (2↑𝑁))))
137123, 136breqtrrd 4651 . . . . 5 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (1 + ((𝐴 − 1) mod (2↑𝑁))) < ((2↑𝑁) + ((𝐴 − (2↑𝑁)) mod (2↑𝑁))))
13819, 20, 2, 137ltsub2dd 10600 . . . 4 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 − ((2↑𝑁) + ((𝐴 − (2↑𝑁)) mod (2↑𝑁)))) < (𝐴 − (1 + ((𝐴 − 1) mod (2↑𝑁)))))
139313ad2ant1 1080 . . . . 5 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝐴 ∈ ℂ)
1408recnd 10028 . . . . 5 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2↑𝑁) ∈ ℂ)
14111recnd 10028 . . . . 5 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (2↑𝑁)) mod (2↑𝑁)) ∈ ℂ)
142139, 140, 141subsub4d 10383 . . . 4 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (2↑𝑁)) − ((𝐴 − (2↑𝑁)) mod (2↑𝑁))) = (𝐴 − ((2↑𝑁) + ((𝐴 − (2↑𝑁)) mod (2↑𝑁)))))
143 1cnd 10016 . . . . 5 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℂ)
14416recnd 10028 . . . . 5 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 − 1) mod (2↑𝑁)) ∈ ℂ)
145139, 143, 144subsub4d 10383 . . . 4 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 − 1) − ((𝐴 − 1) mod (2↑𝑁))) = (𝐴 − (1 + ((𝐴 − 1) mod (2↑𝑁)))))
146138, 142, 1453brtr4d 4655 . . 3 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (2↑𝑁)) − ((𝐴 − (2↑𝑁)) mod (2↑𝑁))) < ((𝐴 − 1) − ((𝐴 − 1) mod (2↑𝑁))))
14712, 17, 10, 146ltdiv1dd 11889 . 2 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 − (2↑𝑁)) − ((𝐴 − (2↑𝑁)) mod (2↑𝑁))) / (2↑𝑁)) < (((𝐴 − 1) − ((𝐴 − 1) mod (2↑𝑁))) / (2↑𝑁)))
1487recnd 10028 . . . . 5 (𝑁 ∈ ℕ → (2↑𝑁) ∈ ℂ)
1491483ad2ant3 1082 . . . 4 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2↑𝑁) ∈ ℂ)
15067a1i 11 . . . . . 6 (𝑁 ∈ ℕ → 2 ≠ 0)
15179, 150, 5expne0d 12970 . . . . 5 (𝑁 ∈ ℕ → (2↑𝑁) ≠ 0)
1521513ad2ant3 1082 . . . 4 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2↑𝑁) ≠ 0)
153 divsub1dir 41625 . . . . 5 ((𝐴 ∈ ℂ ∧ (2↑𝑁) ∈ ℂ ∧ (2↑𝑁) ≠ 0) → ((𝐴 / (2↑𝑁)) − 1) = ((𝐴 − (2↑𝑁)) / (2↑𝑁)))
154153fveq2d 6162 . . . 4 ((𝐴 ∈ ℂ ∧ (2↑𝑁) ∈ ℂ ∧ (2↑𝑁) ≠ 0) → (⌊‘((𝐴 / (2↑𝑁)) − 1)) = (⌊‘((𝐴 − (2↑𝑁)) / (2↑𝑁))))
155139, 149, 152, 154syl3anc 1323 . . 3 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝐴 / (2↑𝑁)) − 1)) = (⌊‘((𝐴 − (2↑𝑁)) / (2↑𝑁))))
156 fldivmod 41631 . . . 4 (((𝐴 − (2↑𝑁)) ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+) → (⌊‘((𝐴 − (2↑𝑁)) / (2↑𝑁))) = (((𝐴 − (2↑𝑁)) − ((𝐴 − (2↑𝑁)) mod (2↑𝑁))) / (2↑𝑁)))
1579, 10, 156syl2anc 692 . . 3 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝐴 − (2↑𝑁)) / (2↑𝑁))) = (((𝐴 − (2↑𝑁)) − ((𝐴 − (2↑𝑁)) mod (2↑𝑁))) / (2↑𝑁)))
158155, 157eqtrd 2655 . 2 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝐴 / (2↑𝑁)) − 1)) = (((𝐴 − (2↑𝑁)) − ((𝐴 − (2↑𝑁)) mod (2↑𝑁))) / (2↑𝑁)))
159 fldivmod 41631 . . 3 (((𝐴 − 1) ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+) → (⌊‘((𝐴 − 1) / (2↑𝑁))) = (((𝐴 − 1) − ((𝐴 − 1) mod (2↑𝑁))) / (2↑𝑁)))
16015, 10, 159syl2anc 692 . 2 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝐴 − 1) / (2↑𝑁))) = (((𝐴 − 1) − ((𝐴 − 1) mod (2↑𝑁))) / (2↑𝑁)))
161147, 158, 1603brtr4d 4655 1 ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝐴 / (2↑𝑁)) − 1)) < (⌊‘((𝐴 − 1) / (2↑𝑁))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  ifcif 4064   class class class wbr 4623  cfv 5857  (class class class)co 6615  cc 9894  cr 9895  0cc0 9896  1c1 9897   + caddc 9899   · cmul 9901   < clt 10034  cmin 10226  -cneg 10227   / cdiv 10644  cn 10980  2c2 11030  0cn0 11252  cz 11337  +crp 11792  cfl 12547   mod cmo 12624  cexp 12816
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-er 7702  df-en 7916  df-dom 7917  df-sdom 7918  df-sup 8308  df-inf 8309  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-n0 11253  df-z 11338  df-uz 11648  df-rp 11793  df-fz 12285  df-fzo 12423  df-fl 12549  df-mod 12625  df-seq 12758  df-exp 12817
This theorem is referenced by:  dignn0flhalflem2  41732
  Copyright terms: Public domain W3C validator