Metamath Proof Explorer


Theorem jm2.27b

Description: Lemma for jm2.27 . Expand existential quantifiers for reverse direction. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Hypotheses jm2.27a1 φA2
jm2.27a2 φB
jm2.27a3 φC
jm2.27a4 φD0
jm2.27a5 φE0
jm2.27a6 φF0
jm2.27a7 φG0
jm2.27a8 φH0
jm2.27a9 φI0
jm2.27a10 φJ0
jm2.27a11 φD2A21C2=1
jm2.27a12 φF2A21E2=1
jm2.27a13 φG2
jm2.27a14 φI2G21H2=1
jm2.27a15 φE=J+12C2
jm2.27a16 φFGA
jm2.27a17 φ2CG1
jm2.27a18 φFHC
jm2.27a19 φ2CHB
jm2.27a20 φBC
Assertion jm2.27b φC=AYrmB

Proof

Step Hyp Ref Expression
1 jm2.27a1 φA2
2 jm2.27a2 φB
3 jm2.27a3 φC
4 jm2.27a4 φD0
5 jm2.27a5 φE0
6 jm2.27a6 φF0
7 jm2.27a7 φG0
8 jm2.27a8 φH0
9 jm2.27a9 φI0
10 jm2.27a10 φJ0
11 jm2.27a11 φD2A21C2=1
12 jm2.27a12 φF2A21E2=1
13 jm2.27a13 φG2
14 jm2.27a14 φI2G21H2=1
15 jm2.27a15 φE=J+12C2
16 jm2.27a16 φFGA
17 jm2.27a17 φ2CG1
18 jm2.27a18 φFHC
19 jm2.27a19 φ2CHB
20 jm2.27a20 φBC
21 3 nnzd φC
22 rmxycomplete A2D0CD2A21C2=1pD=AXrmpC=AYrmp
23 1 4 21 22 syl3anc φD2A21C2=1pD=AXrmpC=AYrmp
24 11 23 mpbid φpD=AXrmpC=AYrmp
25 12 adantr φpD=AXrmpC=AYrmpF2A21E2=1
26 1 adantr φpD=AXrmpC=AYrmpA2
27 6 adantr φpD=AXrmpC=AYrmpF0
28 5 nn0zd φE
29 28 adantr φpD=AXrmpC=AYrmpE
30 rmxycomplete A2F0EF2A21E2=1qF=AXrmqE=AYrmq
31 26 27 29 30 syl3anc φpD=AXrmpC=AYrmpF2A21E2=1qF=AXrmqE=AYrmq
32 25 31 mpbid φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmq
33 14 ad2antrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqI2G21H2=1
34 13 ad2antrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqG2
35 9 ad2antrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqI0
36 8 nn0zd φH
37 36 ad2antrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqH
38 rmxycomplete G2I0HI2G21H2=1rI=GXrmrH=GYrmr
39 34 35 37 38 syl3anc φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqI2G21H2=1rI=GXrmrH=GYrmr
40 33 39 mpbid φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmr
41 1 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrA2
42 2 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrB
43 3 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrC
44 4 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrD0
45 5 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrE0
46 6 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrF0
47 7 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrG0
48 8 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrH0
49 9 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrI0
50 10 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrJ0
51 11 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrD2A21C2=1
52 12 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrF2A21E2=1
53 13 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrG2
54 14 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrI2G21H2=1
55 15 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrE=J+12C2
56 16 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrFGA
57 17 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmr2CG1
58 18 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrFHC
59 19 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmr2CHB
60 20 ad3antrrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrBC
61 simprl φpD=AXrmpC=AYrmpp
62 61 ad2antrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrp
63 simprrl φpD=AXrmpC=AYrmpD=AXrmp
64 63 ad2antrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrD=AXrmp
65 simprrr φpD=AXrmpC=AYrmpC=AYrmp
66 65 ad2antrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrC=AYrmp
67 simplrl φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrq
68 simprl qF=AXrmqE=AYrmqF=AXrmq
69 68 ad2antlr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrF=AXrmq
70 simprr qF=AXrmqE=AYrmqE=AYrmq
71 70 ad2antlr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrE=AYrmq
72 simprl φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrr
73 simprrl φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrI=GXrmr
74 simprrr φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrH=GYrmr
75 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 62 64 66 67 69 71 72 73 74 jm2.27a φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqrI=GXrmrH=GYrmrC=AYrmB
76 40 75 rexlimddv φpD=AXrmpC=AYrmpqF=AXrmqE=AYrmqC=AYrmB
77 32 76 rexlimddv φpD=AXrmpC=AYrmpC=AYrmB
78 24 77 rexlimddv φC=AYrmB