Metamath Proof Explorer


Theorem dyaddisjlem

Description: Lemma for dyaddisj . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypothesis dyadmbl.1 F = x , y 0 x 2 y x + 1 2 y
Assertion dyaddisjlem A B C 0 D 0 C D . A F C . B F D . B F D . A F C . A F C . B F D =

Proof

Step Hyp Ref Expression
1 dyadmbl.1 F = x , y 0 x 2 y x + 1 2 y
2 simplll A B C 0 D 0 C D A
3 simplrl A B C 0 D 0 C D C 0
4 1 dyadval A C 0 A F C = A 2 C A + 1 2 C
5 2 3 4 syl2anc A B C 0 D 0 C D A F C = A 2 C A + 1 2 C
6 5 fveq2d A B C 0 D 0 C D . A F C = . A 2 C A + 1 2 C
7 df-ov A 2 C A + 1 2 C = . A 2 C A + 1 2 C
8 6 7 eqtr4di A B C 0 D 0 C D . A F C = A 2 C A + 1 2 C
9 simpllr A B C 0 D 0 C D B
10 simplrr A B C 0 D 0 C D D 0
11 1 dyadval B D 0 B F D = B 2 D B + 1 2 D
12 9 10 11 syl2anc A B C 0 D 0 C D B F D = B 2 D B + 1 2 D
13 12 fveq2d A B C 0 D 0 C D . B F D = . B 2 D B + 1 2 D
14 df-ov B 2 D B + 1 2 D = . B 2 D B + 1 2 D
15 13 14 eqtr4di A B C 0 D 0 C D . B F D = B 2 D B + 1 2 D
16 8 15 ineq12d A B C 0 D 0 C D . A F C . B F D = A 2 C A + 1 2 C B 2 D B + 1 2 D
17 incom A 2 C A + 1 2 C B 2 D B + 1 2 D = B 2 D B + 1 2 D A 2 C A + 1 2 C
18 16 17 eqtrdi A B C 0 D 0 C D . A F C . B F D = B 2 D B + 1 2 D A 2 C A + 1 2 C
19 18 adantr A B C 0 D 0 C D B 2 D < A 2 C . A F C . B F D = B 2 D B + 1 2 D A 2 C A + 1 2 C
20 2 zred A B C 0 D 0 C D A
21 20 recnd A B C 0 D 0 C D A
22 2nn 2
23 nnexpcl 2 C 0 2 C
24 22 3 23 sylancr A B C 0 D 0 C D 2 C
25 24 nncnd A B C 0 D 0 C D 2 C
26 nnexpcl 2 D 0 2 D
27 22 10 26 sylancr A B C 0 D 0 C D 2 D
28 27 nncnd A B C 0 D 0 C D 2 D
29 24 nnne0d A B C 0 D 0 C D 2 C 0
30 21 25 28 29 div13d A B C 0 D 0 C D A 2 C 2 D = 2 D 2 C A
31 2cnd A B C 0 D 0 C D 2
32 2ne0 2 0
33 32 a1i A B C 0 D 0 C D 2 0
34 3 nn0zd A B C 0 D 0 C D C
35 10 nn0zd A B C 0 D 0 C D D
36 31 33 34 35 expsubd A B C 0 D 0 C D 2 D C = 2 D 2 C
37 2z 2
38 simpr A B C 0 D 0 C D C D
39 znn0sub C D C D D C 0
40 34 35 39 syl2anc A B C 0 D 0 C D C D D C 0
41 38 40 mpbid A B C 0 D 0 C D D C 0
42 zexpcl 2 D C 0 2 D C
43 37 41 42 sylancr A B C 0 D 0 C D 2 D C
44 36 43 eqeltrrd A B C 0 D 0 C D 2 D 2 C
45 44 2 zmulcld A B C 0 D 0 C D 2 D 2 C A
46 30 45 eqeltrd A B C 0 D 0 C D A 2 C 2 D
47 zltp1le B A 2 C 2 D B < A 2 C 2 D B + 1 A 2 C 2 D
48 9 46 47 syl2anc A B C 0 D 0 C D B < A 2 C 2 D B + 1 A 2 C 2 D
49 9 zred A B C 0 D 0 C D B
50 20 24 nndivred A B C 0 D 0 C D A 2 C
51 27 nnred A B C 0 D 0 C D 2 D
52 27 nngt0d A B C 0 D 0 C D 0 < 2 D
53 ltdivmul2 B A 2 C 2 D 0 < 2 D B 2 D < A 2 C B < A 2 C 2 D
54 49 50 51 52 53 syl112anc A B C 0 D 0 C D B 2 D < A 2 C B < A 2 C 2 D
55 peano2re B B + 1
56 49 55 syl A B C 0 D 0 C D B + 1
57 ledivmul2 B + 1 A 2 C 2 D 0 < 2 D B + 1 2 D A 2 C B + 1 A 2 C 2 D
58 56 50 51 52 57 syl112anc A B C 0 D 0 C D B + 1 2 D A 2 C B + 1 A 2 C 2 D
59 48 54 58 3bitr4d A B C 0 D 0 C D B 2 D < A 2 C B + 1 2 D A 2 C
60 49 27 nndivred A B C 0 D 0 C D B 2 D
61 60 rexrd A B C 0 D 0 C D B 2 D *
62 56 27 nndivred A B C 0 D 0 C D B + 1 2 D
63 62 rexrd A B C 0 D 0 C D B + 1 2 D *
64 50 rexrd A B C 0 D 0 C D A 2 C *
65 peano2re A A + 1
66 20 65 syl A B C 0 D 0 C D A + 1
67 66 24 nndivred A B C 0 D 0 C D A + 1 2 C
68 67 rexrd A B C 0 D 0 C D A + 1 2 C *
69 ioodisj B 2 D * B + 1 2 D * A 2 C * A + 1 2 C * B + 1 2 D A 2 C B 2 D B + 1 2 D A 2 C A + 1 2 C =
70 69 ex B 2 D * B + 1 2 D * A 2 C * A + 1 2 C * B + 1 2 D A 2 C B 2 D B + 1 2 D A 2 C A + 1 2 C =
71 61 63 64 68 70 syl22anc A B C 0 D 0 C D B + 1 2 D A 2 C B 2 D B + 1 2 D A 2 C A + 1 2 C =
72 59 71 sylbid A B C 0 D 0 C D B 2 D < A 2 C B 2 D B + 1 2 D A 2 C A + 1 2 C =
73 72 imp A B C 0 D 0 C D B 2 D < A 2 C B 2 D B + 1 2 D A 2 C A + 1 2 C =
74 19 73 eqtrd A B C 0 D 0 C D B 2 D < A 2 C . A F C . B F D =
75 74 3mix3d A B C 0 D 0 C D B 2 D < A 2 C . A F C . B F D . B F D . A F C . A F C . B F D =
76 50 adantr A B C 0 D 0 C D A 2 C B 2 D B 2 D < A + 1 2 C A 2 C
77 67 adantr A B C 0 D 0 C D A 2 C B 2 D B 2 D < A + 1 2 C A + 1 2 C
78 simprl A B C 0 D 0 C D A 2 C B 2 D B 2 D < A + 1 2 C A 2 C B 2 D
79 66 recnd A B C 0 D 0 C D A + 1
80 79 25 28 29 div13d A B C 0 D 0 C D A + 1 2 C 2 D = 2 D 2 C A + 1
81 2 peano2zd A B C 0 D 0 C D A + 1
82 44 81 zmulcld A B C 0 D 0 C D 2 D 2 C A + 1
83 80 82 eqeltrd A B C 0 D 0 C D A + 1 2 C 2 D
84 zltp1le B A + 1 2 C 2 D B < A + 1 2 C 2 D B + 1 A + 1 2 C 2 D
85 9 83 84 syl2anc A B C 0 D 0 C D B < A + 1 2 C 2 D B + 1 A + 1 2 C 2 D
86 ltdivmul2 B A + 1 2 C 2 D 0 < 2 D B 2 D < A + 1 2 C B < A + 1 2 C 2 D
87 49 67 51 52 86 syl112anc A B C 0 D 0 C D B 2 D < A + 1 2 C B < A + 1 2 C 2 D
88 ledivmul2 B + 1 A + 1 2 C 2 D 0 < 2 D B + 1 2 D A + 1 2 C B + 1 A + 1 2 C 2 D
89 56 67 51 52 88 syl112anc A B C 0 D 0 C D B + 1 2 D A + 1 2 C B + 1 A + 1 2 C 2 D
90 85 87 89 3bitr4d A B C 0 D 0 C D B 2 D < A + 1 2 C B + 1 2 D A + 1 2 C
91 90 biimpa A B C 0 D 0 C D B 2 D < A + 1 2 C B + 1 2 D A + 1 2 C
92 91 adantrl A B C 0 D 0 C D A 2 C B 2 D B 2 D < A + 1 2 C B + 1 2 D A + 1 2 C
93 iccss A 2 C A + 1 2 C A 2 C B 2 D B + 1 2 D A + 1 2 C B 2 D B + 1 2 D A 2 C A + 1 2 C
94 76 77 78 92 93 syl22anc A B C 0 D 0 C D A 2 C B 2 D B 2 D < A + 1 2 C B 2 D B + 1 2 D A 2 C A + 1 2 C
95 12 fveq2d A B C 0 D 0 C D . B F D = . B 2 D B + 1 2 D
96 df-ov B 2 D B + 1 2 D = . B 2 D B + 1 2 D
97 95 96 eqtr4di A B C 0 D 0 C D . B F D = B 2 D B + 1 2 D
98 97 adantr A B C 0 D 0 C D A 2 C B 2 D B 2 D < A + 1 2 C . B F D = B 2 D B + 1 2 D
99 5 fveq2d A B C 0 D 0 C D . A F C = . A 2 C A + 1 2 C
100 df-ov A 2 C A + 1 2 C = . A 2 C A + 1 2 C
101 99 100 eqtr4di A B C 0 D 0 C D . A F C = A 2 C A + 1 2 C
102 101 adantr A B C 0 D 0 C D A 2 C B 2 D B 2 D < A + 1 2 C . A F C = A 2 C A + 1 2 C
103 94 98 102 3sstr4d A B C 0 D 0 C D A 2 C B 2 D B 2 D < A + 1 2 C . B F D . A F C
104 103 3mix2d A B C 0 D 0 C D A 2 C B 2 D B 2 D < A + 1 2 C . A F C . B F D . B F D . A F C . A F C . B F D =
105 104 anassrs A B C 0 D 0 C D A 2 C B 2 D B 2 D < A + 1 2 C . A F C . B F D . B F D . A F C . A F C . B F D =
106 16 adantr A B C 0 D 0 C D A + 1 2 C B 2 D . A F C . B F D = A 2 C A + 1 2 C B 2 D B + 1 2 D
107 ioodisj A 2 C * A + 1 2 C * B 2 D * B + 1 2 D * A + 1 2 C B 2 D A 2 C A + 1 2 C B 2 D B + 1 2 D =
108 107 ex A 2 C * A + 1 2 C * B 2 D * B + 1 2 D * A + 1 2 C B 2 D A 2 C A + 1 2 C B 2 D B + 1 2 D =
109 64 68 61 63 108 syl22anc A B C 0 D 0 C D A + 1 2 C B 2 D A 2 C A + 1 2 C B 2 D B + 1 2 D =
110 109 imp A B C 0 D 0 C D A + 1 2 C B 2 D A 2 C A + 1 2 C B 2 D B + 1 2 D =
111 106 110 eqtrd A B C 0 D 0 C D A + 1 2 C B 2 D . A F C . B F D =
112 111 3mix3d A B C 0 D 0 C D A + 1 2 C B 2 D . A F C . B F D . B F D . A F C . A F C . B F D =
113 112 adantlr A B C 0 D 0 C D A 2 C B 2 D A + 1 2 C B 2 D . A F C . B F D . B F D . A F C . A F C . B F D =
114 60 adantr A B C 0 D 0 C D A 2 C B 2 D B 2 D
115 67 adantr A B C 0 D 0 C D A 2 C B 2 D A + 1 2 C
116 105 113 114 115 ltlecasei A B C 0 D 0 C D A 2 C B 2 D . A F C . B F D . B F D . A F C . A F C . B F D =
117 75 116 60 50 ltlecasei A B C 0 D 0 C D . A F C . B F D . B F D . A F C . A F C . B F D =