Metamath Proof Explorer


Theorem dvle2

Description: Collapsed dvle . (Contributed by metakunt, 19-Aug-2024)

Ref Expression
Hypotheses dvle2.1 φ A
dvle2.2 φ B
dvle2.3 φ x A B E : A B cn
dvle2.4 φ x A B G : A B cn
dvle2.5 φ dx A B E d x = x A B F
dvle2.6 φ dx A B G d x = x A B H
dvle2.7 φ x A B F H
dvle2.8 x = A E = P
dvle2.9 x = A G = Q
dvle2.10 x = B E = R
dvle2.11 x = B G = S
dvle2.12 φ P Q
dvle2.13 φ A B
Assertion dvle2 φ R S

Proof

Step Hyp Ref Expression
1 dvle2.1 φ A
2 dvle2.2 φ B
3 dvle2.3 φ x A B E : A B cn
4 dvle2.4 φ x A B G : A B cn
5 dvle2.5 φ dx A B E d x = x A B F
6 dvle2.6 φ dx A B G d x = x A B H
7 dvle2.7 φ x A B F H
8 dvle2.8 x = A E = P
9 dvle2.9 x = A G = Q
10 dvle2.10 x = B E = R
11 dvle2.11 x = B G = S
12 dvle2.12 φ P Q
13 dvle2.13 φ A B
14 10 eleq1d x = B E R
15 cncff x A B E : A B cn x A B E : A B
16 3 15 syl φ x A B E : A B
17 eqid x A B E = x A B E
18 17 fmpt x A B E x A B E : A B
19 16 18 sylibr φ x A B E
20 2 rexrd φ B *
21 2 leidd φ B B
22 20 13 21 3jca φ B * A B B B
23 1 rexrd φ A *
24 elicc1 A * B * B A B B * A B B B
25 23 20 24 syl2anc φ B A B B * A B B B
26 22 25 mpbird φ B A B
27 14 19 26 rspcdva φ R
28 8 eleq1d x = A E P
29 1 leidd φ A A
30 23 29 13 3jca φ A * A A A B
31 elicc1 A * B * A A B A * A A A B
32 23 20 31 syl2anc φ A A B A * A A A B
33 30 32 mpbird φ A A B
34 28 19 33 rspcdva φ P
35 27 34 resubcld φ R P
36 11 eleq1d x = B G S
37 cncff x A B G : A B cn x A B G : A B
38 4 37 syl φ x A B G : A B
39 eqid x A B G = x A B G
40 39 fmpt x A B G x A B G : A B
41 38 40 sylibr φ x A B G
42 36 41 26 rspcdva φ S
43 9 eleq1d x = A G Q
44 43 41 33 rspcdva φ Q
45 42 44 resubcld φ S Q
46 1 2 3 5 4 6 7 33 26 13 8 9 10 11 dvle φ R P S Q
47 35 34 45 44 46 12 le2addd φ R - P + P S - Q + Q
48 27 recnd φ R
49 34 recnd φ P
50 48 49 npcand φ R - P + P = R
51 42 recnd φ S
52 44 recnd φ Q
53 51 52 npcand φ S - Q + Q = S
54 50 53 breq12d φ R - P + P S - Q + Q R S
55 47 54 mpbid φ R S