Metamath Proof Explorer

Theorem dignn0flhalflem2

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

Ref Expression
Assertion dignn0flhalflem2 ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2N+1=A22N

Proof

Step Hyp Ref Expression
1 zre ⊢A∈ℤ→A∈ℝ
2 1 rehalfcld ⊢A∈ℤ→A2∈ℝ
3 2 flcld ⊢A∈ℤ→A2∈ℤ
4 3 zred ⊢A∈ℤ→A2∈ℝ
5 4 3ad2ant1 ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2∈ℝ
6 2re ⊢2∈ℝ
7 6 a1i ⊢N∈ℕ0→2∈ℝ
8 id ⊢N∈ℕ0→N∈ℕ0
9 7 8 reexpcld ⊢N∈ℕ0→2N∈ℝ
10 9 3ad2ant3 ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2N∈ℝ
11 2cnd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2∈ℂ
12 2ne0 ⊢2≠0
13 12 a1i ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2≠0
14 nn0z ⊢N∈ℕ0→N∈ℤ
15 14 3ad2ant3 ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→N∈ℤ
16 11 13 15 expne0d ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2N≠0
17 5 10 16 redivcld ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A22N∈ℝ
18 17 flcld ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A22N∈ℤ
19 1 3ad2ant1 ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A∈ℝ
20 6 a1i ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2∈ℝ
21 simp3 ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→N∈ℕ0
22 1nn0 ⊢1∈ℕ0
23 22 a1i ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→1∈ℕ0
24 21 23 nn0addcld ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→N+1∈ℕ0
25 20 24 reexpcld ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2N+1∈ℝ
26 15 peano2zd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→N+1∈ℤ
27 11 13 26 expne0d ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2N+1≠0
28 19 25 27 redivcld ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2N+1∈ℝ
29 28 flcld ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2N+1∈ℤ
30 nn0p1nn ⊢N∈ℕ0→N+1∈ℕ
31 dignn0flhalflem1 ⊢A∈ℤ∧A−12∈ℕ∧N+1∈ℕ→A2N+1−1<A−12N+1
32 30 31 syl3an3 ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2N+1−1<A−12N+1
33 1zzd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→1∈ℤ
34 flsubz ⊢A2N+1∈ℝ∧1∈ℤ→A2N+1−1=A2N+1−1
35 28 33 34 syl2anc ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2N+1−1=A2N+1−1
36 35 eqcomd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2N+1−1=A2N+1−1
37 nnz ⊢A−12∈ℕ→A−12∈ℤ
38 zob ⊢A∈ℤ→A+12∈ℤ↔A−12∈ℤ
39 37 38 imbitrrid ⊢A∈ℤ→A−12∈ℕ→A+12∈ℤ
40 39 imp ⊢A∈ℤ∧A−12∈ℕ→A+12∈ℤ
41 zofldiv2 ⊢A∈ℤ∧A+12∈ℤ→A2=A−12
42 40 41 syldan ⊢A∈ℤ∧A−12∈ℕ→A2=A−12
43 42 3adant3 ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2=A−12
44 43 fvoveq1d ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A22N=A−122N
45 zcn ⊢A∈ℤ→A∈ℂ
46 1cnd ⊢A∈ℤ→1∈ℂ
47 45 46 subcld ⊢A∈ℤ→A−1∈ℂ
48 2rp ⊢2∈ℝ+
49 48 a1i ⊢A−12∈ℕ→2∈ℝ+
50 49 rpcnne0d ⊢A−12∈ℕ→2∈ℂ∧2≠0
51 48 a1i ⊢N∈ℕ0→2∈ℝ+
52 51 14 rpexpcld ⊢N∈ℕ0→2N∈ℝ+
53 52 rpcnne0d ⊢N∈ℕ0→2N∈ℂ∧2N≠0
54 divdiv1 ⊢A−1∈ℂ∧2∈ℂ∧2≠0∧2N∈ℂ∧2N≠0→A−122N=A−12⁢2N
55 47 50 53 54 syl3an ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A−122N=A−12⁢2N
56 10 recnd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2N∈ℂ
57 11 56 mulcomd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2⁢2N=2N⋅2
58 11 21 expp1d ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2N+1=2N⋅2
59 57 58 eqtr4d ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2⁢2N=2N+1
60 59 oveq2d ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A−12⁢2N=A−12N+1
61 55 60 eqtrd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A−122N=A−12N+1
62 61 fveq2d ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A−122N=A−12N+1
63 44 62 eqtrd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A22N=A−12N+1
64 32 36 63 3brtr4d ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2N+1−1<A22N
65 19 rehalfcld ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2∈ℝ
66 65 10 16 redivcld ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A22N∈ℝ
67 reflcl ⊢A2∈ℝ→A2∈ℝ
68 65 67 syl ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2∈ℝ
69 48 a1i ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2∈ℝ+
70 69 15 rpexpcld ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2N∈ℝ+
71 flle ⊢A2∈ℝ→A2≤A2
72 65 71 syl ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2≤A2
73 68 65 70 72 lediv1dd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A22N≤A22N
74 flwordi ⊢A22N∈ℝ∧A22N∈ℝ∧A22N≤A22N→A22N≤A22N
75 17 66 73 74 syl3anc ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A22N≤A22N
76 divdiv1 ⊢A∈ℂ∧2∈ℂ∧2≠0∧2N∈ℂ∧2N≠0→A22N=A2⁢2N
77 45 50 53 76 syl3an ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A22N=A2⁢2N
78 52 rpcnd ⊢N∈ℕ0→2N∈ℂ
79 78 3ad2ant3 ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2N∈ℂ
80 11 79 mulcomd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2⁢2N=2N⋅2
81 11 13 15 expp1zd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2N+1=2N⋅2
82 80 81 eqtr4d ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→2⁢2N=2N+1
83 82 oveq2d ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2⁢2N=A2N+1
84 77 83 eqtrd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A22N=A2N+1
85 84 eqcomd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2N+1=A22N
86 85 fveq2d ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2N+1=A22N
87 75 86 breqtrrd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A22N≤A2N+1
88 zgtp1leeq ⊢A22N∈ℤ∧A2N+1∈ℤ→A2N+1−1<A22N∧A22N≤A2N+1→A22N=A2N+1
89 88 imp ⊢A22N∈ℤ∧A2N+1∈ℤ∧A2N+1−1<A22N∧A22N≤A2N+1→A22N=A2N+1
90 18 29 64 87 89 syl22anc ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A22N=A2N+1
91 90 eqcomd ⊢A∈ℤ∧A−12∈ℕ∧N∈ℕ0→A2N+1=A22N