Metamath Proof Explorer


Theorem poimirlem23

Description: Lemma for poimir , two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 ( 𝜑𝑁 ∈ ℕ )
poimirlem23.1 ( 𝜑𝑇 : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
poimirlem23.2 ( 𝜑𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
poimirlem23.3 ( 𝜑𝑉 ∈ ( 0 ... 𝑁 ) )
Assertion poimirlem23 ( 𝜑 → ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝𝑁 ) ≠ 0 ↔ ¬ ( 𝑉 = 𝑁 ∧ ( ( 𝑇𝑁 ) = 0 ∧ ( 𝑈𝑁 ) = 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 poimir.0 ( 𝜑𝑁 ∈ ℕ )
2 poimirlem23.1 ( 𝜑𝑇 : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
3 poimirlem23.2 ( 𝜑𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
4 poimirlem23.3 ( 𝜑𝑉 ∈ ( 0 ... 𝑁 ) )
5 ovex ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
6 5 csbex if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
7 6 rgenw 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
8 eqid ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
9 fveq1 ( 𝑝 = if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ( 𝑝𝑁 ) = ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) )
10 9 neeq1d ( 𝑝 = if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ( ( 𝑝𝑁 ) ≠ 0 ↔ ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 ) )
11 df-ne ( ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 ↔ ¬ ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
12 10 11 bitrdi ( 𝑝 = if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ( ( 𝑝𝑁 ) ≠ 0 ↔ ¬ ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
13 8 12 rexrnmptw ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V → ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝𝑁 ) ≠ 0 ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
14 7 13 ax-mp ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝𝑁 ) ≠ 0 ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
15 rexnal ( ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ¬ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
16 14 15 bitri ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝𝑁 ) ≠ 0 ↔ ¬ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
17 1 nnzd ( 𝜑𝑁 ∈ ℤ )
18 elfzelz ( 𝑉 ∈ ( 0 ... 𝑁 ) → 𝑉 ∈ ℤ )
19 4 18 syl ( 𝜑𝑉 ∈ ℤ )
20 zlem1lt ( ( 𝑁 ∈ ℤ ∧ 𝑉 ∈ ℤ ) → ( 𝑁𝑉 ↔ ( 𝑁 − 1 ) < 𝑉 ) )
21 17 19 20 syl2anc ( 𝜑 → ( 𝑁𝑉 ↔ ( 𝑁 − 1 ) < 𝑉 ) )
22 elfzle2 ( 𝑉 ∈ ( 0 ... 𝑁 ) → 𝑉𝑁 )
23 4 22 syl ( 𝜑𝑉𝑁 )
24 19 zred ( 𝜑𝑉 ∈ ℝ )
25 1 nnred ( 𝜑𝑁 ∈ ℝ )
26 24 25 letri3d ( 𝜑 → ( 𝑉 = 𝑁 ↔ ( 𝑉𝑁𝑁𝑉 ) ) )
27 26 biimprd ( 𝜑 → ( ( 𝑉𝑁𝑁𝑉 ) → 𝑉 = 𝑁 ) )
28 23 27 mpand ( 𝜑 → ( 𝑁𝑉𝑉 = 𝑁 ) )
29 21 28 sylbird ( 𝜑 → ( ( 𝑁 − 1 ) < 𝑉𝑉 = 𝑁 ) )
30 29 necon3ad ( 𝜑 → ( 𝑉𝑁 → ¬ ( 𝑁 − 1 ) < 𝑉 ) )
31 nnm1nn0 ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
32 1 31 syl ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
33 nn0fz0 ( ( 𝑁 − 1 ) ∈ ℕ0 ↔ ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
34 32 33 sylib ( 𝜑 → ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
35 34 adantr ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
36 iffalse ( ¬ ( 𝑁 − 1 ) < 𝑉 → if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 𝑁 − 1 ) + 1 ) )
37 1 nncnd ( 𝜑𝑁 ∈ ℂ )
38 npcan1 ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
39 37 38 syl ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
40 36 39 sylan9eqr ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) = 𝑁 )
41 40 csbeq1d ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = 𝑁 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
42 oveq2 ( 𝑗 = 𝑁 → ( 1 ... 𝑗 ) = ( 1 ... 𝑁 ) )
43 42 imaeq2d ( 𝑗 = 𝑁 → ( 𝑈 “ ( 1 ... 𝑗 ) ) = ( 𝑈 “ ( 1 ... 𝑁 ) ) )
44 43 xpeq1d ( 𝑗 = 𝑁 → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( 𝑈 “ ( 1 ... 𝑁 ) ) × { 1 } ) )
45 oveq1 ( 𝑗 = 𝑁 → ( 𝑗 + 1 ) = ( 𝑁 + 1 ) )
46 45 oveq1d ( 𝑗 = 𝑁 → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( 𝑁 + 1 ) ... 𝑁 ) )
47 46 imaeq2d ( 𝑗 = 𝑁 → ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) )
48 47 xpeq1d ( 𝑗 = 𝑁 → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) × { 0 } ) )
49 44 48 uneq12d ( 𝑗 = 𝑁 → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 𝑈 “ ( 1 ... 𝑁 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
50 f1ofo ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
51 foima ( 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
52 3 50 51 3syl ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
53 52 xpeq1d ( 𝜑 → ( ( 𝑈 “ ( 1 ... 𝑁 ) ) × { 1 } ) = ( ( 1 ... 𝑁 ) × { 1 } ) )
54 25 ltp1d ( 𝜑𝑁 < ( 𝑁 + 1 ) )
55 17 peano2zd ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
56 fzn ( ( ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 < ( 𝑁 + 1 ) ↔ ( ( 𝑁 + 1 ) ... 𝑁 ) = ∅ ) )
57 55 17 56 syl2anc ( 𝜑 → ( 𝑁 < ( 𝑁 + 1 ) ↔ ( ( 𝑁 + 1 ) ... 𝑁 ) = ∅ ) )
58 54 57 mpbid ( 𝜑 → ( ( 𝑁 + 1 ) ... 𝑁 ) = ∅ )
59 58 imaeq2d ( 𝜑 → ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) = ( 𝑈 “ ∅ ) )
60 59 xpeq1d ( 𝜑 → ( ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( 𝑈 “ ∅ ) × { 0 } ) )
61 ima0 ( 𝑈 “ ∅ ) = ∅
62 61 xpeq1i ( ( 𝑈 “ ∅ ) × { 0 } ) = ( ∅ × { 0 } )
63 0xp ( ∅ × { 0 } ) = ∅
64 62 63 eqtri ( ( 𝑈 “ ∅ ) × { 0 } ) = ∅
65 60 64 eqtrdi ( 𝜑 → ( ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) × { 0 } ) = ∅ )
66 53 65 uneq12d ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... 𝑁 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 1 ... 𝑁 ) × { 1 } ) ∪ ∅ ) )
67 un0 ( ( ( 1 ... 𝑁 ) × { 1 } ) ∪ ∅ ) = ( ( 1 ... 𝑁 ) × { 1 } )
68 66 67 eqtrdi ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... 𝑁 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( 1 ... 𝑁 ) × { 1 } ) )
69 49 68 sylan9eqr ( ( 𝜑𝑗 = 𝑁 ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( 1 ... 𝑁 ) × { 1 } ) )
70 69 oveq2d ( ( 𝜑𝑗 = 𝑁 ) → ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇f + ( ( 1 ... 𝑁 ) × { 1 } ) ) )
71 1 70 csbied ( 𝜑 𝑁 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇f + ( ( 1 ... 𝑁 ) × { 1 } ) ) )
72 71 adantr ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → 𝑁 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇f + ( ( 1 ... 𝑁 ) × { 1 } ) ) )
73 41 72 eqtrd ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇f + ( ( 1 ... 𝑁 ) × { 1 } ) ) )
74 73 fveq1d ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ( if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = ( ( 𝑇f + ( ( 1 ... 𝑁 ) × { 1 } ) ) ‘ 𝑁 ) )
75 elfzonn0 ( 𝑗 ∈ ( 0 ..^ 𝐾 ) → 𝑗 ∈ ℕ0 )
76 nn0p1nn ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ )
77 75 76 syl ( 𝑗 ∈ ( 0 ..^ 𝐾 ) → ( 𝑗 + 1 ) ∈ ℕ )
78 elsni ( 𝑦 ∈ { 1 } → 𝑦 = 1 )
79 78 oveq2d ( 𝑦 ∈ { 1 } → ( 𝑗 + 𝑦 ) = ( 𝑗 + 1 ) )
80 79 eleq1d ( 𝑦 ∈ { 1 } → ( ( 𝑗 + 𝑦 ) ∈ ℕ ↔ ( 𝑗 + 1 ) ∈ ℕ ) )
81 77 80 syl5ibrcom ( 𝑗 ∈ ( 0 ..^ 𝐾 ) → ( 𝑦 ∈ { 1 } → ( 𝑗 + 𝑦 ) ∈ ℕ ) )
82 81 imp ( ( 𝑗 ∈ ( 0 ..^ 𝐾 ) ∧ 𝑦 ∈ { 1 } ) → ( 𝑗 + 𝑦 ) ∈ ℕ )
83 82 adantl ( ( 𝜑 ∧ ( 𝑗 ∈ ( 0 ..^ 𝐾 ) ∧ 𝑦 ∈ { 1 } ) ) → ( 𝑗 + 𝑦 ) ∈ ℕ )
84 1ex 1 ∈ V
85 84 fconst ( ( 1 ... 𝑁 ) × { 1 } ) : ( 1 ... 𝑁 ) ⟶ { 1 }
86 85 a1i ( 𝜑 → ( ( 1 ... 𝑁 ) × { 1 } ) : ( 1 ... 𝑁 ) ⟶ { 1 } )
87 ovexd ( 𝜑 → ( 1 ... 𝑁 ) ∈ V )
88 inidm ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
89 83 2 86 87 87 88 off ( 𝜑 → ( 𝑇f + ( ( 1 ... 𝑁 ) × { 1 } ) ) : ( 1 ... 𝑁 ) ⟶ ℕ )
90 elfz1end ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( 1 ... 𝑁 ) )
91 1 90 sylib ( 𝜑𝑁 ∈ ( 1 ... 𝑁 ) )
92 89 91 ffvelrnd ( 𝜑 → ( ( 𝑇f + ( ( 1 ... 𝑁 ) × { 1 } ) ) ‘ 𝑁 ) ∈ ℕ )
93 92 adantr ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ( ( 𝑇f + ( ( 1 ... 𝑁 ) × { 1 } ) ) ‘ 𝑁 ) ∈ ℕ )
94 74 93 eqeltrd ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ( if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ∈ ℕ )
95 94 nnne0d ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ( if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 )
96 breq1 ( 𝑦 = ( 𝑁 − 1 ) → ( 𝑦 < 𝑉 ↔ ( 𝑁 − 1 ) < 𝑉 ) )
97 id ( 𝑦 = ( 𝑁 − 1 ) → 𝑦 = ( 𝑁 − 1 ) )
98 oveq1 ( 𝑦 = ( 𝑁 − 1 ) → ( 𝑦 + 1 ) = ( ( 𝑁 − 1 ) + 1 ) )
99 96 97 98 ifbieq12d ( 𝑦 = ( 𝑁 − 1 ) → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) = if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) )
100 99 csbeq1d ( 𝑦 = ( 𝑁 − 1 ) → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
101 100 fveq1d ( 𝑦 = ( 𝑁 − 1 ) → ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = ( if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) )
102 101 neeq1d ( 𝑦 = ( 𝑁 − 1 ) → ( ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 ↔ ( if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 ) )
103 11 102 bitr3id ( 𝑦 = ( 𝑁 − 1 ) → ( ¬ ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 ) )
104 103 rspcev ( ( ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ ( if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 ) → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
105 35 95 104 syl2anc ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
106 105 15 sylib ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ¬ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
107 106 ex ( 𝜑 → ( ¬ ( 𝑁 − 1 ) < 𝑉 → ¬ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
108 30 107 syld ( 𝜑 → ( 𝑉𝑁 → ¬ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
109 108 necon4ad ( 𝜑 → ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 → 𝑉 = 𝑁 ) )
110 109 pm4.71rd ( 𝜑 → ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( 𝑉 = 𝑁 ∧ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) ) )
111 32 nn0zd ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
112 uzid ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) )
113 peano2uz ( ( 𝑁 − 1 ) ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) )
114 111 112 113 3syl ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) )
115 39 114 eqeltrrd ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) )
116 fzss2 ( 𝑁 ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
117 115 116 syl ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
118 117 sselda ( ( 𝜑𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
119 91 adantr ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
120 2 ffnd ( 𝜑𝑇 Fn ( 1 ... 𝑁 ) )
121 120 adantr ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑇 Fn ( 1 ... 𝑁 ) )
122 84 fconst ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( 𝑈 “ ( 1 ... 𝑗 ) ) ⟶ { 1 }
123 c0ex 0 ∈ V
124 123 fconst ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 }
125 122 124 pm3.2i ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( 𝑈 “ ( 1 ... 𝑗 ) ) ⟶ { 1 } ∧ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 } )
126 dff1o3 ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun 𝑈 ) )
127 126 simprbi ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun 𝑈 )
128 imain ( Fun 𝑈 → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
129 3 127 128 3syl ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
130 elfzelz ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℤ )
131 130 zred ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℝ )
132 131 ltp1d ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 < ( 𝑗 + 1 ) )
133 fzdisj ( 𝑗 < ( 𝑗 + 1 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
134 132 133 syl ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
135 134 imaeq2d ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
136 135 61 eqtrdi ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
137 129 136 sylan9req ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
138 fun ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( 𝑈 “ ( 1 ... 𝑗 ) ) ⟶ { 1 } ∧ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 } ) ∧ ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) )
139 125 137 138 sylancr ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) )
140 elfznn0 ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℕ0 )
141 140 76 syl ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ℕ )
142 nnuz ℕ = ( ℤ ‘ 1 )
143 141 142 eleqtrdi ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ( ℤ ‘ 1 ) )
144 elfzuz3 ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ𝑗 ) )
145 fzsplit2 ( ( ( 𝑗 + 1 ) ∈ ( ℤ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ𝑗 ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
146 143 144 145 syl2anc ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
147 146 imaeq2d ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 𝑈 “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
148 imaundi ( 𝑈 “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
149 147 148 eqtr2di ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ( 1 ... 𝑁 ) ) )
150 149 52 sylan9eqr ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
151 150 feq2d ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) ↔ ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) ) )
152 139 151 mpbid ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) )
153 152 ffnd ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
154 ovexd ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 1 ... 𝑁 ) ∈ V )
155 eqidd ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇𝑁 ) = ( 𝑇𝑁 ) )
156 eqidd ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
157 121 153 154 154 88 155 156 ofval ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = ( ( 𝑇𝑁 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ) )
158 119 157 mpdan ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = ( ( 𝑇𝑁 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ) )
159 158 eqeq1d ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( ( 𝑇𝑁 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ) = 0 ) )
160 2 91 ffvelrnd ( 𝜑 → ( 𝑇𝑁 ) ∈ ( 0 ..^ 𝐾 ) )
161 elfzonn0 ( ( 𝑇𝑁 ) ∈ ( 0 ..^ 𝐾 ) → ( 𝑇𝑁 ) ∈ ℕ0 )
162 160 161 syl ( 𝜑 → ( 𝑇𝑁 ) ∈ ℕ0 )
163 162 nn0red ( 𝜑 → ( 𝑇𝑁 ) ∈ ℝ )
164 163 adantr ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑇𝑁 ) ∈ ℝ )
165 162 nn0ge0d ( 𝜑 → 0 ≤ ( 𝑇𝑁 ) )
166 165 adantr ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( 𝑇𝑁 ) )
167 1re 1 ∈ ℝ
168 snssi ( 1 ∈ ℝ → { 1 } ⊆ ℝ )
169 167 168 ax-mp { 1 } ⊆ ℝ
170 0re 0 ∈ ℝ
171 snssi ( 0 ∈ ℝ → { 0 } ⊆ ℝ )
172 170 171 ax-mp { 0 } ⊆ ℝ
173 169 172 unssi ( { 1 } ∪ { 0 } ) ⊆ ℝ
174 152 119 ffvelrnd ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ ( { 1 } ∪ { 0 } ) )
175 173 174 sseldi ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ ℝ )
176 elun ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ ( { 1 } ∪ { 0 } ) ↔ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 1 } ∨ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 0 } ) )
177 0le1 0 ≤ 1
178 elsni ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 1 } → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 1 )
179 177 178 breqtrrid ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 1 } → 0 ≤ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
180 0le0 0 ≤ 0
181 elsni ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 0 } → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
182 180 181 breqtrrid ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 0 } → 0 ≤ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
183 179 182 jaoi ( ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 1 } ∨ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 0 } ) → 0 ≤ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
184 176 183 sylbi ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ ( { 1 } ∪ { 0 } ) → 0 ≤ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
185 174 184 syl ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
186 add20 ( ( ( ( 𝑇𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝑇𝑁 ) ) ∧ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ ℝ ∧ 0 ≤ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ) ) → ( ( ( 𝑇𝑁 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ) = 0 ↔ ( ( 𝑇𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
187 164 166 175 185 186 syl22anc ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑇𝑁 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ) = 0 ↔ ( ( 𝑇𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
188 159 187 bitrd ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( ( 𝑇𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
189 118 188 syldan ( ( 𝜑𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( ( 𝑇𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
190 189 ralbidva ( 𝜑 → ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
191 190 adantr ( ( 𝜑𝑉 = 𝑁 ) → ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
192 breq2 ( 𝑉 = 𝑁 → ( 𝑦 < 𝑉𝑦 < 𝑁 ) )
193 192 ifbid ( 𝑉 = 𝑁 → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < 𝑁 , 𝑦 , ( 𝑦 + 1 ) ) )
194 elfzelz ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℤ )
195 194 zred ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℝ )
196 195 adantl ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 ∈ ℝ )
197 32 nn0red ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
198 197 adantr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℝ )
199 25 adantr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℝ )
200 elfzle2 ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ≤ ( 𝑁 − 1 ) )
201 200 adantl ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 ≤ ( 𝑁 − 1 ) )
202 25 ltm1d ( 𝜑 → ( 𝑁 − 1 ) < 𝑁 )
203 202 adantr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) < 𝑁 )
204 196 198 199 201 203 lelttrd ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 < 𝑁 )
205 204 iftrued ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → if ( 𝑦 < 𝑁 , 𝑦 , ( 𝑦 + 1 ) ) = 𝑦 )
206 193 205 sylan9eqr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑉 = 𝑁 ) → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) = 𝑦 )
207 206 an32s ( ( ( 𝜑𝑉 = 𝑁 ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) = 𝑦 )
208 207 csbeq1d ( ( ( 𝜑𝑉 = 𝑁 ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = 𝑦 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
209 208 fveq1d ( ( ( 𝜑𝑉 = 𝑁 ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = ( 𝑦 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) )
210 209 eqeq1d ( ( ( 𝜑𝑉 = 𝑁 ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( 𝑦 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
211 210 ralbidva ( ( 𝜑𝑉 = 𝑁 ) → ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑦 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
212 nfv 𝑦 ( ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0
213 nfcsb1v 𝑗 𝑦 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
214 nfcv 𝑗 𝑁
215 213 214 nffv 𝑗 ( 𝑦 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 )
216 215 nfeq1 𝑗 ( 𝑦 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0
217 csbeq1a ( 𝑗 = 𝑦 → ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = 𝑦 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
218 217 fveq1d ( 𝑗 = 𝑦 → ( ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = ( 𝑦 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) )
219 218 eqeq1d ( 𝑗 = 𝑦 → ( ( ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( 𝑦 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
220 212 216 219 cbvralw ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑦 / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
221 211 220 bitr4di ( ( 𝜑𝑉 = 𝑁 ) → ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
222 ne0i ( ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ≠ ∅ )
223 r19.3rzv ( ( 0 ... ( 𝑁 − 1 ) ) ≠ ∅ → ( ( 𝑇𝑁 ) = 0 ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑇𝑁 ) = 0 ) )
224 34 222 223 3syl ( 𝜑 → ( ( 𝑇𝑁 ) = 0 ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑇𝑁 ) = 0 ) )
225 elfzelz ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℤ )
226 225 zred ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℝ )
227 226 ltp1d ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑗 < ( 𝑗 + 1 ) )
228 227 133 syl ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
229 228 imaeq2d ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
230 229 61 eqtrdi ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
231 129 230 sylan9req ( ( 𝜑𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
232 231 adantlr ( ( ( 𝜑 ∧ ( 𝑈𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
233 simplr ( ( ( 𝜑 ∧ ( 𝑈𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑈𝑁 ) = 𝑁 )
234 f1ofn ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 Fn ( 1 ... 𝑁 ) )
235 3 234 syl ( 𝜑𝑈 Fn ( 1 ... 𝑁 ) )
236 235 adantr ( ( 𝜑𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑈 Fn ( 1 ... 𝑁 ) )
237 elfznn0 ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℕ0 )
238 237 76 syl ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑗 + 1 ) ∈ ℕ )
239 238 142 eleqtrdi ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑗 + 1 ) ∈ ( ℤ ‘ 1 ) )
240 fzss1 ( ( 𝑗 + 1 ) ∈ ( ℤ ‘ 1 ) → ( ( 𝑗 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
241 239 240 syl ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑗 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
242 241 adantl ( ( 𝜑𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑗 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
243 39 adantr ( ( 𝜑𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
244 elfzuz3 ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ𝑗 ) )
245 eluzp1p1 ( ( 𝑁 − 1 ) ∈ ( ℤ𝑗 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑗 + 1 ) ) )
246 244 245 syl ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑗 + 1 ) ) )
247 246 adantl ( ( 𝜑𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ ‘ ( 𝑗 + 1 ) ) )
248 243 247 eqeltrrd ( ( 𝜑𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ ‘ ( 𝑗 + 1 ) ) )
249 eluzfz2 ( 𝑁 ∈ ( ℤ ‘ ( 𝑗 + 1 ) ) → 𝑁 ∈ ( ( 𝑗 + 1 ) ... 𝑁 ) )
250 248 249 syl ( ( 𝜑𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ( 𝑗 + 1 ) ... 𝑁 ) )
251 fnfvima ( ( 𝑈 Fn ( 1 ... 𝑁 ) ∧ ( ( 𝑗 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) ∧ 𝑁 ∈ ( ( 𝑗 + 1 ) ... 𝑁 ) ) → ( 𝑈𝑁 ) ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
252 236 242 250 251 syl3anc ( ( 𝜑𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑈𝑁 ) ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
253 252 adantlr ( ( ( 𝜑 ∧ ( 𝑈𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑈𝑁 ) ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
254 233 253 eqeltrrd ( ( ( 𝜑 ∧ ( 𝑈𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
255 fnconstg ( 1 ∈ V → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑗 ) ) )
256 84 255 ax-mp ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑗 ) )
257 fnconstg ( 0 ∈ V → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
258 123 257 ax-mp ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) )
259 fvun2 ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑗 ) ) ∧ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ∧ ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑁 ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑁 ) )
260 256 258 259 mp3an12 ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑁 ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑁 ) )
261 232 254 260 syl2anc ( ( ( 𝜑 ∧ ( 𝑈𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑁 ) )
262 123 fvconst2 ( 𝑁 ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) → ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑁 ) = 0 )
263 254 262 syl ( ( ( 𝜑 ∧ ( 𝑈𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑁 ) = 0 )
264 261 263 eqtrd ( ( ( 𝜑 ∧ ( 𝑈𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
265 264 ralrimiva ( ( 𝜑 ∧ ( 𝑈𝑁 ) = 𝑁 ) → ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
266 265 ex ( 𝜑 → ( ( 𝑈𝑁 ) = 𝑁 → ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) )
267 34 adantr ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
268 ax-1ne0 1 ≠ 0
269 imain ( Fun 𝑈 → ( 𝑈 “ ( ( 1 ... ( 𝑁 − 1 ) ) ∩ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) )
270 3 127 269 3syl ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑁 − 1 ) ) ∩ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) )
271 202 39 breqtrrd ( 𝜑 → ( 𝑁 − 1 ) < ( ( 𝑁 − 1 ) + 1 ) )
272 fzdisj ( ( 𝑁 − 1 ) < ( ( 𝑁 − 1 ) + 1 ) → ( ( 1 ... ( 𝑁 − 1 ) ) ∩ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
273 271 272 syl ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∩ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
274 273 imaeq2d ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑁 − 1 ) ) ∩ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
275 274 61 eqtrdi ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑁 − 1 ) ) ∩ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
276 270 275 eqtr3d ( 𝜑 → ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
277 276 adantr ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
278 91 adantr ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
279 elimasni ( 𝑁 ∈ ( 𝑈 “ { 𝑁 } ) → 𝑁 𝑈 𝑁 )
280 fnbrfvb ( ( 𝑈 Fn ( 1 ... 𝑁 ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑈𝑁 ) = 𝑁𝑁 𝑈 𝑁 ) )
281 235 91 280 syl2anc ( 𝜑 → ( ( 𝑈𝑁 ) = 𝑁𝑁 𝑈 𝑁 ) )
282 279 281 syl5ibr ( 𝜑 → ( 𝑁 ∈ ( 𝑈 “ { 𝑁 } ) → ( 𝑈𝑁 ) = 𝑁 ) )
283 282 necon3ad ( 𝜑 → ( ( 𝑈𝑁 ) ≠ 𝑁 → ¬ 𝑁 ∈ ( 𝑈 “ { 𝑁 } ) ) )
284 283 imp ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → ¬ 𝑁 ∈ ( 𝑈 “ { 𝑁 } ) )
285 278 284 eldifd ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → 𝑁 ∈ ( ( 1 ... 𝑁 ) ∖ ( 𝑈 “ { 𝑁 } ) ) )
286 imadif ( Fun 𝑈 → ( 𝑈 “ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) = ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { 𝑁 } ) ) )
287 3 127 286 3syl ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) = ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { 𝑁 } ) ) )
288 difun2 ( ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ∖ { 𝑁 } ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∖ { 𝑁 } )
289 elun ( 𝑗 ∈ ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ↔ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑗 ∈ { 𝑁 } ) )
290 velsn ( 𝑗 ∈ { 𝑁 } ↔ 𝑗 = 𝑁 )
291 290 orbi2i ( ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑗 ∈ { 𝑁 } ) ↔ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑗 = 𝑁 ) )
292 289 291 bitri ( 𝑗 ∈ ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ↔ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑗 = 𝑁 ) )
293 1 142 eleqtrdi ( 𝜑𝑁 ∈ ( ℤ ‘ 1 ) )
294 fzm1 ( 𝑁 ∈ ( ℤ ‘ 1 ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑗 = 𝑁 ) ) )
295 293 294 syl ( 𝜑 → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑗 = 𝑁 ) ) )
296 292 295 bitr4id ( 𝜑 → ( 𝑗 ∈ ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ↔ 𝑗 ∈ ( 1 ... 𝑁 ) ) )
297 296 eqrdv ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) = ( 1 ... 𝑁 ) )
298 297 difeq1d ( 𝜑 → ( ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ∖ { 𝑁 } ) = ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) )
299 197 25 ltnled ( 𝜑 → ( ( 𝑁 − 1 ) < 𝑁 ↔ ¬ 𝑁 ≤ ( 𝑁 − 1 ) ) )
300 202 299 mpbid ( 𝜑 → ¬ 𝑁 ≤ ( 𝑁 − 1 ) )
301 elfzle2 ( 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑁 ≤ ( 𝑁 − 1 ) )
302 300 301 nsyl ( 𝜑 → ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
303 difsn ( ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( ( 1 ... ( 𝑁 − 1 ) ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
304 302 303 syl ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
305 288 298 304 3eqtr3a ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
306 305 imaeq2d ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) = ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) )
307 52 difeq1d ( 𝜑 → ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { 𝑁 } ) ) = ( ( 1 ... 𝑁 ) ∖ ( 𝑈 “ { 𝑁 } ) ) )
308 287 306 307 3eqtr3rd ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ( 𝑈 “ { 𝑁 } ) ) = ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) )
309 308 adantr ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → ( ( 1 ... 𝑁 ) ∖ ( 𝑈 “ { 𝑁 } ) ) = ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) )
310 285 309 eleqtrd ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → 𝑁 ∈ ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) )
311 fnconstg ( 1 ∈ V → ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) )
312 84 311 ax-mp ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) )
313 fnconstg ( 0 ∈ V → ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
314 123 313 ax-mp ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) )
315 fvun1 ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ∧ ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑁 ∈ ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ‘ 𝑁 ) )
316 312 314 315 mp3an12 ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑁 ∈ ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ‘ 𝑁 ) )
317 277 310 316 syl2anc ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ‘ 𝑁 ) )
318 84 fvconst2 ( 𝑁 ∈ ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ‘ 𝑁 ) = 1 )
319 310 318 syl ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ‘ 𝑁 ) = 1 )
320 317 319 eqtrd ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 1 )
321 320 neeq1d ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → ( ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 ↔ 1 ≠ 0 ) )
322 268 321 mpbiri ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 )
323 df-ne ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 ↔ ¬ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
324 oveq2 ( 𝑗 = ( 𝑁 − 1 ) → ( 1 ... 𝑗 ) = ( 1 ... ( 𝑁 − 1 ) ) )
325 324 imaeq2d ( 𝑗 = ( 𝑁 − 1 ) → ( 𝑈 “ ( 1 ... 𝑗 ) ) = ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) )
326 325 xpeq1d ( 𝑗 = ( 𝑁 − 1 ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) )
327 oveq1 ( 𝑗 = ( 𝑁 − 1 ) → ( 𝑗 + 1 ) = ( ( 𝑁 − 1 ) + 1 ) )
328 327 oveq1d ( 𝑗 = ( 𝑁 − 1 ) → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) )
329 328 imaeq2d ( 𝑗 = ( 𝑁 − 1 ) → ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
330 329 xpeq1d ( 𝑗 = ( 𝑁 − 1 ) → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) )
331 326 330 uneq12d ( 𝑗 = ( 𝑁 − 1 ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
332 331 fveq1d ( 𝑗 = ( 𝑁 − 1 ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
333 332 neeq1d ( 𝑗 = ( 𝑁 − 1 ) → ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 ↔ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 ) )
334 323 333 bitr3id ( 𝑗 = ( 𝑁 − 1 ) → ( ¬ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ↔ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 ) )
335 334 rspcev ( ( ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 ) → ∃ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
336 267 322 335 syl2anc ( ( 𝜑 ∧ ( 𝑈𝑁 ) ≠ 𝑁 ) → ∃ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
337 336 ex ( 𝜑 → ( ( 𝑈𝑁 ) ≠ 𝑁 → ∃ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) )
338 rexnal ( ∃ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ↔ ¬ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
339 337 338 syl6ib ( 𝜑 → ( ( 𝑈𝑁 ) ≠ 𝑁 → ¬ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) )
340 339 necon4ad ( 𝜑 → ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 → ( 𝑈𝑁 ) = 𝑁 ) )
341 266 340 impbid ( 𝜑 → ( ( 𝑈𝑁 ) = 𝑁 ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) )
342 224 341 anbi12d ( 𝜑 → ( ( ( 𝑇𝑁 ) = 0 ∧ ( 𝑈𝑁 ) = 𝑁 ) ↔ ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑇𝑁 ) = 0 ∧ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
343 r19.26 ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ↔ ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑇𝑁 ) = 0 ∧ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) )
344 342 343 bitr4di ( 𝜑 → ( ( ( 𝑇𝑁 ) = 0 ∧ ( 𝑈𝑁 ) = 𝑁 ) ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
345 344 adantr ( ( 𝜑𝑉 = 𝑁 ) → ( ( ( 𝑇𝑁 ) = 0 ∧ ( 𝑈𝑁 ) = 𝑁 ) ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
346 191 221 345 3bitr4d ( ( 𝜑𝑉 = 𝑁 ) → ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( ( 𝑇𝑁 ) = 0 ∧ ( 𝑈𝑁 ) = 𝑁 ) ) )
347 346 pm5.32da ( 𝜑 → ( ( 𝑉 = 𝑁 ∧ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) ↔ ( 𝑉 = 𝑁 ∧ ( ( 𝑇𝑁 ) = 0 ∧ ( 𝑈𝑁 ) = 𝑁 ) ) ) )
348 110 347 bitrd ( 𝜑 → ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( 𝑉 = 𝑁 ∧ ( ( 𝑇𝑁 ) = 0 ∧ ( 𝑈𝑁 ) = 𝑁 ) ) ) )
349 348 notbid ( 𝜑 → ( ¬ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ¬ ( 𝑉 = 𝑁 ∧ ( ( 𝑇𝑁 ) = 0 ∧ ( 𝑈𝑁 ) = 𝑁 ) ) ) )
350 16 349 syl5bb ( 𝜑 → ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ( 𝑇f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝𝑁 ) ≠ 0 ↔ ¬ ( 𝑉 = 𝑁 ∧ ( ( 𝑇𝑁 ) = 0 ∧ ( 𝑈𝑁 ) = 𝑁 ) ) ) )