Metamath Proof Explorer


Theorem 3cubeslem3l

Description: Lemma for 3cubes . (Contributed by Igor Ieskov, 22-Jan-2024)

Ref Expression
Hypothesis 3cubeslem1.a φ A
Assertion 3cubeslem3l φ A 3 3 A 2 + 3 2 A + 3 3 = A 7 3 9 + A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3

Proof

Step Hyp Ref Expression
1 3cubeslem1.a φ A
2 3cn 3
3 2 a1i φ 3
4 3nn0 3 0
5 4 a1i φ 3 0
6 3 5 expcld φ 3 3
7 qcn A A
8 1 7 syl φ A
9 8 sqcld φ A 2
10 6 9 mulcld φ 3 3 A 2
11 3 sqcld φ 3 2
12 11 8 mulcld φ 3 2 A
13 10 12 3 cu3addd φ 3 3 A 2 + 3 2 A + 3 3 = 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
14 13 oveq2d φ A 3 3 A 2 + 3 2 A + 3 3 = A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
15 10 5 expcld φ 3 3 A 2 3
16 10 sqcld φ 3 3 A 2 2
17 16 12 mulcld φ 3 3 A 2 2 3 2 A
18 3 17 mulcld φ 3 3 3 A 2 2 3 2 A
19 15 18 addcld φ 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A
20 12 sqcld φ 3 2 A 2
21 10 20 mulcld φ 3 3 A 2 3 2 A 2
22 3 21 mulcld φ 3 3 3 A 2 3 2 A 2
23 12 5 expcld φ 3 2 A 3
24 22 23 addcld φ 3 3 3 A 2 3 2 A 2 + 3 2 A 3
25 19 24 addcld φ 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3
26 16 3 mulcld φ 3 3 A 2 2 3
27 3 26 mulcld φ 3 3 3 A 2 2 3
28 2nn0 2 0
29 28 a1i φ 2 0
30 5 29 nn0mulcld φ 3 2 0
31 30 nn0cnd φ 3 2
32 10 12 mulcld φ 3 3 A 2 3 2 A
33 31 32 mulcld φ 3 2 3 3 A 2 3 2 A
34 33 3 mulcld φ 3 2 3 3 A 2 3 2 A 3
35 27 34 addcld φ 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3
36 20 3 mulcld φ 3 2 A 2 3
37 3 36 mulcld φ 3 3 2 A 2 3
38 35 37 addcld φ 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3
39 25 38 addcld φ 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3
40 10 11 mulcld φ 3 3 A 2 3 2
41 3 40 mulcld φ 3 3 3 A 2 3 2
42 12 11 mulcld φ 3 2 A 3 2
43 3 42 mulcld φ 3 3 2 A 3 2
44 41 43 addcld φ 3 3 3 A 2 3 2 + 3 3 2 A 3 2
45 44 6 addcld φ 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
46 8 39 45 adddid φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
47 8 25 38 adddid φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 = A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3
48 47 oveq1d φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
49 46 48 eqtrd φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
50 8 19 24 adddid φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 = A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3
51 50 oveq1d φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 = A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3
52 51 oveq1d φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
53 49 52 eqtrd φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
54 8 15 18 adddid φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A
55 54 oveq1d φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3
56 55 oveq1d φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3
57 56 oveq1d φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
58 53 57 eqtrd φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
59 8 22 23 adddid φ A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 = A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3
60 59 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3
61 60 oveq1d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3
62 61 oveq1d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
63 58 62 eqtrd φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
64 8 35 37 adddid φ A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 = A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3
65 64 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3
66 65 oveq1d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
67 63 66 eqtrd φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
68 8 27 34 adddid φ A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3
69 68 oveq1d φ A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3
70 69 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3
71 70 oveq1d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
72 67 71 eqtrd φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3
73 8 44 6 adddid φ A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + A 3 3
74 73 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + A 3 3
75 72 74 eqtrd φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + A 3 3
76 8 41 43 adddid φ A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 = A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2
77 76 oveq1d φ A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
78 77 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
79 75 78 eqtrd φ A 3 3 A 2 3 + 3 3 3 A 2 2 3 2 A + 3 3 3 A 2 3 2 A 2 + 3 2 A 3 + 3 3 3 A 2 2 3 + 3 2 3 3 A 2 3 2 A 3 + 3 3 2 A 2 3 + 3 3 3 A 2 3 2 + 3 3 2 A 3 2 + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
80 14 79 eqtrd φ A 3 3 A 2 + 3 2 A + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
81 8 15 mulcld φ A 3 3 A 2 3
82 8 18 mulcld φ A 3 3 3 A 2 2 3 2 A
83 81 82 addcld φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A
84 8 22 mulcld φ A 3 3 3 A 2 3 2 A 2
85 8 23 mulcld φ A 3 2 A 3
86 84 85 addcld φ A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3
87 83 86 addcld φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3
88 8 27 mulcld φ A 3 3 3 A 2 2 3
89 8 34 mulcld φ A 3 2 3 3 A 2 3 2 A 3
90 88 89 addcld φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3
91 8 37 mulcld φ A 3 3 2 A 2 3
92 90 91 addcld φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3
93 8 41 mulcld φ A 3 3 3 A 2 3 2
94 8 43 mulcld φ A 3 3 2 A 3 2
95 93 94 addcld φ A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2
96 8 6 mulcld φ A 3 3
97 95 96 addcld φ A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
98 87 92 97 addassd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
99 92 97 addcld φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
100 83 86 99 addassd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
101 98 100 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
102 86 99 addcld φ A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
103 81 82 102 addassd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
104 101 103 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
105 84 85 99 addassd φ A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
106 105 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
107 106 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
108 104 107 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
109 85 99 addcomd φ A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
110 109 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
111 110 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
112 111 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
113 108 112 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
114 92 97 85 addassd φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
115 114 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
116 115 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
117 116 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
118 113 117 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
119 97 85 addcld φ A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
120 90 91 119 addassd φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
121 120 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
122 121 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
123 122 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
124 118 123 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
125 91 119 addcld φ A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
126 88 89 125 addassd φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
127 126 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
128 127 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
129 128 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
130 124 129 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3
131 91 119 addcomd φ A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3
132 131 oveq2d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 2 3 3 A 2 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3
133 132 oveq2d φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3
134 133 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3
135 134 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3
136 135 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3
137 130 136 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3
138 97 85 addcomd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 = A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3
139 138 oveq1d φ A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3 = A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
140 139 oveq2d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3 = A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
141 140 oveq2d φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
142 141 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
143 142 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
144 143 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 2 A 3 + A 3 3 2 A 2 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
145 137 144 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
146 85 97 91 addassd φ A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
147 146 oveq2d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
148 147 oveq2d φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
149 148 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
150 149 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
151 150 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
152 145 151 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
153 95 96 91 addassd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
154 153 oveq2d φ A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
155 154 oveq2d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
156 155 oveq2d φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
157 156 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
158 157 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
159 158 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
160 152 159 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
161 96 91 addcld φ A 3 3 + A 3 3 2 A 2 3
162 93 94 161 addassd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
163 162 oveq2d φ A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
164 163 oveq2d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
165 164 oveq2d φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
166 165 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
167 166 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
168 167 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
169 160 168 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3
170 94 161 addcomd φ A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2
171 170 oveq2d φ A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2
172 171 oveq2d φ A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2
173 172 oveq2d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2
174 173 oveq2d φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2
175 174 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2
176 175 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2
177 176 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 + A 3 3 2 A 2 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2
178 169 177 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2
179 96 91 addcomd φ A 3 3 + A 3 3 2 A 2 3 = A 3 3 2 A 2 3 + A 3 3
180 179 oveq1d φ A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 = A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
181 180 oveq2d φ A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 = A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
182 181 oveq2d φ A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 = A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
183 182 oveq2d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 = A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
184 183 oveq2d φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
185 184 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
186 185 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
187 186 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
188 178 187 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
189 91 96 94 addassd φ A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
190 189 oveq2d φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
191 190 oveq2d φ A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
192 191 oveq2d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
193 192 oveq2d φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
194 193 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
195 194 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
196 195 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
197 188 196 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2
198 96 94 addcomd φ A 3 3 + A 3 3 2 A 3 2 = A 3 3 2 A 3 2 + A 3 3
199 198 oveq2d φ A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
200 199 oveq2d φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
201 200 oveq2d φ A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
202 201 oveq2d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
203 202 oveq2d φ A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
204 203 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
205 204 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
206 205 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 + A 3 3 2 A 3 2 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
207 197 206 eqtrd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 2 A 3 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 3 2 A 2 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
208 80 207 eqtrd φ A 3 3 A 2 + 3 2 A + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
209 94 96 addcld φ A 3 3 2 A 3 2 + A 3 3
210 91 209 addcld φ A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
211 93 210 addcld φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
212 85 211 addcld φ A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
213 89 212 addcld φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
214 84 88 213 addassd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
215 214 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
216 215 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
217 216 eqcomd φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
218 89 85 211 addassd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
219 218 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
220 219 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
221 220 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
222 217 221 eqtr4d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
223 93 91 209 addassd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
224 223 oveq2d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
225 224 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
226 225 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
227 226 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
228 222 227 eqtr4d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
229 208 228 eqtrd φ A 3 3 A 2 + 3 2 A + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3
230 3 42 mulcomd φ 3 3 2 A 3 2 = 3 2 A 3 2 3
231 230 oveq2d φ A 3 3 2 A 3 2 = A 3 2 A 3 2 3
232 11 8 mulcomd φ 3 2 A = A 3 2
233 232 oveq1d φ 3 2 A 3 2 = A 3 2 3 2
234 233 oveq1d φ 3 2 A 3 2 3 = A 3 2 3 2 3
235 234 oveq2d φ A 3 2 A 3 2 3 = A A 3 2 3 2 3
236 231 235 eqtrd φ A 3 3 2 A 3 2 = A A 3 2 3 2 3
237 8 11 mulcld φ A 3 2
238 237 11 3 mulassd φ A 3 2 3 2 3 = A 3 2 3 2 3
239 238 oveq2d φ A A 3 2 3 2 3 = A A 3 2 3 2 3
240 236 239 eqtrd φ A 3 3 2 A 3 2 = A A 3 2 3 2 3
241 11 3 mulcld φ 3 2 3
242 8 11 241 mulassd φ A 3 2 3 2 3 = A 3 2 3 2 3
243 242 oveq2d φ A A 3 2 3 2 3 = A A 3 2 3 2 3
244 240 243 eqtrd φ A 3 3 2 A 3 2 = A A 3 2 3 2 3
245 11 241 mulcld φ 3 2 3 2 3
246 8 8 245 mulassd φ A A 3 2 3 2 3 = A A 3 2 3 2 3
247 246 eqcomd φ A A 3 2 3 2 3 = A A 3 2 3 2 3
248 11 11 3 mulassd φ 3 2 3 2 3 = 3 2 3 2 3
249 248 oveq2d φ A A 3 2 3 2 3 = A A 3 2 3 2 3
250 247 249 eqtr4d φ A A 3 2 3 2 3 = A A 3 2 3 2 3
251 244 250 eqtrd φ A 3 3 2 A 3 2 = A A 3 2 3 2 3
252 8 sqvald φ A 2 = A A
253 252 eqcomd φ A A = A 2
254 253 oveq1d φ A A 3 2 3 2 3 = A 2 3 2 3 2 3
255 251 254 eqtrd φ A 3 3 2 A 3 2 = A 2 3 2 3 2 3
256 3 29 29 expaddd φ 3 2 + 2 = 3 2 3 2
257 256 oveq1d φ 3 2 + 2 3 = 3 2 3 2 3
258 257 eqcomd φ 3 2 3 2 3 = 3 2 + 2 3
259 29 29 nn0addcld φ 2 + 2 0
260 3 259 expp1d φ 3 2 + 2 + 1 = 3 2 + 2 3
261 258 260 eqtr4d φ 3 2 3 2 3 = 3 2 + 2 + 1
262 261 oveq2d φ A 2 3 2 3 2 3 = A 2 3 2 + 2 + 1
263 255 262 eqtrd φ A 3 3 2 A 3 2 = A 2 3 2 + 2 + 1
264 2p2e4 2 + 2 = 4
265 264 a1i φ 2 + 2 = 4
266 265 oveq1d φ 2 + 2 + 1 = 4 + 1
267 266 oveq2d φ 3 2 + 2 + 1 = 3 4 + 1
268 267 oveq2d φ A 2 3 2 + 2 + 1 = A 2 3 4 + 1
269 263 268 eqtrd φ A 3 3 2 A 3 2 = A 2 3 4 + 1
270 4p1e5 4 + 1 = 5
271 270 a1i φ 4 + 1 = 5
272 271 oveq2d φ 3 4 + 1 = 3 5
273 272 oveq2d φ A 2 3 4 + 1 = A 2 3 5
274 269 273 eqtrd φ A 3 3 2 A 3 2 = A 2 3 5
275 274 oveq1d φ A 3 3 2 A 3 2 + A 3 3 = A 2 3 5 + A 3 3
276 275 oveq2d φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 2 3 5 + A 3 3
277 276 oveq2d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 2 3 5 + A 3 3
278 277 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 2 3 5 + A 3 3
279 278 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 2 3 5 + A 3 3
280 279 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 3 3 2 A 3 2 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 2 3 5 + A 3 3
281 229 280 eqtrd φ A 3 3 A 2 + 3 2 A + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 2 3 5 + A 3 3
282 8 41 mulcomd φ A 3 3 3 A 2 3 2 = 3 3 3 A 2 3 2 A
283 3 40 mulcomd φ 3 3 3 A 2 3 2 = 3 3 A 2 3 2 3
284 283 oveq1d φ 3 3 3 A 2 3 2 A = 3 3 A 2 3 2 3 A
285 282 284 eqtrd φ A 3 3 3 A 2 3 2 = 3 3 A 2 3 2 3 A
286 6 9 mulcomd φ 3 3 A 2 = A 2 3 3
287 286 oveq1d φ 3 3 A 2 3 2 = A 2 3 3 3 2
288 287 oveq1d φ 3 3 A 2 3 2 3 = A 2 3 3 3 2 3
289 288 oveq1d φ 3 3 A 2 3 2 3 A = A 2 3 3 3 2 3 A
290 285 289 eqtrd φ A 3 3 3 A 2 3 2 = A 2 3 3 3 2 3 A
291 9 6 mulcld φ A 2 3 3
292 291 11 mulcld φ A 2 3 3 3 2
293 292 3 8 mulassd φ A 2 3 3 3 2 3 A = A 2 3 3 3 2 3 A
294 290 293 eqtrd φ A 3 3 3 A 2 3 2 = A 2 3 3 3 2 3 A
295 3 8 mulcld φ 3 A
296 291 11 295 mulassd φ A 2 3 3 3 2 3 A = A 2 3 3 3 2 3 A
297 294 296 eqtrd φ A 3 3 3 A 2 3 2 = A 2 3 3 3 2 3 A
298 11 295 mulcld φ 3 2 3 A
299 9 6 298 mulassd φ A 2 3 3 3 2 3 A = A 2 3 3 3 2 3 A
300 297 299 eqtrd φ A 3 3 3 A 2 3 2 = A 2 3 3 3 2 3 A
301 6 298 mulcomd φ 3 3 3 2 3 A = 3 2 3 A 3 3
302 301 oveq2d φ A 2 3 3 3 2 3 A = A 2 3 2 3 A 3 3
303 300 302 eqtrd φ A 3 3 3 A 2 3 2 = A 2 3 2 3 A 3 3
304 11 295 mulcomd φ 3 2 3 A = 3 A 3 2
305 304 oveq1d φ 3 2 3 A 3 3 = 3 A 3 2 3 3
306 305 oveq2d φ A 2 3 2 3 A 3 3 = A 2 3 A 3 2 3 3
307 303 306 eqtrd φ A 3 3 3 A 2 3 2 = A 2 3 A 3 2 3 3
308 3 8 mulcomd φ 3 A = A 3
309 308 oveq1d φ 3 A 3 2 = A 3 3 2
310 309 oveq1d φ 3 A 3 2 3 3 = A 3 3 2 3 3
311 310 oveq2d φ A 2 3 A 3 2 3 3 = A 2 A 3 3 2 3 3
312 307 311 eqtrd φ A 3 3 3 A 2 3 2 = A 2 A 3 3 2 3 3
313 8 3 mulcld φ A 3
314 313 11 6 mulassd φ A 3 3 2 3 3 = A 3 3 2 3 3
315 314 oveq2d φ A 2 A 3 3 2 3 3 = A 2 A 3 3 2 3 3
316 312 315 eqtrd φ A 3 3 3 A 2 3 2 = A 2 A 3 3 2 3 3
317 11 6 mulcld φ 3 2 3 3
318 8 3 317 mulassd φ A 3 3 2 3 3 = A 3 3 2 3 3
319 318 oveq2d φ A 2 A 3 3 2 3 3 = A 2 A 3 3 2 3 3
320 316 319 eqtrd φ A 3 3 3 A 2 3 2 = A 2 A 3 3 2 3 3
321 320 oveq1d φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 2 A 3 3 2 3 3 + A 3 3 2 A 2 3
322 3 317 mulcld φ 3 3 2 3 3
323 9 8 322 mulassd φ A 2 A 3 3 2 3 3 = A 2 A 3 3 2 3 3
324 323 oveq1d φ A 2 A 3 3 2 3 3 + A 3 3 2 A 2 3 = A 2 A 3 3 2 3 3 + A 3 3 2 A 2 3
325 321 324 eqtr4d φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 2 A 3 3 2 3 3 + A 3 3 2 A 2 3
326 8 29 expp1d φ A 2 + 1 = A 2 A
327 326 eqcomd φ A 2 A = A 2 + 1
328 327 oveq1d φ A 2 A 3 3 2 3 3 = A 2 + 1 3 3 2 3 3
329 328 oveq1d φ A 2 A 3 3 2 3 3 + A 3 3 2 A 2 3 = A 2 + 1 3 3 2 3 3 + A 3 3 2 A 2 3
330 325 329 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 2 + 1 3 3 2 3 3 + A 3 3 2 A 2 3
331 2p1e3 2 + 1 = 3
332 331 a1i φ 2 + 1 = 3
333 332 oveq2d φ A 2 + 1 = A 3
334 333 oveq1d φ A 2 + 1 3 3 2 3 3 = A 3 3 3 2 3 3
335 334 oveq1d φ A 2 + 1 3 3 2 3 3 + A 3 3 2 A 2 3 = A 3 3 3 2 3 3 + A 3 3 2 A 2 3
336 330 335 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 3 2 3 3 + A 3 3 2 A 2 3
337 3 5 29 expaddd φ 3 2 + 3 = 3 2 3 3
338 337 oveq2d φ 3 3 2 + 3 = 3 3 2 3 3
339 338 eqcomd φ 3 3 2 3 3 = 3 3 2 + 3
340 29 5 nn0addcld φ 2 + 3 0
341 3 340 expcld φ 3 2 + 3
342 3 341 mulcomd φ 3 3 2 + 3 = 3 2 + 3 3
343 339 342 eqtrd φ 3 3 2 3 3 = 3 2 + 3 3
344 3 340 expp1d φ 3 2 + 3 + 1 = 3 2 + 3 3
345 343 344 eqtr4d φ 3 3 2 3 3 = 3 2 + 3 + 1
346 345 oveq2d φ A 3 3 3 2 3 3 = A 3 3 2 + 3 + 1
347 346 oveq1d φ A 3 3 3 2 3 3 + A 3 3 2 A 2 3 = A 3 3 2 + 3 + 1 + A 3 3 2 A 2 3
348 336 347 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 2 + 3 + 1 + A 3 3 2 A 2 3
349 332 oveq2d φ 2 + 2 + 1 = 2 + 3
350 349 oveq1d φ 2 + 2 + 1 + 1 = 2 + 3 + 1
351 350 oveq2d φ 3 2 + 2 + 1 + 1 = 3 2 + 3 + 1
352 351 oveq2d φ A 3 3 2 + 2 + 1 + 1 = A 3 3 2 + 3 + 1
353 352 oveq1d φ A 3 3 2 + 2 + 1 + 1 + A 3 3 2 A 2 3 = A 3 3 2 + 3 + 1 + A 3 3 2 A 2 3
354 348 353 eqtr4d φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 2 + 2 + 1 + 1 + A 3 3 2 A 2 3
355 29 nn0cnd φ 2
356 ax-1cn 1
357 356 a1i φ 1
358 355 355 357 addassd φ 2 + 2 + 1 = 2 + 2 + 1
359 358 oveq1d φ 2 + 2 + 1 + 1 = 2 + 2 + 1 + 1
360 359 oveq2d φ 3 2 + 2 + 1 + 1 = 3 2 + 2 + 1 + 1
361 360 oveq2d φ A 3 3 2 + 2 + 1 + 1 = A 3 3 2 + 2 + 1 + 1
362 361 oveq1d φ A 3 3 2 + 2 + 1 + 1 + A 3 3 2 A 2 3 = A 3 3 2 + 2 + 1 + 1 + A 3 3 2 A 2 3
363 354 362 eqtr4d φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 2 + 2 + 1 + 1 + A 3 3 2 A 2 3
364 266 oveq1d φ 2 + 2 + 1 + 1 = 4 + 1 + 1
365 364 oveq2d φ 3 2 + 2 + 1 + 1 = 3 4 + 1 + 1
366 365 oveq2d φ A 3 3 2 + 2 + 1 + 1 = A 3 3 4 + 1 + 1
367 366 oveq1d φ A 3 3 2 + 2 + 1 + 1 + A 3 3 2 A 2 3 = A 3 3 4 + 1 + 1 + A 3 3 2 A 2 3
368 363 367 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 4 + 1 + 1 + A 3 3 2 A 2 3
369 271 oveq1d φ 4 + 1 + 1 = 5 + 1
370 369 oveq2d φ 3 4 + 1 + 1 = 3 5 + 1
371 370 oveq2d φ A 3 3 4 + 1 + 1 = A 3 3 5 + 1
372 371 oveq1d φ A 3 3 4 + 1 + 1 + A 3 3 2 A 2 3 = A 3 3 5 + 1 + A 3 3 2 A 2 3
373 368 372 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 5 + 1 + A 3 3 2 A 2 3
374 5p1e6 5 + 1 = 6
375 374 a1i φ 5 + 1 = 6
376 375 oveq2d φ 3 5 + 1 = 3 6
377 376 oveq2d φ A 3 3 5 + 1 = A 3 3 6
378 377 oveq1d φ A 3 3 5 + 1 + A 3 3 2 A 2 3 = A 3 3 6 + A 3 3 2 A 2 3
379 373 378 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 6 + A 3 3 2 A 2 3
380 11 8 29 mulexpd φ 3 2 A 2 = 3 2 2 A 2
381 380 oveq1d φ 3 2 A 2 3 = 3 2 2 A 2 3
382 381 oveq2d φ 3 3 2 A 2 3 = 3 3 2 2 A 2 3
383 382 oveq2d φ A 3 3 2 A 2 3 = A 3 3 2 2 A 2 3
384 383 oveq2d φ A 3 3 6 + A 3 3 2 A 2 3 = A 3 3 6 + A 3 3 2 2 A 2 3
385 379 384 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 6 + A 3 3 2 2 A 2 3
386 11 sqcld φ 3 2 2
387 386 9 mulcld φ 3 2 2 A 2
388 387 3 mulcld φ 3 2 2 A 2 3
389 3 388 mulcld φ 3 3 2 2 A 2 3
390 8 389 mulcomd φ A 3 3 2 2 A 2 3 = 3 3 2 2 A 2 3 A
391 3 388 mulcomd φ 3 3 2 2 A 2 3 = 3 2 2 A 2 3 3
392 391 oveq1d φ 3 3 2 2 A 2 3 A = 3 2 2 A 2 3 3 A
393 390 392 eqtrd φ A 3 3 2 2 A 2 3 = 3 2 2 A 2 3 3 A
394 386 9 mulcomd φ 3 2 2 A 2 = A 2 3 2 2
395 394 oveq1d φ 3 2 2 A 2 3 = A 2 3 2 2 3
396 395 oveq1d φ 3 2 2 A 2 3 3 = A 2 3 2 2 3 3
397 396 oveq1d φ 3 2 2 A 2 3 3 A = A 2 3 2 2 3 3 A
398 393 397 eqtrd φ A 3 3 2 2 A 2 3 = A 2 3 2 2 3 3 A
399 9 386 mulcld φ A 2 3 2 2
400 399 3 mulcld φ A 2 3 2 2 3
401 400 3 8 mulassd φ A 2 3 2 2 3 3 A = A 2 3 2 2 3 3 A
402 398 401 eqtrd φ A 3 3 2 2 A 2 3 = A 2 3 2 2 3 3 A
403 399 3 295 mulassd φ A 2 3 2 2 3 3 A = A 2 3 2 2 3 3 A
404 402 403 eqtrd φ A 3 3 2 2 A 2 3 = A 2 3 2 2 3 3 A
405 3 295 mulcld φ 3 3 A
406 9 386 405 mulassd φ A 2 3 2 2 3 3 A = A 2 3 2 2 3 3 A
407 404 406 eqtrd φ A 3 3 2 2 A 2 3 = A 2 3 2 2 3 3 A
408 386 405 mulcomd φ 3 2 2 3 3 A = 3 3 A 3 2 2
409 408 oveq2d φ A 2 3 2 2 3 3 A = A 2 3 3 A 3 2 2
410 407 409 eqtrd φ A 3 3 2 2 A 2 3 = A 2 3 3 A 3 2 2
411 3 295 mulcomd φ 3 3 A = 3 A 3
412 411 oveq1d φ 3 3 A 3 2 2 = 3 A 3 3 2 2
413 412 oveq2d φ A 2 3 3 A 3 2 2 = A 2 3 A 3 3 2 2
414 410 413 eqtrd φ A 3 3 2 2 A 2 3 = A 2 3 A 3 3 2 2
415 308 oveq1d φ 3 A 3 = A 3 3
416 415 oveq1d φ 3 A 3 3 2 2 = A 3 3 3 2 2
417 416 oveq2d φ A 2 3 A 3 3 2 2 = A 2 A 3 3 3 2 2
418 414 417 eqtrd φ A 3 3 2 2 A 2 3 = A 2 A 3 3 3 2 2
419 313 3 386 mulassd φ A 3 3 3 2 2 = A 3 3 3 2 2
420 419 oveq2d φ A 2 A 3 3 3 2 2 = A 2 A 3 3 3 2 2
421 418 420 eqtrd φ A 3 3 2 2 A 2 3 = A 2 A 3 3 3 2 2
422 3 386 mulcld φ 3 3 2 2
423 8 3 422 mulassd φ A 3 3 3 2 2 = A 3 3 3 2 2
424 423 oveq2d φ A 2 A 3 3 3 2 2 = A 2 A 3 3 3 2 2
425 421 424 eqtrd φ A 3 3 2 2 A 2 3 = A 2 A 3 3 3 2 2
426 425 oveq2d φ A 3 3 6 + A 3 3 2 2 A 2 3 = A 3 3 6 + A 2 A 3 3 3 2 2
427 385 426 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 6 + A 2 A 3 3 3 2 2
428 3 422 mulcld φ 3 3 3 2 2
429 9 8 428 mulassd φ A 2 A 3 3 3 2 2 = A 2 A 3 3 3 2 2
430 429 oveq2d φ A 3 3 6 + A 2 A 3 3 3 2 2 = A 3 3 6 + A 2 A 3 3 3 2 2
431 427 430 eqtr4d φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 6 + A 2 A 3 3 3 2 2
432 327 oveq1d φ A 2 A 3 3 3 2 2 = A 2 + 1 3 3 3 2 2
433 432 oveq2d φ A 3 3 6 + A 2 A 3 3 3 2 2 = A 3 3 6 + A 2 + 1 3 3 3 2 2
434 431 433 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 6 + A 2 + 1 3 3 3 2 2
435 333 oveq1d φ A 2 + 1 3 3 3 2 2 = A 3 3 3 3 2 2
436 435 oveq2d φ A 3 3 6 + A 2 + 1 3 3 3 2 2 = A 3 3 6 + A 3 3 3 3 2 2
437 434 436 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 6 + A 3 3 3 3 2 2
438 8 5 expcld φ A 3
439 6nn0 6 0
440 439 a1i φ 6 0
441 3 440 expcld φ 3 6
442 438 441 428 adddid φ A 3 3 6 + 3 3 3 2 2 = A 3 3 6 + A 3 3 3 3 2 2
443 442 eqcomd φ A 3 3 6 + A 3 3 3 3 2 2 = A 3 3 6 + 3 3 3 2 2
444 437 443 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 6 + 3 3 3 2 2
445 3 29 29 expmuld φ 3 2 2 = 3 2 2
446 445 oveq2d φ 3 3 2 2 = 3 3 2 2
447 446 oveq2d φ 3 3 3 2 2 = 3 3 3 2 2
448 447 eqcomd φ 3 3 3 2 2 = 3 3 3 2 2
449 29 29 nn0mulcld φ 2 2 0
450 3 449 expcld φ 3 2 2
451 3 450 mulcomd φ 3 3 2 2 = 3 2 2 3
452 451 oveq2d φ 3 3 3 2 2 = 3 3 2 2 3
453 448 452 eqtrd φ 3 3 3 2 2 = 3 3 2 2 3
454 3 449 expp1d φ 3 2 2 + 1 = 3 2 2 3
455 454 oveq2d φ 3 3 2 2 + 1 = 3 3 2 2 3
456 453 455 eqtr4d φ 3 3 3 2 2 = 3 3 2 2 + 1
457 1nn0 1 0
458 457 a1i φ 1 0
459 449 458 nn0addcld φ 2 2 + 1 0
460 3 459 expcld φ 3 2 2 + 1
461 3 460 mulcomd φ 3 3 2 2 + 1 = 3 2 2 + 1 3
462 456 461 eqtrd φ 3 3 3 2 2 = 3 2 2 + 1 3
463 3 459 expp1d φ 3 2 2 + 1 + 1 = 3 2 2 + 1 3
464 462 463 eqtr4d φ 3 3 3 2 2 = 3 2 2 + 1 + 1
465 464 oveq2d φ 3 6 + 3 3 3 2 2 = 3 6 + 3 2 2 + 1 + 1
466 465 oveq2d φ A 3 3 6 + 3 3 3 2 2 = A 3 3 6 + 3 2 2 + 1 + 1
467 444 466 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 6 + 3 2 2 + 1 + 1
468 2t2e4 2 2 = 4
469 468 a1i φ 2 2 = 4
470 469 oveq1d φ 2 2 + 1 = 4 + 1
471 470 oveq1d φ 2 2 + 1 + 1 = 4 + 1 + 1
472 471 oveq2d φ 3 2 2 + 1 + 1 = 3 4 + 1 + 1
473 472 oveq2d φ 3 6 + 3 2 2 + 1 + 1 = 3 6 + 3 4 + 1 + 1
474 473 oveq2d φ A 3 3 6 + 3 2 2 + 1 + 1 = A 3 3 6 + 3 4 + 1 + 1
475 467 474 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 6 + 3 4 + 1 + 1
476 370 oveq2d φ 3 6 + 3 4 + 1 + 1 = 3 6 + 3 5 + 1
477 476 oveq2d φ A 3 3 6 + 3 4 + 1 + 1 = A 3 3 6 + 3 5 + 1
478 475 477 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 6 + 3 5 + 1
479 376 oveq2d φ 3 6 + 3 5 + 1 = 3 6 + 3 6
480 479 oveq2d φ A 3 3 6 + 3 5 + 1 = A 3 3 6 + 3 6
481 478 480 eqtrd φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 = A 3 3 6 + 3 6
482 481 oveq1d φ A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 2 3 5 + A 3 3 = A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
483 482 oveq2d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 2 3 5 + A 3 3 = A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
484 483 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 2 3 5 + A 3 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
485 484 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 2 3 5 + A 3 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
486 485 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 3 A 2 3 2 + A 3 3 2 A 2 3 + A 2 3 5 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
487 281 486 eqtrd φ A 3 3 A 2 + 3 2 A + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
488 8 34 mulcomd φ A 3 2 3 3 A 2 3 2 A 3 = 3 2 3 3 A 2 3 2 A 3 A
489 31 32 mulcomd φ 3 2 3 3 A 2 3 2 A = 3 3 A 2 3 2 A 3 2
490 489 oveq1d φ 3 2 3 3 A 2 3 2 A 3 = 3 3 A 2 3 2 A 3 2 3
491 490 oveq1d φ 3 2 3 3 A 2 3 2 A 3 A = 3 3 A 2 3 2 A 3 2 3 A
492 488 491 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = 3 3 A 2 3 2 A 3 2 3 A
493 286 oveq1d φ 3 3 A 2 3 2 A = A 2 3 3 3 2 A
494 493 oveq1d φ 3 3 A 2 3 2 A 3 2 = A 2 3 3 3 2 A 3 2
495 494 oveq1d φ 3 3 A 2 3 2 A 3 2 3 = A 2 3 3 3 2 A 3 2 3
496 495 oveq1d φ 3 3 A 2 3 2 A 3 2 3 A = A 2 3 3 3 2 A 3 2 3 A
497 492 496 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 3 3 3 2 A 3 2 3 A
498 291 12 mulcld φ A 2 3 3 3 2 A
499 498 31 mulcld φ A 2 3 3 3 2 A 3 2
500 499 3 8 mulassd φ A 2 3 3 3 2 A 3 2 3 A = A 2 3 3 3 2 A 3 2 3 A
501 497 500 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 3 3 3 2 A 3 2 3 A
502 498 31 295 mulassd φ A 2 3 3 3 2 A 3 2 3 A = A 2 3 3 3 2 A 3 2 3 A
503 501 502 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 3 3 3 2 A 3 2 3 A
504 31 295 mulcld φ 3 2 3 A
505 291 12 504 mulassd φ A 2 3 3 3 2 A 3 2 3 A = A 2 3 3 3 2 A 3 2 3 A
506 503 505 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 3 3 3 2 A 3 2 3 A
507 12 504 mulcld φ 3 2 A 3 2 3 A
508 9 6 507 mulassd φ A 2 3 3 3 2 A 3 2 3 A = A 2 3 3 3 2 A 3 2 3 A
509 506 508 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 3 3 3 2 A 3 2 3 A
510 6 507 mulcomd φ 3 3 3 2 A 3 2 3 A = 3 2 A 3 2 3 A 3 3
511 510 oveq2d φ A 2 3 3 3 2 A 3 2 3 A = A 2 3 2 A 3 2 3 A 3 3
512 509 511 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 3 2 A 3 2 3 A 3 3
513 232 oveq1d φ 3 2 A 3 2 3 A = A 3 2 3 2 3 A
514 513 oveq1d φ 3 2 A 3 2 3 A 3 3 = A 3 2 3 2 3 A 3 3
515 514 oveq2d φ A 2 3 2 A 3 2 3 A 3 3 = A 2 A 3 2 3 2 3 A 3 3
516 512 515 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 A 3 2 3 2 3 A 3 3
517 237 504 6 mulassd φ A 3 2 3 2 3 A 3 3 = A 3 2 3 2 3 A 3 3
518 517 oveq2d φ A 2 A 3 2 3 2 3 A 3 3 = A 2 A 3 2 3 2 3 A 3 3
519 516 518 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 A 3 2 3 2 3 A 3 3
520 504 6 mulcld φ 3 2 3 A 3 3
521 8 11 520 mulassd φ A 3 2 3 2 3 A 3 3 = A 3 2 3 2 3 A 3 3
522 521 oveq2d φ A 2 A 3 2 3 2 3 A 3 3 = A 2 A 3 2 3 2 3 A 3 3
523 519 522 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 A 3 2 3 2 3 A 3 3
524 11 520 mulcomd φ 3 2 3 2 3 A 3 3 = 3 2 3 A 3 3 3 2
525 524 oveq2d φ A 3 2 3 2 3 A 3 3 = A 3 2 3 A 3 3 3 2
526 525 oveq2d φ A 2 A 3 2 3 2 3 A 3 3 = A 2 A 3 2 3 A 3 3 3 2
527 523 526 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 A 3 2 3 A 3 3 3 2
528 31 295 mulcomd φ 3 2 3 A = 3 A 3 2
529 528 oveq1d φ 3 2 3 A 3 3 = 3 A 3 2 3 3
530 529 oveq1d φ 3 2 3 A 3 3 3 2 = 3 A 3 2 3 3 3 2
531 530 oveq2d φ A 3 2 3 A 3 3 3 2 = A 3 A 3 2 3 3 3 2
532 531 oveq2d φ A 2 A 3 2 3 A 3 3 3 2 = A 2 A 3 A 3 2 3 3 3 2
533 527 532 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 A 3 A 3 2 3 3 3 2
534 308 oveq1d φ 3 A 3 2 = A 3 3 2
535 534 oveq1d φ 3 A 3 2 3 3 = A 3 3 2 3 3
536 535 oveq1d φ 3 A 3 2 3 3 3 2 = A 3 3 2 3 3 3 2
537 536 oveq2d φ A 3 A 3 2 3 3 3 2 = A A 3 3 2 3 3 3 2
538 537 oveq2d φ A 2 A 3 A 3 2 3 3 3 2 = A 2 A A 3 3 2 3 3 3 2
539 533 538 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 A A 3 3 2 3 3 3 2
540 313 31 mulcld φ A 3 3 2
541 540 6 11 mulassd φ A 3 3 2 3 3 3 2 = A 3 3 2 3 3 3 2
542 541 oveq2d φ A A 3 3 2 3 3 3 2 = A A 3 3 2 3 3 3 2
543 542 oveq2d φ A 2 A A 3 3 2 3 3 3 2 = A 2 A A 3 3 2 3 3 3 2
544 539 543 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 A A 3 3 2 3 3 3 2
545 6 11 mulcld φ 3 3 3 2
546 313 31 545 mulassd φ A 3 3 2 3 3 3 2 = A 3 3 2 3 3 3 2
547 546 oveq2d φ A A 3 3 2 3 3 3 2 = A A 3 3 2 3 3 3 2
548 547 oveq2d φ A 2 A A 3 3 2 3 3 3 2 = A 2 A A 3 3 2 3 3 3 2
549 544 548 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 A A 3 3 2 3 3 3 2
550 31 545 mulcld φ 3 2 3 3 3 2
551 8 3 550 mulassd φ A 3 3 2 3 3 3 2 = A 3 3 2 3 3 3 2
552 551 oveq2d φ A A 3 3 2 3 3 3 2 = A A 3 3 2 3 3 3 2
553 552 oveq2d φ A 2 A A 3 3 2 3 3 3 2 = A 2 A A 3 3 2 3 3 3 2
554 549 553 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 A A 3 3 2 3 3 3 2
555 3 355 545 mulassd φ 3 2 3 3 3 2 = 3 2 3 3 3 2
556 555 oveq2d φ 3 3 2 3 3 3 2 = 3 3 2 3 3 3 2
557 556 oveq2d φ A 3 3 2 3 3 3 2 = A 3 3 2 3 3 3 2
558 557 oveq2d φ A A 3 3 2 3 3 3 2 = A A 3 3 2 3 3 3 2
559 558 oveq2d φ A 2 A A 3 3 2 3 3 3 2 = A 2 A A 3 3 2 3 3 3 2
560 554 559 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 = A 2 A A 3 3 2 3 3 3 2
561 560 oveq1d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 2 A A 3 3 2 3 3 3 2 + A 3 2 A 3
562 355 545 mulcld φ 2 3 3 3 2
563 3 562 mulcld φ 3 2 3 3 3 2
564 3 563 mulcld φ 3 3 2 3 3 3 2
565 8 564 mulcld φ A 3 3 2 3 3 3 2
566 9 8 565 mulassd φ A 2 A A 3 3 2 3 3 3 2 = A 2 A A 3 3 2 3 3 3 2
567 566 oveq1d φ A 2 A A 3 3 2 3 3 3 2 + A 3 2 A 3 = A 2 A A 3 3 2 3 3 3 2 + A 3 2 A 3
568 561 567 eqtr4d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 2 A A 3 3 2 3 3 3 2 + A 3 2 A 3
569 9 8 mulcld φ A 2 A
570 569 8 564 mulassd φ A 2 A A 3 3 2 3 3 3 2 = A 2 A A 3 3 2 3 3 3 2
571 570 oveq1d φ A 2 A A 3 3 2 3 3 3 2 + A 3 2 A 3 = A 2 A A 3 3 2 3 3 3 2 + A 3 2 A 3
572 568 571 eqtr4d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 2 A A 3 3 2 3 3 3 2 + A 3 2 A 3
573 327 oveq1d φ A 2 A A = A 2 + 1 A
574 29 458 nn0addcld φ 2 + 1 0
575 8 574 expp1d φ A 2 + 1 + 1 = A 2 + 1 A
576 573 575 eqtr4d φ A 2 A A = A 2 + 1 + 1
577 576 oveq1d φ A 2 A A 3 3 2 3 3 3 2 = A 2 + 1 + 1 3 3 2 3 3 3 2
578 577 oveq1d φ A 2 A A 3 3 2 3 3 3 2 + A 3 2 A 3 = A 2 + 1 + 1 3 3 2 3 3 3 2 + A 3 2 A 3
579 572 578 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 2 + 1 + 1 3 3 2 3 3 3 2 + A 3 2 A 3
580 332 oveq1d φ 2 + 1 + 1 = 3 + 1
581 580 oveq2d φ A 2 + 1 + 1 = A 3 + 1
582 581 oveq1d φ A 2 + 1 + 1 3 3 2 3 3 3 2 = A 3 + 1 3 3 2 3 3 3 2
583 582 oveq1d φ A 2 + 1 + 1 3 3 2 3 3 3 2 + A 3 2 A 3 = A 3 + 1 3 3 2 3 3 3 2 + A 3 2 A 3
584 579 583 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 3 + 1 3 3 2 3 3 3 2 + A 3 2 A 3
585 3p1e4 3 + 1 = 4
586 585 a1i φ 3 + 1 = 4
587 586 oveq2d φ A 3 + 1 = A 4
588 587 oveq1d φ A 3 + 1 3 3 2 3 3 3 2 = A 4 3 3 2 3 3 3 2
589 588 oveq1d φ A 3 + 1 3 3 2 3 3 3 2 + A 3 2 A 3 = A 4 3 3 2 3 3 3 2 + A 3 2 A 3
590 584 589 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 3 2 3 3 3 2 + A 3 2 A 3
591 3 29 5 expaddd φ 3 3 + 2 = 3 3 3 2
592 591 oveq2d φ 2 3 3 + 2 = 2 3 3 3 2
593 592 oveq2d φ 3 2 3 3 + 2 = 3 2 3 3 3 2
594 593 oveq2d φ 3 3 2 3 3 + 2 = 3 3 2 3 3 3 2
595 594 eqcomd φ 3 3 2 3 3 3 2 = 3 3 2 3 3 + 2
596 595 oveq2d φ A 4 3 3 2 3 3 3 2 = A 4 3 3 2 3 3 + 2
597 596 oveq1d φ A 4 3 3 2 3 3 3 2 + A 3 2 A 3 = A 4 3 3 2 3 3 + 2 + A 3 2 A 3
598 590 597 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 3 2 3 3 + 2 + A 3 2 A 3
599 3p2e5 3 + 2 = 5
600 599 a1i φ 3 + 2 = 5
601 600 oveq2d φ 3 3 + 2 = 3 5
602 601 oveq2d φ 2 3 3 + 2 = 2 3 5
603 602 oveq2d φ 3 2 3 3 + 2 = 3 2 3 5
604 603 oveq2d φ 3 3 2 3 3 + 2 = 3 3 2 3 5
605 604 oveq2d φ A 4 3 3 2 3 3 + 2 = A 4 3 3 2 3 5
606 605 oveq1d φ A 4 3 3 2 3 3 + 2 + A 3 2 A 3 = A 4 3 3 2 3 5 + A 3 2 A 3
607 598 606 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 3 2 3 5 + A 3 2 A 3
608 5nn0 5 0
609 608 a1i φ 5 0
610 3 609 expcld φ 3 5
611 355 610 mulcomd φ 2 3 5 = 3 5 2
612 611 oveq2d φ 3 2 3 5 = 3 3 5 2
613 612 oveq2d φ 3 3 2 3 5 = 3 3 3 5 2
614 613 oveq2d φ A 4 3 3 2 3 5 = A 4 3 3 3 5 2
615 614 oveq1d φ A 4 3 3 2 3 5 + A 3 2 A 3 = A 4 3 3 3 5 2 + A 3 2 A 3
616 607 615 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 3 3 5 2 + A 3 2 A 3
617 3 610 355 mulassd φ 3 3 5 2 = 3 3 5 2
618 617 oveq2d φ 3 3 3 5 2 = 3 3 3 5 2
619 618 oveq2d φ A 4 3 3 3 5 2 = A 4 3 3 3 5 2
620 619 oveq1d φ A 4 3 3 3 5 2 + A 3 2 A 3 = A 4 3 3 3 5 2 + A 3 2 A 3
621 616 620 eqtr4d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 3 3 5 2 + A 3 2 A 3
622 3 610 mulcld φ 3 3 5
623 3 622 355 mulassd φ 3 3 3 5 2 = 3 3 3 5 2
624 623 oveq2d φ A 4 3 3 3 5 2 = A 4 3 3 3 5 2
625 624 oveq1d φ A 4 3 3 3 5 2 + A 3 2 A 3 = A 4 3 3 3 5 2 + A 3 2 A 3
626 621 625 eqtr4d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 3 3 5 2 + A 3 2 A 3
627 3 610 mulcomd φ 3 3 5 = 3 5 3
628 627 oveq2d φ 3 3 3 5 = 3 3 5 3
629 3 609 expp1d φ 3 5 + 1 = 3 5 3
630 629 oveq2d φ 3 3 5 + 1 = 3 3 5 3
631 628 630 eqtr4d φ 3 3 3 5 = 3 3 5 + 1
632 609 458 nn0addcld φ 5 + 1 0
633 3 632 expcld φ 3 5 + 1
634 3 633 mulcomd φ 3 3 5 + 1 = 3 5 + 1 3
635 631 634 eqtrd φ 3 3 3 5 = 3 5 + 1 3
636 3 632 expp1d φ 3 5 + 1 + 1 = 3 5 + 1 3
637 635 636 eqtr4d φ 3 3 3 5 = 3 5 + 1 + 1
638 637 oveq1d φ 3 3 3 5 2 = 3 5 + 1 + 1 2
639 638 oveq2d φ A 4 3 3 3 5 2 = A 4 3 5 + 1 + 1 2
640 639 oveq1d φ A 4 3 3 3 5 2 + A 3 2 A 3 = A 4 3 5 + 1 + 1 2 + A 3 2 A 3
641 626 640 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 5 + 1 + 1 2 + A 3 2 A 3
642 375 oveq1d φ 5 + 1 + 1 = 6 + 1
643 642 oveq2d φ 3 5 + 1 + 1 = 3 6 + 1
644 643 oveq1d φ 3 5 + 1 + 1 2 = 3 6 + 1 2
645 644 oveq2d φ A 4 3 5 + 1 + 1 2 = A 4 3 6 + 1 2
646 645 oveq1d φ A 4 3 5 + 1 + 1 2 + A 3 2 A 3 = A 4 3 6 + 1 2 + A 3 2 A 3
647 641 646 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 6 + 1 2 + A 3 2 A 3
648 6p1e7 6 + 1 = 7
649 648 a1i φ 6 + 1 = 7
650 649 oveq2d φ 3 6 + 1 = 3 7
651 650 oveq1d φ 3 6 + 1 2 = 3 7 2
652 651 oveq2d φ A 4 3 6 + 1 2 = A 4 3 7 2
653 652 oveq1d φ A 4 3 6 + 1 2 + A 3 2 A 3 = A 4 3 7 2 + A 3 2 A 3
654 647 653 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 7 2 + A 3 2 A 3
655 11 8 5 mulexpd φ 3 2 A 3 = 3 2 3 A 3
656 655 oveq2d φ A 3 2 A 3 = A 3 2 3 A 3
657 656 oveq2d φ A 4 3 7 2 + A 3 2 A 3 = A 4 3 7 2 + A 3 2 3 A 3
658 654 657 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 7 2 + A 3 2 3 A 3
659 11 5 expcld φ 3 2 3
660 659 438 mulcld φ 3 2 3 A 3
661 8 660 mulcomd φ A 3 2 3 A 3 = 3 2 3 A 3 A
662 659 438 mulcomd φ 3 2 3 A 3 = A 3 3 2 3
663 662 oveq1d φ 3 2 3 A 3 A = A 3 3 2 3 A
664 661 663 eqtrd φ A 3 2 3 A 3 = A 3 3 2 3 A
665 438 659 8 mulassd φ A 3 3 2 3 A = A 3 3 2 3 A
666 664 665 eqtrd φ A 3 2 3 A 3 = A 3 3 2 3 A
667 659 8 mulcomd φ 3 2 3 A = A 3 2 3
668 667 oveq2d φ A 3 3 2 3 A = A 3 A 3 2 3
669 666 668 eqtrd φ A 3 2 3 A 3 = A 3 A 3 2 3
670 669 oveq2d φ A 4 3 7 2 + A 3 2 3 A 3 = A 4 3 7 2 + A 3 A 3 2 3
671 658 670 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 7 2 + A 3 A 3 2 3
672 438 8 659 mulassd φ A 3 A 3 2 3 = A 3 A 3 2 3
673 672 oveq2d φ A 4 3 7 2 + A 3 A 3 2 3 = A 4 3 7 2 + A 3 A 3 2 3
674 671 673 eqtr4d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 7 2 + A 3 A 3 2 3
675 8 5 expp1d φ A 3 + 1 = A 3 A
676 675 eqcomd φ A 3 A = A 3 + 1
677 676 oveq1d φ A 3 A 3 2 3 = A 3 + 1 3 2 3
678 677 oveq2d φ A 4 3 7 2 + A 3 A 3 2 3 = A 4 3 7 2 + A 3 + 1 3 2 3
679 674 678 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 7 2 + A 3 + 1 3 2 3
680 587 oveq1d φ A 3 + 1 3 2 3 = A 4 3 2 3
681 680 oveq2d φ A 4 3 7 2 + A 3 + 1 3 2 3 = A 4 3 7 2 + A 4 3 2 3
682 679 681 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 7 2 + A 4 3 2 3
683 3 5 29 expmuld φ 3 2 3 = 3 2 3
684 683 eqcomd φ 3 2 3 = 3 2 3
685 684 oveq2d φ A 4 3 2 3 = A 4 3 2 3
686 685 oveq2d φ A 4 3 7 2 + A 4 3 2 3 = A 4 3 7 2 + A 4 3 2 3
687 682 686 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 7 2 + A 4 3 2 3
688 2cn 2
689 3t2e6 3 2 = 6
690 2 688 689 mulcomli 2 3 = 6
691 690 a1i φ 2 3 = 6
692 691 oveq2d φ 3 2 3 = 3 6
693 692 oveq2d φ A 4 3 2 3 = A 4 3 6
694 693 oveq2d φ A 4 3 7 2 + A 4 3 2 3 = A 4 3 7 2 + A 4 3 6
695 687 694 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 7 2 + A 4 3 6
696 4nn0 4 0
697 696 a1i φ 4 0
698 8 697 expcld φ A 4
699 7nn0 7 0
700 699 a1i φ 7 0
701 3 700 expcld φ 3 7
702 701 355 mulcld φ 3 7 2
703 698 702 441 adddid φ A 4 3 7 2 + 3 6 = A 4 3 7 2 + A 4 3 6
704 703 eqcomd φ A 4 3 7 2 + A 4 3 6 = A 4 3 7 2 + 3 6
705 695 704 eqtrd φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 = A 4 3 7 2 + 3 6
706 705 oveq1d φ A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3 = A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
707 706 oveq2d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3 = A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
708 707 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3 = A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
709 708 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 3 2 3 3 A 2 3 2 A 3 + A 3 2 A 3 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
710 487 709 eqtrd φ A 3 3 A 2 + 3 2 A + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
711 380 oveq2d φ 3 3 A 2 3 2 A 2 = 3 3 A 2 3 2 2 A 2
712 711 oveq2d φ 3 3 3 A 2 3 2 A 2 = 3 3 3 A 2 3 2 2 A 2
713 712 oveq2d φ A 3 3 3 A 2 3 2 A 2 = A 3 3 3 A 2 3 2 2 A 2
714 713 oveq1d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 3 3 3 A 2 3 2 2 A 2 + A 3 3 3 A 2 2 3
715 10 387 mulcld φ 3 3 A 2 3 2 2 A 2
716 3 715 mulcld φ 3 3 3 A 2 3 2 2 A 2
717 8 716 mulcomd φ A 3 3 3 A 2 3 2 2 A 2 = 3 3 3 A 2 3 2 2 A 2 A
718 3 715 mulcomd φ 3 3 3 A 2 3 2 2 A 2 = 3 3 A 2 3 2 2 A 2 3
719 718 oveq1d φ 3 3 3 A 2 3 2 2 A 2 A = 3 3 A 2 3 2 2 A 2 3 A
720 717 719 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = 3 3 A 2 3 2 2 A 2 3 A
721 286 oveq1d φ 3 3 A 2 3 2 2 A 2 = A 2 3 3 3 2 2 A 2
722 721 oveq1d φ 3 3 A 2 3 2 2 A 2 3 = A 2 3 3 3 2 2 A 2 3
723 722 oveq1d φ 3 3 A 2 3 2 2 A 2 3 A = A 2 3 3 3 2 2 A 2 3 A
724 720 723 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = A 2 3 3 3 2 2 A 2 3 A
725 291 387 mulcld φ A 2 3 3 3 2 2 A 2
726 725 3 8 mulassd φ A 2 3 3 3 2 2 A 2 3 A = A 2 3 3 3 2 2 A 2 3 A
727 724 726 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = A 2 3 3 3 2 2 A 2 3 A
728 291 387 295 mulassd φ A 2 3 3 3 2 2 A 2 3 A = A 2 3 3 3 2 2 A 2 3 A
729 727 728 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = A 2 3 3 3 2 2 A 2 3 A
730 387 295 mulcld φ 3 2 2 A 2 3 A
731 9 6 730 mulassd φ A 2 3 3 3 2 2 A 2 3 A = A 2 3 3 3 2 2 A 2 3 A
732 729 731 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = A 2 3 3 3 2 2 A 2 3 A
733 6 730 mulcomd φ 3 3 3 2 2 A 2 3 A = 3 2 2 A 2 3 A 3 3
734 733 oveq2d φ A 2 3 3 3 2 2 A 2 3 A = A 2 3 2 2 A 2 3 A 3 3
735 732 734 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = A 2 3 2 2 A 2 3 A 3 3
736 394 oveq1d φ 3 2 2 A 2 3 A = A 2 3 2 2 3 A
737 736 oveq1d φ 3 2 2 A 2 3 A 3 3 = A 2 3 2 2 3 A 3 3
738 737 oveq2d φ A 2 3 2 2 A 2 3 A 3 3 = A 2 A 2 3 2 2 3 A 3 3
739 735 738 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = A 2 A 2 3 2 2 3 A 3 3
740 399 295 6 mulassd φ A 2 3 2 2 3 A 3 3 = A 2 3 2 2 3 A 3 3
741 740 oveq2d φ A 2 A 2 3 2 2 3 A 3 3 = A 2 A 2 3 2 2 3 A 3 3
742 739 741 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = A 2 A 2 3 2 2 3 A 3 3
743 295 6 mulcld φ 3 A 3 3
744 9 386 743 mulassd φ A 2 3 2 2 3 A 3 3 = A 2 3 2 2 3 A 3 3
745 744 oveq2d φ A 2 A 2 3 2 2 3 A 3 3 = A 2 A 2 3 2 2 3 A 3 3
746 742 745 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = A 2 A 2 3 2 2 3 A 3 3
747 386 743 mulcomd φ 3 2 2 3 A 3 3 = 3 A 3 3 3 2 2
748 747 oveq2d φ A 2 3 2 2 3 A 3 3 = A 2 3 A 3 3 3 2 2
749 748 oveq2d φ A 2 A 2 3 2 2 3 A 3 3 = A 2 A 2 3 A 3 3 3 2 2
750 746 749 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = A 2 A 2 3 A 3 3 3 2 2
751 308 oveq1d φ 3 A 3 3 = A 3 3 3
752 751 oveq1d φ 3 A 3 3 3 2 2 = A 3 3 3 3 2 2
753 752 oveq2d φ A 2 3 A 3 3 3 2 2 = A 2 A 3 3 3 3 2 2
754 753 oveq2d φ A 2 A 2 3 A 3 3 3 2 2 = A 2 A 2 A 3 3 3 3 2 2
755 750 754 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = A 2 A 2 A 3 3 3 3 2 2
756 313 6 386 mulassd φ A 3 3 3 3 2 2 = A 3 3 3 3 2 2
757 756 oveq2d φ A 2 A 3 3 3 3 2 2 = A 2 A 3 3 3 3 2 2
758 757 oveq2d φ A 2 A 2 A 3 3 3 3 2 2 = A 2 A 2 A 3 3 3 3 2 2
759 755 758 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = A 2 A 2 A 3 3 3 3 2 2
760 6 386 mulcld φ 3 3 3 2 2
761 8 3 760 mulassd φ A 3 3 3 3 2 2 = A 3 3 3 3 2 2
762 761 oveq2d φ A 2 A 3 3 3 3 2 2 = A 2 A 3 3 3 3 2 2
763 762 oveq2d φ A 2 A 2 A 3 3 3 3 2 2 = A 2 A 2 A 3 3 3 3 2 2
764 759 763 eqtrd φ A 3 3 3 A 2 3 2 2 A 2 = A 2 A 2 A 3 3 3 3 2 2
765 764 oveq1d φ A 3 3 3 A 2 3 2 2 A 2 + A 3 3 3 A 2 2 3 = A 2 A 2 A 3 3 3 3 2 2 + A 3 3 3 A 2 2 3
766 714 765 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 2 A 2 A 3 3 3 3 2 2 + A 3 3 3 A 2 2 3
767 3 760 mulcld φ 3 3 3 3 2 2
768 8 767 mulcld φ A 3 3 3 3 2 2
769 9 9 768 mulassd φ A 2 A 2 A 3 3 3 3 2 2 = A 2 A 2 A 3 3 3 3 2 2
770 769 oveq1d φ A 2 A 2 A 3 3 3 3 2 2 + A 3 3 3 A 2 2 3 = A 2 A 2 A 3 3 3 3 2 2 + A 3 3 3 A 2 2 3
771 766 770 eqtr4d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 2 A 2 A 3 3 3 3 2 2 + A 3 3 3 A 2 2 3
772 9 9 mulcld φ A 2 A 2
773 772 8 767 mulassd φ A 2 A 2 A 3 3 3 3 2 2 = A 2 A 2 A 3 3 3 3 2 2
774 773 oveq1d φ A 2 A 2 A 3 3 3 3 2 2 + A 3 3 3 A 2 2 3 = A 2 A 2 A 3 3 3 3 2 2 + A 3 3 3 A 2 2 3
775 771 774 eqtr4d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 2 A 2 A 3 3 3 3 2 2 + A 3 3 3 A 2 2 3
776 8 29 29 expaddd φ A 2 + 2 = A 2 A 2
777 776 oveq1d φ A 2 + 2 A = A 2 A 2 A
778 777 eqcomd φ A 2 A 2 A = A 2 + 2 A
779 8 259 expp1d φ A 2 + 2 + 1 = A 2 + 2 A
780 778 779 eqtr4d φ A 2 A 2 A = A 2 + 2 + 1
781 780 oveq1d φ A 2 A 2 A 3 3 3 3 2 2 = A 2 + 2 + 1 3 3 3 3 2 2
782 781 oveq1d φ A 2 A 2 A 3 3 3 3 2 2 + A 3 3 3 A 2 2 3 = A 2 + 2 + 1 3 3 3 3 2 2 + A 3 3 3 A 2 2 3
783 775 782 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 2 + 2 + 1 3 3 3 3 2 2 + A 3 3 3 A 2 2 3
784 266 oveq2d φ A 2 + 2 + 1 = A 4 + 1
785 784 oveq1d φ A 2 + 2 + 1 3 3 3 3 2 2 = A 4 + 1 3 3 3 3 2 2
786 785 oveq1d φ A 2 + 2 + 1 3 3 3 3 2 2 + A 3 3 3 A 2 2 3 = A 4 + 1 3 3 3 3 2 2 + A 3 3 3 A 2 2 3
787 783 786 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 4 + 1 3 3 3 3 2 2 + A 3 3 3 A 2 2 3
788 271 oveq2d φ A 4 + 1 = A 5
789 788 oveq1d φ A 4 + 1 3 3 3 3 2 2 = A 5 3 3 3 3 2 2
790 789 oveq1d φ A 4 + 1 3 3 3 3 2 2 + A 3 3 3 A 2 2 3 = A 5 3 3 3 3 2 2 + A 3 3 3 A 2 2 3
791 787 790 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 3 3 3 2 2 + A 3 3 3 A 2 2 3
792 445 oveq2d φ 3 3 3 2 2 = 3 3 3 2 2
793 792 oveq2d φ 3 3 3 3 2 2 = 3 3 3 3 2 2
794 793 eqcomd φ 3 3 3 3 2 2 = 3 3 3 3 2 2
795 3 449 5 expaddd φ 3 3 + 2 2 = 3 3 3 2 2
796 795 oveq2d φ 3 3 3 + 2 2 = 3 3 3 3 2 2
797 794 796 eqtr4d φ 3 3 3 3 2 2 = 3 3 3 + 2 2
798 5 449 nn0addcld φ 3 + 2 2 0
799 3 798 expcld φ 3 3 + 2 2
800 3 799 mulcomd φ 3 3 3 + 2 2 = 3 3 + 2 2 3
801 797 800 eqtrd φ 3 3 3 3 2 2 = 3 3 + 2 2 3
802 3 798 expp1d φ 3 3 + 2 2 + 1 = 3 3 + 2 2 3
803 801 802 eqtr4d φ 3 3 3 3 2 2 = 3 3 + 2 2 + 1
804 803 oveq2d φ A 5 3 3 3 3 2 2 = A 5 3 3 + 2 2 + 1
805 804 oveq1d φ A 5 3 3 3 3 2 2 + A 3 3 3 A 2 2 3 = A 5 3 3 + 2 2 + 1 + A 3 3 3 A 2 2 3
806 791 805 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 3 + 2 2 + 1 + A 3 3 3 A 2 2 3
807 469 oveq2d φ 3 + 2 2 = 3 + 4
808 807 oveq1d φ 3 + 2 2 + 1 = 3 + 4 + 1
809 808 oveq2d φ 3 3 + 2 2 + 1 = 3 3 + 4 + 1
810 809 oveq2d φ A 5 3 3 + 2 2 + 1 = A 5 3 3 + 4 + 1
811 810 oveq1d φ A 5 3 3 + 2 2 + 1 + A 3 3 3 A 2 2 3 = A 5 3 3 + 4 + 1 + A 3 3 3 A 2 2 3
812 806 811 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 3 + 4 + 1 + A 3 3 3 A 2 2 3
813 586 oveq2d φ 3 + 3 + 1 = 3 + 4
814 813 oveq1d φ 3 + 3 + 1 + 1 = 3 + 4 + 1
815 814 oveq2d φ 3 3 + 3 + 1 + 1 = 3 3 + 4 + 1
816 815 oveq2d φ A 5 3 3 + 3 + 1 + 1 = A 5 3 3 + 4 + 1
817 816 oveq1d φ A 5 3 3 + 3 + 1 + 1 + A 3 3 3 A 2 2 3 = A 5 3 3 + 4 + 1 + A 3 3 3 A 2 2 3
818 812 817 eqtr4d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 3 + 3 + 1 + 1 + A 3 3 3 A 2 2 3
819 3 3 357 addassd φ 3 + 3 + 1 = 3 + 3 + 1
820 819 oveq1d φ 3 + 3 + 1 + 1 = 3 + 3 + 1 + 1
821 820 oveq2d φ 3 3 + 3 + 1 + 1 = 3 3 + 3 + 1 + 1
822 821 oveq2d φ A 5 3 3 + 3 + 1 + 1 = A 5 3 3 + 3 + 1 + 1
823 822 oveq1d φ A 5 3 3 + 3 + 1 + 1 + A 3 3 3 A 2 2 3 = A 5 3 3 + 3 + 1 + 1 + A 3 3 3 A 2 2 3
824 818 823 eqtr4d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 3 + 3 + 1 + 1 + A 3 3 3 A 2 2 3
825 3p3e6 3 + 3 = 6
826 825 a1i φ 3 + 3 = 6
827 826 oveq1d φ 3 + 3 + 1 = 6 + 1
828 827 oveq1d φ 3 + 3 + 1 + 1 = 6 + 1 + 1
829 828 oveq2d φ 3 3 + 3 + 1 + 1 = 3 6 + 1 + 1
830 829 oveq2d φ A 5 3 3 + 3 + 1 + 1 = A 5 3 6 + 1 + 1
831 830 oveq1d φ A 5 3 3 + 3 + 1 + 1 + A 3 3 3 A 2 2 3 = A 5 3 6 + 1 + 1 + A 3 3 3 A 2 2 3
832 824 831 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 6 + 1 + 1 + A 3 3 3 A 2 2 3
833 649 oveq1d φ 6 + 1 + 1 = 7 + 1
834 833 oveq2d φ 3 6 + 1 + 1 = 3 7 + 1
835 834 oveq2d φ A 5 3 6 + 1 + 1 = A 5 3 7 + 1
836 835 oveq1d φ A 5 3 6 + 1 + 1 + A 3 3 3 A 2 2 3 = A 5 3 7 + 1 + A 3 3 3 A 2 2 3
837 832 836 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 7 + 1 + A 3 3 3 A 2 2 3
838 7p1e8 7 + 1 = 8
839 838 a1i φ 7 + 1 = 8
840 839 oveq2d φ 3 7 + 1 = 3 8
841 840 oveq2d φ A 5 3 7 + 1 = A 5 3 8
842 841 oveq1d φ A 5 3 7 + 1 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 3 3 3 A 2 2 3
843 837 842 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 3 3 3 A 2 2 3
844 6 9 29 mulexpd φ 3 3 A 2 2 = 3 3 2 A 2 2
845 844 oveq1d φ 3 3 A 2 2 3 = 3 3 2 A 2 2 3
846 845 oveq2d φ 3 3 3 A 2 2 3 = 3 3 3 2 A 2 2 3
847 846 oveq2d φ A 3 3 3 A 2 2 3 = A 3 3 3 2 A 2 2 3
848 847 oveq2d φ A 5 3 8 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 3 3 3 2 A 2 2 3
849 843 848 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 3 3 3 2 A 2 2 3
850 3 29 5 expmuld φ 3 3 2 = 3 3 2
851 850 oveq1d φ 3 3 2 A 2 2 = 3 3 2 A 2 2
852 851 oveq1d φ 3 3 2 A 2 2 3 = 3 3 2 A 2 2 3
853 852 oveq2d φ 3 3 3 2 A 2 2 3 = 3 3 3 2 A 2 2 3
854 853 oveq2d φ A 3 3 3 2 A 2 2 3 = A 3 3 3 2 A 2 2 3
855 854 eqcomd φ A 3 3 3 2 A 2 2 3 = A 3 3 3 2 A 2 2 3
856 8 29 29 expmuld φ A 2 2 = A 2 2
857 856 oveq2d φ 3 3 2 A 2 2 = 3 3 2 A 2 2
858 857 oveq1d φ 3 3 2 A 2 2 3 = 3 3 2 A 2 2 3
859 858 oveq2d φ 3 3 3 2 A 2 2 3 = 3 3 3 2 A 2 2 3
860 859 oveq2d φ A 3 3 3 2 A 2 2 3 = A 3 3 3 2 A 2 2 3
861 855 860 eqtr4d φ A 3 3 3 2 A 2 2 3 = A 3 3 3 2 A 2 2 3
862 861 oveq2d φ A 5 3 8 + A 3 3 3 2 A 2 2 3 = A 5 3 8 + A 3 3 3 2 A 2 2 3
863 849 862 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 3 3 3 2 A 2 2 3
864 689 a1i φ 3 2 = 6
865 864 oveq2d φ 3 3 2 = 3 6
866 865 oveq1d φ 3 3 2 A 2 2 = 3 6 A 2 2
867 866 oveq1d φ 3 3 2 A 2 2 3 = 3 6 A 2 2 3
868 867 oveq2d φ 3 3 3 2 A 2 2 3 = 3 3 6 A 2 2 3
869 868 oveq2d φ A 3 3 3 2 A 2 2 3 = A 3 3 6 A 2 2 3
870 869 oveq2d φ A 5 3 8 + A 3 3 3 2 A 2 2 3 = A 5 3 8 + A 3 3 6 A 2 2 3
871 863 870 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 3 3 6 A 2 2 3
872 469 oveq2d φ A 2 2 = A 4
873 872 oveq2d φ 3 6 A 2 2 = 3 6 A 4
874 873 oveq1d φ 3 6 A 2 2 3 = 3 6 A 4 3
875 874 oveq2d φ 3 3 6 A 2 2 3 = 3 3 6 A 4 3
876 875 oveq2d φ A 3 3 6 A 2 2 3 = A 3 3 6 A 4 3
877 876 oveq2d φ A 5 3 8 + A 3 3 6 A 2 2 3 = A 5 3 8 + A 3 3 6 A 4 3
878 871 877 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 3 3 6 A 4 3
879 441 698 mulcld φ 3 6 A 4
880 879 3 mulcld φ 3 6 A 4 3
881 3 880 mulcld φ 3 3 6 A 4 3
882 8 881 mulcomd φ A 3 3 6 A 4 3 = 3 3 6 A 4 3 A
883 3 880 mulcomd φ 3 3 6 A 4 3 = 3 6 A 4 3 3
884 883 oveq1d φ 3 3 6 A 4 3 A = 3 6 A 4 3 3 A
885 882 884 eqtrd φ A 3 3 6 A 4 3 = 3 6 A 4 3 3 A
886 441 698 mulcomd φ 3 6 A 4 = A 4 3 6
887 886 oveq1d φ 3 6 A 4 3 = A 4 3 6 3
888 887 oveq1d φ 3 6 A 4 3 3 = A 4 3 6 3 3
889 888 oveq1d φ 3 6 A 4 3 3 A = A 4 3 6 3 3 A
890 885 889 eqtrd φ A 3 3 6 A 4 3 = A 4 3 6 3 3 A
891 698 441 mulcld φ A 4 3 6
892 891 3 mulcld φ A 4 3 6 3
893 892 3 8 mulassd φ A 4 3 6 3 3 A = A 4 3 6 3 3 A
894 890 893 eqtrd φ A 3 3 6 A 4 3 = A 4 3 6 3 3 A
895 891 3 295 mulassd φ A 4 3 6 3 3 A = A 4 3 6 3 3 A
896 894 895 eqtrd φ A 3 3 6 A 4 3 = A 4 3 6 3 3 A
897 698 441 405 mulassd φ A 4 3 6 3 3 A = A 4 3 6 3 3 A
898 896 897 eqtrd φ A 3 3 6 A 4 3 = A 4 3 6 3 3 A
899 441 405 mulcomd φ 3 6 3 3 A = 3 3 A 3 6
900 899 oveq2d φ A 4 3 6 3 3 A = A 4 3 3 A 3 6
901 898 900 eqtrd φ A 3 3 6 A 4 3 = A 4 3 3 A 3 6
902 411 oveq1d φ 3 3 A 3 6 = 3 A 3 3 6
903 902 oveq2d φ A 4 3 3 A 3 6 = A 4 3 A 3 3 6
904 901 903 eqtrd φ A 3 3 6 A 4 3 = A 4 3 A 3 3 6
905 415 oveq1d φ 3 A 3 3 6 = A 3 3 3 6
906 905 oveq2d φ A 4 3 A 3 3 6 = A 4 A 3 3 3 6
907 904 906 eqtrd φ A 3 3 6 A 4 3 = A 4 A 3 3 3 6
908 313 3 441 mulassd φ A 3 3 3 6 = A 3 3 3 6
909 908 oveq2d φ A 4 A 3 3 3 6 = A 4 A 3 3 3 6
910 907 909 eqtrd φ A 3 3 6 A 4 3 = A 4 A 3 3 3 6
911 3 441 mulcld φ 3 3 6
912 8 3 911 mulassd φ A 3 3 3 6 = A 3 3 3 6
913 912 oveq2d φ A 4 A 3 3 3 6 = A 4 A 3 3 3 6
914 910 913 eqtrd φ A 3 3 6 A 4 3 = A 4 A 3 3 3 6
915 914 oveq2d φ A 5 3 8 + A 3 3 6 A 4 3 = A 5 3 8 + A 4 A 3 3 3 6
916 878 915 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 4 A 3 3 3 6
917 3 911 mulcld φ 3 3 3 6
918 698 8 917 mulassd φ A 4 A 3 3 3 6 = A 4 A 3 3 3 6
919 918 oveq2d φ A 5 3 8 + A 4 A 3 3 3 6 = A 5 3 8 + A 4 A 3 3 3 6
920 916 919 eqtr4d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 4 A 3 3 3 6
921 8 697 expp1d φ A 4 + 1 = A 4 A
922 921 eqcomd φ A 4 A = A 4 + 1
923 922 oveq1d φ A 4 A 3 3 3 6 = A 4 + 1 3 3 3 6
924 923 oveq2d φ A 5 3 8 + A 4 A 3 3 3 6 = A 5 3 8 + A 4 + 1 3 3 3 6
925 920 924 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 4 + 1 3 3 3 6
926 788 oveq1d φ A 4 + 1 3 3 3 6 = A 5 3 3 3 6
927 926 oveq2d φ A 5 3 8 + A 4 + 1 3 3 3 6 = A 5 3 8 + A 5 3 3 3 6
928 925 927 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 5 3 3 3 6
929 3 441 mulcomd φ 3 3 6 = 3 6 3
930 929 oveq2d φ 3 3 3 6 = 3 3 6 3
931 3 440 expp1d φ 3 6 + 1 = 3 6 3
932 931 oveq2d φ 3 3 6 + 1 = 3 3 6 3
933 930 932 eqtr4d φ 3 3 3 6 = 3 3 6 + 1
934 440 458 nn0addcld φ 6 + 1 0
935 3 934 expcld φ 3 6 + 1
936 3 935 mulcomd φ 3 3 6 + 1 = 3 6 + 1 3
937 933 936 eqtrd φ 3 3 3 6 = 3 6 + 1 3
938 3 934 expp1d φ 3 6 + 1 + 1 = 3 6 + 1 3
939 937 938 eqtr4d φ 3 3 3 6 = 3 6 + 1 + 1
940 939 oveq2d φ A 5 3 3 3 6 = A 5 3 6 + 1 + 1
941 940 oveq2d φ A 5 3 8 + A 5 3 3 3 6 = A 5 3 8 + A 5 3 6 + 1 + 1
942 928 941 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 5 3 6 + 1 + 1
943 835 oveq2d φ A 5 3 8 + A 5 3 6 + 1 + 1 = A 5 3 8 + A 5 3 7 + 1
944 942 943 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 5 3 7 + 1
945 841 oveq2d φ A 5 3 8 + A 5 3 7 + 1 = A 5 3 8 + A 5 3 8
946 944 945 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + A 5 3 8
947 8 609 expcld φ A 5
948 8nn0 8 0
949 948 a1i φ 8 0
950 3 949 expcld φ 3 8
951 947 950 950 adddid φ A 5 3 8 + 3 8 = A 5 3 8 + A 5 3 8
952 951 eqcomd φ A 5 3 8 + A 5 3 8 = A 5 3 8 + 3 8
953 946 952 eqtrd φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 = A 5 3 8 + 3 8
954 953 oveq1d φ A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3 = A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
955 954 oveq2d φ A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3 = A 3 3 3 A 2 2 3 2 A + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
956 955 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 3 3 3 A 2 3 2 A 2 + A 3 3 3 A 2 2 3 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
957 710 956 eqtrd φ A 3 3 A 2 + 3 2 A + 3 3 = A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
958 844 oveq1d φ 3 3 A 2 2 3 2 A = 3 3 2 A 2 2 3 2 A
959 958 oveq2d φ 3 3 3 A 2 2 3 2 A = 3 3 3 2 A 2 2 3 2 A
960 959 oveq2d φ A 3 3 3 A 2 2 3 2 A = A 3 3 3 2 A 2 2 3 2 A
961 6 sqcld φ 3 3 2
962 9 sqcld φ A 2 2
963 961 962 mulcld φ 3 3 2 A 2 2
964 963 12 mulcld φ 3 3 2 A 2 2 3 2 A
965 3 964 mulcld φ 3 3 3 2 A 2 2 3 2 A
966 8 965 mulcomd φ A 3 3 3 2 A 2 2 3 2 A = 3 3 3 2 A 2 2 3 2 A A
967 3 964 mulcomd φ 3 3 3 2 A 2 2 3 2 A = 3 3 2 A 2 2 3 2 A 3
968 967 oveq1d φ 3 3 3 2 A 2 2 3 2 A A = 3 3 2 A 2 2 3 2 A 3 A
969 966 968 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = 3 3 2 A 2 2 3 2 A 3 A
970 961 962 mulcomd φ 3 3 2 A 2 2 = A 2 2 3 3 2
971 970 oveq1d φ 3 3 2 A 2 2 3 2 A = A 2 2 3 3 2 3 2 A
972 971 oveq1d φ 3 3 2 A 2 2 3 2 A 3 = A 2 2 3 3 2 3 2 A 3
973 972 oveq1d φ 3 3 2 A 2 2 3 2 A 3 A = A 2 2 3 3 2 3 2 A 3 A
974 969 973 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = A 2 2 3 3 2 3 2 A 3 A
975 962 961 mulcld φ A 2 2 3 3 2
976 975 12 mulcld φ A 2 2 3 3 2 3 2 A
977 976 3 8 mulassd φ A 2 2 3 3 2 3 2 A 3 A = A 2 2 3 3 2 3 2 A 3 A
978 974 977 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = A 2 2 3 3 2 3 2 A 3 A
979 975 12 295 mulassd φ A 2 2 3 3 2 3 2 A 3 A = A 2 2 3 3 2 3 2 A 3 A
980 978 979 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = A 2 2 3 3 2 3 2 A 3 A
981 12 295 mulcld φ 3 2 A 3 A
982 962 961 981 mulassd φ A 2 2 3 3 2 3 2 A 3 A = A 2 2 3 3 2 3 2 A 3 A
983 980 982 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = A 2 2 3 3 2 3 2 A 3 A
984 961 981 mulcomd φ 3 3 2 3 2 A 3 A = 3 2 A 3 A 3 3 2
985 984 oveq2d φ A 2 2 3 3 2 3 2 A 3 A = A 2 2 3 2 A 3 A 3 3 2
986 983 985 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = A 2 2 3 2 A 3 A 3 3 2
987 232 oveq1d φ 3 2 A 3 A = A 3 2 3 A
988 987 oveq1d φ 3 2 A 3 A 3 3 2 = A 3 2 3 A 3 3 2
989 988 oveq2d φ A 2 2 3 2 A 3 A 3 3 2 = A 2 2 A 3 2 3 A 3 3 2
990 986 989 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = A 2 2 A 3 2 3 A 3 3 2
991 237 295 961 mulassd φ A 3 2 3 A 3 3 2 = A 3 2 3 A 3 3 2
992 991 oveq2d φ A 2 2 A 3 2 3 A 3 3 2 = A 2 2 A 3 2 3 A 3 3 2
993 990 992 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = A 2 2 A 3 2 3 A 3 3 2
994 295 961 mulcld φ 3 A 3 3 2
995 8 11 994 mulassd φ A 3 2 3 A 3 3 2 = A 3 2 3 A 3 3 2
996 995 oveq2d φ A 2 2 A 3 2 3 A 3 3 2 = A 2 2 A 3 2 3 A 3 3 2
997 993 996 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = A 2 2 A 3 2 3 A 3 3 2
998 11 994 mulcomd φ 3 2 3 A 3 3 2 = 3 A 3 3 2 3 2
999 998 oveq2d φ A 3 2 3 A 3 3 2 = A 3 A 3 3 2 3 2
1000 999 oveq2d φ A 2 2 A 3 2 3 A 3 3 2 = A 2 2 A 3 A 3 3 2 3 2
1001 997 1000 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = A 2 2 A 3 A 3 3 2 3 2
1002 308 oveq1d φ 3 A 3 3 2 = A 3 3 3 2
1003 1002 oveq1d φ 3 A 3 3 2 3 2 = A 3 3 3 2 3 2
1004 1003 oveq2d φ A 3 A 3 3 2 3 2 = A A 3 3 3 2 3 2
1005 1004 oveq2d φ A 2 2 A 3 A 3 3 2 3 2 = A 2 2 A A 3 3 3 2 3 2
1006 1001 1005 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = A 2 2 A A 3 3 3 2 3 2
1007 313 961 11 mulassd φ A 3 3 3 2 3 2 = A 3 3 3 2 3 2
1008 1007 oveq2d φ A A 3 3 3 2 3 2 = A A 3 3 3 2 3 2
1009 1008 oveq2d φ A 2 2 A A 3 3 3 2 3 2 = A 2 2 A A 3 3 3 2 3 2
1010 1006 1009 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = A 2 2 A A 3 3 3 2 3 2
1011 961 11 mulcld φ 3 3 2 3 2
1012 8 3 1011 mulassd φ A 3 3 3 2 3 2 = A 3 3 3 2 3 2
1013 1012 oveq2d φ A A 3 3 3 2 3 2 = A A 3 3 3 2 3 2
1014 1013 oveq2d φ A 2 2 A A 3 3 3 2 3 2 = A 2 2 A A 3 3 3 2 3 2
1015 1010 1014 eqtrd φ A 3 3 3 2 A 2 2 3 2 A = A 2 2 A A 3 3 3 2 3 2
1016 960 1015 eqtrd φ A 3 3 3 A 2 2 3 2 A = A 2 2 A A 3 3 3 2 3 2
1017 3 1011 mulcld φ 3 3 3 2 3 2
1018 8 1017 mulcld φ A 3 3 3 2 3 2
1019 962 8 1018 mulassd φ A 2 2 A A 3 3 3 2 3 2 = A 2 2 A A 3 3 3 2 3 2
1020 1016 1019 eqtr4d φ A 3 3 3 A 2 2 3 2 A = A 2 2 A A 3 3 3 2 3 2
1021 962 8 mulcld φ A 2 2 A
1022 1021 8 1017 mulassd φ A 2 2 A A 3 3 3 2 3 2 = A 2 2 A A 3 3 3 2 3 2
1023 1020 1022 eqtr4d φ A 3 3 3 A 2 2 3 2 A = A 2 2 A A 3 3 3 2 3 2
1024 856 oveq1d φ A 2 2 A = A 2 2 A
1025 1024 oveq1d φ A 2 2 A A = A 2 2 A A
1026 1025 eqcomd φ A 2 2 A A = A 2 2 A A
1027 8 449 expp1d φ A 2 2 + 1 = A 2 2 A
1028 1027 oveq1d φ A 2 2 + 1 A = A 2 2 A A
1029 1026 1028 eqtr4d φ A 2 2 A A = A 2 2 + 1 A
1030 8 459 expp1d φ A 2 2 + 1 + 1 = A 2 2 + 1 A
1031 1029 1030 eqtr4d φ A 2 2 A A = A 2 2 + 1 + 1
1032 1031 oveq1d φ A 2 2 A A 3 3 3 2 3 2 = A 2 2 + 1 + 1 3 3 3 2 3 2
1033 1023 1032 eqtrd φ A 3 3 3 A 2 2 3 2 A = A 2 2 + 1 + 1 3 3 3 2 3 2
1034 471 oveq2d φ A 2 2 + 1 + 1 = A 4 + 1 + 1
1035 1034 oveq1d φ A 2 2 + 1 + 1 3 3 3 2 3 2 = A 4 + 1 + 1 3 3 3 2 3 2
1036 1033 1035 eqtrd φ A 3 3 3 A 2 2 3 2 A = A 4 + 1 + 1 3 3 3 2 3 2
1037 369 oveq2d φ A 4 + 1 + 1 = A 5 + 1
1038 1037 oveq1d φ A 4 + 1 + 1 3 3 3 2 3 2 = A 5 + 1 3 3 3 2 3 2
1039 1036 1038 eqtrd φ A 3 3 3 A 2 2 3 2 A = A 5 + 1 3 3 3 2 3 2
1040 375 oveq2d φ A 5 + 1 = A 6
1041 1040 oveq1d φ A 5 + 1 3 3 3 2 3 2 = A 6 3 3 3 2 3 2
1042 1039 1041 eqtrd φ A 3 3 3 A 2 2 3 2 A = A 6 3 3 3 2 3 2
1043 850 oveq1d φ 3 3 2 3 2 = 3 3 2 3 2
1044 1043 oveq2d φ 3 3 3 2 3 2 = 3 3 3 2 3 2
1045 1044 eqcomd φ 3 3 3 2 3 2 = 3 3 3 2 3 2
1046 3 29 30 expaddd φ 3 3 2 + 2 = 3 3 2 3 2
1047 1046 oveq2d φ 3 3 3 2 + 2 = 3 3 3 2 3 2
1048 1045 1047 eqtr4d φ 3 3 3 2 3 2 = 3 3 3 2 + 2
1049 30 29 nn0addcld φ 3 2 + 2 0
1050 3 1049 expcld φ 3 3 2 + 2
1051 3 1050 mulcomd φ 3 3 3 2 + 2 = 3 3 2 + 2 3
1052 1048 1051 eqtrd φ 3 3 3 2 3 2 = 3 3 2 + 2 3
1053 3 1049 expp1d φ 3 3 2 + 2 + 1 = 3 3 2 + 2 3
1054 1052 1053 eqtr4d φ 3 3 3 2 3 2 = 3 3 2 + 2 + 1
1055 1054 oveq2d φ A 6 3 3 3 2 3 2 = A 6 3 3 2 + 2 + 1
1056 1042 1055 eqtrd φ A 3 3 3 A 2 2 3 2 A = A 6 3 3 2 + 2 + 1
1057 864 oveq1d φ 3 2 + 2 = 6 + 2
1058 1057 oveq1d φ 3 2 + 2 + 1 = 6 + 2 + 1
1059 1058 oveq2d φ 3 3 2 + 2 + 1 = 3 6 + 2 + 1
1060 1059 oveq2d φ A 6 3 3 2 + 2 + 1 = A 6 3 6 + 2 + 1
1061 1056 1060 eqtrd φ A 3 3 3 A 2 2 3 2 A = A 6 3 6 + 2 + 1
1062 6p2e8 6 + 2 = 8
1063 1062 a1i φ 6 + 2 = 8
1064 1063 oveq1d φ 6 + 2 + 1 = 8 + 1
1065 1064 oveq2d φ 3 6 + 2 + 1 = 3 8 + 1
1066 1065 oveq2d φ A 6 3 6 + 2 + 1 = A 6 3 8 + 1
1067 1061 1066 eqtrd φ A 3 3 3 A 2 2 3 2 A = A 6 3 8 + 1
1068 8p1e9 8 + 1 = 9
1069 1068 a1i φ 8 + 1 = 9
1070 1069 oveq2d φ 3 8 + 1 = 3 9
1071 1070 oveq2d φ A 6 3 8 + 1 = A 6 3 9
1072 1067 1071 eqtrd φ A 3 3 3 A 2 2 3 2 A = A 6 3 9
1073 1072 oveq1d φ A 3 3 3 A 2 2 3 2 A + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3 = A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
1074 1073 oveq2d φ A 3 3 A 2 3 + A 3 3 3 A 2 2 3 2 A + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3 = A 3 3 A 2 3 + A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
1075 957 1074 eqtrd φ A 3 3 A 2 + 3 2 A + 3 3 = A 3 3 A 2 3 + A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
1076 6 9 5 mulexpd φ 3 3 A 2 3 = 3 3 3 A 2 3
1077 1076 oveq2d φ A 3 3 A 2 3 = A 3 3 3 A 2 3
1078 6 5 expcld φ 3 3 3
1079 9 5 expcld φ A 2 3
1080 1078 1079 mulcomd φ 3 3 3 A 2 3 = A 2 3 3 3 3
1081 1080 oveq2d φ A 3 3 3 A 2 3 = A A 2 3 3 3 3
1082 1077 1081 eqtrd φ A 3 3 A 2 3 = A A 2 3 3 3 3
1083 8 1079 1078 mulassd φ A A 2 3 3 3 3 = A A 2 3 3 3 3
1084 1082 1083 eqtr4d φ A 3 3 A 2 3 = A A 2 3 3 3 3
1085 8 5 29 expmuld φ A 2 3 = A 2 3
1086 1085 oveq2d φ A A 2 3 = A A 2 3
1087 1086 eqcomd φ A A 2 3 = A A 2 3
1088 29 5 nn0mulcld φ 2 3 0
1089 8 1088 expcld φ A 2 3
1090 8 1089 mulcomd φ A A 2 3 = A 2 3 A
1091 1087 1090 eqtrd φ A A 2 3 = A 2 3 A
1092 8 1088 expp1d φ A 2 3 + 1 = A 2 3 A
1093 1091 1092 eqtr4d φ A A 2 3 = A 2 3 + 1
1094 1093 oveq1d φ A A 2 3 3 3 3 = A 2 3 + 1 3 3 3
1095 1084 1094 eqtrd φ A 3 3 A 2 3 = A 2 3 + 1 3 3 3
1096 691 oveq1d φ 2 3 + 1 = 6 + 1
1097 1096 oveq2d φ A 2 3 + 1 = A 6 + 1
1098 1097 oveq1d φ A 2 3 + 1 3 3 3 = A 6 + 1 3 3 3
1099 1095 1098 eqtrd φ A 3 3 A 2 3 = A 6 + 1 3 3 3
1100 649 oveq2d φ A 6 + 1 = A 7
1101 1100 oveq1d φ A 6 + 1 3 3 3 = A 7 3 3 3
1102 1099 1101 eqtrd φ A 3 3 A 2 3 = A 7 3 3 3
1103 1102 oveq1d φ A 3 3 A 2 3 + A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3 = A 7 3 3 3 + A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
1104 1075 1103 eqtrd φ A 3 3 A 2 + 3 2 A + 3 3 = A 7 3 3 3 + A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
1105 3 5 5 expmuld φ 3 3 3 = 3 3 3
1106 1105 eqcomd φ 3 3 3 = 3 3 3
1107 1106 oveq2d φ A 7 3 3 3 = A 7 3 3 3
1108 1107 oveq1d φ A 7 3 3 3 + A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3 = A 7 3 3 3 + A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
1109 1104 1108 eqtrd φ A 3 3 A 2 + 3 2 A + 3 3 = A 7 3 3 3 + A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
1110 3t3e9 3 3 = 9
1111 1110 a1i φ 3 3 = 9
1112 1111 oveq2d φ 3 3 3 = 3 9
1113 1112 oveq2d φ A 7 3 3 3 = A 7 3 9
1114 1113 oveq1d φ A 7 3 3 3 + A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3 = A 7 3 9 + A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3
1115 1109 1114 eqtrd φ A 3 3 A 2 + 3 2 A + 3 3 = A 7 3 9 + A 6 3 9 + A 5 3 8 + 3 8 + A 4 3 7 2 + 3 6 + A 3 3 6 + 3 6 + A 2 3 5 + A 3 3